Lists

In this example we will show an induction proof over lists. In the following denotes the empty list,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:

PROPOSITION:

under the assumptions

,

.