Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ο be given.
Let x1 of type ο be given.
Let x2 of type ο be given.
Apply unknownprop_6c693c6a2aae4a815ab9dda6ac030d427fa2267caf48088e8c9791aaf5b51416 with λ x3 x4 : ο → ο → ο → ο . not (x4 x0 x1 x2) ⟶ (not x0 ⟶ not x1 ⟶ not x2 ⟶ False) ⟶ (x0 ⟶ x1 ⟶ False) ⟶ (x0 ⟶ x2 ⟶ False) ⟶ (x1 ⟶ x2 ⟶ False) ⟶ False.
Assume H0: not ((λ x3 x4 x5 : ο . or (and (exactly1of2 x3 x4) (not x5)) (and (and (not x3) (not x4)) x5)) x0 x1 x2).
Assume H1: not x0 ⟶ not x1 ⟶ not x2 ⟶ False.
Assume H2: x0 ⟶ x1 ⟶ False.
Assume H3: x0 ⟶ x2 ⟶ False.
Assume H4: x1 ⟶ x2 ⟶ False.
Apply unknownprop_f85aa429acea90bb5debe460a66fa5f521ae89262b26067dee6e29fd96c2cb64 with and (exactly1of2 x0 x1) (not x2), and (and (not x0) (not x1)) x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H5: not (and (exactly1of2 x0 x1) (not x2)).
Assume H6: not (and (and (not x0) (not x1)) x2).
Apply unknownprop_5aa3e99525b633063b3bdf7de851f763cb73cb264458fc7777fd7e7d458d63b5 with exactly1of2 x0 x1, not x2 leaving 3 subgoals.
The subproof is completed by applying H5.
Assume H7: not (exactly1of2 x0 x1).
Apply unknownprop_3da24d51bcee755e70413ee89aaa40a0b231132f51a75cb86f122fc0fbfbaea8 with x0, x1 leaving 3 subgoals.
The subproof is completed by applying H7.
Assume H8: x0.
Assume H9: x1.
Apply H2 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Assume H8: not x0.
Assume H9: not x1.
Apply unknownprop_5aa3e99525b633063b3bdf7de851f763cb73cb264458fc7777fd7e7d458d63b5 with and (not x0) (not x1), x2 leaving 3 subgoals.
The subproof is completed by applying H6.
Assume H10: not (and (not x0) (not x1)).
Apply unknownprop_5aa3e99525b633063b3bdf7de851f763cb73cb264458fc7777fd7e7d458d63b5 with not x0, not x1 leaving 3 subgoals.
The subproof is completed by applying H10.
Assume H11: not (not x0).
Apply notE with not x0 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H8.
Assume H11: not (not x1).
Apply notE with not x1 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H9.
Assume H10: not x2.
Apply H1 leaving 3 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
Assume H7: not (not x2).
Apply unknownprop_5aa3e99525b633063b3bdf7de851f763cb73cb264458fc7777fd7e7d458d63b5 with and (not x0) (not x1), x2 leaving 3 subgoals.
The subproof is completed by applying H6.
Assume H8: not (and (not x0) (not x1)).
Apply unknownprop_5aa3e99525b633063b3bdf7de851f763cb73cb264458fc7777fd7e7d458d63b5 with not x0, not x1 leaving 3 subgoals.
The subproof is completed by applying H8.
Assume H9: not (not x0).
Apply H3 leaving 2 subgoals.
Apply unknownprop_1e0cb2b8ae8b2a70437458035764f08e7eaba30fc84a0048f28b1466366514c4 with x0.
The subproof is completed by applying H9.
Apply unknownprop_1e0cb2b8ae8b2a70437458035764f08e7eaba30fc84a0048f28b1466366514c4 with x2.
The subproof is completed by applying H7.
Assume H9: not (not x1).
Apply H4 leaving 2 subgoals.
Apply unknownprop_1e0cb2b8ae8b2a70437458035764f08e7eaba30fc84a0048f28b1466366514c4 with x1.
The subproof is completed by applying H9.
Apply unknownprop_1e0cb2b8ae8b2a70437458035764f08e7eaba30fc84a0048f28b1466366514c4 with x2.
The subproof is completed by applying H7.
Assume H8: not x2.
Apply notE with not x2 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
■