Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 . SNo x0SNo x1SNo x2SNo x3SNo x4mul_SNo x0 (mul_SNo x1 (mul_SNo x2 (mul_SNo x3 x4))) = mul_SNo x3 (mul_SNo x4 (mul_SNo x0 (mul_SNo x1 x2)))
as obj
-
as prop
1b9b9..
theory
HotG
stx
19513..
address
TMFDN..