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) | (inc^{n }x = n : inc^{n+1 }x ) |
⇒ { inc is a function } | |
(inc(inc^{n }x ) = inc (n : inc^{n+1 }x )) | |
= { 1a } | |
(inc(inc^{n }x) = n +1 : inc(inc^{n+1 }x )) | |
= { def. of iterated functional composition } | |
(3) | (inc^{n+1 }x = n+1 : inc^{n+2 }x ) |
* *
*
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.