YES (VAR X Y X1 X2) (RULES a__nats -> a__adx(a__zeros) a__zeros -> cons(0,zeros) a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) a__hd(cons(X,Y)) -> mark(X) a__tl(cons(X,Y)) -> mark(Y) mark(nats) -> a__nats mark(adx(X)) -> a__adx(mark(X)) mark(zeros) -> a__zeros mark(incr(X)) -> a__incr(mark(X)) mark(hd(X)) -> a__hd(mark(X)) mark(tl(X)) -> a__tl(mark(X)) mark(cons(X1,X2)) -> cons(X1,X2) mark(0) -> 0 mark(s(X)) -> s(X) a__nats -> nats a__adx(X) -> adx(X) a__zeros -> zeros a__incr(X) -> incr(X) a__hd(X) -> hd(X) a__tl(X) -> tl(X) ) Proving termination of rewriting for ExIntrod_GM04_GM: -> Dependency pairs: nF_a__nats -> nF_a__adx(a__zeros) nF_a__nats -> nF_a__zeros nF_a__adx(cons(X,Y)) -> nF_a__incr(cons(X,adx(Y))) nF_a__hd(cons(X,Y)) -> nF_mark(X) nF_a__tl(cons(X,Y)) -> nF_mark(Y) nF_mark(nats) -> nF_a__nats nF_mark(adx(X)) -> nF_a__adx(mark(X)) nF_mark(adx(X)) -> nF_mark(X) nF_mark(zeros) -> nF_a__zeros nF_mark(incr(X)) -> nF_a__incr(mark(X)) nF_mark(incr(X)) -> nF_mark(X) nF_mark(hd(X)) -> nF_a__hd(mark(X)) nF_mark(hd(X)) -> nF_mark(X) nF_mark(tl(X)) -> nF_a__tl(mark(X)) nF_mark(tl(X)) -> nF_mark(X) -> Proof of termination for ExIntrod_GM04_GM_1: -> -> Dependency pairs in cycle: nF_a__hd(cons(X,Y)) -> nF_mark(X) nF_mark(hd(X)) -> nF_a__hd(mark(X)) nF_mark(tl(X)) -> nF_mark(X) nF_mark(hd(X)) -> nF_mark(X) nF_mark(incr(X)) -> nF_mark(X) nF_mark(adx(X)) -> nF_mark(X) nF_a__tl(cons(X,Y)) -> nF_mark(Y) nF_mark(tl(X)) -> nF_a__tl(mark(X)) UsableRules: a__nats -> a__adx(a__zeros) a__zeros -> cons(0,zeros) a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) a__hd(cons(X,Y)) -> mark(X) a__tl(cons(X,Y)) -> mark(Y) mark(nats) -> a__nats mark(adx(X)) -> a__adx(mark(X)) mark(zeros) -> a__zeros mark(incr(X)) -> a__incr(mark(X)) mark(hd(X)) -> a__hd(mark(X)) mark(tl(X)) -> a__tl(mark(X)) mark(cons(X1,X2)) -> cons(X1,X2) mark(0) -> 0 mark(s(X)) -> s(X) a__nats -> nats a__adx(X) -> adx(X) a__zeros -> zeros a__incr(X) -> incr(X) a__hd(X) -> hd(X) a__tl(X) -> tl(X) Polynomial Interpretation: [a__nats] = 1 [a__adx](X) = X [a__zeros] = 1 [cons](X1,X2) = X1 + X2 + 1 [0] = 0 [zeros] = 0 [a__incr](X) = X [s](X) = 0 [incr](X) = X [adx](X) = X [a__hd](X) = X [mark](X) = X + 1 [a__tl](X) = X + 1 [nats] = 0 [hd](X) = X [tl](X) = X + 1 [nF_a__hd](X) = X [nF_mark](X) = X + 1 [nF_a__tl](X) = X TIME: 5.3843e-2 -> -> Dependency pairs in cycle: nF_a__hd(cons(X,Y)) -> nF_mark(X) nF_mark(hd(X)) -> nF_a__hd(mark(X)) nF_mark(adx(X)) -> nF_mark(X) nF_mark(incr(X)) -> nF_mark(X) nF_mark(hd(X)) -> nF_mark(X) nF_mark(tl(X)) -> nF_mark(X) UsableRules: a__nats -> a__adx(a__zeros) a__zeros -> cons(0,zeros) a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) a__hd(cons(X,Y)) -> mark(X) a__tl(cons(X,Y)) -> mark(Y) mark(nats) -> a__nats mark(adx(X)) -> a__adx(mark(X)) mark(zeros) -> a__zeros mark(incr(X)) -> a__incr(mark(X)) mark(hd(X)) -> a__hd(mark(X)) mark(tl(X)) -> a__tl(mark(X)) mark(cons(X1,X2)) -> cons(X1,X2) mark(0) -> 0 mark(s(X)) -> s(X) a__nats -> nats a__adx(X) -> adx(X) a__zeros -> zeros a__incr(X) -> incr(X) a__hd(X) -> hd(X) a__tl(X) -> tl(X) Polynomial Interpretation: [a__nats] = 1 [a__adx](X) = X [a__zeros] = 1 [cons](X1,X2) = X1 + X2 [0] = 1 [zeros] = 0 [a__incr](X) = X [s](X) = 0 [incr](X) = X [adx](X) = X [a__hd](X) = X + 1 [mark](X) = X + 1 [a__tl](X) = X + 1 [nats] = 1 [hd](X) = X + 1 [tl](X) = X + 1 [nF_a__hd](X) = X [nF_mark](X) = X TIME: 5.0744e-2 -> -> Dependency pairs in cycle: nF_a__hd(cons(X,Y)) -> nF_mark(X) nF_mark(hd(X)) -> nF_a__hd(mark(X)) nF_mark(hd(X)) -> nF_mark(X) nF_mark(incr(X)) -> nF_mark(X) nF_mark(adx(X)) -> nF_mark(X) UsableRules: a__nats -> a__adx(a__zeros) a__zeros -> cons(0,zeros) a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) a__hd(cons(X,Y)) -> mark(X) a__tl(cons(X,Y)) -> mark(Y) mark(nats) -> a__nats mark(adx(X)) -> a__adx(mark(X)) mark(zeros) -> a__zeros mark(incr(X)) -> a__incr(mark(X)) mark(hd(X)) -> a__hd(mark(X)) mark(tl(X)) -> a__tl(mark(X)) mark(cons(X1,X2)) -> cons(X1,X2) mark(0) -> 0 mark(s(X)) -> s(X) a__nats -> nats a__adx(X) -> adx(X) a__zeros -> zeros a__incr(X) -> incr(X) a__hd(X) -> hd(X) a__tl(X) -> tl(X) Polynomial Interpretation: [a__nats] = 1 [a__adx](X) = X + 1 [a__zeros] = 0 [cons](X1,X2) = X1 + X2 [0] = 0 [zeros] = 0 [a__incr](X) = X [s](X) = 0 [incr](X) = X [adx](X) = X + 1 [a__hd](X) = X [mark](X) = X [a__tl](X) = X [nats] = 1 [hd](X) = X [tl](X) = X [nF_a__hd](X) = X [nF_mark](X) = X TIME: 4.7315e-2 -> -> Dependency pairs in cycle: nF_a__hd(cons(X,Y)) -> nF_mark(X) nF_mark(hd(X)) -> nF_a__hd(mark(X)) nF_mark(incr(X)) -> nF_mark(X) nF_mark(hd(X)) -> nF_mark(X) UsableRules: a__nats -> a__adx(a__zeros) a__zeros -> cons(0,zeros) a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) a__hd(cons(X,Y)) -> mark(X) a__tl(cons(X,Y)) -> mark(Y) mark(nats) -> a__nats mark(adx(X)) -> a__adx(mark(X)) mark(zeros) -> a__zeros mark(incr(X)) -> a__incr(mark(X)) mark(hd(X)) -> a__hd(mark(X)) mark(tl(X)) -> a__tl(mark(X)) mark(cons(X1,X2)) -> cons(X1,X2) mark(0) -> 0 mark(s(X)) -> s(X) a__nats -> nats a__adx(X) -> adx(X) a__zeros -> zeros a__incr(X) -> incr(X) a__hd(X) -> hd(X) a__tl(X) -> tl(X) Polynomial Interpretation: [a__nats] = 1 [a__adx](X) = X [a__zeros] = 1 [cons](X1,X2) = X1 + X2 [0] = 1 [zeros] = 0 [a__incr](X) = X [s](X) = 0 [incr](X) = X [adx](X) = X [a__hd](X) = X + 1 [mark](X) = X + 1 [a__tl](X) = X + 1 [nats] = 1 [hd](X) = X + 1 [tl](X) = X + 1 [nF_a__hd](X) = X [nF_mark](X) = X TIME: 5.1454e-2 -> -> Dependency pairs in cycle: nF_a__hd(cons(X,Y)) -> nF_mark(X) nF_mark(hd(X)) -> nF_a__hd(mark(X)) nF_mark(incr(X)) -> nF_mark(X) UsableRules: a__nats -> a__adx(a__zeros) a__zeros -> cons(0,zeros) a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) a__hd(cons(X,Y)) -> mark(X) a__tl(cons(X,Y)) -> mark(Y) mark(nats) -> a__nats mark(adx(X)) -> a__adx(mark(X)) mark(zeros) -> a__zeros mark(incr(X)) -> a__incr(mark(X)) mark(hd(X)) -> a__hd(mark(X)) mark(tl(X)) -> a__tl(mark(X)) mark(cons(X1,X2)) -> cons(X1,X2) mark(0) -> 0 mark(s(X)) -> s(X) a__nats -> nats a__adx(X) -> adx(X) a__zeros -> zeros a__incr(X) -> incr(X) a__hd(X) -> hd(X) a__tl(X) -> tl(X) Polynomial Interpretation: [a__nats] = 1 [a__adx](X) = X [a__zeros] = 1 [cons](X1,X2) = X1 + X2 + 1 [0] = 0 [zeros] = 0 [a__incr](X) = X [s](X) = 0 [incr](X) = X [adx](X) = X [a__hd](X) = X + 1 [mark](X) = X + 1 [a__tl](X) = X [nats] = 0 [hd](X) = X + 1 [tl](X) = X [nF_a__hd](X) = X [nF_mark](X) = X + 1 TIME: 5.0622e-2 -> -> Dependency pairs in cycle: nF_mark(incr(X)) -> nF_mark(X) Termination proved: Cycles verify subterm criterion. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 1 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic Termination was proved succesfully.