Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . nat_p x0(x0 = 0∀ x1 : ο . x1)∀ x1 . nat_p x1∀ x2 : ο . (∀ x3 . and (x3int) (and (SNoLe (mul_SNo 2 (abs_SNo x3)) x0) (divides_nat x0 (add_SNo x1 (minus_SNo x3))))x2)x2
as obj
-
as prop
2a08a..
theory
HotG
stx
cd4cc..
address
TMX2T..