YES Problem: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(a(x1)))) -> a(a(l(c(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(a(x1)))) -> c#(r(x1)) l#(r(a(a(x1)))) -> c#(c(r(x1))) l#(r(a(a(x1)))) -> c#(c(c(r(x1)))) l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) l#(r(a(a(x1)))) -> a#(a(l(c(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(a(x1)))) -> a(a(l(c(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(a(x1)))) -> c#(r(x1)) l#(r(a(a(x1)))) -> c#(c(r(x1))) l#(r(a(a(x1)))) -> c#(c(c(r(x1)))) l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) l#(r(a(a(x1)))) -> a#(a(l(c(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(a(x1)))) -> a(a(l(c(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(a(x1)))) -> c#(r(x1)) -> c#(a(r(x1))) -> a#(x1) l#(r(a(a(x1)))) -> c#(c(r(x1))) -> c#(a(r(x1))) -> a#(x1) l#(r(a(a(x1)))) -> c#(c(c(r(x1)))) -> c#(a(r(x1))) -> a#(x1) l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) -> l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) -> l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) -> l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) -> l#(r(a(a(x1)))) -> c#(c(c(r(x1)))) l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) -> l#(r(a(a(x1)))) -> c#(c(r(x1))) l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) -> l#(r(a(a(x1)))) -> c#(r(x1)) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(c(x1)) -> c#(a(x1)) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(c(x1)) -> a#(x1) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(l(x1)) -> a#(x1) l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) -> a#(c(x1)) -> c#(a(x1)) l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) -> a#(c(x1)) -> a#(x1) l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) -> a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(l(c(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(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> c#(c(c(r(x1)))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> c#(c(r(x1))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(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(a(x1)))) -> c#(r(x1)) l#(r(a(a(x1)))) -> c#(c(r(x1))) l#(r(a(a(x1)))) -> c#(c(c(r(x1)))) l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) l#(r(a(a(x1)))) -> a#(a(l(c(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(a(x1)))) -> a(a(l(c(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(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(l(x1)) -> a#(x1) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(c(x1)) -> a#(x1) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(c(x1)) -> c#(a(x1)) l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) -> a#(l(x1)) -> a#(x1) l#(r(a(a(x1)))) -> a#(l(c(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(a(x1)))) -> c#(r(x1)) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> c#(c(r(x1))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> c#(c(c(r(x1)))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> l#(c(c(c(r(x1))))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> a#(a(l(c(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: 7 #arcs: 25/121 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(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) a#(l(x1)) -> a#(x1) l#(r(a(a(x1)))) -> a#(l(c(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(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) Arctic Interpretation Processor: dimension: 1 interpretation: [c#](x0) = x0 + 0, [l#](x0) = 8x0 + 0, [a#](x0) = 4x0 + 0, [r](x0) = 8x0 + 0, [c](x0) = x0 + 8, [a](x0) = x0 + 0, [l](x0) = 4x0 + 8 orientation: c#(a(r(x1))) = 8x1 + 0 >= 4x1 + 0 = a#(x1) a#(c(x1)) = 4x1 + 12 >= x1 + 0 = c#(a(x1)) a#(c(x1)) = 4x1 + 12 >= 4x1 + 0 = a#(x1) a#(l(x1)) = 8x1 + 12 >= 8x1 + 8 = l#(a(x1)) l#(r(a(a(x1)))) = 16x1 + 16 >= 16x1 + 16 = a#(a(l(c(c(c(r(x1))))))) a#(l(x1)) = 8x1 + 12 >= 4x1 + 0 = a#(x1) l#(r(a(a(x1)))) = 16x1 + 16 >= 16x1 + 16 = a#(l(c(c(c(r(x1)))))) a(l(x1)) = 4x1 + 8 >= 4x1 + 8 = l(a(x1)) a(c(x1)) = x1 + 8 >= x1 + 8 = c(a(x1)) c(a(r(x1))) = 8x1 + 8 >= 8x1 + 8 = r(a(x1)) l(r(a(a(x1)))) = 12x1 + 12 >= 12x1 + 12 = a(a(l(c(c(c(r(x1))))))) problem: DPs: c#(a(r(x1))) -> a#(x1) a#(c(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) l#(r(a(a(x1)))) -> a#(l(c(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(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) EDG Processor: DPs: c#(a(r(x1))) -> a#(x1) a#(c(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) l#(r(a(a(x1)))) -> a#(l(c(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(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) graph: 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(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(c(x1)) -> a#(x1) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) -> a#(l(x1)) -> l#(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(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) CDG Processor: DPs: c#(a(r(x1))) -> a#(x1) a#(c(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) l#(r(a(a(x1)))) -> a#(l(c(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(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) graph: c#(a(r(x1))) -> a#(x1) -> a#(l(x1)) -> l#(a(x1)) c#(a(r(x1))) -> a#(x1) -> a#(c(x1)) -> a#(x1) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) -> a#(l(x1)) -> l#(a(x1)) a#(c(x1)) -> a#(x1) -> a#(l(x1)) -> l#(a(x1)) a#(c(x1)) -> a#(x1) -> a#(c(x1)) -> a#(x1) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> a#(l(c(c(c(r(x1)))))) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) SCC Processor: #sccs: 2 #rules: 4 #arcs: 8/25 DPs: a#(c(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(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) Arctic Interpretation Processor: dimension: 1 interpretation: [a#](x0) = 14x0, [r](x0) = 0, [c](x0) = 2x0 + 8, [a](x0) = x0 + 0, [l](x0) = 0 orientation: a#(c(x1)) = 16x1 + 22 >= 14x1 = a#(x1) a(l(x1)) = 0 >= 0 = l(a(x1)) a(c(x1)) = 2x1 + 8 >= 2x1 + 8 = c(a(x1)) c(a(r(x1))) = 8 >= 0 = r(a(x1)) l(r(a(a(x1)))) = 0 >= 0 = a(a(l(c(c(c(r(x1))))))) problem: DPs: TRS: a(l(x1)) -> l(a(x1)) a(c(x1)) -> c(a(x1)) c(a(r(x1))) -> r(a(x1)) l(r(a(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) Qed DPs: a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) l#(r(a(a(x1)))) -> a#(l(c(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(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) Arctic Interpretation Processor: dimension: 1 interpretation: [l#](x0) = x0 + 0, [a#](x0) = x0 + 0, [r](x0) = 4x0 + 0, [c](x0) = x0 + 0, [a](x0) = 4x0 + 0, [l](x0) = 4x0 + 0 orientation: a#(l(x1)) = 4x1 + 0 >= 4x1 + 0 = l#(a(x1)) l#(r(a(a(x1)))) = 12x1 + 8 >= 12x1 + 8 = a#(a(l(c(c(c(r(x1))))))) l#(r(a(a(x1)))) = 12x1 + 8 >= 8x1 + 4 = a#(l(c(c(c(r(x1)))))) a(l(x1)) = 8x1 + 4 >= 8x1 + 4 = l(a(x1)) a(c(x1)) = 4x1 + 4 >= 4x1 + 0 = c(a(x1)) c(a(r(x1))) = 8x1 + 4 >= 8x1 + 4 = r(a(x1)) l(r(a(a(x1)))) = 16x1 + 12 >= 16x1 + 12 = a(a(l(c(c(c(r(x1))))))) problem: DPs: a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(a(l(c(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(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) EDG Processor: DPs: a#(l(x1)) -> l#(a(x1)) l#(r(a(a(x1)))) -> a#(a(l(c(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(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) graph: l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) -> a#(l(x1)) -> l#(a(x1)) a#(l(x1)) -> l#(a(x1)) -> l#(r(a(a(x1)))) -> a#(a(l(c(c(c(r(x1))))))) Matrix Interpretation Processor: dim=1 interpretation: [l#](x0) = 5/2x0, [a#](x0) = 6x0, [r](x0) = 2, [c](x0) = 1/2x0, [a](x0) = 2x0, [l](x0) = x0 orientation: a#(l(x1)) = 6x1 >= 5x1 = l#(a(x1)) l#(r(a(a(x1)))) = 5 >= 3 = a#(a(l(c(c(c(r(x1))))))) a(l(x1)) = 2x1 >= 2x1 = l(a(x1)) a(c(x1)) = x1 >= x1 = c(a(x1)) c(a(r(x1))) = 2 >= 2 = r(a(x1)) l(r(a(a(x1)))) = 2 >= 1 = a(a(l(c(c(c(r(x1))))))) problem: DPs: a#(l(x1)) -> l#(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(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) EDG Processor: DPs: a#(l(x1)) -> l#(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(a(x1)))) -> a(a(l(c(c(c(r(x1))))))) graph: Qed