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.
Assume H0: x1not x0.
Assume H1: x1not x2.
Assume H2: x0not x2.
Assume H3: not x1or x0 x2.
Apply xm with x2, exactly1of3 x0 x1 x2 leaving 2 subgoals.
Assume H4: x2.
Apply orIR with and (exactly1of2 x0 x1) (not x2), and (and (not x0) (not x1)) x2.
Apply and3I with not x0, not x1, x2 leaving 3 subgoals.
Assume H5: x0.
Apply H2 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Assume H5: x1.
Apply H1 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
The subproof is completed by applying H4.
Assume H4: not x2.
Apply orIL with and (exactly1of2 x0 x1) (not x2), and (and (not x0) (not x1)) x2.
Apply andI with exactly1of2 x0 x1, not x2 leaving 2 subgoals.
Apply exactly1of2_impI2 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H5: not x1.
Apply H3 with x0 leaving 3 subgoals.
The subproof is completed by applying H5.
Assume H6: x0.
The subproof is completed by applying H6.
Assume H6: x2.
Apply H4 with x0.
The subproof is completed by applying H6.
The subproof is completed by applying H4.