Search for blocks/addresses/...

Proofgold Term Root Disambiguation

{x0 ∈ SNoS_ (ordsucc omega)|and (and (x0 = omega∀ x1 : ο . x1) (x0 = minus_SNo omega∀ x1 : ο . x1)) (∀ x1 . x1SNoS_ omega(∀ x2 . x2omegaSNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2))x1 = x0)}
as obj
5277e..real
as prop
-
theory
HotG
stx
9ae9f..
address
TMRYW..real