diff --git a/tests/et.8pus b/tests/et.8pus new file mode 100644 index 0000000..90a3ebd --- /dev/null +++ b/tests/et.8pus @@ -0,0 +1,26 @@ +( (A /\ B) /\ C -> A /\ (B /\ C) ) /\ ( A /\ (B /\ C) -> (A /\ B) /\ C ) +split. +intro et. +elim et. +intro ab. +intro c. +elim ab. +intro a. +intro b. +split. +assumption. +split. +assumption. +assumption. +intro et. +elim et. +intro a. +intro bc. +elim bc. +intro b. +intro c. +split. +split. +assumption. +assumption. +assumption. diff --git a/tests/ou.8pus b/tests/ou.8pus new file mode 100644 index 0000000..2ae8cc6 --- /dev/null +++ b/tests/ou.8pus @@ -0,0 +1,32 @@ +(A \/ (B \/ C) -> (A \/ B) \/ C) /\ ((A \/ B) \/ C -> A \/ (B \/ C)) +split. +intro ou. +elim ou. +intro a. +left. +left. +assumption. +intro bc. +elim bc. +intro b. +left. +right. +assumption. +intro c. +right. +assumption. +intro ou. +elim ou. +intro ab. +elim ab. +intro a. +left. +assumption. +intro b. +right. +left. +assumption. +intro c. +right. +right. +assumption.