Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . SNo x0SNoLt 0 x0(∀ x1 . x1SNoS_ omega(∀ x2 . x2omegaSNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2))x1 = x0)(∀ x1 . x1omega∀ x2 : ο . (∀ x3 . and (x3SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 (eps_ x1))))x2)x2)∀ x1 . x1omega∀ x2 : ο . (∀ x3 . x3SNoS_ omegaSNoLt 0 x3SNoLt x3 x0SNoLt x0 (add_SNo x3 (eps_ x1))x2)x2
as obj
-
as prop
947a7..SNo_prereal_incr_lower_pos
theory
HotG
stx
19513..
address
TMbWM..SNo_prereal_incr_lower_pos