mod SORTING is protecting NAT . sort List . subsort Nat < List . op nil : -> List [ctor] . op _;_ : List List -> List [ctor assoc id: nil] . vars N M : Nat . vars L Q : List . *** include here your rule or rules endm *** testing by search that your rule or rules are DETERMINISTIC (yield a single final result) search 5 ; 4 ; 3 ; 2 ; 1 ; 0 =>! L . *** SINGLE solution should be 0 ; 1 ; 2 ; 3 ; 4 ; 5 search 3 ; 4 ; 3 ; 5 ; 1 ; 0 =>! L . *** SINGLE solution should be 0 ; 1 ; 3 ; 3 ; 4 ; 5 search 3 ; 4 ; 3 ; 5 ; 1 ; 4 =>! L . *** SINGLE solution should be 1 ; 3 ; 3 ; 4 ; 4 ; 5 search 3 ; 4 ; 3 ; 4 ; 1 ; 4 =>! L . *** SINGLE solution should be 1 ; 3 ; 3 ; 4 ; 4 ; 4 *** testing that your rules yield the correct result rewrite 5 ; 4 ; 3 ; 2 ; 1 ; 0 . *** should be 0 ; 1 ; 2 ; 3 ; 4 ; 5 rewrite 3 ; 4 ; 3 ; 5 ; 1 ; 0 . *** should be 0 ; 1 ; 3 ; 3 ; 4 ; 5 rewrite 3 ; 4 ; 3 ; 5 ; 1 ; 4 . *** should be 1 ; 3 ; 3 ; 4 ; 4 ; 5 rewrite 3 ; 4 ; 3 ; 4 ; 1 ; 4 . *** should be 1 ; 3 ; 3 ; 4 ; 4 ; 4