Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . In x2 (mul_nat x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x1 ⟶ x2 = add_nat x4 (mul_nat x5 x0) ⟶ (∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x1 ⟶ x2 = add_nat x6 (mul_nat x7 x0) ⟶ and (x6 = x4) (x7 = x5)) ⟶ x3) ⟶ x3

as obj
-

as prop
1c648..^{quot_rem_nat_impred}

theory
HF

stx
b2d3f..

address
TMUzS..^{quot_rem_nat_impred}