The diagonalizing sorcerer Roseacrucis has resurrected the Sumcheck Sphinx; it blocks the entrance to the Library. To defeat it, you must answer its many riddles, all of which happen to consist of deciding the validity of theorems in the first-order theory of the natural numbers with addition.

The Sphinx asks its riddles in rapidfire succession, but accompanied by your faithful addition automaton, they are all summarily decided.

• 1+1=2: one plus one equals two.
• Ax.Ay.x+y=y+x: addition is commutative.
• Ex.Ay.x>y: there exists a largest natural.
• Ee.Ae'.(Ax.e'+x=x <-> e=e'): the additive identity exists and is unique.
• Ax.Ey.2y=x: every natural is even.
• Ax.Ey.(2y=x | 2y+1=x): every natural is either even or odd.
• Ax.Ay.Az.((x=y & y=z) -> x=z): equality is transitive.
• Ax.Ay.(x<=y <-> y<=x): less-than-or-equal-to is symmetric.
• Ax.Ay.((x<=y & y<=x) -> x=y): less-than-or-equal-to is antisymmetric.
• Ax.Ay.(x+1=y+1 -> x=y): the successor function is injective.

C-h p addition-automaton
For constant c and variable x, the following are terms:

• c
• x
• cx

The following are relations:

• =
• !=
• <=
• <
• >=
• >

The following are operators:

• &
• |
• ->
• <->

For terms a and b, relation ★, operator ∗, and theorems φ and ψ, the following are theorems:

• a+...★b+...
• (φ ∗ ψ ∗ ...)
• ~φ
• Ax.φ
• Ex.φ