Simple unary arithmetic to test inductive theorem prover. Authors: Frank Pfenning and Carsten Schuermann