Proofgold Proposition

∀ 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

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_mul_SNo_com__1__0

proofgold address
TMMWS..^{Conj_mul_SNo_com__1__0}

creator
35053 PrNpY../65012..

owner
35061 PrNpY../bd40c..

term root
107a2..