Proofgold Proposition

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

type
prop

theory
HotG

name
mul_SNo_SNoCut_SNoR_interpolate_impred

proof
PUMGC..

Megalodon
mul_SNo_SNoCut_SNoR_interpolate_impred

proofgold address
TMSSk..^{mul_SNo_SNoCut_SNoR_interpolate_impred}

creator
27765 PrQUS../e0450..

owner
27765 PrQUS../e0450..

term root
54422..