A very simple exercise in SASL

  The idea is to prove the equality of two recursively defined infinite sequences by showing that the one satisfies the defining equation of the other. Here we shall try this out on the simplest example I can think of.

  Let us consider the equations

(0)	from n = n : from (n+1)
(1a)	inc(a:b) = a+1 : inc b
(1b)	x = 0 : inc x .

We have to prove x = from 0 . We observe

(2)	(incn x = n : incn+1x )
	⇒    { inc is a function }
	(inc(incnx ) = inc (n : incn+1x ))
	=    { 1a }
	(inc(incnx) = n +1 : inc(incn+1x ))
	=    { def. of iterated functional composition }
(3)	(incn+1x = n+1 : incn+2x )

With (2)⇒(3) providing the induction step and —since    x = inc⁰ x    by the definition of iterated functional definition— (1b) providing the base, (2) has been proved for all n. Since (2) is the same equation in    incⁿx    as (0) is in from   n   ,   incⁿ x = from n   has been established for all n, in particular for n=0  , which completes the proof.

  I tried it the other way round , viz. I tried to show that from 0 was a solution of (1b), but this became a mess.
It is too warm and too humid to write much more now.