- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] sort(nil) -> nil [2] sort(cons(x,y)) -> insert(x,sort(y)) [3] insert(x,nil) -> cons(x,nil) [4] insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v) [5] choose(x,cons(v,w),y,0) -> cons(x,cons(v,w)) [6] choose(x,cons(v,w),0,s(z)) -> cons(v,insert(x,w)) [7] choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 2 components: { --> } { --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_sort -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_choose -> 2 Marked_insert -> 2 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Subterm criterion) ST: Marked_choose -> 3 APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] sort(nil) -> nil [2] sort(cons(x,y)) -> insert(x,sort(y)) [3] insert(x,nil) -> cons(x,nil) [4] insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v) [5] choose(x,cons(v,w),y,0) -> cons(x,cons(v,w)) [6] choose(x,cons(v,w),0,s(z)) -> cons(v,insert(x,w)) [7] choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} ]} ]} Cime worked for 0.012954 seconds (real time) Cime Exit Status: 0