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) 1and (and (SNo x2) (SNoLe 0 x2)) (SNoLt x0 (mul_SNo x2 x2))
as obj
-
as prop
95a41..SNo_sqrtaux_1_prop
theory
HotG
stx
8fb89..
address
TMWQ9..SNo_sqrtaux_1_prop