YES Problem: a(a(d(d(x1)))) -> d(d(b(b(x1)))) a(a(x1)) -> b(b(b(b(b(b(x1)))))) b(b(d(d(b(b(x1)))))) -> a(a(c(c(x1)))) c(c(x1)) -> d(d(x1)) Proof: DP Processor: DPs: a#(a(d(d(x1)))) -> b#(x1) a#(a(d(d(x1)))) -> b#(b(x1)) a#(a(x1)) -> b#(x1) a#(a(x1)) -> b#(b(x1)) a#(a(x1)) -> b#(b(b(x1))) a#(a(x1)) -> b#(b(b(b(x1)))) a#(a(x1)) -> b#(b(b(b(b(x1))))) a#(a(x1)) -> b#(b(b(b(b(b(x1)))))) b#(b(d(d(b(b(x1)))))) -> c#(x1) b#(b(d(d(b(b(x1)))))) -> c#(c(x1)) b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) TRS: a(a(d(d(x1)))) -> d(d(b(b(x1)))) a(a(x1)) -> b(b(b(b(b(b(x1)))))) b(b(d(d(b(b(x1)))))) -> a(a(c(c(x1)))) c(c(x1)) -> d(d(x1)) TDG Processor: DPs: a#(a(d(d(x1)))) -> b#(x1) a#(a(d(d(x1)))) -> b#(b(x1)) a#(a(x1)) -> b#(x1) a#(a(x1)) -> b#(b(x1)) a#(a(x1)) -> b#(b(b(x1))) a#(a(x1)) -> b#(b(b(b(x1)))) a#(a(x1)) -> b#(b(b(b(b(x1))))) a#(a(x1)) -> b#(b(b(b(b(b(x1)))))) b#(b(d(d(b(b(x1)))))) -> c#(x1) b#(b(d(d(b(b(x1)))))) -> c#(c(x1)) b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) TRS: a(a(d(d(x1)))) -> d(d(b(b(x1)))) a(a(x1)) -> b(b(b(b(b(b(x1)))))) b(b(d(d(b(b(x1)))))) -> a(a(c(c(x1)))) c(c(x1)) -> d(d(x1)) graph: b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) -> a#(a(x1)) -> b#(b(b(b(b(b(x1)))))) b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) -> a#(a(x1)) -> b#(b(b(b(b(x1))))) b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) -> a#(a(x1)) -> b#(b(b(b(x1)))) b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) -> a#(a(x1)) -> b#(b(b(x1))) b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) -> a#(a(x1)) -> b#(b(x1)) b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) -> a#(a(x1)) -> b#(x1) b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) -> a#(a(d(d(x1)))) -> b#(b(x1)) b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) -> a#(a(d(d(x1)))) -> b#(x1) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) -> a#(a(x1)) -> b#(b(b(b(b(b(x1)))))) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) -> a#(a(x1)) -> b#(b(b(b(b(x1))))) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) -> a#(a(x1)) -> b#(b(b(b(x1)))) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) -> a#(a(x1)) -> b#(b(b(x1))) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) -> a#(a(x1)) -> b#(b(x1)) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) -> a#(a(x1)) -> b#(x1) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) -> a#(a(d(d(x1)))) -> b#(b(x1)) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) -> a#(a(d(d(x1)))) -> b#(x1) a#(a(d(d(x1)))) -> b#(b(x1)) -> b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) a#(a(d(d(x1)))) -> b#(b(x1)) -> b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) a#(a(d(d(x1)))) -> b#(b(x1)) -> b#(b(d(d(b(b(x1)))))) -> c#(c(x1)) a#(a(d(d(x1)))) -> b#(b(x1)) -> b#(b(d(d(b(b(x1)))))) -> c#(x1) a#(a(d(d(x1)))) -> b#(x1) -> b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) a#(a(d(d(x1)))) -> b#(x1) -> b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) a#(a(d(d(x1)))) -> b#(x1) -> b#(b(d(d(b(b(x1)))))) -> c#(c(x1)) a#(a(d(d(x1)))) -> b#(x1) -> b#(b(d(d(b(b(x1)))))) -> c#(x1) a#(a(x1)) -> b#(b(b(b(b(b(x1)))))) -> b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) a#(a(x1)) -> b#(b(b(b(b(b(x1)))))) -> b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) a#(a(x1)) -> b#(b(b(b(b(b(x1)))))) -> b#(b(d(d(b(b(x1)))))) -> c#(c(x1)) a#(a(x1)) -> b#(b(b(b(b(b(x1)))))) -> b#(b(d(d(b(b(x1)))))) -> c#(x1) a#(a(x1)) -> b#(b(b(b(b(x1))))) -> b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) a#(a(x1)) -> b#(b(b(b(b(x1))))) -> b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) a#(a(x1)) -> b#(b(b(b(b(x1))))) -> b#(b(d(d(b(b(x1)))))) -> c#(c(x1)) a#(a(x1)) -> b#(b(b(b(b(x1))))) -> b#(b(d(d(b(b(x1)))))) -> c#(x1) a#(a(x1)) -> b#(b(b(b(x1)))) -> b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) a#(a(x1)) -> b#(b(b(b(x1)))) -> b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) a#(a(x1)) -> b#(b(b(b(x1)))) -> b#(b(d(d(b(b(x1)))))) -> c#(c(x1)) a#(a(x1)) -> b#(b(b(b(x1)))) -> b#(b(d(d(b(b(x1)))))) -> c#(x1) a#(a(x1)) -> b#(b(b(x1))) -> b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) a#(a(x1)) -> b#(b(b(x1))) -> b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) a#(a(x1)) -> b#(b(b(x1))) -> b#(b(d(d(b(b(x1)))))) -> c#(c(x1)) a#(a(x1)) -> b#(b(b(x1))) -> b#(b(d(d(b(b(x1)))))) -> c#(x1) a#(a(x1)) -> b#(b(x1)) -> b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) a#(a(x1)) -> b#(b(x1)) -> b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) a#(a(x1)) -> b#(b(x1)) -> b#(b(d(d(b(b(x1)))))) -> c#(c(x1)) a#(a(x1)) -> b#(b(x1)) -> b#(b(d(d(b(b(x1)))))) -> c#(x1) a#(a(x1)) -> b#(x1) -> b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) a#(a(x1)) -> b#(x1) -> b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) a#(a(x1)) -> b#(x1) -> b#(b(d(d(b(b(x1)))))) -> c#(c(x1)) a#(a(x1)) -> b#(x1) -> b#(b(d(d(b(b(x1)))))) -> c#(x1) SCC Processor: #sccs: 1 #rules: 10 #arcs: 48/144 DPs: b#(b(d(d(b(b(x1)))))) -> a#(c(c(x1))) a#(a(d(d(x1)))) -> b#(x1) b#(b(d(d(b(b(x1)))))) -> a#(a(c(c(x1)))) a#(a(d(d(x1)))) -> b#(b(x1)) a#(a(x1)) -> b#(x1) a#(a(x1)) -> b#(b(x1)) a#(a(x1)) -> b#(b(b(x1))) a#(a(x1)) -> b#(b(b(b(x1)))) a#(a(x1)) -> b#(b(b(b(b(x1))))) a#(a(x1)) -> b#(b(b(b(b(b(x1)))))) TRS: a(a(d(d(x1)))) -> d(d(b(b(x1)))) a(a(x1)) -> b(b(b(b(b(b(x1)))))) b(b(d(d(b(b(x1)))))) -> a(a(c(c(x1)))) c(c(x1)) -> d(d(x1)) Matrix Interpretation Processor: dim=1 interpretation: [b#](x0) = x0, [a#](x0) = x0 + 1, [c](x0) = 4x0 + 2, [b](x0) = x0 + 1, [a](x0) = x0 + 16, [d](x0) = 4x0 + 2 orientation: b#(b(d(d(b(b(x1)))))) = 16x1 + 43 >= 16x1 + 11 = a#(c(c(x1))) a#(a(d(d(x1)))) = 16x1 + 27 >= x1 = b#(x1) b#(b(d(d(b(b(x1)))))) = 16x1 + 43 >= 16x1 + 27 = a#(a(c(c(x1)))) a#(a(d(d(x1)))) = 16x1 + 27 >= x1 + 1 = b#(b(x1)) a#(a(x1)) = x1 + 17 >= x1 = b#(x1) a#(a(x1)) = x1 + 17 >= x1 + 1 = b#(b(x1)) a#(a(x1)) = x1 + 17 >= x1 + 2 = b#(b(b(x1))) a#(a(x1)) = x1 + 17 >= x1 + 3 = b#(b(b(b(x1)))) a#(a(x1)) = x1 + 17 >= x1 + 4 = b#(b(b(b(b(x1))))) a#(a(x1)) = x1 + 17 >= x1 + 5 = b#(b(b(b(b(b(x1)))))) a(a(d(d(x1)))) = 16x1 + 42 >= 16x1 + 42 = d(d(b(b(x1)))) a(a(x1)) = x1 + 32 >= x1 + 6 = b(b(b(b(b(b(x1)))))) b(b(d(d(b(b(x1)))))) = 16x1 + 44 >= 16x1 + 42 = a(a(c(c(x1)))) c(c(x1)) = 16x1 + 10 >= 16x1 + 10 = d(d(x1)) problem: DPs: TRS: a(a(d(d(x1)))) -> d(d(b(b(x1)))) a(a(x1)) -> b(b(b(b(b(b(x1)))))) b(b(d(d(b(b(x1)))))) -> a(a(c(c(x1)))) c(c(x1)) -> d(d(x1)) Qed