Proofgold Proposition

∀ x0 x1 x2 x3 x4 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1) ⟶ (∀ x5 . x5 ∈ SNoS_ omega ⟶ (∀ x6 . x6 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x5 (minus_SNo x0))) (eps_ x6)) ⟶ x5 = x0) ⟶ (∀ x5 . x5 ∈ omega ⟶ SNo (ap (lam omega (λ x6 . add_SNo (ap x2 (ordsucc x6)) (ap x3 (ordsucc x6)))) x5)) ⟶ (∀ x5 . x5 ∈ omega ⟶ SNoLt (add_SNo x0 x1) (add_SNo (ap (lam omega (λ x6 . add_SNo (ap x2 (ordsucc x6)) (ap x3 (ordsucc x6)))) x5) (eps_ x5))) ⟶ SNoLt x4 x0 ⟶ x4 ∈ SNoS_ omega ⟶ not (∀ x5 : ο . (∀ x6 . and (x6 ∈ omega) (SNoLe (add_SNo x4 x1) (ap (lam omega (λ x7 . add_SNo (ap x2 (ordsucc x7)) (ap x3 (ordsucc x7)))) x6)) ⟶ x5) ⟶ x5) ⟶ SNoLt 0 (add_SNo x0 (minus_SNo x4)) ⟶ x4 = x0 ⟶ ∀ x5 : ο . x5

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_real_add_SNo__18__6

proofgold address
TMZUF..^{Conj_real_add_SNo__18__6}

creator
35053 PrNpY../ad7ed..

owner
35061 PrNpY../16606..

term root
fd987..