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 u9 x0.
Assume H2: 4402e.. x0 x1.
Assume H3: cf2df.. x0 x1.
Apply unknownprop_5af272e668d2d4cb72a765ba9a805ccc7fcec5ab9afe42c7f545b5c5a9294852 with u8, x0, 0946c.. 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 u8 (setminus x0 (Sing x3)))) x2.
Apply H4 with 0946c.. x0 x1.
Assume H5: x2 ∈ x0.
Assume H6: atleastp u8 (setminus x0 (Sing x2)).
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply unknownprop_d130c2da353f8a96ebfd044dc62865ee3ee198eb4370e3aa9882d0f235dc1fef with setminus x0 (Sing x2), x1, 0946c.. x0 x1 leaving 183 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).
Assume H20: 372ed.. x1 x3 x4 x5 x6 x7 x8 x9 x10.
Apply unknownprop_2503b41b87628a0fe73525e7982d2924584a1691e66e4c73b8f17229b60cff32 with setminus x0 (Sing x2), x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, 0946c.. x0 x1 leaving 14 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.
Apply unknownprop_01df244cb3ea0b30b181ac74a8c84b0f04ebf3b2c8ab5bad325a7a85ef809ec1 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).
Assume H20: f7c3d.. x1 x3 x4 x5 x6 x7 x8 x9 x10.
Apply unknownprop_97eaf25d02394840101a836c283d80091df066a4464287689bde7c692088236b with setminus x0 (Sing x2), x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, 0946c.. x0 x1 leaving 14 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.
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■