Proofgold Proposition

∀ x0 x1 x2 x3 x4 x5 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ (∀ x6 . x6 ∈ SNoL x0 ⟶ ∀ x7 . x7 ∈ SNoL x1 ⟶ SNoLt (add_SNo (mul_SNo x6 x1) (mul_SNo x0 x7)) (add_SNo x2 (mul_SNo x6 x7))) ⟶ SNo x3 ⟶ SNoLt x2 x3 ⟶ x4 ∈ SNoL x0 ⟶ x5 ∈ SNoL x1 ⟶ SNoLe (add_SNo x3 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) ⟶ SNo x5 ⟶ SNo (mul_SNo x4 x5) ⟶ SNoLt (add_SNo x3 (mul_SNo x4 x5)) (add_SNo x2 (mul_SNo x4 x5)) ⟶ SNoLt (mul_SNo x0 x1) x3

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_mul_SNo_SNoL_interpolate__5__9

proofgold address
TMcAa..^{Conj_mul_SNo_SNoL_interpolate__5__9}

creator
35053 PrNpY../8e14d..

owner
35061 PrNpY../38897..

term root
25b05..