Prove Correctness of the Representation
In order to show that the append function properly models the world of sets we must prove:
- ret (append (?, r)) = (ret ?) ? (ret r)
-
The standard way to prove something about a sequence is by using sequence induction
To show that P(?) holds for for all sequences ? establish:
- P(<>)
- if P(?) holds for any sequence ?, then so does P(<x> ^ ?)
i.e. ?x: ; ?:seq X ? P(?) ? P(<x> ^ ?)