list.owl

sum(z, ?x, ?x).
sum(s(?x), ?y, s(?z)) :- sum(?x, ?y, ?z).

append(nil, ?x, cs(?x, nil)).
append(cs(?head, ?tail), ?x, cs(?head, ?next)) :- append(?tail, ?x, ?next).

reverse(nil, nil).
reverse(cs(?head, ?tail), ?rev) :-  reverse(?tail, ?revtail) & append(?revtail, ?head, ?rev).
reverse_inv(?x, ?y) :- reverse(?y, ?x).

reverse_acc(nil, ?acc, ?acc).
reverse_acc(cs(?x, ?xs), ?z, ?acc) :- reverse_acc(?xs, ?z, cs(?x, ?acc)).

length(nil, z).
length(cs(?x, ?l), s(?ll)) :- length(?l, ?ll).

less(?x, ?y) :- sum(?x, ?z, ?y).
high(?x, ?y) :- sum(?y, s(?z), ?x).

insert(?x, nil, cs(?x, nil)).
insert(?x, cs(?h, ?t), cs(?x, cs(?h, ?t))) :- less(?x, ?h).
insert(?x, cs(?h, ?t), cs(?h, ?z)) :- high(?x, ?h) & insert(?x, ?t, ?z).

sort(nil, nil).
sort(cs(?h, ?t), ?s) :- sort(?t, ?ss) & insert(?h, ?ss, ?s).