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) = x0 + 0, [a#](x0) = x0 + 0, [t#](x0) = x0, [l](x0) = x0, [n](x0) = 0, [s](x0) = x0 + 4, [e](x0) = x0 + 14, [m](x0) = 0, [a](x0) = x0 + 0, [t](x0) = 0, [o](x0) = x0 + 0 orientation: n#(s(x1)) = x1 + 4 >= x1 = t#(x1) t#(o(x1)) = x1 + 0 >= x1 + 0 = a#(x1) a#(l(x1)) = x1 + 0 >= x1 = t#(x1) t#(e(x1)) = x1 + 14 >= x1 + 4 = n#(s(x1)) n#(s(x1)) = x1 + 4 >= 0 = a#(l(a(t(x1)))) t(o(x1)) = 0 >= 0 = m(a(x1)) t(e(x1)) = 0 >= 0 = n(s(x1)) a(l(x1)) = x1 + 0 >= 0 = a(t(x1)) o(m(a(x1))) = 0 >= 0 = t(e(n(x1))) s(a(x1)) = x1 + 4 >= 0 = l(a(t(o(m(a(t(e(x1)))))))) n(s(x1)) = 0 >= 0 = a(l(a(t(x1)))) problem: DPs: n#(s(x1)) -> t#(x1) t#(o(x1)) -> a#(x1) a#(l(x1)) -> t#(x1) t#(e(x1)) -> n#(s(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)))) EDG Processor: DPs: n#(s(x1)) -> t#(x1) t#(o(x1)) -> a#(x1) a#(l(x1)) -> t#(x1) t#(e(x1)) -> n#(s(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: n#(s(x1)) -> t#(x1) -> t#(o(x1)) -> a#(x1) n#(s(x1)) -> t#(x1) -> t#(e(x1)) -> n#(s(x1)) a#(l(x1)) -> t#(x1) -> t#(o(x1)) -> a#(x1) a#(l(x1)) -> t#(x1) -> t#(e(x1)) -> n#(s(x1)) t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> t#(x1) t#(o(x1)) -> a#(x1) -> a#(l(x1)) -> t#(x1) CDG Processor: DPs: n#(s(x1)) -> t#(x1) t#(o(x1)) -> a#(x1) a#(l(x1)) -> t#(x1) t#(e(x1)) -> n#(s(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: t#(e(x1)) -> n#(s(x1)) -> n#(s(x1)) -> t#(x1) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/16