Beweis
cadd p (k+m) (xs++xs') (ys++ys') [c]
= code p (k+m+1) ( deco p (k+m) (xs++xs') + deco p (k+m) (ys++ys') + c)
= code p (k+m+1) ((deco p k xs)*p^m + deco p m xs' + (deco p k ys)*p^m + deco p m ys' + c)
= code p (k+m+1) ((deco p k xs + deco p k ys + d)*p^m + r) where (d,r) = (z `div`p^m, z `mod` p^m) z = deco p m xs' + deco p m ys' + c)
= code p (k+1)(deco p k xs + deco p k ys + d) ++ zs where (d:zs) = code p (m+1) (deco p m xs' + deco p m ys' + c)
= cadd p k xs ys d ++ zs where (d:zs) = cadd p m xs' ys' c
= splice k (cadd p k) (cadd p m) (xs++xs') (ys++ys') [c]