YES (VAR X XS X1 X2) (RULES active(nats) -> mark(cons(0,incr(nats))) active(pairs) -> mark(cons(0,incr(odds))) active(odds) -> mark(incr(pairs)) active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS))) active(head(cons(X,XS))) -> mark(X) active(tail(cons(X,XS))) -> mark(XS) mark(nats) -> active(nats) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0) -> active(0) mark(incr(X)) -> active(incr(mark(X))) mark(pairs) -> active(pairs) mark(odds) -> active(odds) mark(s(X)) -> active(s(mark(X))) mark(head(X)) -> active(head(mark(X))) mark(tail(X)) -> active(tail(mark(X))) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) head(mark(X)) -> head(X) head(active(X)) -> head(X) tail(mark(X)) -> tail(X) tail(active(X)) -> tail(X) ) Proving termination of rewriting for Ex1_Luc04b_iGM: -> Dependency pairs: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_active(nats) -> nF_cons(0,incr(nats)) nF_active(nats) -> nF_incr(nats) nF_active(pairs) -> nF_mark(cons(0,incr(odds))) nF_active(pairs) -> nF_cons(0,incr(odds)) nF_active(pairs) -> nF_incr(odds) nF_active(odds) -> nF_mark(incr(pairs)) nF_active(odds) -> nF_incr(pairs) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_active(incr(cons(X,XS))) -> nF_cons(s(X),incr(XS)) nF_active(incr(cons(X,XS))) -> nF_s(X) nF_active(incr(cons(X,XS))) -> nF_incr(XS) nF_active(head(cons(X,XS))) -> nF_mark(X) nF_active(tail(cons(X,XS))) -> nF_mark(XS) nF_mark(nats) -> nF_active(nats) nF_mark(cons(X1,X2)) -> nF_active(cons(mark(X1),X2)) nF_mark(cons(X1,X2)) -> nF_cons(mark(X1),X2) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_mark(0) -> nF_active(0) nF_mark(incr(X)) -> nF_active(incr(mark(X))) nF_mark(incr(X)) -> nF_incr(mark(X)) nF_mark(incr(X)) -> nF_mark(X) nF_mark(pairs) -> nF_active(pairs) nF_mark(odds) -> nF_active(odds) nF_mark(s(X)) -> nF_active(s(mark(X))) nF_mark(s(X)) -> nF_s(mark(X)) nF_mark(s(X)) -> nF_mark(X) nF_mark(head(X)) -> nF_active(head(mark(X))) nF_mark(head(X)) -> nF_head(mark(X)) nF_mark(head(X)) -> nF_mark(X) nF_mark(tail(X)) -> nF_active(tail(mark(X))) nF_mark(tail(X)) -> nF_tail(mark(X)) nF_mark(tail(X)) -> nF_mark(X) nF_cons(mark(X1),X2) -> nF_cons(X1,X2) nF_cons(X1,mark(X2)) -> nF_cons(X1,X2) nF_cons(active(X1),X2) -> nF_cons(X1,X2) nF_cons(X1,active(X2)) -> nF_cons(X1,X2) nF_incr(mark(X)) -> nF_incr(X) nF_incr(active(X)) -> nF_incr(X) nF_s(mark(X)) -> nF_s(X) nF_s(active(X)) -> nF_s(X) nF_head(mark(X)) -> nF_head(X) nF_head(active(X)) -> nF_head(X) nF_tail(mark(X)) -> nF_tail(X) nF_tail(active(X)) -> nF_tail(X) -> Dependency pairs narrowed: nF_mark(incr(X)) -> nF_active(incr(mark(X))) nF_mark(s(X)) -> nF_active(s(mark(X))) nF_mark(head(X)) -> nF_active(head(mark(X))) nF_mark(tail(X)) -> nF_active(tail(mark(X))) -> New dependency pairs: nF_mark(incr(X)) -> nF_active(incr(X)) nF_mark(s(X)) -> nF_active(s(X)) nF_mark(head(X)) -> nF_active(head(X)) nF_mark(tail(X)) -> nF_active(tail(X)) -> Proof of termination for Ex1_Luc04b_iGM_1_1: -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(tail(X)) -> nF_active(tail(X)) nF_mark(tail(X)) -> nF_mark(X) nF_mark(head(X)) -> nF_mark(X) nF_mark(s(X)) -> nF_mark(X) nF_mark(incr(X)) -> nF_mark(X) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_active(tail(cons(X,XS))) -> nF_mark(XS) nF_mark(head(X)) -> nF_active(head(X)) nF_active(head(cons(X,XS))) -> nF_mark(X) nF_mark(s(X)) -> nF_active(s(X)) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(pairs) -> nF_mark(cons(0,incr(odds))) nF_mark(pairs) -> nF_active(pairs) nF_mark(cons(X1,X2)) -> nF_active(cons(mark(X1),X2)) nF_mark(nats) -> nF_active(nats) UsableRules: active(nats) -> mark(cons(0,incr(nats))) active(pairs) -> mark(cons(0,incr(odds))) active(odds) -> mark(incr(pairs)) active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS))) active(head(cons(X,XS))) -> mark(X) active(tail(cons(X,XS))) -> mark(XS) mark(nats) -> active(nats) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(0) -> active(0) mark(incr(X)) -> active(incr(mark(X))) mark(pairs) -> active(pairs) mark(odds) -> active(odds) mark(s(X)) -> active(s(mark(X))) mark(head(X)) -> active(head(mark(X))) mark(tail(X)) -> active(tail(mark(X))) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) head(mark(X)) -> head(X) head(active(X)) -> head(X) tail(mark(X)) -> tail(X) tail(active(X)) -> tail(X) Polynomial Interpretation: [active](X) = X [nats] = 1 [mark](X) = 1 [cons](X1,X2) = 0 [0] = 0 [incr](X) = 1 [pairs] = 1 [odds] = 1 [s](X) = 0 [head](X) = 1 [tail](X) = 1 [nF_active](X) = X [nF_mark](X) = 1 TIME: 9.3757e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(nats) -> nF_active(nats) nF_active(pairs) -> nF_mark(cons(0,incr(odds))) nF_mark(pairs) -> nF_active(pairs) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(head(cons(X,XS))) -> nF_mark(X) nF_mark(s(X)) -> nF_active(s(X)) nF_active(tail(cons(X,XS))) -> nF_mark(XS) nF_mark(head(X)) -> nF_active(head(X)) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_mark(incr(X)) -> nF_mark(X) nF_mark(s(X)) -> nF_mark(X) nF_mark(head(X)) -> nF_mark(X) nF_mark(tail(X)) -> nF_mark(X) nF_mark(tail(X)) -> nF_active(tail(X)) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) head(mark(X)) -> head(X) head(active(X)) -> head(X) tail(mark(X)) -> tail(X) tail(active(X)) -> tail(X) Polynomial Interpretation: [active](X) = X [nats] = 0 [mark](X) = X [cons](X1,X2) = X1 + X2 [0] = 0 [incr](X) = X [pairs] = 0 [odds] = 0 [s](X) = X [head](X) = X + 1 [tail](X) = X + 1 [nF_active](X) = X [nF_mark](X) = X TIME: 7.5509e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(tail(X)) -> nF_active(tail(X)) nF_mark(head(X)) -> nF_mark(X) nF_mark(s(X)) -> nF_mark(X) nF_mark(incr(X)) -> nF_mark(X) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_active(tail(cons(X,XS))) -> nF_mark(XS) nF_mark(head(X)) -> nF_active(head(X)) nF_active(head(cons(X,XS))) -> nF_mark(X) nF_mark(s(X)) -> nF_active(s(X)) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(pairs) -> nF_mark(cons(0,incr(odds))) nF_mark(pairs) -> nF_active(pairs) nF_mark(nats) -> nF_active(nats) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) head(mark(X)) -> head(X) head(active(X)) -> head(X) tail(mark(X)) -> tail(X) tail(active(X)) -> tail(X) Polynomial Interpretation: [active](X) = 0 [nats] = 1 [mark](X) = 0 [cons](X1,X2) = 0 [0] = 0 [incr](X) = 1 [pairs] = 1 [odds] = 1 [s](X) = 0 [head](X) = 1 [tail](X) = 1 [nF_active](X) = X [nF_mark](X) = 1 TIME: 7.4838e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(nats) -> nF_active(nats) nF_active(pairs) -> nF_mark(cons(0,incr(odds))) nF_mark(pairs) -> nF_active(pairs) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(head(cons(X,XS))) -> nF_mark(X) nF_mark(head(X)) -> nF_active(head(X)) nF_active(tail(cons(X,XS))) -> nF_mark(XS) nF_mark(tail(X)) -> nF_active(tail(X)) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_mark(incr(X)) -> nF_mark(X) nF_mark(s(X)) -> nF_mark(X) nF_mark(head(X)) -> nF_mark(X) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) head(mark(X)) -> head(X) head(active(X)) -> head(X) tail(mark(X)) -> tail(X) tail(active(X)) -> tail(X) Polynomial Interpretation: [active](X) = X [nats] = 0 [mark](X) = X [cons](X1,X2) = X1 + X2 [0] = 0 [incr](X) = X [pairs] = 0 [odds] = 0 [s](X) = X [head](X) = X + 1 [tail](X) = X + 1 [nF_active](X) = X [nF_mark](X) = X TIME: 7.4081e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(tail(X)) -> nF_active(tail(X)) nF_mark(s(X)) -> nF_mark(X) nF_mark(incr(X)) -> nF_mark(X) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_active(tail(cons(X,XS))) -> nF_mark(XS) nF_mark(head(X)) -> nF_active(head(X)) nF_active(head(cons(X,XS))) -> nF_mark(X) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(pairs) -> nF_mark(cons(0,incr(odds))) nF_mark(pairs) -> nF_active(pairs) nF_mark(nats) -> nF_active(nats) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) head(mark(X)) -> head(X) head(active(X)) -> head(X) tail(mark(X)) -> tail(X) tail(active(X)) -> tail(X) Polynomial Interpretation: [active](X) = X [nats] = 1 [mark](X) = X [cons](X1,X2) = X1 + X2 [0] = 0 [incr](X) = X [pairs] = 0 [odds] = 0 [s](X) = X [head](X) = X + 1 [tail](X) = X [nF_active](X) = X [nF_mark](X) = X TIME: 7.294e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(nats) -> nF_active(nats) nF_active(pairs) -> nF_mark(cons(0,incr(odds))) nF_mark(pairs) -> nF_active(pairs) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(tail(cons(X,XS))) -> nF_mark(XS) nF_mark(head(X)) -> nF_active(head(X)) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_mark(incr(X)) -> nF_mark(X) nF_mark(s(X)) -> nF_mark(X) nF_mark(tail(X)) -> nF_active(tail(X)) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) head(mark(X)) -> head(X) head(active(X)) -> head(X) tail(mark(X)) -> tail(X) tail(active(X)) -> tail(X) Polynomial Interpretation: [active](X) = 0 [nats] = 1 [mark](X) = 0 [cons](X1,X2) = 0 [0] = 0 [incr](X) = 1 [pairs] = 1 [odds] = 1 [s](X) = 0 [head](X) = 0 [tail](X) = 1 [nF_active](X) = X [nF_mark](X) = 1 TIME: 7.5073e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(tail(X)) -> nF_active(tail(X)) nF_mark(s(X)) -> nF_mark(X) nF_mark(incr(X)) -> nF_mark(X) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_active(tail(cons(X,XS))) -> nF_mark(XS) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(pairs) -> nF_mark(cons(0,incr(odds))) nF_mark(pairs) -> nF_active(pairs) nF_mark(nats) -> nF_active(nats) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) tail(mark(X)) -> tail(X) tail(active(X)) -> tail(X) Polynomial Interpretation: [active](X) = X [nats] = 0 [mark](X) = X [cons](X1,X2) = X1 + X2 [0] = 0 [incr](X) = X [pairs] = 0 [odds] = 0 [s](X) = X [head](X) = 0 [tail](X) = X + 1 [nF_active](X) = X [nF_mark](X) = X TIME: 7.157e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(nats) -> nF_active(nats) nF_active(pairs) -> nF_mark(cons(0,incr(odds))) nF_mark(pairs) -> nF_active(pairs) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_mark(incr(X)) -> nF_mark(X) nF_mark(s(X)) -> nF_mark(X) nF_mark(tail(X)) -> nF_active(tail(X)) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) tail(mark(X)) -> tail(X) tail(active(X)) -> tail(X) Polynomial Interpretation: [active](X) = 0 [nats] = 1 [mark](X) = 0 [cons](X1,X2) = 0 [0] = 0 [incr](X) = 1 [pairs] = 1 [odds] = 1 [s](X) = 0 [head](X) = 0 [tail](X) = 0 [nF_active](X) = X [nF_mark](X) = 1 TIME: 6.9111e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_mark(s(X)) -> nF_mark(X) nF_mark(incr(X)) -> nF_mark(X) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(pairs) -> nF_mark(cons(0,incr(odds))) nF_mark(pairs) -> nF_active(pairs) nF_mark(nats) -> nF_active(nats) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) Polynomial Interpretation: [active](X) = X [nats] = 1 [mark](X) = X [cons](X1,X2) = X1 [0] = 0 [incr](X) = X [pairs] = 1 [odds] = 1 [s](X) = X [head](X) = 0 [tail](X) = 0 [nF_active](X) = X [nF_mark](X) = X TIME: 6.8653e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(nats) -> nF_active(nats) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_mark(incr(X)) -> nF_mark(X) nF_mark(s(X)) -> nF_mark(X) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) Polynomial Interpretation: [active](X) = X [nats] = 1 [mark](X) = X [cons](X1,X2) = X1 [0] = 0 [incr](X) = X + 1 [pairs] = 0 [odds] = 1 [s](X) = X + 1 [head](X) = 0 [tail](X) = 0 [nF_active](X) = X [nF_mark](X) = X TIME: 6.3443e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_mark(incr(X)) -> nF_mark(X) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_mark(nats) -> nF_active(nats) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) Polynomial Interpretation: [active](X) = X [nats] = 1 [mark](X) = X [cons](X1,X2) = X1 [0] = 0 [incr](X) = X [pairs] = 0 [odds] = 0 [s](X) = 0 [head](X) = 0 [tail](X) = 0 [nF_active](X) = 0 [nF_mark](X) = X TIME: 6.421e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_mark(incr(X)) -> nF_mark(X) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) Polynomial Interpretation: [active](X) = X [nats] = 0 [mark](X) = X [cons](X1,X2) = X1 [0] = 0 [incr](X) = X + 1 [pairs] = 0 [odds] = 1 [s](X) = 0 [head](X) = 0 [tail](X) = 0 [nF_active](X) = X [nF_mark](X) = X TIME: 6.2964e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_mark(cons(X1,X2)) -> nF_mark(X1) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_active(odds) -> nF_mark(incr(pairs)) nF_mark(odds) -> nF_active(odds) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) Polynomial Interpretation: [active](X) = X [nats] = 0 [mark](X) = X [cons](X1,X2) = X1 [0] = 0 [incr](X) = 0 [pairs] = 0 [odds] = 1 [s](X) = 0 [head](X) = 0 [tail](X) = 0 [nF_active](X) = 0 [nF_mark](X) = X TIME: 6.2446e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(odds) -> nF_mark(incr(pairs)) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_mark(cons(X1,X2)) -> nF_mark(X1) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) Polynomial Interpretation: [active](X) = X [nats] = 1 [mark](X) = X [cons](X1,X2) = X1 + 1 [0] = 0 [incr](X) = X [pairs] = 0 [odds] = 0 [s](X) = 0 [head](X) = 0 [tail](X) = 0 [nF_active](X) = X [nF_mark](X) = X TIME: 6.2521e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) nF_active(odds) -> nF_mark(incr(pairs)) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) Polynomial Interpretation: [active](X) = 0 [nats] = 0 [mark](X) = 0 [cons](X1,X2) = 0 [0] = 0 [incr](X) = 0 [pairs] = 0 [odds] = 1 [s](X) = 0 [head](X) = 0 [tail](X) = 0 [nF_active](X) = X [nF_mark](X) = 0 TIME: 6.0608e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(incr(X)) -> nF_active(incr(X)) nF_active(incr(cons(X,XS))) -> nF_mark(cons(s(X),incr(XS))) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) Polynomial Interpretation: [active](X) = 0 [nats] = 0 [mark](X) = 0 [cons](X1,X2) = 0 [0] = 0 [incr](X) = 1 [pairs] = 0 [odds] = 0 [s](X) = 0 [head](X) = 0 [tail](X) = 0 [nF_active](X) = 1 [nF_mark](X) = X TIME: 5.9978e-2 -> -> Dependency pairs in cycle: nF_active(nats) -> nF_mark(cons(0,incr(nats))) nF_mark(incr(X)) -> nF_active(incr(X)) UsableRules: cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) incr(mark(X)) -> incr(X) incr(active(X)) -> incr(X) Polynomial Interpretation: [active](X) = 0 [nats] = 1 [mark](X) = 0 [cons](X1,X2) = 0 [0] = 0 [incr](X) = 0 [pairs] = 0 [odds] = 0 [s](X) = 0 [head](X) = 0 [tail](X) = 0 [nF_active](X) = X [nF_mark](X) = 1 TIME: 5.6721e-2 -> Proof of termination for Ex1_Luc04b_iGM_1_2: -> -> Dependency pairs in cycle: nF_cons(X1,active(X2)) -> nF_cons(X1,X2) nF_cons(active(X1),X2) -> nF_cons(X1,X2) nF_cons(X1,mark(X2)) -> nF_cons(X1,X2) nF_cons(mark(X1),X2) -> nF_cons(X1,X2) Dependency pairs oriented using subterm criterion. -> -> Dependency pairs in cycle: nF_cons(X1,active(X2)) -> nF_cons(X1,X2) nF_cons(X1,mark(X2)) -> nF_cons(X1,X2) Termination proved: Cycles verify subterm criterion. -> Proof of termination for Ex1_Luc04b_iGM_1_3: -> -> Dependency pairs in cycle: nF_incr(active(X)) -> nF_incr(X) nF_incr(mark(X)) -> nF_incr(X) Termination proved: Cycles verify subterm criterion. -> Proof of termination for Ex1_Luc04b_iGM_1_4: -> -> Dependency pairs in cycle: nF_s(active(X)) -> nF_s(X) nF_s(mark(X)) -> nF_s(X) Termination proved: Cycles verify subterm criterion. -> Proof of termination for Ex1_Luc04b_iGM_1_5: -> -> Dependency pairs in cycle: nF_head(active(X)) -> nF_head(X) nF_head(mark(X)) -> nF_head(X) Termination proved: Cycles verify subterm criterion. -> Proof of termination for Ex1_Luc04b_iGM_1_6: -> -> Dependency pairs in cycle: nF_tail(active(X)) -> nF_tail(X) nF_tail(mark(X)) -> nF_tail(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.