Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι be given.
Assume H0: ordinal x1.
Let x2 of type ι be given.
Assume H1: prim1 x2 (4ae4a.. x1).
Let x3 of type ι → ο be given.
Assume H2: cae4c.. x0 x1 x3.
Let x4 of type ι be given.
Assume H3: prim1 x4 x2.
Let x5 of type ι → ο be given.
Assume H4: 8356a.. x0 x4 x5.
Apply H0 with 40dde.. x4 x5 x2 x3.
Assume H5: TransSet x1.
Assume H6: ∀ x6 . prim1 x6 x1 ⟶ TransSet x6.
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply H4 with 40dde.. x4 x5 x2 x3.
Let x6 of type ι be given.
Assume H12: (λ x7 . and (ordinal x7) (∃ x8 : ι → ο . and (x0 x7 x8) (35b9b.. x4 x5 x7 x8))) x6.
Apply H12 with 40dde.. x4 x5 x2 x3.
Assume H13: ordinal x6.
Assume H14: ∃ x7 : ι → ο . and (x0 x6 x7) (35b9b.. x4 x5 x6 x7).
Apply H14 with 40dde.. x4 x5 x2 x3.
Let x7 of type ι → ο be given.
Assume H15: (λ x8 : ι → ο . and (x0 x6 x8) (35b9b.. x4 x5 x6 x8)) x7.
Apply H15 with 40dde.. x4 x5 x2 x3.
Assume H16: x0 x6 x7.
Assume H17: 35b9b.. x4 x5 x6 x7.
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Apply unknownprop_73b6444bcb1b9cb998566f55e286e78644e785a99d955b3281cf269899ab486c with x4, x2, x5, x3, 40dde.. x4 x5 x2 x3 leaving 4 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L8.
Assume H22: or (40dde.. x4 x5 x2 x3) (and (x4 = x2) (PNoEq_ x4 x5 x3)).
Apply H22 with 40dde.. x4 x5 x2 x3 leaving 2 subgoals.
Assume H23: 40dde.. x4 x5 x2 x3.
The subproof is completed by applying H23.
Assume H23: and (x4 = x2) (PNoEq_ x4 x5 x3).
Apply H23 with 40dde.. x4 x5 x2 x3.
Assume H24: x4 = x2.
Apply FalseE with PNoEq_ x4 x5 x3 ⟶ 40dde.. x4 x5 x2 x3.
Apply In_irref with x2.
Apply H24 with λ x8 x9 . prim1 x8 x2.
The subproof is completed by applying H3.
Assume H22: 40dde.. x2 x3 x4 x5.
Apply FalseE with 40dde.. x4 x5 x2 x3.
Apply unknownprop_1c12738cd89f8c615a541c15b6797bba2a5be97ab5e514c9fd76b3fef06e2aa9 with x2, x4, x3, x5, False leaving 4 subgoals.
The subproof is completed by applying H22.
Apply unknownprop_c3bea5de1408165b06631f86b9f132e6a4154b60456b567e9159f0db1e9656af with x2, x4, λ x8 x9 . PNoLt_ x9 x3 x5 ⟶ False.
Apply unknownprop_71c983f9883b4f28b7b9554926463bb4627a33e675a17eaba24400b257e59781 with x4, x2, λ x8 x9 . PNoLt_ x9 x3 x5 ⟶ False leaving 2 subgoals.
The subproof is completed by applying L11.
Assume H23: PNoLt_ x4 x3 x5.
Apply H23 with False.
Apply unknownprop_ab808d03ac7e78aa83f072ed699b3ccc158aab0a67cf54e5638eb5435d34c11d with x1, x3, ∀ x8 . (λ x9 . and (prim1 x9 x4) (and (and (PNoEq_ x9 x3 x5) (not (x3 x9))) (x5 x9))) x8 ⟶ False.
Apply unknownprop_37f5b5c6ee0011f262b499567d54413188e5bd83bd5555e5f3caca08d2fd472f with x1, x4, x1, x3, x5, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L10.
The subproof is completed by applying H0.
Apply unknownprop_ac970f51deca19d20e9a8350c3518ea802533ebd2768fe799c9b97ea3dd03596 with x1, x4, x3, x5.
Apply unknownprop_c3bea5de1408165b06631f86b9f132e6a4154b60456b567e9159f0db1e9656af with x1, x4, λ x8 x9 . PNoLt_ x9 x3 x5.
Apply unknownprop_71c983f9883b4f28b7b9554926463bb4627a33e675a17eaba24400b257e59781 with x4, x1, λ x8 x9 . PNoLt_ x9 x3 x5 leaving 2 subgoals.
The subproof is completed by applying L21.
The subproof is completed by applying H23.
The subproof is completed by applying L19.
Assume H23: prim1 x2 ....
...
...
■