Proofgold Proposition

∀ x0 x1 x2 x3 x4 x5 . SNoCutP x0 x1 ⟶ SNoCutP x2 x3 ⟶ x4 = SNoCut x0 x1 ⟶ x5 = SNoCut x2 x3 ⟶ ∀ x6 : ο . (∀ x7 x8 x9 x10 . (∀ x11 . x11 ∈ x7 ⟶ ∀ x12 : ο . (∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x2 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNoLt x13 x4 ⟶ SNoLt x14 x5 ⟶ x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14))) ⟶ x12) ⟶ x12) ⟶ (∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x2 ⟶ add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12))) ∈ x7) ⟶ (∀ x11 . x11 ∈ x8 ⟶ ∀ x12 : ο . (∀ x13 . x13 ∈ x1 ⟶ ∀ x14 . x14 ∈ x3 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNoLt x4 x13 ⟶ SNoLt x5 x14 ⟶ x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14))) ⟶ x12) ⟶ x12) ⟶ (∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x3 ⟶ add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12))) ∈ x8) ⟶ (∀ x11 . x11 ∈ x9 ⟶ ∀ x12 : ο . (∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x3 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNoLt x13 x4 ⟶ SNoLt x5 x14 ⟶ x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14))) ⟶ x12) ⟶ x12) ⟶ (∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x3 ⟶ add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12))) ∈ x9) ⟶ (∀ x11 . x11 ∈ x10 ⟶ ∀ x12 : ο . (∀ x13 . x13 ∈ x1 ⟶ ∀ x14 . x14 ∈ x2 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNoLt x4 x13 ⟶ SNoLt x14 x5 ⟶ x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14))) ⟶ x12) ⟶ x12) ⟶ (∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x2 ⟶ add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12))) ∈ x10) ⟶ SNoCutP (binunion x7 x8) (binunion x9 x10) ⟶ mul_SNo x4 x5 = SNoCut (binunion x7 x8) (binunion x9 x10) ⟶ x6) ⟶ x6

type
prop

theory
HotG

name
mul_SNoCut_abs

proof
PUSR1..

Megalodon
mul_SNoCut_abs

proofgold address
TMGHM..^{mul_SNoCut_abs}

creator
27738 PrQUS../58ed5..

owner
27738 PrQUS../58ed5..

term root
0c7af..