Specification sort-invariants

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   oarray-perm
with
   

   
   
   
   predicates  Inv-main : array × array × nat;
               Inv-first-inner : array × array × elem × elem × nat × nat;
               Inv-last-inner : array × array × elem × elem × nat × nat;
               Inv-end : array × array × nat × nat × elem;
   
   
   
   

   

   axioms Inv-main :  ⊦ Inv-main(A, A0, i) ↔ # A ≠ 0 ∧ # A = # A0 ∧ i ≤ # A ∧ sorted(A, 0, i) ∧ perm(A, A0);
          used for: ls;
          Inv-first-inner
          : ⊦   Inv-first-inner(A, A0, x, y, i, j)
              ↔   # A ≠ 0 ∧ # A = # A0 ∧ i ≤ # A ∧ j ≤ i ∧ y ≤ x ∧ (j ≠ i → x < A[j + 2]) ∧ sorted(A, 0, j)
                ∧ sorted(A, j + 2, i + 2) ∧ (j ≠ i ∧ j ≠ 0 → A[j - 1] ≤ A[j + 2]) ∧ perm(A[j, y][j + 1, x], A0);
          used for: ls;
          Inv-last-inner
          : ⊦   Inv-last-inner(A, A0, x, y, i, j)
              ↔   # A ≠ 0 ∧ # A = # A0 ∧ i ≤ # A ∧ j ≤ i ∧ y ≤ x ∧ y ≤ A[j + 1] ∧ sorted(A, 0, j) ∧ sorted(A, j + 1, i + 2)
                ∧ (j ≠ 0 → A[j - 1] ≤ A[j + 1]) ∧ perm(A[j, y], A0);
          used for: ls;
          Inv-end
          : ⊦   Inv-end(A, A0, i, j, y)
              ↔ # A ≠ 0 ∧ # A = # A0 ∧ j ≤ i ∧ (j ≠ i → y ≤ A[j + 1]) ∧ sorted(A, 0, (j = i ⊃ i;i + 1)) ∧ perm(A[j, y], A0);
          used for: ls;

   

   
end enrich