Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . SNo x0SNoLe 0 x0∀ x1 . nat_p x1∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0and (and (SNo x2) (SNoLe 0 x2)) (SNoLt (mul_SNo x2 x2) x0)
as obj
-
as prop
8db9d..SNo_sqrtaux_0_prop
theory
HotG
stx
8fb89..
address
TMTXt..SNo_sqrtaux_0_prop