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 theorem is invalid.


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


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

The following are relations:

The following are operators:

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