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) (Sing 0) 0), λ x2 x3 . lam 2 (λ x4 . If_i (x4 = 0) (binunion (binunion (ap x3 0) (SNo_recipauxset (ap x3 0) x0 (SNoR x0) x1)) (SNo_recipauxset (ap x3 1) x0 (SNoL_pos x0) x1)) (binunion (binunion (ap x3 1) (SNo_recipauxset (ap x3 0) x0 (SNoL_pos x0) x1)) (SNo_recipauxset (ap x3 1) x0 (SNoR x0) x1))).