From 5d65bcdc36abd3188aa823e99a367cdddcde87cd Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Tue, 17 May 2022 13:59:35 +0200 Subject: [PATCH] Et et ou --- tests/et.8pus | 26 ++++++++++++++++++++++++++ tests/ou.8pus | 32 ++++++++++++++++++++++++++++++++ 2 files changed, 58 insertions(+) create mode 100644 tests/et.8pus create mode 100644 tests/ou.8pus 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.