In this example we will show an induction proof over lists. In the following[Graphics:submitted.nbgr306.gif] denotes the empty list,[Graphics:submitted.nbgr307.gif]the length of a list, overbared variables and constants are sequences (they can contain 0 or more elements).

The theorem states that adding an element somewhere in the interior of a list it increases the length of the list by 1. (Note that the definition of the lists length states that prepending an element to a list (adding it at the begining) increases the length of the list by 1.) The proof of the theorem follows:


[Graphics:submitted.nbgr308.gif] [Graphics:submitted.nbgr309.gif]

under the assumptions

[Graphics:submitted.nbgr310.gif] [Graphics:submitted.nbgr311.gif],

[Graphics:submitted.nbgr312.gif] [Graphics:submitted.nbgr313.gif].