- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] prime(0) -> false [2] prime(s(0)) -> false [3] prime(s(s(x))) -> prime1(s(s(x)),s(x)) [4] prime1(x,0) -> false [5] prime1(x,s(0)) -> true [6] prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y))) [7] divp(x,y) -> =(rem(x,y),0) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Subterm criterion) ST: Marked_prime1 -> 2 APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] prime(0) -> false [2] prime(s(0)) -> false [3] prime(s(s(x))) -> prime1(s(s(x)),s(x)) [4] prime1(x,0) -> false [5] prime1(x,s(0)) -> true [6] prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y))) [7] divp(x,y) -> =(rem(x,y),0) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} Cime worked for 0.004062 seconds (real time) Cime Exit Status: 0