enrich
   natarray, 
   list-of-natarray, 
   array-set
with
   functions 
       greaterPerms : array → array-set;
       smallerPerms : array → array-set;
       allPerms : array → array-set;
       . .toSet : list-of-natarray → array-set;
   
   predicates 
       . ≤ . : array × array;
       max : array;
       min : array;
       nextperm : array × array;
       ordered≤ : list-of-natarray;
       hasGreaterElem : array × nat;
   
   procedures next#  : array : bool nonfunctional ;
              permut#  : array × list-of-natarray nonfunctional ;
              sort#  : array nonfunctional ;
   variables 
       hasNext : bool;
       i : nat;
       j : nat;
       temp : nat;
       ar : array;
       listofar : list-of-natarray;
       arx : list-of-natarray;
       n : nat;
       m : nat;
   
   partial functions 
       EndIncreasingPart : array → nat with λ ar. ordered≤(ar);
       PosNextGreaterElem : nat × array → nat with λ m, ar. hasGreaterElem(ar, m);
   
   
   axioms 
      hasGreaterElem-base: ¬ hasGreaterElem([], m);
      
      hasGreaterElem-rec1: n ≤ m → hasGreaterElem(n + ar, m) ↔ hasGreaterElem(ar, m);
      
      hasGreaterElem-rec2: n > m → (hasGreaterElem(n + ar, m) ↔ true);
      
      EndIncreasingPart-base: m1 > m2 → EndIncreasingPart(m1 ' + m2 ') = 0;
      
      EndIncreasingPart-rec: m1 ≤ m2 → EndIncreasingPart(m1 ' + m2 ' + ar) = 1 + EndIncreasingPart(m2 ' + ar);
      
      toSet: ar ∈ arx.toSet ↔ ar ∈ arx;
      used for: s, ls;
      
      all-perms: ar0 ∈ allPerms(ar) ↔ perm(ar, ar0);
      used for: s, ls;
      
      smaller-perms: ar0 ∈ smallerPerms(ar) ↔ ar ≠ ar0 ∧ perm(ar, ar0) ∧ ar0 ≤ ar;
      used for: s, ls;
      
      greater-perms: ar0 ∈ greaterPerms(ar) ↔ ar ≠ ar0 ∧ perm(ar, ar0) ∧ ar ≤ ar0;
      used for: s, ls;
      
      ordered-arraylist-base0: ordered≤([]);
      used for: s, ls;
      
      ordered-arraylist-base1: ordered≤(ar ');
      used for: s, ls;
      
      ordered-arraylist-rec: ordered≤(ar0 ' + ar1 ' + arx) ↔ ar0 ≤ ar1 ∧ ordered≤(ar1 ' + arx);
      used for: s, ls;
      
      lexicographic-base1: [] ≤ [];
      used for: s, ls;
      
      lexicographic-base2: [] ≤ ar2;
      used for: s, ls;
      
      lexicographic-base3: ¬ ar1 ≤ [];
      used for: as, las;
      
      lexicographic-rec1: n ' + ar1 ≤ m ' + ar2 ↔ (n = m ⊃ ar1 ≤ ar2;n ≤ m);
      used for: s, ls;
      
      maximum-permutation: max(ar1) ↔ (∀ ar2. perm(ar1, ar2) → ar2 ≤ ar1);
      
      minimum-permutation: min(ar1) ↔ (∀ ar2. perm(ar1, ar2) → ar1 ≤ ar2);
      
      next-permutation: 
      nextperm(ar1, ar2) ↔ perm(ar1, ar2) ∧ ar1 ≠ ar2 ∧ ar1 ≤ ar2 ∧ (∀ ar3. perm(ar1, ar3) ∧ ar3 ≠ ar1 ∧ ar3 ≠ ar2 → ¬(ar1 ≤ ar3 ∧ ar3 ≤ ar2));
      
      sort-def: ar0 = ar ⊦ ⟨sort#(; ar)⟩ (ordered≤(ar) ∧ perm(ar0, ar));
   
   declarations 
      permut: 
      permut#(; ar, listofar)
      {listofar := []; sort#(; ar); 
       let hasNext = true
       in while hasNext
          do {/* invariant   ¬ dups(listofar) ∧ perm(ar, ar`) ∧ ordered≤(listofar)
                           ∧ (hasNext ⊃ listofar.toSet = smallerPerms(ar);listofar.toSet = smallerPerms(ar) ++ ar) ∧ (¬ hasNext → max(ar))
                 wfbound # greaterPerms(ar) + (hasNext ⊃ 1;0) */; 
              listofar := listofar + ar; next#(; ar; hasNext)}
      };
      
      
      next: 
      next#(; ar; hasNext)
      {let ghostar = ar
       in if # ar = 0
          then hasNext := false
          else let i = (# ar)-1
               in {while i > 0 ∧ ar[i -1] ≥ ar[i]
                   do {/* next-perm: invariant i < # ar wfbound i;
                          next-proper-permutation: invariant i < # ar ∧ ordered≤(rev(subarray(ar, i, # ar - i))) wfbound i */; 
                       i := i -1}; 
                   if i ≤ 0
                   then hasNext := false
                   else {let j = (# ar)-1
                         in {while ar[j] ≤ ar[i -1]
                             do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j;
                                    next-proper-permutation: 
                                    invariant   j < # ar ∧ i ≤ j ∧ i ≠ 0 ∧ ordered≤(rev(subarray(ar, i, # ar - i)))
                                              ∧ (∀ n. n > j ∧ n < # ar → ar[n] ≤ ar[i - 1])
                                    wfbound j */; 
                                 j := j -1}; 
                             let temp = ar[i -1]
                             in {ar[i -1] := ar[j]; ar[j] := temp; 
                                 /* next-proper-permutation: 
                                      ordered≤(rev(subarray(ar, i, # ar - i))) ∧ (∀ n. n ≥ j ∧ n < # ar → ar[n] < ar[i - 1])
                                    ∧ ghostar ≠ ar ∧ ghostar ≤ ar ∧ ghostar[j] = ar[i - 1] */; 
                                 let ghost_j = j
                                 in {j := (# ar)-1; 
                                     while i < j
                                     do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j;
                                            next-proper-permutation: 
                                            invariant   j < # ar ∧ i < # ar ∧ i ≠ 0 ∧ i` ≤ i ∧ perm(ghostar, ar)
                                                      ∧ subarray(ghostar, 0, i` - 1) = subarray(ar, 0, i` - 1) ∧ ghostar[ghost_j] = ar[i` - 1]
                                                      ∧ (  i < j
                                                         →   rev(subarray(ar`, i`, # ar - i`))
                                                           =   subarray(ar, i`, i - i`) + rev(subarray(ar, i, j + 1 - i))
                                                             + subarray(ar, j + 1, # ar - j + 1))
                                                      ∧ (i ≥ j → rev(subarray(ar`, i`, # ar - i`)) = subarray(ar, i`, # ar - i`))
                                            wfbound j */; 
                                         temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i +1; j := j -1}}}}; 
                         hasNext := true}}
      };
      
      
   
   
end enrich