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 u12 x0.
Assume H2: 4402e.. x0 x1.
Assume H3: cf2df.. x0 x1.
Apply unknownprop_5af272e668d2d4cb72a765ba9a805ccc7fcec5ab9afe42c7f545b5c5a9294852 with u11, x0, 50e24.. 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 u11 (setminus x0 (Sing x3)))) x2.
Apply H4 with 50e24.. x0 x1.
Assume H5: x2 ∈ x0.
Assume H6: atleastp u11 (setminus x0 (Sing x2)).
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply unknownprop_81333edfacc9168b3b3f89407e06b1e8a8dc6547b388adc8951b14927468048b with setminus x0 (Sing x2), x1, 50e24.. x0 x1 leaving 109 subgoals.
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.
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).
Let x13 of type ι be given.
Assume H22: x13 ∈ setminus x0 (Sing x2).
Assume H23: 40920.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13.
Apply unknownprop_64ee1da855e89adb9c71c08e3cdb48156cac6b39db2226b89ff50f09e8ae77ee with setminus x0 (Sing x2), x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, 50e24.. x0 x1 leaving 17 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.
The subproof is completed by applying H23.
Apply unknownprop_37794886bf9a5629303e3fd31d3cef10a1d9802d65fd3e7d6618631a94b5df44 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_54a84190779d6d26f2ccaaddf0ad55cf6457f21e462f1256d1efcbc98cc56bc1 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_dbfcfa9e38042a21f1ecc388740d9853d765abb0159a11906bf2d9a2049f6227 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 ...).
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■