% Natural numbers nat : type. %name nat N. z : nat. s : nat -> nat. 0 = z. 1 = s 0. 2 = s 1. 3 = s 2. 4 = s 3. 5 = s 4. 6 = s 5. 7 = s 6. 8 = s 7. 9 = s 8. % ... another job for Sisyphos. % Order on natural numbers leq : nat -> nat -> type. %name leq L. %mode leq +N +M. % leq/z : ... % leq/s : ... %worlds () (leq _ _). %terminates M (leq N M). % Ascendingly sorted lists % alist N contains only elements >= N. alist : nat -> type. %name alist AL. % ... % Descendingly sorted lists. % dlist N contains only element <= N. dlist : nat -> type. %name dlist DL. % ... % Reversing an alist revapp : alist N -> leq M N -> dlist M -> dlist M' -> type. %mode revapp +A +L +D -D. % ... %worlds () (revapp _ _ _ _). %terminates A (revapp A _ _ _). %covers revapp +A +L +D -D. %total A (revapp A _ _ _). reverse : alist N -> dlist M -> type. %mode reverse +A -D. % ... %worlds () (reverse _ _). %total A (reverse A _). % Testing the implementation alist1 : alist 0 = acons 0 leq/z (acons 1 (leq/s leq/z) anil). %query 1 1 reverse alist1 D.