Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . SNoCutP x0 x1 ⟶ SNoCutP x2 x3 ⟶ ∀ x4 x5 . x4 = SNoCut x0 x1 ⟶ x5 = SNoCut x2 x3 ⟶ ∀ x6 . x6 ∈ SNoR (mul_SNo x4 x5) ⟶ or (∀ x7 : ο . (∀ x8 . and (x8 ∈ x0) (∀ x9 : ο . (∀ x10 . and (x10 ∈ x3) (SNoLe (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x10)) (add_SNo x6 (mul_SNo x8 x10))) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) (∀ x7 : ο . (∀ x8 . and (x8 ∈ x1) (∀ x9 : ο . (∀ x10 . and (x10 ∈ x2) (SNoLe (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x10)) (add_SNo x6 (mul_SNo x8 x10))) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7)

as obj
-

as prop
a2fa8..^{mul_SNo_SNoCut_SNoR_interpolate}

theory
HotG

stx
9a4a7..

address
TMbFi..^{mul_SNo_SNoCut_SNoR_interpolate}