Proofgold Proposition

∀ x0 . x0 ∈ real ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ setexp (SNoS_ omega) omega ⟶ ∀ x3 . x3 ∈ setexp (SNoS_ omega) omega ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt (ap x2 x4) x0) ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt x0 (add_SNo (ap x2 x4) (eps_ x4))) ⟶ (∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ x4 ⟶ SNoLt (ap x2 x5) (ap x2 x4)) ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt (add_SNo (ap x3 x4) (minus_SNo (eps_ x4))) x0) ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt x0 (ap x3 x4)) ⟶ (∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ x4 ⟶ SNoLt (ap x3 x4) (ap x3 x5)) ⟶ SNoCutP (prim5 omega (ap x2)) (prim5 omega (ap x3)) ⟶ x0 = SNoCut (prim5 omega (ap x2)) (prim5 omega (ap x3)) ⟶ x1) ⟶ x1

type
prop

theory
HotG

name
SNo_approx_real_rep

proof
PUK9h..

Megalodon
SNo_approx_real_rep

proofgold address
TMWxN..^{SNo_approx_real_rep}

creator
12306 PrGxv../cef4b..

owner
12306 PrGxv../cef4b..

term root
91bef..