Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . SNo x0∀ x1 . SNo x1mul_SNo x0 x1 = SNoCut (binunion {add_SNo (mul_SNo (ap x3 0) x1) (add_SNo (mul_SNo x0 (ap x3 1)) (minus_SNo (mul_SNo (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoL x0) (SNoL x1)} {add_SNo (mul_SNo (ap x3 0) x1) (add_SNo (mul_SNo x0 (ap x3 1)) (minus_SNo (mul_SNo (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoR x0) (SNoR x1)}) (binunion {add_SNo (mul_SNo (ap x3 0) x1) (add_SNo (mul_SNo x0 (ap x3 1)) (minus_SNo (mul_SNo (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoL x0) (SNoR x1)} {add_SNo (mul_SNo (ap x3 0) x1) (add_SNo (mul_SNo x0 (ap x3 1)) (minus_SNo (mul_SNo (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoR x0) (SNoL x1)})
type
prop
theory
HotG
name
mul_SNo_eq
proof
PUK1b..
Megalodon
mul_SNo_eq
proofgold address
TMR2S..mul_SNo_eq
creator
4949 Pr6Pc../1acda..
owner
4949 Pr6Pc../1acda..
term root
726bd..