enrich
   rowcol-upd
, 
   nat-pot, 
   nat-even, 
   oarray-sort

with
   functions 
       #clean0rows : matrix × elem → nat;
      comment: #clean0rows counts the number of initial rows where all elements are < i;
       #clean1rows : matrix × elem → nat;
      comment: #clean0rows counts the number of final rows where all elements are ≥ i;
       #dirtyrows : matrix × elem → nat;
      comment: clean0rows counts the the rows between clean1 and clean0 rows;
       log2↑ : nat → nat;
      comment: ⌈log_2(n)⌉, the smallest natural number greater or equal to real-valued log_2(n), 1 for 0;
       countevn : array × (elem → bool) → nat;
      comment: count all elements that satisfy p with even index ;
       countodd : array × (elem → bool) → nat;
      comment: count all elements that satisfy p with odd index ;
   
   predicates 
       srowsorted : matrix × nat × matrix;
      comment: first matrix is a version of second one with first n rows sorted;
       scolsorted : matrix × nat × matrix;
      comment: first matrix is a version of second one with first n colums sorted;
       rowsincreasing : matrix × nat;
      comment: the elements in row n are bigger than all elements in smaller rows;
       . .dirtyrows≤ ( . ) : matrix × nat;
      comment: the number of dirty rows = all rows - all< - all≥ ;
   
   procedures sortrow# nat × bool : matrix nonfunctional nondeterministic;
              sortcol# nat : matrix nonfunctional nondeterministic;
              sortrows#  : matrix nonfunctional nondeterministic;
              sortrowssnake#  : matrix nonfunctional nondeterministic;
              sortcols#  : matrix nonfunctional nondeterministic;
              shearsort#  : matrix nonfunctional nondeterministic;
   variables 
       mx : matrix;
       a : array;
       i : elem;
       j : elem;
       m : nat;
       n : nat;
       r : nat;
       c : nat;
       bound : nat;
       asc : bool;
       p : elem → bool;
   
   partial functions 
       . /↑ . : nat × nat → nat prio 11 right with λ m, n. n ≠ 0;
      comment: whole number division, but rounding up, not down;
       countevn : array × nat × nat × (elem → bool) → nat with λ a, m, n, p. m ≤ n ∧ n ≤ # a;
      comment: count all elements that satisfy p with even index between lower and upper bound;
       countodd : array × nat × nat × (elem → bool) → nat with λ a, m, n, p. m ≤ n ∧ n ≤ # a;
      comment: count all elements that satisfy p with odd index between lower and upper bound;
   
   
   axioms 
      countevn-base: m ≤ # a ⊦ countevn(a, m, m, p) = 0;
      used for: s, ls;
      
      countevn-rec: m ≤ n, n ≤ # a ⊦ countevn(a, m, n + 1, p) = countevn(a, m, n, p) + (even(n) ∧ p(a[n]) ⊃ 1;0);
      used for: s, ls;
      
      countevn-def: countevn(a, p) = countevn(a, 0, # a, p);
      
      countodd-base: m ≤ # a ⊦ countodd(a, m, m, p) = 0;
      used for: s, ls;
      
      countodd-rec: m ≤ n, n ≤ # a ⊦ countodd(a, m, n + 1, p) = countodd(a, m, n, p) + (odd(n) ∧ p(a[n]) ⊃ 1;0);
      used for: s, ls;
      
      countodd-def: countodd(a, p) = countodd(a, 0, # a, p);
      
      divup-def: m /↑ n = (∃ n0. m = n0 * n ⊃ m / n;m / n + 1);
      
      log2up-def: log2↑(n) = (∃ m. n = 2^ m ⊃ log2 n;log2(2 * n + 1));
      
      dirtyrows-def: #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx;
      
      clean0rows-bounded: ¬ #r mx < #clean0rows(mx, i);
      used for: las;
      
      clean0rows-notallls: #clean0rows(mx, i) < #r mx → count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0;
      
      clean0rows-allls: r < #clean0rows(mx, i) → count(mx[r]r, λ j. ¬ j < i) = 0;
      
      clean1rows-bounded: ¬ #r mx < #clean1rows(mx, i);
      used for: las;
      
      clean1rows-notallge: #clean1rows(mx, i) + r + 1 = #r mx → count(mx[r]r, λ j. j < i) ≠ 0;
      
      clean1rows-allge: #r mx ≤ #clean1rows(mx, i) + r ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0;
      
      dirtyrowsbound-def: mx.dirtyrows≤(bound) ↔ (∀ i. #dirtyrows(mx, i) ≤ bound);
      
      rowno-updrow: #c mx = # a, r < #r mx ⊦ #r mx[r, a]r = #r mx;
      used for: ls;
      
      rowno-updcol: #r mx = # a, c < #c mx ⊦ #r mx[c, a]c = #r mx;
      used for: ls;
      
      colno-updrow: #c mx = # a, r < #r mx ⊦ #c mx[r, a]r = #c mx;
      used for: ls;
      
      colno-updcol: #r mx = # a, c < #c mx ⊦ #c mx[c, a]c = #c mx;
      used for: ls;
      
      scolsorted-def: 
        m ≤ #c mx
      → (  scolsorted(mx, m, mx0)
         ↔   #r mx = #r mx0 ∧ #c mx = #c mx0
           ∧ (∀ c. c < #c mx → (c < m ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c)));
      
      srowsorted-def: 
        m ≤ #r mx
      → (  srowsorted(mx, m, mx0)
         ↔   #r mx = #r mx0 ∧ #c mx = #c mx0
           ∧ (∀ r. r < #r mx → (r < m ⊃ perm(mx0[r]r, mx[r]r) ∧ ordered≤((even(r) ⊃ mx[r]r;rev(mx[r]r)));mx0[r]r = mx[r]r)));
      
      rowsincreasing-def: 
      rowsincreasing(mx, r) ↔ (∀ r1, r2, c1, c2. r1 < r2 ∧ r2 < r ∧ c1 < #c mx ∧ c2 < #c mx → ¬ mx[r2, c2] < mx[r1, c1]);
      comment: all elements in row r1 are less or equal to all elements in row r2 when r1 < r2 < r;
   
   declarations 
      sortcol: 
      sortcol#(m; mx){choose a with # a = #r mx ∧ perm(mx[m]c, a) ∧ ordered≤(a) in mx[m]c := a};
      
      
      sortrow: 
      sortrow#(m, asc; mx){choose a with # a = #c mx ∧ perm(mx[m]r, a) ∧ ordered≤((asc ⊃ a;rev(a))) in mx[m]r := a};
      
      
      sortcols: 
      sortcols#(; mx)
      {let m = 0
       in while m < #c mx
          do {/* invariant   scolsorted(mx, m, mx`) ∧ perm(mx`.toArr, mx.toArr) ∧ #c mx = #c mx` ∧ #r mx = #r mx` ∧ m ≤ #c mx
                           ∧ #c mx ≠ 0
                 wfbound #c mx - m */; 
              /* use contract sortcol-correct and skip call */; sortcol#(m; mx); m := m + 1}
      };
      
      
      sortrows: 
      sortrows#(; mx)
      {let m = 0
       in while m < #r mx
          do {/* invariant   ordered≤(toArr(mx, m)) ∧ rowsincreasing(mx, #r mx) ∧ perm(mx`.toArr, mx.toArr) ∧ #c mx = #c mx`
                           ∧ #r mx = #r mx` ∧ m ≤ #r mx
                 wfbound #r mx - m */; 
              /* use contract sortrow-correct and skip call */; sortrow#(m, true; mx); m := m + 1}
      };
      
      
      sortrowssnake: 
      sortrowssnake#(; mx)
      {let m = 0
       in while m < #r mx
          do {/* invariant   srowsorted(mx, m, mx`) ∧ perm(mx`.toArr, mx.toArr) ∧ #c mx = #c mx` ∧ #r mx = #r mx` ∧ m ≤ #r mx
                           ∧ #c mx ≠ 0
                 wfbound #r mx - m */; 
              /* use contract sortrowsnake-correct and skip call */; sortrow#(m, even(m); mx); m := m + 1}
      };
      
      
      shearsort: 
      shearsort#(; mx)
      {let n = log2↑(#r mx)
       in while n > 0
          do {/* invariant   perm(mx`.toArr, mx.toArr) ∧ #c mx = #c mx` ∧ #r mx = #r mx` ∧ #c mx ≠ 0
                           ∧ mx.dirtyrows≤(#r mx /↑ 2^(n` - n)) ∧ n ≤ n` ∧ (n = 0 → scolsorted(mx, #c mx, mx))
                 wfbound n */; 
              /* use contract sortrowssnake-correct and skip call */; sortrowssnake#(; mx); /* use contract sortcols-correct and skip call */; 
              sortcols#(; mx); n := n - 1}; 
       /* use contract sortrows-correct and skip call */; sortrows#(; mx)
      };
      
      
   
   
end enrich