// number theory:

// 0 is not a successor:
FORALL x
	[NOT Equal(Zero, Succ(x))]

FORALL x y
	[Equal(Succ(x), Succ(y)) <-> Equal(x, y)]

// addition:
FORALL x
	[Equal(Plus(x, Zero), x)]

FORALL x y
	[Equal(Plus(x, Succ(y)), Succ(Plus(x, y)))]

// multiplication:
FORALL x
	[Equal(Times(x, Zero), Zero)]

FORALL x y
	[Equal(Times(x, Succ(y)), Plus(Times(x, y), x))]

// equality:
FORALL x
	[Equal(x, x)]

FORALL x y
	[Equal(x, y) -> Equal(y, x)]

FORALL x y z
	[Equal(x, y) AND Equal(y, z) -> Equal(x, z)]

// even and odd:
FORALL x
	[Even(x) <-> EXISTS y [ Equal(x, Plus(y, y))]]

FORALL x
	[Odd(x) <-> EXISTS y [ Equal(x, Succ(Plus(y, y)))]]

// prime numbers:
FORALL x
	[Prime(x) <->
		FORALL y z [Equal(x, Times(y, z)) -> Equal(y, x) OR Equal(y, Succ(Zero))]]
