Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . SNo x0SNoLe 0 x0and (and (SNo (sqrt_SNo_nonneg x0)) (SNoLe 0 (sqrt_SNo_nonneg x0))) (mul_SNo (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x0) = x0)
as obj
-
as prop
b09b9..sqrt_SNo_nonneg_prop1
theory
HotG
stx
8fb89..