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 u13 x0.
Assume H2: 4402e.. x0 x1.
Assume H3: cf2df.. x0 x1.
Let x2 of type ο be given.
Assume H4: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ 6799e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x2.
Apply unknownprop_5af272e668d2d4cb72a765ba9a805ccc7fcec5ab9afe42c7f545b5c5a9294852 with u12, x0, x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Assume H5: (λ x4 . and (x4 ∈ x0) (atleastp u12 (setminus x0 (Sing x4)))) x3.
Apply H5 with x2.
Assume H6: x3 ∈ x0.
Assume H7: atleastp u12 (setminus x0 (Sing x3)).
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Apply unknownprop_4d3a304ee708e4dde8cc412738da20a8afb41db314e5b7176ec7b8216d27d904 with setminus x0 (Sing x3), x1, x2 leaving 16 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying H7.
The subproof is completed by applying L9.
The subproof is completed by applying L10.
Let x4 of type ι be given.
Assume H13: x4 ∈ setminus x0 (Sing x3).
Let x5 of type ι be given.
Assume H14: x5 ∈ setminus x0 (Sing x3).
Let x6 of type ι be given.
Assume H15: x6 ∈ setminus x0 (Sing x3).
Let x7 of type ι be given.
Assume H16: x7 ∈ setminus x0 (Sing x3).
Let x8 of type ι be given.
Assume H17: x8 ∈ setminus x0 (Sing x3).
Let x9 of type ι be given.
Assume H18: x9 ∈ setminus x0 (Sing x3).
Let x10 of type ι be given.
Assume H19: x10 ∈ setminus x0 (Sing x3).
Let x11 of type ι be given.
Assume H20: x11 ∈ setminus x0 (Sing x3).
Let x12 of type ι be given.
Assume H21: x12 ∈ setminus x0 (Sing x3).
Let x13 of type ι be given.
Assume H22: x13 ∈ setminus x0 (Sing x3).
Let x14 of type ι be given.
Assume H23: x14 ∈ setminus x0 (Sing x3).
Let x15 of type ι be given.
Assume H24: x15 ∈ setminus x0 (Sing x3).
Assume H25: d1f25.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15.
Apply unknownprop_3b7b17c96119c45521ca37b9abaa00f9c083c489edc4ddac9ad811e050e2b762 with setminus x0 (Sing x3), x0, x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x2 leaving 18 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 H6.
The subproof is completed by applying L11.
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.
The subproof is completed by applying H24.
The subproof is completed by applying H25.
Let x4 of type ι be given.
Assume H13: x4 ∈ setminus x0 ....
...
...
...
...
...
...
...
...
...
...
...
■