Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: ordinal x0.
Assume H1: ordinal x1.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Assume H2: or (40dde.. x0 x2 x1 x3) (and (x0 = x1) (PNoEq_ x0 x2 x3)).
Assume H3: or (40dde.. x1 x3 x0 x2) (and (x1 = x0) (PNoEq_ x1 x3 x2)).
Apply H2 with and (x0 = x1) (PNoEq_ x0 x2 x3) leaving 2 subgoals.
Assume H4: 40dde.. x0 x2 x1 x3.
Apply FalseE with and (x0 = x1) (PNoEq_ x0 x2 x3).
Apply H3 with False leaving 2 subgoals.
Assume H5: 40dde.. x1 x3 x0 x2.
Apply unknownprop_ab808d03ac7e78aa83f072ed699b3ccc158aab0a67cf54e5638eb5435d34c11d with x0, x2.
Apply unknownprop_37f5b5c6ee0011f262b499567d54413188e5bd83bd5555e5f3caca08d2fd472f with x0, x1, x0, x2, x3, x2 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H5: and (x1 = x0) (PNoEq_ x1 x3 x2).
Apply H5 with False.
Assume H6: x1 = x0.
Assume H7: PNoEq_ x1 x3 x2.
Apply unknownprop_1c12738cd89f8c615a541c15b6797bba2a5be97ab5e514c9fd76b3fef06e2aa9 with x0, x1, x2, x3, False leaving 4 subgoals.
The subproof is completed by applying H4.
Assume H8: PNoLt_ (d3786.. x0 x1) x2 x3.
Apply H8 with False.
Let x4 of type ι be given.
Assume H9: (λ x5 . and (prim1 x5 (d3786.. x0 x1)) (and (and (PNoEq_ x5 x2 x3) (not (x2 x5))) (x3 x5))) x4.
Apply H9 with False.
Assume H10: prim1 x4 (d3786.. x0 x1).
Apply unknownprop_1ac99d32a7ae5dc08fd640ea6c8b661df6b3535fe85e88b30b17c3701cb4c7ce with x0, x1, x4, and (and (PNoEq_ x4 x2 x3) (not (x2 x4))) (x3 x4) ⟶ False leaving 2 subgoals.
The subproof is completed by applying H10.
Assume H11: prim1 x4 x0.
Assume H12: prim1 x4 x1.
Assume H13: and (and (PNoEq_ x4 x2 x3) (not (x2 x4))) (x3 x4).
Apply H13 with False.
Assume H14: and (PNoEq_ x4 x2 x3) (not (x2 x4)).
Apply H14 with x3 x4 ⟶ False.
Assume H15: PNoEq_ x4 x2 x3.
Assume H16: not (x2 x4).
Assume H17: x3 x4.
Apply H16.
Apply iffEL with x3 x4, x2 x4 leaving 2 subgoals.
Apply H7 with x4.
The subproof is completed by applying H12.
The subproof is completed by applying H17.
Assume H8: prim1 x0 x1.
Assume H9: PNoEq_ x0 x2 x3.
Assume H10: x3 x0.
Apply In_irref with x0.
Apply H6 with λ x4 x5 . prim1 x0 x4.
The subproof is completed by applying H8.
Assume H8: prim1 x1 x0.
Assume H9: PNoEq_ x1 x2 x3.
Assume H10: not (x2 x1).
Apply In_irref with x0.
Apply H6 with λ x4 x5 . prim1 x4 x0.
The subproof is completed by applying H8.
Assume H4: and (x0 = x1) (PNoEq_ x0 x2 x3).
The subproof is completed by applying H4.
■