diff --git a/tests/irrefutabilite-peirce.8pus b/tests/irrefutabilite-peirce.8pus new file mode 100644 index 0000000..3b6b1e8 --- /dev/null +++ b/tests/irrefutabilite-peirce.8pus @@ -0,0 +1,38 @@ +~~(((A -> B) -> A) -> A) +intro peirce. +cut ~~(A \/ ~A). +intro te. +apply te. +intro te2. +elim te2. +intro a. +cut ~A. +intro f. +apply f. +assumption. +intro a2. +apply peirce. +intro f. +assumption. +intro na. +apply peirce. +intro f. +apply f. +intro a. +cut False. +intro false. +elim false. +apply na. +assumption. +intro f. +cut ~A. +intro f2. +cut A \/ ~A. +assumption. +right. +assumption. +intro a. +cut A \/ ~A. +assumption. +left. +assumption.