YES Problem: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) Proof: DP Processor: DPs: a#(l(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) a#(c(x1)) -> a#(x1) a#(c(x1)) -> c#(a(x1)) c#(a(r(x1))) -> a#(x1) l#(r(a(x1))) -> c#(r(x1)) l#(r(a(x1))) -> c#(c(r(x1))) l#(r(a(x1))) -> l#(c(c(r(x1)))) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) TDG Processor: DPs: a#(l(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) a#(c(x1)) -> a#(x1) a#(c(x1)) -> c#(a(x1)) c#(a(r(x1))) -> a#(x1) l#(r(a(x1))) -> c#(r(x1)) l#(r(a(x1))) -> c#(c(r(x1))) l#(r(a(x1))) -> l#(c(c(r(x1)))) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) graph: c#(a(r(x1))) -> a#(x1) -> a#(c(x1)) -> c#(a(x1)) c#(a(r(x1))) -> a#(x1) -> a#(c(x1)) -> a#(x1) c#(a(r(x1))) -> a#(x1) -> a#(l(x1)) -> l#(a(x1)) c#(a(r(x1))) -> a#(x1) -> a#(l(x1)) -> a#(x1) l#(r(a(x1))) -> c#(r(x1)) -> c#(a(r(x1))) -> a#(x1) l#(r(a(x1))) -> c#(c(r(x1))) -> c#(a(r(x1))) -> a#(x1) l#(r(a(x1))) -> l#(c(c(r(x1)))) -> l#(r(a(x1))) -> a#(l(c(c(r(x1))))) l#(r(a(x1))) -> l#(c(c(r(x1)))) -> l#(r(a(x1))) -> l#(c(c(r(x1)))) l#(r(a(x1))) -> l#(c(c(r(x1)))) -> l#(r(a(x1))) -> c#(c(r(x1))) l#(r(a(x1))) -> l#(c(c(r(x1)))) -> l#(r(a(x1))) -> c#(r(x1)) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) -> a#(c(x1)) -> c#(a(x1)) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) -> a#(c(x1)) -> a#(x1) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) -> a#(l(x1)) -> l#(a(x1)) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) -> a#(l(x1)) -> a#(x1) a#(c(x1)) -> c#(a(x1)) -> c#(a(r(x1))) -> a#(x1) a#(c(x1)) -> a#(x1) -> a#(c(x1)) -> c#(a(x1)) a#(c(x1)) -> a#(x1) -> a#(c(x1)) -> a#(x1) a#(c(x1)) -> a#(x1) -> a#(l(x1)) -> l#(a(x1)) a#(c(x1)) -> a#(x1) -> a#(l(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(x1))) -> a#(l(c(c(r(x1))))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(x1))) -> l#(c(c(r(x1)))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(x1))) -> c#(c(r(x1))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(x1))) -> c#(r(x1)) a#(l(x1)) -> a#(x1) -> a#(c(x1)) -> c#(a(x1)) a#(l(x1)) -> a#(x1) -> a#(c(x1)) -> a#(x1) a#(l(x1)) -> a#(x1) -> a#(l(x1)) -> l#(a(x1)) a#(l(x1)) -> a#(x1) -> a#(l(x1)) -> a#(x1) EDG Processor: DPs: a#(l(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) a#(c(x1)) -> a#(x1) a#(c(x1)) -> c#(a(x1)) c#(a(r(x1))) -> a#(x1) l#(r(a(x1))) -> c#(r(x1)) l#(r(a(x1))) -> c#(c(r(x1))) l#(r(a(x1))) -> l#(c(c(r(x1)))) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) graph: c#(a(r(x1))) -> a#(x1) -> a#(l(x1)) -> a#(x1) c#(a(r(x1))) -> a#(x1) -> a#(l(x1)) -> l#(a(x1)) c#(a(r(x1))) -> a#(x1) -> a#(c(x1)) -> a#(x1) c#(a(r(x1))) -> a#(x1) -> a#(c(x1)) -> c#(a(x1)) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) -> a#(l(x1)) -> a#(x1) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) -> a#(l(x1)) -> l#(a(x1)) a#(c(x1)) -> c#(a(x1)) -> c#(a(r(x1))) -> a#(x1) a#(c(x1)) -> a#(x1) -> a#(l(x1)) -> a#(x1) a#(c(x1)) -> a#(x1) -> a#(l(x1)) -> l#(a(x1)) a#(c(x1)) -> a#(x1) -> a#(c(x1)) -> a#(x1) a#(c(x1)) -> a#(x1) -> a#(c(x1)) -> c#(a(x1)) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(x1))) -> c#(r(x1)) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(x1))) -> c#(c(r(x1))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(x1))) -> l#(c(c(r(x1)))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(x1))) -> a#(l(c(c(r(x1))))) a#(l(x1)) -> a#(x1) -> a#(l(x1)) -> a#(x1) a#(l(x1)) -> a#(x1) -> a#(l(x1)) -> l#(a(x1)) a#(l(x1)) -> a#(x1) -> a#(c(x1)) -> a#(x1) a#(l(x1)) -> a#(x1) -> a#(c(x1)) -> c#(a(x1)) SCC Processor: #sccs: 1 #rules: 6 #arcs: 19/81 DPs: c#(a(r(x1))) -> a#(x1) a#(c(x1)) -> c#(a(x1)) a#(c(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) a#(l(x1)) -> a#(x1) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) Arctic Interpretation Processor: dimension: 1 interpretation: [c#](x0) = x0 + -16, [l#](x0) = 4x0 + 0, [a#](x0) = x0, [r](x0) = x0 + -2, [c](x0) = x0 + -2, [a](x0) = x0 + -2, [l](x0) = 4x0 + 2 orientation: c#(a(r(x1))) = x1 + -2 >= x1 = a#(x1) a#(c(x1)) = x1 + -2 >= x1 + -2 = c#(a(x1)) a#(c(x1)) = x1 + -2 >= x1 = a#(x1) a#(l(x1)) = 4x1 + 2 >= 4x1 + 2 = l#(a(x1)) l#(r(a(x1))) = 4x1 + 2 >= 4x1 + 2 = a#(l(c(c(r(x1))))) a#(l(x1)) = 4x1 + 2 >= x1 = a#(x1) a(l(x1)) = 4x1 + 2 >= 4x1 + 2 = l(a(x1)) a(c(x1)) = x1 + -2 >= x1 + -2 = c(a(x1)) c(a(r(x1))) = x1 + -2 >= x1 + -2 = r(a(x1)) l(r(a(x1))) = 4x1 + 2 >= 4x1 + 2 = a(l(c(c(r(x1))))) problem: DPs: c#(a(r(x1))) -> a#(x1) a#(c(x1)) -> c#(a(x1)) a#(c(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) EDG Processor: DPs: c#(a(r(x1))) -> a#(x1) a#(c(x1)) -> c#(a(x1)) a#(c(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) graph: c#(a(r(x1))) -> a#(x1) -> a#(c(x1)) -> c#(a(x1)) c#(a(r(x1))) -> a#(x1) -> a#(c(x1)) -> a#(x1) c#(a(r(x1))) -> a#(x1) -> a#(l(x1)) -> l#(a(x1)) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) -> a#(l(x1)) -> l#(a(x1)) a#(c(x1)) -> c#(a(x1)) -> c#(a(r(x1))) -> a#(x1) a#(c(x1)) -> a#(x1) -> a#(c(x1)) -> c#(a(x1)) a#(c(x1)) -> a#(x1) -> a#(c(x1)) -> a#(x1) a#(c(x1)) -> a#(x1) -> a#(l(x1)) -> l#(a(x1)) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(x1))) -> a#(l(c(c(r(x1))))) SCC Processor: #sccs: 2 #rules: 5 #arcs: 9/25 DPs: c#(a(r(x1))) -> a#(x1) a#(c(x1)) -> a#(x1) a#(c(x1)) -> c#(a(x1)) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) Arctic Interpretation Processor: dimension: 1 interpretation: [c#](x0) = x0 + 0, [a#](x0) = x0 + -16, [r](x0) = 1x0, [c](x0) = x0 + 0, [a](x0) = x0, [l](x0) = x0 + 0 orientation: c#(a(r(x1))) = 1x1 + 0 >= x1 + -16 = a#(x1) a#(c(x1)) = x1 + 0 >= x1 + -16 = a#(x1) a#(c(x1)) = x1 + 0 >= x1 + 0 = c#(a(x1)) a(l(x1)) = x1 + 0 >= x1 + 0 = l(a(x1)) a(c(x1)) = x1 + 0 >= x1 + 0 = c(a(x1)) c(a(r(x1))) = 1x1 + 0 >= 1x1 = r(a(x1)) l(r(a(x1))) = 1x1 + 0 >= 1x1 + 0 = a(l(c(c(r(x1))))) problem: DPs: a#(c(x1)) -> a#(x1) a#(c(x1)) -> c#(a(x1)) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) EDG Processor: DPs: a#(c(x1)) -> a#(x1) a#(c(x1)) -> c#(a(x1)) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) graph: a#(c(x1)) -> a#(x1) -> a#(c(x1)) -> a#(x1) a#(c(x1)) -> a#(x1) -> a#(c(x1)) -> c#(a(x1)) CDG Processor: DPs: a#(c(x1)) -> a#(x1) a#(c(x1)) -> c#(a(x1)) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) graph: Qed DPs: a#(l(x1)) -> l#(a(x1)) l#(r(a(x1))) -> a#(l(c(c(r(x1))))) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) Matrix Interpretation Processor: dim=4 interpretation: [l#](x0) = [0 0 0 1]x0, [a#](x0) = [0 0 1 0]x0 + [1], [0 0 0 0] [0] [0 0 0 0] [0] [r](x0) = [0 0 0 0]x0 + [0] [1 1 0 1] [1], [0 0 0 1] [1 0 0 0] [c](x0) = [0 0 0 0]x0 [0 1 0 0] , [0 1 0 0] [0 0 0 1] [a](x0) = [0 1 0 0]x0 [1 0 0 0] , [1 1 0 1] [1 1 0 1] [l](x0) = [1 0 0 1]x0 [1 1 0 1] orientation: a#(l(x1)) = [1 0 0 1]x1 + [1] >= [1 0 0 0]x1 = l#(a(x1)) l#(r(a(x1))) = [1 1 0 1]x1 + [1] >= [1] = a#(l(c(c(r(x1))))) [1 1 0 1] [1 1 0 1] [1 1 0 1] [1 1 0 1] a(l(x1)) = [1 1 0 1]x1 >= [1 1 0 0]x1 = l(a(x1)) [1 1 0 1] [1 1 0 1] [1 0 0 0] [1 0 0 0] [0 1 0 0] [0 1 0 0] a(c(x1)) = [1 0 0 0]x1 >= [0 0 0 0]x1 = c(a(x1)) [0 0 0 1] [0 0 0 1] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] c(a(r(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = r(a(x1)) [1 1 0 1] [1] [1 1 0 1] [1] [1 1 0 1] [1] [1 1 0 1] [1] [1 1 0 1] [1] [1 1 0 1] [1] l(r(a(x1))) = [1 1 0 1]x1 + [1] >= [1 1 0 1]x1 + [1] = a(l(c(c(r(x1))))) [1 1 0 1] [1] [1 1 0 1] [1] problem: DPs: l#(r(a(x1))) -> a#(l(c(c(r(x1))))) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) EDG Processor: DPs: l#(r(a(x1))) -> a#(l(c(c(r(x1))))) TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(x1))) -> a(l(c(c(r(x1))))) graph: Qed