Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nat_p x2 ⟶ SNo_recipaux x0 x1 (ordsucc x2) = lam 2 (λ x4 . If_i (x4 = 0) (binunion (binunion (ap (SNo_recipaux x0 x1 x2) 0) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 0) x0 (SNoR x0) x1)) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 1) x0 (SNoL_pos x0) x1)) (binunion (binunion (ap (SNo_recipaux x0 x1 x2) 1) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 0) x0 (SNoL_pos x0) x1)) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 1) x0 (SNoR x0) x1)))

as obj
-

as prop
55b10..^{SNo_recipaux_S}

theory
HotG

stx
87341..

address
TMSsj..^{SNo_recipaux_S}