Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 x5 . x0realx1realx2setexp (SNoS_ omega) omegax3setexp (SNoS_ omega) omega(∀ x6 . x6omegaSNoLt (ap x2 x6) x0)(∀ x6 . x6omegaSNoLt x0 (add_SNo (ap x2 x6) (eps_ x6)))(∀ x6 . x6omega∀ x7 . x7x6SNoLt (ap x2 x7) (ap x2 x6))(∀ x6 . x6omegaSNoLt (add_SNo (ap x3 x6) (minus_SNo (eps_ x6))) x0)(∀ x6 . x6omegaSNoLt x0 (ap x3 x6))(∀ x6 . x6omega∀ x7 . x7x6SNoLt (ap x3 x6) (ap x3 x7))x4setexp (SNoS_ omega) omegax5setexp (SNoS_ omega) omega(∀ x6 . x6omegaSNoLt (ap x4 x6) x1)(∀ x6 . x6omegaSNoLt x1 (add_SNo (ap x4 x6) (eps_ x6)))(∀ x6 . x6omega∀ x7 . x7x6SNoLt (ap x4 x7) (ap x4 x6))(∀ x6 . x6omegaSNoLt (add_SNo (ap x5 x6) (minus_SNo (eps_ x6))) x1)(∀ x6 . x6omegaSNoLt x1 (ap x5 x6))SNo x0SNo x1SNo (add_SNo x0 x1)(∀ x6 . x6SNoS_ omega(∀ x7 . x7omegaSNoLt (abs_SNo (add_SNo x6 (minus_SNo x0))) (eps_ x7))x6 = x0)(∀ x6 . x6SNoS_ omega(∀ x7 . x7omegaSNoLt (abs_SNo (add_SNo x6 (minus_SNo x1))) (eps_ x7))x6 = x1)add_SNo x0 x1real
as obj
-
as prop
7312b..Conj_real_add_SNo__44__17
theory
HotG
stx
b740c..
address
TMRMt..Conj_real_add_SNo__44__17