Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ο be given.
Assume H0: ∀ x1 . and (Subq x1 (Power (Power (Power (Power 0))))) (∀ x2 . (∀ x3 . Subq x3 x2 ⟶ ∀ x4 x5 . and (not (tuple_p x4 x5)) (and (exactly5 x1) (not (atleast2 x3))) ⟶ SNo_ (Sing (SNoLev x1)) x5) ⟶ x2 = x2) ⟶ x0.
Apply H0 with Power (Power (Power (Power 0))).
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with Subq (Power (Power (Power (Power 0)))) (Power (Power (Power (Power 0)))), ∀ x1 . (∀ x2 . Subq x2 x1 ⟶ ∀ x3 x4 . and (not (tuple_p x3 x4)) (and (exactly5 (Power (Power (Power (Power 0))))) (not (atleast2 x2))) ⟶ SNo_ (Sing (SNoLev (Power (Power (Power (Power 0)))))) x4) ⟶ x1 = x1 leaving 2 subgoals.
set y1 to be ...
set y2 to be ...
set y3 to be ...
set y4 to be ...
set y5 to be ...
set y6 to be ...
Claim L1: ...
...
Apply L1 with λ x7 x8 : ο . y6 x7, λ x7 x8 : ο . y6 x7, λ x7 x8 : ο . y6 x7, λ x7 x8 : ο . y6 x7 leaving 4 subgoals.
Let x7 of type ο → ο → ο be given.
Assume H2: x7 (Subq (Power (Power (Power (Power 0)))) (Power (Power (Power (Power 0)))) = (λ x8 x9 . ∀ x10 . In x10 x8 ⟶ In x10 x9) (Power (Power (Power (Power 0)))) (Power (Power (Power (Power 0))))) (Subq (Power (Power (Power (Power 0)))) (Power (Power (Power (Power 0)))) = (λ x8 x9 . ∀ x10 . In x10 x8 ⟶ In x10 x9) (Power (Power (Power (Power 0)))) (Power (Power (Power (Power 0))))).
The subproof is completed by applying H2.
set y7 to be λ x7 : ι → ο . Subq (Power (Power (Power (Power 0)))) (Power (Power (Power (Power 0)))) = x7 (Power (Power (Power (Power 0))))
set y8 to be λ x8 : ι → ι → ο . Subq (Power (Power (Power (Power 0)))) = x8 (Power (Power (Power (Power 0))))
Apply unknownprop_5d43e074a46031aba9b972e1346a32eab5bc6d7f8cd872222d3a15fe3889dd90 with λ x9 x10 : ι → ι → ο . y8 x9, λ x9 x10 : ι → ο . y8 x9 leaving 2 subgoals.
Let x9 of type (ι → ο) → (ι → ο) → ο be given.
Assume H2: x9 (Subq (Power (Power (Power (Power 0))))) (Subq (Power (Power (Power (Power 0))))).
The subproof is completed by applying H2.
Let x9 of type ο → ο → ο be given.
Assume H2: x9 (Subq (Power (Power (Power (Power 0)))) (Power (Power (Power (Power 0))))) (Subq (Power (Power (Power (Power 0)))) (Power (Power (Power (Power 0))))).
The subproof is completed by applying H2.
Let x7 of type ο → ο → ο be given.
Assume H2: x7 (Subq (Power (Power (Power (Power 0)))) (Power (Power (Power (Power 0))))) (Subq ... ...).
...
...
...
■