Proofgold Proposition

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

type
prop

theory
HotG

name
mul_SNo_SNoCut_SNoL_interpolate

proof
PUMGC..

Megalodon
mul_SNo_SNoCut_SNoL_interpolate

proofgold address
TMFWq..^{mul_SNo_SNoCut_SNoL_interpolate}

creator
27765 PrQUS../91cfe..

owner
27765 PrQUS../91cfe..

term root
a1d92..