Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2.
Assume H1: atleastp u11 x0.
Assume H2: 4402e.. x0 x1.
Assume H3: cf2df.. x0 x1.
Apply unknownprop_5af272e668d2d4cb72a765ba9a805ccc7fcec5ab9afe42c7f545b5c5a9294852 with u10, x0, a0244.. x0 x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H4: (λ x3 . and (x3 ∈ x0) (atleastp u10 (setminus x0 (Sing x3)))) x2.
Apply H4 with a0244.. x0 x1.
Assume H5: x2 ∈ x0.
Assume H6: atleastp u10 (setminus x0 (Sing x2)).
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply unknownprop_59db2a57c573c0fc5cfcdd26d1534389515c42913469b6e2577f33335a9bbf16 with x0, x1, x2, setminus x0 (Sing x2), a0244.. x0 x1 leaving 167 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
The subproof is completed by applying L7.
The subproof is completed by applying H6.
The subproof is completed by applying L8.
The subproof is completed by applying L9.
Assume H12: a0244.. x0 x1.
The subproof is completed by applying H12.
Apply unknownprop_68b92c133b687f977852f631b5b305ae65394e3c3367a0e7ec6b6039ccf2df7a with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_209cdb7ee12e89211a94a7ece2e372c148bceffca498a658d063cb9356fb8d62 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Let x3 of type ι be given.
Assume H12: x3 ∈ setminus x0 (Sing x2).
Let x4 of type ι be given.
Assume H13: x4 ∈ setminus x0 (Sing x2).
Let x5 of type ι be given.
Assume H14: x5 ∈ setminus x0 (Sing x2).
Let x6 of type ι be given.
Assume H15: x6 ∈ setminus x0 (Sing x2).
Let x7 of type ι be given.
Assume H16: x7 ∈ setminus x0 (Sing x2).
Let x8 of type ι be given.
Assume H17: x8 ∈ setminus x0 (Sing x2).
Let x9 of type ι be given.
Assume H18: x9 ∈ setminus x0 (Sing x2).
Let x10 of type ι be given.
Assume H19: x10 ∈ setminus x0 (Sing x2).
Let x11 of type ι be given.
Assume H20: x11 ∈ setminus x0 (Sing x2).
Let x12 of type ι be given.
Assume H21: x12 ∈ setminus x0 (Sing x2).
Assume H22: 0d539.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12.
Apply unknownprop_44ba0182dfeeb45a26a26fb7d11fc3205cee1ddf2fec2deb66c50f85cd865920 with setminus x0 (Sing x2), x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, a0244.. x0 x1 leaving 16 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
The subproof is completed by applying H17.
The subproof is completed by applying H18.
The subproof is completed by applying H19.
The subproof is completed by applying H20.
The subproof is completed by applying H21.
The subproof is completed by applying H22.
Apply unknownprop_2b827b77f579e13f78993563546314e5f1ca84892d07fe7b10c3bcd2ecc0ef36 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Let x3 of type ι be given.
Assume H12: x3 ∈ setminus x0 (Sing x2).
Let x4 of type ι be given.
Assume H13: x4 ∈ setminus x0 (Sing x2).
Let x5 of type ι be given.
Assume H14: x5 ∈ setminus x0 (Sing x2).
Let x6 of type ι be given.
Assume H15: x6 ∈ setminus x0 (Sing x2).
Let x7 of type ι be given.
Assume H16: x7 ∈ setminus x0 (Sing x2).
Let x8 of type ι be given.
Assume H17: x8 ∈ setminus x0 (Sing x2).
Let x9 of type ι be given.
Assume H18: x9 ∈ setminus x0 (Sing x2).
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■