15.9 Nachfolgeroperation (Zähler)
Spezifikation:
succ p k xs = code p (k+1) (decode p k xs + 1)
Dies ist der Addiererspezifikation sehr ähnlich. Wir versuchen also, den Addierererentwurf wiederzu-verwenden.
Rechnung:
succ p k xs
= code p (k+1) (decode p k xs + 1)
= code p (k+1) (decode p k xs + 0 + 1)
= code p (k+1) (decode p k xs + decode p k (copy k 0) + 1)
= cadd p k (shuf k (xs ++ copy k 0) ++ [1])