YES TRS: { rev(nil()) -> nil(), rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)), rev1(x, cons(y, l)) -> rev1(y, l), rev1(0(), nil()) -> 0(), rev1(s(x), nil()) -> s(x), rev2(x, nil()) -> nil(), rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l)))} DP: Strict: { rev#(cons(x, l)) -> rev1#(x, l), rev#(cons(x, l)) -> rev2#(x, l), rev1#(x, cons(y, l)) -> rev1#(y, l), rev2#(x, cons(y, l)) -> rev#(cons(x, rev2(y, l))), rev2#(x, cons(y, l)) -> rev2#(y, l)} Weak: { rev(nil()) -> nil(), rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)), rev1(x, cons(y, l)) -> rev1(y, l), rev1(0(), nil()) -> 0(), rev1(s(x), nil()) -> s(x), rev2(x, nil()) -> nil(), rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l)))} EDG: {(rev#(cons(x, l)) -> rev2#(x, l), rev2#(x, cons(y, l)) -> rev2#(y, l)) (rev#(cons(x, l)) -> rev2#(x, l), rev2#(x, cons(y, l)) -> rev#(cons(x, rev2(y, l)))) (rev2#(x, cons(y, l)) -> rev2#(y, l), rev2#(x, cons(y, l)) -> rev2#(y, l)) (rev2#(x, cons(y, l)) -> rev2#(y, l), rev2#(x, cons(y, l)) -> rev#(cons(x, rev2(y, l)))) (rev2#(x, cons(y, l)) -> rev#(cons(x, rev2(y, l))), rev#(cons(x, l)) -> rev1#(x, l)) (rev2#(x, cons(y, l)) -> rev#(cons(x, rev2(y, l))), rev#(cons(x, l)) -> rev2#(x, l)) (rev1#(x, cons(y, l)) -> rev1#(y, l), rev1#(x, cons(y, l)) -> rev1#(y, l)) (rev#(cons(x, l)) -> rev1#(x, l), rev1#(x, cons(y, l)) -> rev1#(y, l))} SCCS: Scc: {rev1#(x, cons(y, l)) -> rev1#(y, l)} Scc: { rev#(cons(x, l)) -> rev2#(x, l), rev2#(x, cons(y, l)) -> rev#(cons(x, rev2(y, l))), rev2#(x, cons(y, l)) -> rev2#(y, l)} SCC: Strict: {rev1#(x, cons(y, l)) -> rev1#(y, l)} Weak: { rev(nil()) -> nil(), rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)), rev1(x, cons(y, l)) -> rev1(y, l), rev1(0(), nil()) -> 0(), rev1(s(x), nil()) -> s(x), rev2(x, nil()) -> nil(), rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l)))} SPSC: Simple Projection: pi(rev1#) = 1 Strict: {} Qed SCC: Strict: { rev#(cons(x, l)) -> rev2#(x, l), rev2#(x, cons(y, l)) -> rev#(cons(x, rev2(y, l))), rev2#(x, cons(y, l)) -> rev2#(y, l)} Weak: { rev(nil()) -> nil(), rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)), rev1(x, cons(y, l)) -> rev1(y, l), rev1(0(), nil()) -> 0(), rev1(s(x), nil()) -> s(x), rev2(x, nil()) -> nil(), rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l)))} POLY: Argument Filtering: pi(s) = [], pi(0) = [], pi(rev2#) = 1, pi(rev2) = 1, pi(rev1) = [], pi(cons) = [1], pi(rev#) = 0, pi(rev) = 0, pi(nil) = [] Usable Rules: {} Interpretation: [cons](x0) = x0 + 1 Strict: {rev2#(x, cons(y, l)) -> rev#(cons(x, rev2(y, l)))} Weak: { rev(nil()) -> nil(), rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)), rev1(x, cons(y, l)) -> rev1(y, l), rev1(0(), nil()) -> 0(), rev1(s(x), nil()) -> s(x), rev2(x, nil()) -> nil(), rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l)))} EDG: {} SCCS: Qed