Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 x5 . SNo x1 ⟶ (∀ x6 . x6 ∈ SNoS_ (SNoLev x0) ⟶ mul_SNo x6 x1 = mul_SNo x1 x6) ⟶ (∀ x6 . x6 ∈ SNoS_ (SNoLev x1) ⟶ mul_SNo x0 x6 = mul_SNo x6 x0) ⟶ (∀ x6 . x6 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x7 . x7 ∈ SNoS_ (SNoLev x1) ⟶ mul_SNo x6 x7 = mul_SNo x7 x6) ⟶ (∀ x6 . x6 ∈ x3 ⟶ ∀ x7 : ο . (∀ x8 . x8 ∈ SNoL x0 ⟶ ∀ x9 . x9 ∈ SNoR x1 ⟶ x6 = add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9))) ⟶ x7) ⟶ (∀ x8 . x8 ∈ SNoR x0 ⟶ ∀ x9 . x9 ∈ SNoL x1 ⟶ x6 = add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9))) ⟶ x7) ⟶ x7) ⟶ (∀ x6 . x6 ∈ SNoL x0 ⟶ ∀ x7 . x7 ∈ SNoR x1 ⟶ add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ∈ x3) ⟶ (∀ x6 . x6 ∈ SNoR x0 ⟶ ∀ x7 . x7 ∈ SNoL x1 ⟶ add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ∈ x3) ⟶ (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 : ο . (∀ x8 . x8 ∈ SNoL x1 ⟶ ∀ x9 . x9 ∈ SNoR x0 ⟶ x6 = add_SNo (mul_SNo x8 x0) (add_SNo (mul_SNo x1 x9) (minus_SNo (mul_SNo x8 x9))) ⟶ x7) ⟶ (∀ x8 . x8 ∈ SNoR x1 ⟶ ∀ x9 . x9 ∈ SNoL x0 ⟶ x6 = add_SNo (mul_SNo x8 x0) (add_SNo (mul_SNo x1 x9) (minus_SNo (mul_SNo x8 x9))) ⟶ x7) ⟶ x7) ⟶ (∀ x6 . x6 ∈ SNoL x1 ⟶ ∀ x7 . x7 ∈ SNoR x0 ⟶ add_SNo (mul_SNo x6 x0) (add_SNo (mul_SNo x1 x7) (minus_SNo (mul_SNo x6 x7))) ∈ x5) ⟶ (∀ x6 . x6 ∈ SNoR x1 ⟶ ∀ x7 . x7 ∈ SNoL x0 ⟶ add_SNo (mul_SNo x6 x0) (add_SNo (mul_SNo x1 x7) (minus_SNo (mul_SNo x6 x7))) ∈ x5) ⟶ x2 = x4 ⟶ x3 = x5 ⟶ SNoCut x2 x3 = SNoCut x4 x5

as obj
-

as prop
7b761..^{Conj_mul_SNo_com__1__0}

theory
HotG

stx
b740c..

address
TMYUn..^{Conj_mul_SNo_com__1__0}