c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder free type Nat ::= 0 | Succ(prec:Nat)
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder pred __<=__ : Nat*Nat
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder forall x,y:Nat
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . not Succ(x) <= 0
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . Succ(x)<=Succ(y) <=> x<=y
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder pred __<=__ : Nat * Nat
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder forall x,y,z : Nat
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . x <= x %(reflexive)%
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . x <= z if x <= y /\ y <= z %(transitive)%
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . x = y if x <= y /\ y <= x %(antisymmetric)%
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . x <= y \/ y <= x %(dichotomous)%
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . x = y => x <= y
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder free type List[Nat] ::= Nil | Cons(head:Nat; tail:List[Nat])
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder pred elem : Nat * List[Nat]
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder forall x,y:Nat; l:List[Nat]
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . not elem (x,Nil)
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . elem(x,Cons(y,l)) <=> x=y \/ elem(x,l)
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder preds is_ordered : List[Nat];
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder permutation : List[Nat] * List[Nat]
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder vars x,y:Nat; L,L1,L2:List[Nat]
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . is_ordered(Nil)
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . is_ordered(Cons(x,Nil))
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . is_ordered(Cons(x,(Cons(y,L)))) <=> x<=y /\ is_ordered(Cons(y,L))
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . permutation(L1,L2) <=> (forall x:Nat . elem(x,L1) <=> elem(x,L2))
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder op sorter : List[Nat]->List[Nat]
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder var L:List[Nat]
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . is_ordered(sorter(L))
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . permutation(L,sorter(L))
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder ops insert : Nat*List[Nat] -> List[Nat];
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder insert_sort : List[Nat]->List[Nat]
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder vars x,y:Nat; L:List[Nat]
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . insert(x,Nil) = Cons(x,Nil)
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . insert(x,Cons(y,L)) = Cons(x,insert(y,L)) when x<=y else Cons(y,insert(x,L))
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . insert_sort(Nil) = Nil
c6b11bbe64a712a10d5d9e58152a7dba35edd056Christian Maeder . insert_sort(Cons(x,L)) = insert(x,insert_sort(L))