enrich
olist
with
functions
sort : list → list;
variables
x : list;
y : list;
z : list;
a : elem;
b : elem;
c : elem;
axioms
Ordered: ordered≤(sort(x));
Perm: perm(x, sort(x));
end enrich