## The Tape Proof

The end-sequent formalizes the statement: on a tape with infinitely many
cells, which are all labelled by either *0* or *1*, there are two
cells labelled by the same number.*f(n)=0* expresses that the cell with
number *n* is labelled by *0*. Indexing of cells is done by number
terms defined over *0*,*1* and *+*.

The example is taken from Urban (C. Urban: *Classical Logic and Computation*, Ph.D. Thesis, University of Cambridge Computer Laboratory, 2000.). It is formalized in LK but we use the extensions by equality rules and definition introduction to give a simpler formalization and allow an easier analysis of the proof.

The example proof uses two lemmas:

- there are infinitely many cells labelled by
*0*and - there are infinitely many cells labelled by
*1*.

These lemmas are eliminiated by CERES and a more direct argument is obtained in the resulting proof.

The example starts with a formalization of the proof as an HLK file. From this file a CERES input file gets generated via the HLK compiler. The XML files tape.xml and tape-out.xml can be displayed with the ProofTool.

`$ hlk -o tape.xml tape.hlk the-proof`

`$ hlk --ceres -o tape-in.xml tape.hlk the-proof`

`$ ceres --cutelim -ac tape-in.xml the-proof tape-out.xml`

The intermediary input and output files of the automated theorem prover Otter are: tape.in and tape.out.