Proofgold Term Root Disambiguation

λ x0 x1 x2 . λ x3 : ι → ι . famunion x0 (λ x4 . {mul_SNo (add_SNo 1 (mul_SNo (add_SNo x5 (minus_SNo x1)) x4)) (x3 x5)|x5 ∈ x2})

as obj
d4094..^{SNo_recipauxset}

as prop
-

theory
HotG

stx
87341..

address
TMa2B..^{SNo_recipauxset}