Search for blocks/addresses/...

Proofgold Proposition

∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 . SNo x0SNo x1(∀ x6 . x6SNoS_ (SNoLev x0)∀ x7 . SNo x7x2 x6 x7 = x3 x6 x7)(∀ x6 . x6SNoS_ (SNoLev x1)x2 x0 x6 = x3 x0 x6)x5SNoR x1x4SNoS_ (SNoLev x0)add_SNo (x2 x4 x1) (add_SNo (x2 x0 x5) (minus_SNo (x2 x4 x5))) = add_SNo (x3 x4 x1) (add_SNo (x3 x0 x5) (minus_SNo (x3 x4 x5)))
type
prop
theory
HotG
name
-
proof
PURzn..
Megalodon
Conj_mul_SNo_eq__18__4
proofgold address
TMM7v..Conj_mul_SNo_eq__18__4
creator
35045 PrNpY../f8957..
owner
35047 PrNpY../49e9a..
term root
e7a1e..