Define the following relationships on (list A):
Show that the second one is an equivalence relation.
- The list l' is obtained from l by transposing two consecutive
- The list l' is obtained from l by a finite number of such transpositions. We say that l' is a permutation of l.
Look at this file
You could also define the relationship perm as
(Rstar _ transpose). In this case, you first have
to load the module Rstar of the library Relations,
and prove that the reflexive transitive closure of a symmetric relation
is symmetric too.
Follow this link