Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . x0real∀ x1 : ο . (SNo x0SNoLev x0ordsucc omegax0SNoS_ (ordsucc omega)SNoLt (minus_SNo omega) x0SNoLt x0 omega(∀ x2 . x2SNoS_ omega(∀ x3 . x3omegaSNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3))x2 = x0)(∀ x2 . x2omega∀ x3 : ο . (∀ x4 . and (x4SNoS_ omega) (and (SNoLt x4 x0) (SNoLt x0 (add_SNo x4 (eps_ x2))))x3)x3)x1)x1
as obj
-
as prop
447bb..real_E
theory
HotG
stx
9ae9f..
address
TMM6B..real_E