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 : ι → ο . 40dde.. x0 x3 x1 x4 ⟶ 40dde.. x1 x4 x2 x5 ⟶ 40dde.. x0 x3 x2 x5.
Assume H3: TransSet x0.
Assume H4: ∀ x3 . prim1 x3 x0 ⟶ TransSet x3.
Apply H2 with ∀ x3 x4 x5 : ι → ο . 40dde.. x0 x3 x1 x4 ⟶ 40dde.. x1 x4 x2 x5 ⟶ 40dde.. x0 x3 x2 x5.
Assume H5: TransSet x2.
Assume H6: ∀ x3 . prim1 x3 x2 ⟶ TransSet x3.
Let x3 of type ι → ο be given.
Let x4 of type ι → ο be given.
Let x5 of type ι → ο be given.
Assume H7: 40dde.. x0 x3 x1 x4.
Assume H8: 40dde.. x1 x4 x2 x5.
Apply unknownprop_1c12738cd89f8c615a541c15b6797bba2a5be97ab5e514c9fd76b3fef06e2aa9 with x0, x1, x3, x4, 40dde.. x0 x3 x2 x5 leaving 4 subgoals.
The subproof is completed by applying H7.
Assume H9: PNoLt_ (d3786.. x0 x1) x3 x4.
Apply H9 with 40dde.. x0 x3 x2 x5.
Let x6 of type ι be given.
Assume H10: (λ x7 . and (prim1 x7 (d3786.. x0 x1)) (and (and (PNoEq_ x7 x3 x4) (not (x3 x7))) (x4 x7))) x6.
Apply H10 with 40dde.. x0 x3 x2 x5.
Assume H11: prim1 x6 (d3786.. x0 x1).
Apply unknownprop_1ac99d32a7ae5dc08fd640ea6c8b661df6b3535fe85e88b30b17c3701cb4c7ce with x0, x1, x6, and (and (PNoEq_ x6 x3 x4) (not (x3 x6))) (x4 x6) ⟶ 40dde.. x0 x3 x2 x5 leaving 2 subgoals.
The subproof is completed by applying H11.
Assume H12: prim1 x6 x0.
Assume H13: prim1 x6 x1.
Assume H14: and (and (PNoEq_ x6 x3 x4) (not (x3 x6))) (x4 x6).
Apply H14 with 40dde.. x0 x3 x2 x5.
Assume H15: and (PNoEq_ x6 x3 x4) (not (x3 x6)).
Apply H15 with x4 x6 ⟶ 40dde.. x0 x3 x2 x5.
Assume H16: PNoEq_ x6 x3 x4.
Assume H17: not (x3 x6).
Assume H18: x4 x6.
Claim L19: ...
...
Apply unknownprop_1c12738cd89f8c615a541c15b6797bba2a5be97ab5e514c9fd76b3fef06e2aa9 with x1, x2, x4, x5, 40dde.. x0 x3 x2 x5 leaving 4 subgoals.
The subproof is completed by applying H8.
Assume H20: PNoLt_ (d3786.. x1 x2) x4 x5.
Apply H20 with 40dde.. x0 x3 x2 x5.
Let x7 of type ι be given.
Assume H21: (λ x8 . and (prim1 x8 (d3786.. x1 x2)) (and (and (PNoEq_ x8 x4 x5) (not (x4 x8))) (x5 x8))) x7.
Apply H21 with 40dde.. x0 x3 x2 x5.
Assume H22: prim1 x7 (d3786.. x1 x2).
Apply unknownprop_1ac99d32a7ae5dc08fd640ea6c8b661df6b3535fe85e88b30b17c3701cb4c7ce with x1, x2, x7, and (and (PNoEq_ x7 x4 ...) ...) ... ⟶ 40dde.. x0 x3 x2 x5 leaving 2 subgoals.
...
...
...
...
...
...
■