Search for blocks/addresses/...

Proofgold Proof

pf
set y0 to be ...
set y1 to be ...
Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with (∀ x2 . Subq x2 y0 ⟶ ∃ x3 . and (In x3 x2) (∀ x4 . ((∀ x5 . (∃ x6 . and (Subq x6 x2) (((exactly5 x5 ⟶ not (exactly2 x4)) ⟶ (exactly3 x5 ⟶ not (SNo x5)) ⟶ not (atleast6 x5)) ⟶ not (exactly4 x6))) ⟶ not (exactly4 x3)) ⟶ atleast2 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0)) ⟶ not (Subq x4 x3))) ⟶ y1.
Assume H0: not ((∀ x2 . Subq x2 y0 ⟶ ∃ x3 . and (In x3 x2) (∀ x4 . ((∀ x5 . (∃ x6 . and (Subq x6 x2) (((exactly5 x5 ⟶ not (exactly2 x4)) ⟶ (exactly3 x5 ⟶ not (SNo x5)) ⟶ not (atleast6 x5)) ⟶ not (exactly4 x6))) ⟶ not (exactly4 x3)) ⟶ atleast2 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0)) ⟶ not (Subq x4 x3))) ⟶ y1).
set y2 to be ...
Claim L1: ...
...
set y3 to be ...
Claim L2: ...
...
Apply notE with Subq 0 y0 leaving 2 subgoals.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with Subq 0 y0.
Assume H3: Subq 0 y0.
Apply notE with In (Eps_i (y3 0)) 0 leaving 2 subgoals.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with In (Eps_i (y3 0)) 0.
Assume H4: In (Eps_i (y3 0)) 0.
Claim L5: In (Eps_i (y3 0)) 0
The subproof is completed by applying H4.
Apply notE with In (Eps_i (y3 0)) 0 leaving 2 subgoals.
Apply unknownprop_e71e48a383f529f68afdc14358189461de3d3a97993b62a8cb1f5e89e6531b39 with λ x4 . In x4 0, Eps_i (y3 0).
The subproof is completed by applying unknownprop_641980b1f679699e58af9b75e8660e324a5a8b56d6549ff9c993636d65c0d9dc.
The subproof is completed by applying L5.
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with In (Eps_i (y3 0)) 0.
Assume H7: not (In (Eps_i (y3 0)) 0).
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply notE with not (In (Eps_i (y3 0)) 0) leaving 2 subgoals.
Apply unknownprop_b6f324b8b8816479c1306f727dc14fcaec89d74751f4c27e6f83110cd1b0b495 with In (Eps_i (y3 0)) 0.
Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with In (Eps_i (y3 0)) 0, ∀ x4 . ((∀ x5 . (∃ x6 . and (Subq x6 0) (((exactly5 x5 ⟶ not (exactly2 x4)) ⟶ (exactly3 x5 ⟶ not (SNo x5)) ⟶ not (atleast6 x5)) ⟶ not (exactly4 x6))) ⟶ not (exactly4 (Eps_i (y3 0)))) ⟶ atleast2 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0)) ⟶ not (Subq x4 (Eps_i (y3 0))).
set y4 to be ...
set y5 to be ...
Apply L9 with λ x6 x7 : ι → ι → ο . y5 x6, λ x6 x7 : ι → ο . y5 x6 leaving 3 subgoals.
Let x6 of type (ι → ο) → (ι → ο) → ο be given.
Assume H12: x6 (y4 0) (y4 0).
The subproof is completed by applying H12.
The subproof is completed by applying Eps_i_ex with y5 0.
Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with ∀ x6 . ... ⟶ ∃ x7 . and (In x7 x6) (∀ x8 . ... ⟶ not (Subq x8 ...)), ..., 0 leaving 2 subgoals.
...
...
...
...
■