Proofgold Proposition

∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10))))) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x7 x9)))) ⟶ (∀ x6 . 1eb0a.. x6 ⟶ SNo (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . 1eb0a.. x7 ⟶ and (SNo (x6 x7)) (∃ x8 . and (SNo x8) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) x8))) ⟶ ∀ x7 . 1eb0a.. x7 ⟶ SNo (053de.. x0 x1 x2 x3 x4 x5 x6 x7)

type
prop

theory
HotG

name
-

proof
PUY4m..

Megalodon
-

proofgold address
TMcSR..

creator
28250 PrQUS../f6eb4..

owner
28250 PrQUS../f6eb4..

term root
4271d..