Commit aac4df35 authored by Maarten de Mol's avatar Maarten de Mol
Browse files

Renamed theorem "not_not" to "remove_double_negation" to prevent naming...

Renamed theorem "not_not" to "remove_double_negation" to prevent naming conflicts with section ints.
parent ffc00319
......@@ -18,7 +18,6 @@ SECTION DEFINES:
THEOREM implies_x_true : (ALL P {{P -> TRUE} <-> TRUE})
THEOREM invert_implies : (ALL P (ALL Q {{P -> Q} <-> {~Q -> ~P}}))
THEOREM not_false : {~FALSE <-> TRUE}
THEOREM not_not : (ALL P {~~P <-> P})
THEOREM not_true : {~TRUE <-> FALSE}
THEOREM or_false_x : (ALL P {{FALSE \/ P} <-> P})
THEOREM or_not_left : (ALL P (ALL Q {~P -> {{P \/ Q} <-> Q}}))
......@@ -27,6 +26,7 @@ SECTION DEFINES:
THEOREM or_x_false : (ALL P {{P \/ FALSE} <-> P})
THEOREM or_x_true : (ALL P {{P \/ TRUE} <-> TRUE})
THEOREM reflexive_implies : (ALL P {{P -> P} <-> TRUE})
THEOREM remove_double_negation : (ALL P {~~P <-> P})
THEOREM split_iff : (ALL P (ALL Q {{P <-> Q} <-> {{P -> Q} /\ {Q -> P}}}))
THEOREM symmetric_and : (ALL P (ALL Q {{P /\ Q} <-> {Q /\ P}}))
THEOREM symmetric_or : (ALL P (ALL Q {{P \/ Q} <-> {Q \/ P}}))
......@@ -299,20 +299,6 @@ PROOF:
Contradiction.
ExFalso H2.
THEOREM:
not_not
DEPENDS:
PROOF:
Introduce P.
SplitIff.
1. Introduce H1.
Contradiction.
Absurd H1 H2.
2. Introduce H1.
Contradiction.
Absurd H1 H2.
THEOREM:
not_true
DEPENDS:
......@@ -423,6 +409,20 @@ PROOF:
2. Introduce H1 H2.
Exact H2.
THEOREM:
remove_double_negation
DEPENDS:
PROOF:
Introduce P.
SplitIff.
1. Introduce H1.
Contradiction.
Absurd H1 H2.
2. Introduce H1.
Contradiction.
Absurd H1 H2.
THEOREM:
split_iff
DEPENDS:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment