Proofgold Proposition

∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ setexp (SNoS_ omega) omega ⟶ ∀ x2 . x2 ∈ setexp (SNoS_ omega) omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (ap x1 x3) x0) ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt x0 (add_SNo (ap x1 x3) (eps_ x3))) ⟶ (∀ x3 . x3 ∈ omega ⟶ ∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x1 x4) (ap x1 x3)) ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt x0 (ap x2 x3)) ⟶ (∀ x3 . x3 ∈ omega ⟶ ∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x2 x3) (ap x2 x4)) ⟶ x0 = SNoCut (prim5 omega (ap x1)) (prim5 omega (ap x2)) ⟶ x0 ∈ real

type
prop

theory
HotG

name
SNo_approx_real

proof
PUK9h..

Megalodon
SNo_approx_real

proofgold address
TMQyK..^{SNo_approx_real}

creator
12306 PrGxv../49e72..

owner
12306 PrGxv../49e72..

term root
8b24c..