Proofgold Term Root Disambiguation

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

as obj
-

as prop
182e5..^{SNo_sqrtaux_0}

theory
HotG

stx
87341..

address
TMaKi..^{SNo_sqrtaux_0}