Search for blocks/addresses/...

Proofgold Proof

pf
set y0 to be ...
set y1 to be ...
set y2 to be ...
Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with (∃ x3 . and (y0 x3) (∃ x4 . and (y1 x3 x4) (∃ x5 . and (In x5 0) (∀ x6 . In x6 x5 ⟶ ∃ x7 . atleast2 x7)))) ⟶ y2.
Assume H0: not ((∃ x3 . and (y0 x3) (∃ x4 . and (y1 x3 x4) (∃ x5 . and (In x5 0) (∀ x6 . In x6 x5 ⟶ ∃ x7 . atleast2 x7)))) ⟶ y2).
set y3 to be ...
Claim L1: ...
...
set y4 to be ...
Claim L2: ...
...
set y5 to be ...
Claim L3: ...
...
Apply notE with In (Eps_i y3) 0 leaving 2 subgoals.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with In (Eps_i y3) 0.
Assume H4: In (Eps_i y3) 0.
Claim L5: In (Eps_i y3) 0
The subproof is completed by applying H4.
Apply notE with In (Eps_i y3) 0 leaving 2 subgoals.
Apply unknownprop_e71e48a383f529f68afdc14358189461de3d3a97993b62a8cb1f5e89e6531b39 with λ x6 . In x6 0, Eps_i y3.
The subproof is completed by applying unknownprop_641980b1f679699e58af9b75e8660e324a5a8b56d6549ff9c993636d65c0d9dc.
The subproof is completed by applying L5.
Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with In (Eps_i y3) 0, ∀ x6 . In x6 (Eps_i y3) ⟶ ∃ x7 . atleast2 x7.
set y6 to be ...
Apply L1 with λ x7 x8 : ι → ο . y6 x7 leaving 2 subgoals.
The subproof is completed by applying Eps_i_ex with y4.
Apply unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with y2 (Eps_i (y6 y1 y2)) (Eps_i (y5 y2 y6 y1)), ∃ x7 . and (In x7 0) (∀ x8 . In x8 x7 ⟶ ∃ x9 . atleast2 x9).
set y7 to be ...
set y8 to be ...
set y9 to be ...
set y10 to be ...
Apply L2 with λ x11 x12 : (ι → ι → ο) → ((ι → ο) → (ι → ι → ο) → ι → ο) → (ι → ο) → ι → ο . y10 x11, λ x11 x12 : ((ι → ο) → (ι → ι → ο) → ι → ο) → (ι → ο) → ι → ο . y10 x11, λ x11 x12 : (ι → ο) → ι → ο . y10 x11, λ x11 x12 : ι → ο . y10 x11 leaving 5 subgoals.
Let x11 of type (((ι → ο) → (ι → ι → ο) → ι → ο) → (ι → ο) → ι → ο) → (((ι → ο) → (ι → ι → ο) → ι → ο) → (ι → ο) → ι → ο) → ο be given.
Assume H4: x11 (y6 y3) (y6 y3).
The subproof is completed by applying H4.
Let x11 of type ((ι → ο) → ι → ο) → ((ι → ο) → ι → ο) → ο be given.
Assume H4: x11 (y7 y4 y8) (y7 y4 y8).
The subproof is completed by applying H4.
Let x11 of type (ι → ο) → (ι → ο) → ο be given.
Assume H4: x11 (y8 y5 y9 y4) (y8 y5 y9 y4).
The subproof is completed by applying H4.
The subproof is completed by applying Eps_i_ex with y9 y6 y10 y5.
Apply unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with y5 (Eps_i (y10 y5 y6)), ∃ x11 . and (y6 (Eps_i (y10 y5 y6)) x11) (∃ x12 . and (In x12 0) (∀ x13 . In x13 x12 ⟶ ∃ x14 . atleast2 x14)).
set y11 to be ...
set y12 to be ...
set y13 to be ...
Apply L3 with λ x14 x15 : (ι → ο) → (ι → ι → ο) → ι → ο . y13 x14, λ x14 x15 : (ι → ι → ο) → ι → ο . y13 x14, λ x14 x15 : ι → ο . y13 x14 leaving 4 subgoals.
Let x14 of type ((ι → ι → ο) → ι → ο) → ((ι → ι → ο) → ι → ο) → ο be given.
Assume H4: x14 (y11 y6) (y11 y6).
The subproof is completed by applying H4.
Let x14 of type (ι → ο) → (ι → ο) → ο be given.
Assume H4: x14 (y12 y7 y8) (y12 y7 y8).
The subproof is completed by applying H4.
The subproof is completed by applying Eps_i_ex with y13 y8 y9.
Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with ∃ x14 . and (y8 x14) (∃ x15 . and (y9 x14 x15) (∃ x16 . and (In x16 0) (∀ x17 . In x17 x16 ⟶ ∃ x18 . atleast2 x18))), not y10.
Apply unknownprop_f900d1a90bf5d347b18522211f82fb33d0afc1127e77502891326c698226d151 with ∃ x14 . and (y8 x14) (∃ x15 . and (y9 x14 x15) (∃ x16 . and (In x16 0) (∀ x17 . In x17 x16 ⟶ ∃ x18 . atleast2 x18))), ....
...
■