Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . x0real∀ x1 : ο . (∀ x2 . x2setexp (SNoS_ omega) omega∀ x3 . x3setexp (SNoS_ omega) omega(∀ x4 . x4omegaSNoLt (ap x2 x4) x0)(∀ x4 . x4omegaSNoLt x0 (add_SNo (ap x2 x4) (eps_ x4)))(∀ x4 . x4omega∀ x5 . x5x4SNoLt (ap x2 x5) (ap x2 x4))(∀ x4 . x4omegaSNoLt (add_SNo (ap x3 x4) (minus_SNo (eps_ x4))) x0)(∀ x4 . x4omegaSNoLt x0 (ap x3 x4))(∀ x4 . x4omega∀ x5 . x5x4SNoLt (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
as obj
-
as prop
a38d2..SNo_approx_real_rep
theory
HotG
stx
64dcd..
address
TMVrL..SNo_approx_real_rep