Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . SNo_sqrtaux x0 x1 0 = lam 2 (λ x3 . If_i (x3 = 0) (prim5 (SNoL_nonneg x0) x1) (prim5 (SNoR x0) x1))

type
prop

theory
HotG

name
SNo_sqrtaux_0

proof
PUewm..

Megalodon
SNo_sqrtaux_0

proofgold address
TMZVZ..^{SNo_sqrtaux_0}

creator
27779 PrQUS../dd1e6..

owner
27779 PrQUS../dd1e6..

term root
d46ed..