Proofgold Proposition

∀ x0 . SNo x0 ⟶ ∀ x1 . SNo x1 ⟶ ∀ x2 : ο . (SNo (mul_SNo x0 x1) ⟶ (∀ x3 . x3 ∈ SNoL x0 ⟶ ∀ x4 . x4 ∈ SNoL x1 ⟶ SNoLt (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4))) ⟶ (∀ x3 . x3 ∈ SNoR x0 ⟶ ∀ x4 . x4 ∈ SNoR x1 ⟶ SNoLt (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4))) ⟶ (∀ x3 . x3 ∈ SNoL x0 ⟶ ∀ x4 . x4 ∈ SNoR x1 ⟶ SNoLt (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)) (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4))) ⟶ (∀ x3 . x3 ∈ SNoR x0 ⟶ ∀ x4 . x4 ∈ SNoL x1 ⟶ SNoLt (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)) (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4))) ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
mul_SNo_prop_1

proof
PUcff..

Megalodon
mul_SNo_prop_1

proofgold address
TMZ8J..^{mul_SNo_prop_1}

creator
4971 Pr6Pc../d9897..

owner
4971 Pr6Pc../d9897..

term root
3018e..