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: bc2b0.. x0 x1 x3.
Let x4 of type ι be given.
Assume H3: prim1 x4 x2.
Let x5 of type ι → ο be given.
Assume H4: 610d8.. x0 x4 x5.
Apply H0 with 40dde.. x2 x3 x4 x5.
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.. x2 x3 x4 x5.
Let x6 of type ι be given.
Assume H12: (λ x7 . and (ordinal x7) (∃ x8 : ι → ο . and (x0 x7 x8) (35b9b.. x7 x8 x4 x5))) x6.
Apply H12 with 40dde.. x2 x3 x4 x5.
Assume H13: ordinal x6.
Assume H14: ∃ x7 : ι → ο . and (x0 x6 x7) (35b9b.. x6 x7 x4 x5).
Apply H14 with 40dde.. x2 x3 x4 x5.
Let x7 of type ι → ο be given.
Assume H15: (λ x8 : ι → ο . and (x0 x6 x8) (35b9b.. x6 x8 x4 x5)) x7.
Apply H15 with 40dde.. x2 x3 x4 x5.
Assume H16: x0 x6 x7.
Assume H17: 35b9b.. x6 x7 x4 x5.
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Apply unknownprop_73b6444bcb1b9cb998566f55e286e78644e785a99d955b3281cf269899ab486c with x4, x2, x5, x3, 40dde.. x2 x3 x4 x5 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.. x2 x3 x4 x5 leaving 2 subgoals.
Assume H23: 40dde.. x4 x5 x2 x3.
Apply FalseE with 40dde.. x2 x3 x4 x5.
Apply unknownprop_1c12738cd89f8c615a541c15b6797bba2a5be97ab5e514c9fd76b3fef06e2aa9 with x4, x2, x5, x3, False leaving 4 subgoals.
The subproof is completed by applying H23.
Apply unknownprop_71c983f9883b4f28b7b9554926463bb4627a33e675a17eaba24400b257e59781 with x4, x2, λ x8 x9 . PNoLt_ x9 x5 x3 ⟶ False leaving 2 subgoals.
The subproof is completed by applying L11.
Assume H24: PNoLt_ x4 x5 x3.
Apply H24 with False.
Apply unknownprop_ab808d03ac7e78aa83f072ed699b3ccc158aab0a67cf54e5638eb5435d34c11d with x1, x3, ∀ x8 . (λ x9 . and (prim1 x9 x4) (and (and (PNoEq_ x9 x5 x3) (not (x5 x9))) (x3 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.
The subproof is completed by applying L19.
Apply unknownprop_ac970f51deca19d20e9a8350c3518ea802533ebd2768fe799c9b97ea3dd03596 with x4, x1, x5, x3.
Apply unknownprop_71c983f9883b4f28b7b9554926463bb4627a33e675a17eaba24400b257e59781 with x4, x1, λ x8 x9 . PNoLt_ x9 x5 x3 leaving 2 subgoals.
The subproof is completed by applying L21.
The subproof is completed by applying H24.
Assume H24: prim1 x4 x2.
Assume H25: PNoEq_ x4 x5 x3.
Assume H26: x3 x4.
Apply unknownprop_ab808d03ac7e78aa83f072ed699b3ccc158aab0a67cf54e5638eb5435d34c11d with x1, x3.
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.
The subproof is completed by applying L19.
Apply unknownprop_9bcd3ca68066c7069c00444b0b53fe3ae6267cb29974000b72e5fe8327360c0b with x4, x1, x5, x3 leaving 3 subgoals.
The subproof is completed by applying L20.
The subproof is completed by applying H25.
The subproof is completed by applying H26.
Assume H24: prim1 x2 x4.
Apply FalseE with PNoEq_ x2 x5 x3 ⟶ not (x5 x2) ⟶ False.
Apply unknownprop_f1a526a64fd91875cd825eea7f2e7776b7f0e7be5dcee74dc03af1d7886d1eb6 with x2, x4 leaving 2 subgoals.
The subproof is completed by applying H24.
The subproof is completed by applying H3.
Assume H23: and (x4 = x2) (PNoEq_ x4 x5 x3).
Apply H23 with 40dde.. x2 x3 x4 x5.
Assume H24: x4 = x2.
...
...
■