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 x1))) (eps_ x6)) ⟶ x5 = x1) ⟶ (∀ 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 (ap (lam omega (λ x6 . add_SNo (ap x2 (ordsucc x6)) (ap x3 (ordsucc x6)))) x5) (minus_SNo (eps_ x5))) (add_SNo x0 x1)) ⟶ SNo x4 ⟶ SNoLt x1 x4 ⟶ x4 ∈ SNoS_ omega ⟶ not (∀ x5 : ο . (∀ x6 . and (x6 ∈ omega) (SNoLe (ap (lam omega (λ x7 . add_SNo (ap x2 (ordsucc x7)) (ap x3 (ordsucc x7)))) x6) (add_SNo x0 x4)) ⟶ x5) ⟶ x5) ⟶ x4 = x1 ⟶ ∀ x5 : ο . x5

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_real_add_SNo__6__10

proofgold address
TMcut..^{Conj_real_add_SNo__6__10}

creator
35053 PrNpY../86779..

owner
35061 PrNpY../0d173..

term root
40aea..