Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 x5 x6 x7 . (∀ x8 . x8 ∈ x6 ⟶ ∀ x9 : ο . (∀ x10 . x10 ∈ x2 ⟶ ∀ x11 . x11 ∈ x3 ⟶ x8 = add_SNo (mul_SNo x10 x1) (add_SNo (mul_SNo x0 x11) (minus_SNo (mul_SNo x10 x11))) ⟶ x9) ⟶ (∀ x10 . x10 ∈ x4 ⟶ ∀ x11 . x11 ∈ x5 ⟶ x8 = add_SNo (mul_SNo x10 x1) (add_SNo (mul_SNo x0 x11) (minus_SNo (mul_SNo x10 x11))) ⟶ x9) ⟶ x9) ⟶ (∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x3 ⟶ add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9))) ∈ x7) ⟶ (∀ x8 . x8 ∈ x4 ⟶ ∀ x9 . x9 ∈ x5 ⟶ add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9))) ∈ x7) ⟶ x6 ⊆ x7

as obj
-

as prop
e8bfa..^{mul_SNo_Subq_lem}

theory
HotG

stx
0d8c8..

address
TMEpm..^{mul_SNo_Subq_lem}