Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . x0real∀ x1 : ο . (∀ x2 . x2setexp (SNoS_ omega) omega(∀ x3 . x3omegaSNoLt (add_SNo (ap x2 x3) (minus_SNo (eps_ x3))) x0)(∀ x3 . x3omegaSNoLt x0 (ap x2 x3))(∀ x3 . x3omega∀ x4 . x4x3SNoLt (ap x2 x3) (ap x2 x4))x1)x1
as obj
-
as prop
355d3..
theory
HotG
stx
9ae9f..
address
TMUuu..