Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . SNo x0(∀ x1 . x1SNoR_omega x0∀ x2 : ο . (∀ x3 . and (x3omega) (SNoLt x0 (add_SNo x1 (minus_SNo (eps_ x3))))x2)x2)f8473.. (SNoR_omega x0)
as obj
-
as prop
58c46..diadic_open_SNoR_omega_I
theory
HotG
stx
705e2..
address
TMVns..diadic_open_SNoR_omega_I