YES Problem: b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1))))))) Proof: DP Processor: DPs: b#(b(a(b(b(b(x1)))))) -> b#(a(x1)) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) TRS: b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1))))))) EDG Processor: DPs: b#(b(a(b(b(b(x1)))))) -> b#(a(x1)) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) TRS: b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1))))))) graph: b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) -> b#(b(a(b(b(b(x1)))))) -> b#(a(x1)) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) -> b#(b(a(b(b(b(x1)))))) -> b#(a(x1)) b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(a(x1)) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) -> b#(b(a(b(b(b(x1)))))) -> b#(a(x1)) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) CDG Processor: DPs: b#(b(a(b(b(b(x1)))))) -> b#(a(x1)) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) TRS: b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1))))))) graph: b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) -> b#(b(a(b(b(b(x1)))))) -> b#(a(x1)) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(a(x1)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 10/25 DPs: b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) TRS: b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1))))))) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = x0, [a](x0) = x0, [b](x0) = 4x0 orientation: b#(b(a(b(b(b(x1)))))) = 16x1 >= 4x1 = b#(b(a(x1))) b#(b(a(b(b(b(x1)))))) = 16x1 >= 12x1 = b#(b(b(b(a(x1))))) b(b(a(b(b(b(x1)))))) = 20x1 >= 20x1 = a(b(b(b(b(b(a(x1))))))) problem: DPs: TRS: b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1))))))) Qed