Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 . SNo x0SNoLt 0 x0x1SNoL_pos x0SNo x2mul_SNo x1 x2 = 1SNo x3SNoLt 1 (mul_SNo x0 x3)SNo x4add_SNo 1 (minus_SNo (mul_SNo x0 x4)) = mul_SNo (add_SNo 1 (minus_SNo (mul_SNo x0 x3))) (mul_SNo (add_SNo x1 (minus_SNo x0)) x2)SNoLt (mul_SNo x0 x4) 1
as obj
-
as prop
1a06f..SNo_recip_lem2
theory
HotG
stx
87341..
address
TMKBz..SNo_recip_lem2