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 (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 ⟶ 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 x4 x1)) ⟶ x5) ⟶ x5) ⟶ SNoLt 0 (add_SNo x4 (minus_SNo x0)) ⟶ x4 = x0 ⟶ ∀ x5 : ο . x5

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_real_add_SNo__10__7

proofgold address
TMUhQ..^{Conj_real_add_SNo__10__7}

creator
35053 PrNpY../4f8d2..

owner
35061 PrNpY../80554..

term root
0e831..