YES Problem: t(o(x1)) -> m(a(x1)) t(e(x1)) -> n(s(x1)) a(l(x1)) -> a(t(x1)) o(m(a(x1))) -> t(e(n(x1))) s(a(x1)) -> l(a(t(o(m(a(t(e(x1)))))))) n(s(x1)) -> a(l(a(t(x1)))) Proof: DP Processor: DPs: t#(o(x1)) -> a#(x1) t#(e(x1)) -> s#(x1) t#(e(x1)) -> n#(s(x1)) a#(l(x1)) -> t#(x1) a#(l(x1)) -> a#(t(x1)) o#(m(a(x1))) -> n#(x1) o#(m(a(x1))) -> t#(e(n(x1))) s#(a(x1)) -> t#(e(x1)) s#(a(x1)) -> a#(t(e(x1))) s#(a(x1)) -> o#(m(a(t(e(x1))))) s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) s#(a(x1)) -> a#(t(o(m(a(t(e(x1))))))) n#(s(x1)) -> t#(x1) n#(s(x1)) -> a#(t(x1)) n#(s(x1)) -> a#(l(a(t(x1)))) TRS: t(o(x1)) -> m(a(x1)) t(e(x1)) -> n(s(x1)) a(l(x1)) -> a(t(x1)) o(m(a(x1))) -> t(e(n(x1))) s(a(x1)) -> l(a(t(o(m(a(t(e(x1)))))))) n(s(x1)) -> a(l(a(t(x1)))) TDG Processor: DPs: t#(o(x1)) -> a#(x1) t#(e(x1)) -> s#(x1) t#(e(x1)) -> n#(s(x1)) a#(l(x1)) -> t#(x1) a#(l(x1)) -> a#(t(x1)) o#(m(a(x1))) -> n#(x1) o#(m(a(x1))) -> t#(e(n(x1))) s#(a(x1)) -> t#(e(x1)) s#(a(x1)) -> a#(t(e(x1))) s#(a(x1)) -> o#(m(a(t(e(x1))))) s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) s#(a(x1)) -> a#(t(o(m(a(t(e(x1))))))) n#(s(x1)) -> t#(x1) n#(s(x1)) -> a#(t(x1)) n#(s(x1)) -> a#(l(a(t(x1)))) TRS: t(o(x1)) -> m(a(x1)) t(e(x1)) -> n(s(x1)) a(l(x1)) -> a(t(x1)) o(m(a(x1))) -> t(e(n(x1))) s(a(x1)) -> l(a(t(o(m(a(t(e(x1)))))))) n(s(x1)) -> a(l(a(t(x1)))) graph: o#(m(a(x1))) -> n#(x1) -> n#(s(x1)) -> a#(l(a(t(x1)))) o#(m(a(x1))) -> n#(x1) -> n#(s(x1)) -> a#(t(x1)) o#(m(a(x1))) -> n#(x1) -> n#(s(x1)) -> t#(x1) o#(m(a(x1))) -> t#(e(n(x1))) -> t#(e(x1)) -> n#(s(x1)) o#(m(a(x1))) -> t#(e(n(x1))) -> t#(e(x1)) -> s#(x1) o#(m(a(x1))) -> t#(e(n(x1))) -> t#(o(x1)) -> a#(x1) n#(s(x1)) -> a#(l(a(t(x1)))) -> a#(l(x1)) -> a#(t(x1)) n#(s(x1)) -> a#(l(a(t(x1)))) -> a#(l(x1)) -> t#(x1) n#(s(x1)) -> a#(t(x1)) -> a#(l(x1)) -> a#(t(x1)) n#(s(x1)) -> a#(t(x1)) -> a#(l(x1)) -> t#(x1) n#(s(x1)) -> t#(x1) -> t#(e(x1)) -> n#(s(x1)) n#(s(x1)) -> t#(x1) -> t#(e(x1)) -> s#(x1) n#(s(x1)) -> t#(x1) -> t#(o(x1)) -> a#(x1) s#(a(x1)) -> o#(m(a(t(e(x1))))) -> o#(m(a(x1))) -> t#(e(n(x1))) s#(a(x1)) -> o#(m(a(t(e(x1))))) -> o#(m(a(x1))) -> n#(x1) s#(a(x1)) -> a#(t(e(x1))) -> a#(l(x1)) -> a#(t(x1)) s#(a(x1)) -> a#(t(e(x1))) -> a#(l(x1)) -> t#(x1) s#(a(x1)) -> a#(t(o(m(a(t(e(x1))))))) -> a#(l(x1)) -> a#(t(x1)) s#(a(x1)) -> a#(t(o(m(a(t(e(x1))))))) -> a#(l(x1)) -> t#(x1) s#(a(x1)) -> t#(e(x1)) -> t#(e(x1)) -> n#(s(x1)) s#(a(x1)) -> t#(e(x1)) -> t#(e(x1)) -> s#(x1) s#(a(x1)) -> t#(e(x1)) -> t#(o(x1)) -> a#(x1) s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) -> t#(e(x1)) -> n#(s(x1)) s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) -> t#(e(x1)) -> s#(x1) s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) -> t#(o(x1)) -> a#(x1) a#(l(x1)) -> a#(t(x1)) -> a#(l(x1)) -> a#(t(x1)) a#(l(x1)) -> a#(t(x1)) -> a#(l(x1)) -> t#(x1) a#(l(x1)) -> t#(x1) -> t#(e(x1)) -> n#(s(x1)) a#(l(x1)) -> t#(x1) -> t#(e(x1)) -> s#(x1) a#(l(x1)) -> t#(x1) -> t#(o(x1)) -> a#(x1) t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> a#(l(a(t(x1)))) t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> a#(t(x1)) t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> t#(x1) t#(e(x1)) -> s#(x1) -> s#(a(x1)) -> a#(t(o(m(a(t(e(x1))))))) t#(e(x1)) -> s#(x1) -> s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) t#(e(x1)) -> s#(x1) -> s#(a(x1)) -> o#(m(a(t(e(x1))))) t#(e(x1)) -> s#(x1) -> s#(a(x1)) -> a#(t(e(x1))) t#(e(x1)) -> s#(x1) -> s#(a(x1)) -> t#(e(x1)) t#(o(x1)) -> a#(x1) -> a#(l(x1)) -> a#(t(x1)) t#(o(x1)) -> a#(x1) -> a#(l(x1)) -> t#(x1) EDG Processor: DPs: t#(o(x1)) -> a#(x1) t#(e(x1)) -> s#(x1) t#(e(x1)) -> n#(s(x1)) a#(l(x1)) -> t#(x1) a#(l(x1)) -> a#(t(x1)) o#(m(a(x1))) -> n#(x1) o#(m(a(x1))) -> t#(e(n(x1))) s#(a(x1)) -> t#(e(x1)) s#(a(x1)) -> a#(t(e(x1))) s#(a(x1)) -> o#(m(a(t(e(x1))))) s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) s#(a(x1)) -> a#(t(o(m(a(t(e(x1))))))) n#(s(x1)) -> t#(x1) n#(s(x1)) -> a#(t(x1)) n#(s(x1)) -> a#(l(a(t(x1)))) TRS: t(o(x1)) -> m(a(x1)) t(e(x1)) -> n(s(x1)) a(l(x1)) -> a(t(x1)) o(m(a(x1))) -> t(e(n(x1))) s(a(x1)) -> l(a(t(o(m(a(t(e(x1)))))))) n(s(x1)) -> a(l(a(t(x1)))) graph: o#(m(a(x1))) -> n#(x1) -> n#(s(x1)) -> t#(x1) o#(m(a(x1))) -> n#(x1) -> n#(s(x1)) -> a#(t(x1)) o#(m(a(x1))) -> n#(x1) -> n#(s(x1)) -> a#(l(a(t(x1)))) o#(m(a(x1))) -> t#(e(n(x1))) -> t#(e(x1)) -> s#(x1) o#(m(a(x1))) -> t#(e(n(x1))) -> t#(e(x1)) -> n#(s(x1)) n#(s(x1)) -> a#(l(a(t(x1)))) -> a#(l(x1)) -> t#(x1) n#(s(x1)) -> a#(l(a(t(x1)))) -> a#(l(x1)) -> a#(t(x1)) n#(s(x1)) -> a#(t(x1)) -> a#(l(x1)) -> t#(x1) n#(s(x1)) -> a#(t(x1)) -> a#(l(x1)) -> a#(t(x1)) n#(s(x1)) -> t#(x1) -> t#(o(x1)) -> a#(x1) n#(s(x1)) -> t#(x1) -> t#(e(x1)) -> s#(x1) n#(s(x1)) -> t#(x1) -> t#(e(x1)) -> n#(s(x1)) s#(a(x1)) -> o#(m(a(t(e(x1))))) -> o#(m(a(x1))) -> n#(x1) s#(a(x1)) -> o#(m(a(t(e(x1))))) -> o#(m(a(x1))) -> t#(e(n(x1))) s#(a(x1)) -> a#(t(e(x1))) -> a#(l(x1)) -> t#(x1) s#(a(x1)) -> a#(t(e(x1))) -> a#(l(x1)) -> a#(t(x1)) s#(a(x1)) -> a#(t(o(m(a(t(e(x1))))))) -> a#(l(x1)) -> t#(x1) s#(a(x1)) -> a#(t(o(m(a(t(e(x1))))))) -> a#(l(x1)) -> a#(t(x1)) s#(a(x1)) -> t#(e(x1)) -> t#(e(x1)) -> s#(x1) s#(a(x1)) -> t#(e(x1)) -> t#(e(x1)) -> n#(s(x1)) s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) -> t#(o(x1)) -> a#(x1) a#(l(x1)) -> a#(t(x1)) -> a#(l(x1)) -> t#(x1) a#(l(x1)) -> a#(t(x1)) -> a#(l(x1)) -> a#(t(x1)) a#(l(x1)) -> t#(x1) -> t#(o(x1)) -> a#(x1) a#(l(x1)) -> t#(x1) -> t#(e(x1)) -> s#(x1) a#(l(x1)) -> t#(x1) -> t#(e(x1)) -> n#(s(x1)) t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> t#(x1) t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> a#(t(x1)) t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> a#(l(a(t(x1)))) t#(e(x1)) -> s#(x1) -> s#(a(x1)) -> t#(e(x1)) t#(e(x1)) -> s#(x1) -> s#(a(x1)) -> a#(t(e(x1))) t#(e(x1)) -> s#(x1) -> s#(a(x1)) -> o#(m(a(t(e(x1))))) t#(e(x1)) -> s#(x1) -> s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) t#(e(x1)) -> s#(x1) -> s#(a(x1)) -> a#(t(o(m(a(t(e(x1))))))) t#(o(x1)) -> a#(x1) -> a#(l(x1)) -> t#(x1) t#(o(x1)) -> a#(x1) -> a#(l(x1)) -> a#(t(x1)) CDG Processor: DPs: t#(o(x1)) -> a#(x1) t#(e(x1)) -> s#(x1) t#(e(x1)) -> n#(s(x1)) a#(l(x1)) -> t#(x1) a#(l(x1)) -> a#(t(x1)) o#(m(a(x1))) -> n#(x1) o#(m(a(x1))) -> t#(e(n(x1))) s#(a(x1)) -> t#(e(x1)) s#(a(x1)) -> a#(t(e(x1))) s#(a(x1)) -> o#(m(a(t(e(x1))))) s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) s#(a(x1)) -> a#(t(o(m(a(t(e(x1))))))) n#(s(x1)) -> t#(x1) n#(s(x1)) -> a#(t(x1)) n#(s(x1)) -> a#(l(a(t(x1)))) TRS: t(o(x1)) -> m(a(x1)) t(e(x1)) -> n(s(x1)) a(l(x1)) -> a(t(x1)) o(m(a(x1))) -> t(e(n(x1))) s(a(x1)) -> l(a(t(o(m(a(t(e(x1)))))))) n(s(x1)) -> a(l(a(t(x1)))) graph: o#(m(a(x1))) -> n#(x1) -> n#(s(x1)) -> a#(l(a(t(x1)))) o#(m(a(x1))) -> n#(x1) -> n#(s(x1)) -> a#(t(x1)) o#(m(a(x1))) -> n#(x1) -> n#(s(x1)) -> t#(x1) o#(m(a(x1))) -> t#(e(n(x1))) -> t#(e(x1)) -> n#(s(x1)) o#(m(a(x1))) -> t#(e(n(x1))) -> t#(e(x1)) -> s#(x1) n#(s(x1)) -> a#(l(a(t(x1)))) -> a#(l(x1)) -> a#(t(x1)) n#(s(x1)) -> a#(l(a(t(x1)))) -> a#(l(x1)) -> t#(x1) n#(s(x1)) -> t#(x1) -> t#(e(x1)) -> n#(s(x1)) n#(s(x1)) -> t#(x1) -> t#(e(x1)) -> s#(x1) n#(s(x1)) -> t#(x1) -> t#(o(x1)) -> a#(x1) s#(a(x1)) -> o#(m(a(t(e(x1))))) -> o#(m(a(x1))) -> t#(e(n(x1))) s#(a(x1)) -> o#(m(a(t(e(x1))))) -> o#(m(a(x1))) -> n#(x1) s#(a(x1)) -> t#(e(x1)) -> t#(e(x1)) -> n#(s(x1)) s#(a(x1)) -> t#(e(x1)) -> t#(e(x1)) -> s#(x1) s#(a(x1)) -> t#(o(m(a(t(e(x1)))))) -> t#(o(x1)) -> a#(x1) a#(l(x1)) -> t#(x1) -> t#(e(x1)) -> n#(s(x1)) a#(l(x1)) -> t#(x1) -> t#(e(x1)) -> s#(x1) a#(l(x1)) -> t#(x1) -> t#(o(x1)) -> a#(x1) t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> a#(l(a(t(x1)))) t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> a#(t(x1)) t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> t#(x1) t#(o(x1)) -> a#(x1) -> a#(l(x1)) -> a#(t(x1)) t#(o(x1)) -> a#(x1) -> a#(l(x1)) -> t#(x1) SCC Processor: #sccs: 1 #rules: 5 #arcs: 23/225 DPs: n#(s(x1)) -> t#(x1) t#(o(x1)) -> a#(x1) a#(l(x1)) -> t#(x1) t#(e(x1)) -> n#(s(x1)) n#(s(x1)) -> a#(l(a(t(x1)))) TRS: t(o(x1)) -> m(a(x1)) t(e(x1)) -> n(s(x1)) a(l(x1)) -> a(t(x1)) o(m(a(x1))) -> t(e(n(x1))) s(a(x1)) -> l(a(t(o(m(a(t(e(x1)))))))) n(s(x1)) -> a(l(a(t(x1)))) Arctic Interpretation Processor: dimension: 1 interpretation: [n#](x0) = -4x0 + 0, [a#](x0) = x0 + -15, [t#](x0) = x0, [l](x0) = 1x0 + 0, [n](x0) = -4x0 + 1, [s](x0) = 6x0 + 11, [e](x0) = 3x0 + 8, [m](x0) = -9x0 + 0, [a](x0) = x0, [t](x0) = x0, [o](x0) = 9x0 + 4 orientation: n#(s(x1)) = 2x1 + 7 >= x1 = t#(x1) t#(o(x1)) = 9x1 + 4 >= x1 + -15 = a#(x1) a#(l(x1)) = 1x1 + 0 >= x1 = t#(x1) t#(e(x1)) = 3x1 + 8 >= 2x1 + 7 = n#(s(x1)) n#(s(x1)) = 2x1 + 7 >= 1x1 + 0 = a#(l(a(t(x1)))) t(o(x1)) = 9x1 + 4 >= -9x1 + 0 = m(a(x1)) t(e(x1)) = 3x1 + 8 >= 2x1 + 7 = n(s(x1)) a(l(x1)) = 1x1 + 0 >= x1 = a(t(x1)) o(m(a(x1))) = x1 + 9 >= -1x1 + 8 = t(e(n(x1))) s(a(x1)) = 6x1 + 11 >= 4x1 + 10 = l(a(t(o(m(a(t(e(x1)))))))) n(s(x1)) = 2x1 + 7 >= 1x1 + 0 = a(l(a(t(x1)))) problem: DPs: TRS: t(o(x1)) -> m(a(x1)) t(e(x1)) -> n(s(x1)) a(l(x1)) -> a(t(x1)) o(m(a(x1))) -> t(e(n(x1))) s(a(x1)) -> l(a(t(o(m(a(t(e(x1)))))))) n(s(x1)) -> a(l(a(t(x1)))) Qed