Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . x0int∀ x1 . x1intnot (and (x0 = 0) (x1 = 0))∀ x2 . iff (gcd_reln x0 x1 x2) (and (and (int_lin_comb x0 x1 x2) (SNoLt 0 x2)) (∀ x3 . int_lin_comb x0 x1 x3SNoLt 0 x3SNoLe x2 x3))
as obj
-
as prop
ed22b..BezoutThm
theory
HotG
stx
e9e67..