Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ int) (∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x1 = add_SNo (mul_SNo x3 x0) x5) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2

as obj
-

as prop
60c3e..^{quotient_remainder_int}

theory
HotG

stx
e9e67..

address
TMGvF..^{quotient_remainder_int}