Proofgold Proposition

∀ x0 x1 . (∀ x2 . x2 ∈ SNoL x0 ⟶ ∀ x3 . x3 ∈ SNoL 1 ⟶ SNoLt (add_SNo (mul_SNo x2 1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 1) (mul_SNo x2 x3))) ⟶ 0 ∈ SNoL 1 ⟶ x1 ∈ SNoL x0 ⟶ SNo x1 ⟶ add_SNo (mul_SNo x1 1) (mul_SNo x0 0) = x1 ⟶ add_SNo (mul_SNo x0 1) (mul_SNo x1 0) = mul_SNo x0 1 ⟶ SNoLt x1 (mul_SNo x0 1)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_mul_SNo_oneR__3__0

proofgold address
TMFB5..^{Conj_mul_SNo_oneR__3__0}

creator
35053 PrNpY../b6a26..

owner
35061 PrNpY../d02a9..

term root
07831..