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 x2.
Let x3 of type ι → ο be given.
Assume H1: a59df.. x0 x1 x2 x3.
Claim L2: ...
...
Apply H1 with 47618.. x0 x1 x2 x3.
Assume H3: 8033b.. x0 x1 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)).
Assume H4: 8033b.. x0 x1 (4ae4a.. x2) (λ x4 . or (x3 x4) (x4 = x2)).
Apply H3 with 47618.. x0 x1 x2 x3.
Assume H5: 6f2c4.. x0 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)).
Assume H6: dafc2.. x1 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)).
Apply H4 with 47618.. x0 x1 x2 x3.
Assume H7: 6f2c4.. x0 (4ae4a.. x2) (λ x4 . or (x3 x4) (x4 = x2)).
Assume H8: dafc2.. x1 (4ae4a.. x2) (λ x4 . or (x3 x4) (x4 = x2)).
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Apply andI with cae4c.. x0 x2 x3, bc2b0.. x1 x2 x3 leaving 2 subgoals.
Let x4 of type ι be given.
Assume H13: ordinal x4.
Let x5 of type ι → ο be given.
Assume H14: x0 x4 x5.
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Apply unknownprop_73b6444bcb1b9cb998566f55e286e78644e785a99d955b3281cf269899ab486c with x2, x4, x3, x5, 40dde.. x4 x5 x2 x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H13.
Assume H18: or (40dde.. x2 x3 x4 x5) (and (x2 = x4) (PNoEq_ x2 x3 x5)).
Apply H18 with 40dde.. x4 x5 x2 x3 leaving 2 subgoals.
Assume H19: 40dde.. x2 x3 x4 x5.
Apply unknownprop_1c12738cd89f8c615a541c15b6797bba2a5be97ab5e514c9fd76b3fef06e2aa9 with x2, x4, x3, x5, 40dde.. x4 x5 x2 x3 leaving 4 subgoals.
The subproof is completed by applying H19.
Assume H20: PNoLt_ (d3786.. x2 x4) x3 x5.
Apply H20 with 40dde.. x4 x5 x2 x3.
Let x6 of type ι be given.
Assume H21: (λ x7 . and (prim1 x7 (d3786.. x2 x4)) (and (and (PNoEq_ x7 x3 x5) (not (x3 x7))) (x5 x7))) x6.
Apply H21 with 40dde.. x4 x5 x2 x3.
Assume H22: prim1 x6 (d3786.. x2 x4).
Assume H23: and (and (PNoEq_ x6 x3 x5) (not (x3 x6))) (x5 x6).
Apply H23 with 40dde.. x4 x5 x2 x3.
Assume H24: and (PNoEq_ x6 x3 x5) (not (x3 x6)).
Apply H24 with x5 x6 ⟶ 40dde.. x4 x5 x2 x3.
Assume H25: PNoEq_ x6 x3 x5.
Assume H26: not (x3 x6).
Assume H27: x5 x6.
Apply FalseE with 40dde.. x4 x5 x2 x3.
Apply unknownprop_1ac99d32a7ae5dc08fd640ea6c8b661df6b3535fe85e88b30b17c3701cb4c7ce with x2, x4, x6, False leaving 2 subgoals.
The subproof is completed by applying H22.
Assume H28: prim1 x6 x2.
Assume H29: ....
...
...
...
...
...
...
■