Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ιι be given.
The subproof is completed by applying nat_primrec_0 with lam 2 (λ x2 . If_i (x2 = 0) {x1 x3|x3 ∈ SNoL_nonneg x0} {x1 x3|x3 ∈ SNoR x0}), λ x2 x3 . lam 2 (λ x4 . If_i (x4 = 0) (binunion (ap x3 0) (SNo_sqrtauxset (ap x3 0) (ap x3 1) x0)) (binunion (binunion (ap x3 1) (SNo_sqrtauxset (ap x3 0) (ap x3 0) x0)) (SNo_sqrtauxset (ap x3 1) (ap x3 1) x0))).