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: ordinal x0.
Assume H1: ordinal x1.
Assume H2: ordinal x2.
Apply H0 with ∀ x3 x4 x5 : ι → ο . PNoLt x0 x3 x1 x4PNoLt x1 x4 x2 x5PNoLt x0 x3 x2 x5.
Assume H3: TransSet x0.
Assume H4: ∀ x3 . x3x0TransSet x3.
Apply H2 with ∀ x3 x4 x5 : ι → ο . PNoLt x0 x3 x1 x4PNoLt x1 x4 x2 x5PNoLt x0 x3 x2 x5.
Assume H5: TransSet x2.
Assume H6: ∀ x3 . x3x2TransSet x3.
Let x3 of type ιο be given.
Let x4 of type ιο be given.
Let x5 of type ιο be given.
Assume H7: PNoLt x0 x3 x1 x4.
Assume H8: PNoLt x1 x4 x2 x5.
Apply PNoLtE with x0, x1, x3, x4, PNoLt x0 x3 x2 x5 leaving 4 subgoals.
The subproof is completed by applying H7.
Assume H9: PNoLt_ (binintersect x0 x1) x3 x4.
Apply H9 with PNoLt x0 x3 x2 x5.
Let x6 of type ι be given.
Assume H10: (λ x7 . and (x7binintersect x0 x1) (and (and (PNoEq_ x7 x3 x4) (not (x3 x7))) (x4 x7))) x6.
Apply H10 with PNoLt x0 x3 x2 x5.
Assume H11: x6binintersect x0 x1.
Apply binintersectE with x0, x1, x6, and (and (PNoEq_ x6 x3 x4) (not (x3 x6))) (x4 x6)PNoLt x0 x3 x2 x5 leaving 2 subgoals.
The subproof is completed by applying H11.
Assume H12: x6x0.
Assume H13: x6x1.
Assume H14: and (and (PNoEq_ x6 x3 x4) (not (x3 x6))) (x4 x6).
Apply H14 with PNoLt x0 x3 x2 x5.
Assume H15: and (PNoEq_ x6 x3 x4) (not (x3 x6)).
Apply H15 with x4 x6PNoLt x0 x3 x2 x5.
Assume H16: PNoEq_ x6 x3 x4.
Assume H17: not (x3 x6).
Assume H18: x4 x6.
Claim L19: ...
...
Apply PNoLtE with x1, x2, x4, x5, PNoLt x0 x3 x2 x5 leaving 4 subgoals.
The subproof is completed by applying H8.
Assume H20: PNoLt_ (binintersect x1 x2) x4 x5.
Apply H20 with PNoLt x0 x3 x2 x5.
Let x7 of type ι be given.
Assume H21: (λ x8 . and (x8binintersect x1 x2) (and (and (PNoEq_ x8 x4 x5) (not (x4 x8))) (x5 x8))) x7.
Apply H21 with PNoLt x0 x3 x2 x5.
Assume H22: x7binintersect x1 x2.
Apply binintersectE with x1, x2, x7, and (and (PNoEq_ x7 x4 x5) (not (x4 x7))) ...PNoLt x0 x3 x2 x5 leaving 2 subgoals.
...
...
...
...
...
...