si (len xs) > 1alors il existe x1:elt,
x2:eltet xs':listtels que
xs = (cons x1 (cons x2 xs'))
Attention, la contrainte que l'on a sur xsvaut aussi pour
l'hypothèse d'induction. C'est à dire que celle-ci est devenue
" ys:list.
((len ys) < (len (cons x1 (cons x2 xs'))))
Þ (is-perm ys (do-perm ys)) = true
Le résultat cherché et, dans ce cas
(is-perm (cons x1 (cons x2 xs')) (do-perm (cons x1 (cons
x2 xs'))) = true
En utilisant [A12] , on se ramène à chercher à montrer que
(is-perm (cons x1 (cons x2 xs')) (cons x2 (cons x1 (do-perm xs')))) =
true
On va terminer la preuve en utilisant [A9] .
(1) Comme (len xs') < (len (cons x1 (cons x2 xs'))), notre
hypothèse d'induction nous donne que
(is-perm xs' (do-perm xs')) = true
(2) Or (do-perm xs') = (rem x2 (cons x2 (do-perm xs'))). On a
donc également que
(is-perm xs' (rem x2 (cons x2 (do-perm xs')))) = true.
(3) De plus, (mem x2 (cons x2 (do-perm xs'))) = true.
(4) en appliquant (2) et (3) à [A9] , on obtient que
(is-perm (cons x2 xs) (cons x2 (do-perm xs'))) = true
On poursuit selon le même principe :
(5) Or (cons x2 (do-perm xs')) =
(rem x1 (cons x2 (cons x1 (do-perm xs')))), donc
(is-perm (cons x2 xs) (rem x1 (cons x2 (cons x1 (do-perm
xs'))))) = true.
(6) On a aussi
(mem x1 (cons x2 (cons x1 (do-perm xs')))) = true
(7) En appliquant (6) et (5) à [A9] , on obtient enfin que
(is-perm (cons x1 (cons x2 xs')) (cons x2 (cons x1 (do-perm xs')))) =
true