Proofgold Proposition

∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo (minus_SNo x0) ⟶ x2 ∈ SNoS_ omega ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x4)) ⟶ SNo x2 ⟶ SNo (add_SNo x2 (minus_SNo x0)) ⟶ (∀ x4 . x4 ∈ SNoS_ omega ⟶ (∀ x5 . x5 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x4 (minus_SNo (ap x1 (ordsucc x3))))) (eps_ x5)) ⟶ x4 = ap x1 (ordsucc x3)) ⟶ SNo (ap x1 (ordsucc x3)) ⟶ SNoLt (ap x1 (ordsucc x3)) x2 ⟶ SNoLt 0 (add_SNo x2 (minus_SNo (ap x1 (ordsucc x3)))) ⟶ SNoLt x0 (ap x1 (ordsucc x3)) ⟶ abs_SNo (add_SNo x2 (minus_SNo x0)) = add_SNo x2 (minus_SNo x0) ⟶ x2 = ap x1 (ordsucc x3) ⟶ SNoLt x2 (ap x1 x3)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_SNo_approx_real__10__10

proofgold address
TMcRd..^{Conj_SNo_approx_real__10__10}

creator
35053 PrNpY../2925e..

owner
35061 PrNpY../1dd38..

term root
500c6..