39 lines
421 B
Plaintext
39 lines
421 B
Plaintext
~~(((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.
|