## Examples

To make yourself familiar with the system CERES and the additional tools we have prepared the following examples:

- Very simple examples just to get a glimpse of how cut-elimination is done with CERES and how the workflow with the auxiliary tools molds.
- Instances of a proof schema which gives exponential cut-free proves. These examples clearly justify and suggest the use of computer aided cut-elimination systems.
- A convenient sized proof of a simple but practical mathematical statement.
- A larger proof of a still simple but more practical mathematical statement.
- A huge formal proof of a significant number-theoretical mathematical statement with a complex indirect topological proof.
- A second-order proof, showing that the least number principle implies the fact that every number greater than 1 has a prime divisor.