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 u10 x0.
Assume H2: 4402e.. x0 x1.
Assume H3: cf2df.. x0 x1.
Apply unknownprop_5af272e668d2d4cb72a765ba9a805ccc7fcec5ab9afe42c7f545b5c5a9294852 with u9, x0, 5bab1.. 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 u9 (setminus x0 (Sing x3)))) x2.
Apply H4 with 5bab1.. x0 x1.
Assume H5: x2 ∈ x0.
Assume H6: atleastp u9 (setminus x0 (Sing x2)).
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply unknownprop_16b3ab46f2a769d272bb7d84429b5755cdf1b29bc1c680745c4bda6d1b6e9013 with x0, x1, x2, setminus x0 (Sing x2), 5bab1.. x0 x1 leaving 155 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: 5bab1.. x0 x1.
The subproof is completed by applying H12.
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).
Assume H21: 06ba7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11.
Apply unknownprop_7405970cf441c5334e5a48d43db2f55997a590b7ada0907e23c5841dea9a46be with setminus x0 (Sing x2), x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, 5bab1.. x0 x1 leaving 15 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.
Apply unknownprop_b05830c71e1f162207cd6b318d1795660e83efd7c5b47b448a2c87eac97d4045 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_dbec4fbebba29119482220cc5f43283e4665fb589f8e0eef7c651c8eb3725cec 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_0cc403f2174c8077f5e819fac1da480f0fd35b57e2dced6ed71745a6eafa5b3a 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_f6b22937f2ca2f93b896d0ac769320213d90d3c76ac50c53d02629aa7f84bdd0 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_fed7234f56f6a4a09e8568f10e2996a74ad202692f18776aba7fc8cbdea12327 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_74d69e5cfedfad33160bd6f66288614a41abbef991042edcc2f22bd8692d2ad9 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_85110c3ad5b253b1838ac4eecc91753f016d7532ac1dae9bab77d29703f8149a 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_980ded8cbfc1b90a4fe56940f1963d452ec52fb2102e5e1b85b8e4c30764bc41 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_82b892ad037827628f79739044ea40b9cef6912e36888f955071d5e2c53bb12f 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_b29ec5c5f915f393f3e6b80977fbd03036239902e982d42e46ffcd5d50346565 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.
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■