Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι(ιο) → ο be given.
Let x1 of type ι(ιο) → ο be given.
Assume H0: ed32f.. x0 x1.
Let x2 of type ι be given.
Assume H1: ordinal x2.
Apply H1 with PNo_lenbdd x2 x0PNo_lenbdd x2 x1∃ x3 . and (prim1 x3 (4ae4a.. x2)) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4).
Assume H2: TransSet x2.
Assume H3: ∀ x3 . prim1 x3 x2TransSet x3.
Assume H4: PNo_lenbdd x2 x0.
Assume H5: PNo_lenbdd x2 x1.
Claim L6: ...
...
Apply unknownprop_279ca38e3c0e2b4f26dd5774d309c0af105ab029ebe30b2ac5354aa8f00721d3 with x0, x1, x2, ∃ x3 . and (prim1 x3 (4ae4a.. x2)) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H7: ∃ x3 : ι → ο . 078b6.. x0 x1 x2 x3.
Apply H7 with ∃ x3 . and (prim1 x3 (4ae4a.. x2)) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4).
Let x3 of type ιο be given.
Assume H8: 078b6.. x0 x1 x2 x3.
Apply H8 with ∃ x4 . and (prim1 x4 (4ae4a.. x2)) (∃ x5 : ι → ο . a59df.. x0 x1 x4 x5).
Assume H9: 8033b.. x0 x1 x2 x3.
Apply H9 with (∀ x4 : ι → ο . 8033b.. x0 x1 x2 x4PNoEq_ x2 x3 x4)∃ x4 . and (prim1 x4 (4ae4a.. x2)) (∃ x5 : ι → ο . a59df.. x0 x1 x4 x5).
Assume H10: 6f2c4.. x0 x2 x3.
Assume H11: dafc2.. x1 x2 x3.
Assume H12: ∀ x4 : ι → ο . 8033b.. x0 x1 x2 x4PNoEq_ x2 x3 x4.
Let x4 of type ο be given.
Assume H13: ∀ x5 . and (prim1 x5 (4ae4a.. x2)) (∃ x6 : ι → ο . a59df.. x0 x1 x5 x6)x4.
Apply H13 with x2.
Apply andI with prim1 x2 (4ae4a.. x2), ∃ x5 : ι → ο . a59df.. x0 x1 x2 x5 leaving 2 subgoals.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x2.
Let x5 of type ο be given.
Assume H14: ∀ x6 : ι → ο . a59df.. x0 x1 x2 x6x5.
Apply H14 with x3.
Apply unknownprop_b612bf4d512ad6227e8bff43683128e0125ebf717976bdcb0c23c328b2d194b7 with x0, x1, x2, x3 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H9.
Assume H7: ∃ x3 . and (prim1 x3 x2) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4).
Apply H7 with ∃ x3 . and (prim1 x3 (4ae4a.. x2)) (∃ x4 : ι → ο . a59df.. x0 x1 x3 x4).
Let x3 of type ι be given.
Assume H8: (λ x4 . and (prim1 x4 x2) (∃ x5 : ι → ο . a59df.. x0 x1 x4 x5)) x3.
Apply H8 with ∃ x4 . and (prim1 x4 (4ae4a.. x2)) (∃ x5 : ι → ο . a59df.. x0 x1 x4 x5).
Assume H9: prim1 x3 x2.
Assume H10: ∃ x4 : ι → ο . a59df.. x0 x1 x3 x4.
Let x4 of type ο be given.
Assume H11: ∀ x5 . and (prim1 x5 (4ae4a.. x2)) ...x4.
...