Ajout de Et, ou et des tests associés.

2022-05-16 04:01:23 +02:00
parent 905b86af2d
commit 627214787e
10 changed files with 224 additions and 10 deletions
@@ -0,0 +1,6 @@
+(A /\ B) -> A
+intro et.
+elim et.
+intro a.
+intro b.
+assumption.
@@ -0,0 +1,12 @@
+(A \/ B) -> (~A -> B)
+intro ou.
+intro aa.
+elim ou.
+intro a.
+cut False.
+intro ff.
+elim ff.
+apply aa.
+assumption.
+intro b.
+assumption.
@@ -0,0 +1,15 @@
+(A/\B)->(A->C)->(B->D)->(C/\D)
+intro et.
+intro i1.
+intro i2.
+split.
+apply i1.
+elim et.
+intro a.
+intro b.
+assumption.
+apply i2.
+elim et.
+intro a.
+intro b.
+assumption.
@@ -0,0 +1,13 @@
+(A \/ B) -> (A -> C) -> (B -> D) -> (C \/ D)
+intro ou.
+intro i1.
+intro i2.
+elim ou.
+intro a.
+left.
+apply i1.
+assumption.
+intro b.
+right.
+apply i2.
+assumption.