MAYBE Problem: a(0(),b(0(),x)) -> b(0(),a(0(),x)) a(0(),x) -> b(0(),b(0(),x)) a(0(),a(1(),a(x,y))) -> a(1(),a(0(),a(x,y))) b(0(),a(1(),a(x,y))) -> b(1(),a(0(),a(x,y))) a(0(),a(x,y)) -> a(1(),a(1(),a(x,y))) Proof: DP Processor: DPs: a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),x) -> b#(0(),x) a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) a#(0(),a(x,y)) -> a#(1(),a(x,y)) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) TRS: a(0(),b(0(),x)) -> b(0(),a(0(),x)) a(0(),x) -> b(0(),b(0(),x)) a(0(),a(1(),a(x,y))) -> a(1(),a(0(),a(x,y))) b(0(),a(1(),a(x,y))) -> b(1(),a(0(),a(x,y))) a(0(),a(x,y)) -> a(1(),a(1(),a(x,y))) TDG Processor: DPs: a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),x) -> b#(0(),x) a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) a#(0(),a(x,y)) -> a#(1(),a(x,y)) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) TRS: a(0(),b(0(),x)) -> b(0(),a(0(),x)) a(0(),x) -> b(0(),b(0(),x)) a(0(),a(1(),a(x,y))) -> a(1(),a(0(),a(x,y))) b(0(),a(1(),a(x,y))) -> b(1(),a(0(),a(x,y))) a(0(),a(x,y)) -> a(1(),a(1(),a(x,y))) graph: b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) -> b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) -> b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(x,y)) -> a#(1(),a(x,y)) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),x) -> b#(0(),b(0(),x)) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),x) -> b#(0(),x) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) -> a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) -> a#(0(),a(x,y)) -> a#(1(),a(x,y)) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) -> a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) -> a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) -> a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) -> a#(0(),x) -> b#(0(),x) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) -> a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) -> a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(x,y)) -> a#(1(),a(x,y)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),x) -> b#(0(),x) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(1(),a(x,y)) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) -> a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) -> a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) -> a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) -> a#(0(),x) -> b#(0(),x) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) -> a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) -> a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),a(x,y)) -> a#(1(),a(x,y)) -> a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) a#(0(),a(x,y)) -> a#(1(),a(x,y)) -> a#(0(),a(x,y)) -> a#(1(),a(x,y)) a#(0(),a(x,y)) -> a#(1(),a(x,y)) -> a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) a#(0(),a(x,y)) -> a#(1(),a(x,y)) -> a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),a(x,y)) -> a#(1(),a(x,y)) -> a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),a(x,y)) -> a#(1(),a(x,y)) -> a#(0(),x) -> b#(0(),x) a#(0(),a(x,y)) -> a#(1(),a(x,y)) -> a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),a(x,y)) -> a#(1(),a(x,y)) -> a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) -> b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) -> b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),a(x,y)) -> a#(1(),a(x,y)) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),x) -> b#(0(),x) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),x) -> b#(0(),b(0(),x)) -> b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) a#(0(),x) -> b#(0(),b(0(),x)) -> b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),x) -> b#(0(),x) -> b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) a#(0(),x) -> b#(0(),x) -> b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) EDG Processor: DPs: a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),x) -> b#(0(),x) a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) a#(0(),a(x,y)) -> a#(1(),a(x,y)) a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) TRS: a(0(),b(0(),x)) -> b(0(),a(0(),x)) a(0(),x) -> b(0(),b(0(),x)) a(0(),a(1(),a(x,y))) -> a(1(),a(0(),a(x,y))) b(0(),a(1(),a(x,y))) -> b(1(),a(0(),a(x,y))) a(0(),a(x,y)) -> a(1(),a(1(),a(x,y))) graph: b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),b(0(),x)) -> a#(0(),x) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),x) -> b#(0(),x) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),x) -> b#(0(),b(0(),x)) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(x,y)) -> a#(1(),a(x,y)) b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),x) -> b#(0(),x) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(x,y)) -> a#(1(),a(x,y)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) -> a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) -> b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) -> b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),b(0(),x)) -> a#(0(),x) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),x) -> b#(0(),x) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),a(1(),a(x,y))) -> a#(1(),a(0(),a(x,y))) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),a(x,y)) -> a#(1(),a(x,y)) a#(0(),b(0(),x)) -> a#(0(),x) -> a#(0(),a(x,y)) -> a#(1(),a(1(),a(x,y))) a#(0(),x) -> b#(0(),b(0(),x)) -> b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),x) -> b#(0(),b(0(),x)) -> b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) a#(0(),x) -> b#(0(),x) -> b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),x) -> b#(0(),x) -> b#(0(),a(1(),a(x,y))) -> b#(1(),a(0(),a(x,y))) SCC Processor: #sccs: 1 #rules: 6 #arcs: 30/100 DPs: b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),x) -> b#(0(),x) a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) a#(0(),b(0(),x)) -> a#(0(),x) TRS: a(0(),b(0(),x)) -> b(0(),a(0(),x)) a(0(),x) -> b(0(),b(0(),x)) a(0(),a(1(),a(x,y))) -> a(1(),a(0(),a(x,y))) b(0(),a(1(),a(x,y))) -> b(1(),a(0(),a(x,y))) a(0(),a(x,y)) -> a(1(),a(1(),a(x,y))) Matrix Interpretation Processor: dim=1 interpretation: [b#](x0, x1) = 2x0 + 2x1, [a#](x0, x1) = 4x0 + 2x1, [1] = 0, [a](x0, x1) = x0 + x1 + 1, [b](x0, x1) = x0 + x1, [0] = 1 orientation: b#(0(),a(1(),a(x,y))) = 2x + 2y + 6 >= 2x + 2y + 6 = a#(0(),a(x,y)) a#(0(),a(1(),a(x,y))) = 2x + 2y + 8 >= 2x + 2y + 6 = a#(0(),a(x,y)) a#(0(),x) = 2x + 4 >= 2x + 4 = b#(0(),b(0(),x)) a#(0(),x) = 2x + 4 >= 2x + 2 = b#(0(),x) a#(0(),b(0(),x)) = 2x + 6 >= 2x + 6 = b#(0(),a(0(),x)) a#(0(),b(0(),x)) = 2x + 6 >= 2x + 4 = a#(0(),x) a(0(),b(0(),x)) = x + 3 >= x + 3 = b(0(),a(0(),x)) a(0(),x) = x + 2 >= x + 2 = b(0(),b(0(),x)) a(0(),a(1(),a(x,y))) = x + y + 4 >= x + y + 4 = a(1(),a(0(),a(x,y))) b(0(),a(1(),a(x,y))) = x + y + 3 >= x + y + 3 = b(1(),a(0(),a(x,y))) a(0(),a(x,y)) = x + y + 3 >= x + y + 3 = a(1(),a(1(),a(x,y))) problem: DPs: b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),x) -> b#(0(),b(0(),x)) a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) TRS: a(0(),b(0(),x)) -> b(0(),a(0(),x)) a(0(),x) -> b(0(),b(0(),x)) a(0(),a(1(),a(x,y))) -> a(1(),a(0(),a(x,y))) b(0(),a(1(),a(x,y))) -> b(1(),a(0(),a(x,y))) a(0(),a(x,y)) -> a(1(),a(1(),a(x,y))) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0, x1) = x0 + x1 + -16, [a#](x0, x1) = -7x0 + -5x1 + 1, [1] = 0, [a](x0, x1) = 1, [b](x0, x1) = x0 + 0, [0] = 0 orientation: b#(0(),a(1(),a(x,y))) = 1 >= 1 = a#(0(),a(x,y)) a#(0(),x) = -5x + 1 >= 0 = b#(0(),b(0(),x)) a#(0(),b(0(),x)) = 1 >= 1 = b#(0(),a(0(),x)) a(0(),b(0(),x)) = 1 >= 0 = b(0(),a(0(),x)) a(0(),x) = 1 >= 0 = b(0(),b(0(),x)) a(0(),a(1(),a(x,y))) = 1 >= 1 = a(1(),a(0(),a(x,y))) b(0(),a(1(),a(x,y))) = 0 >= 0 = b(1(),a(0(),a(x,y))) a(0(),a(x,y)) = 1 >= 1 = a(1(),a(1(),a(x,y))) problem: DPs: b#(0(),a(1(),a(x,y))) -> a#(0(),a(x,y)) a#(0(),b(0(),x)) -> b#(0(),a(0(),x)) TRS: a(0(),b(0(),x)) -> b(0(),a(0(),x)) a(0(),x) -> b(0(),b(0(),x)) a(0(),a(1(),a(x,y))) -> a(1(),a(0(),a(x,y))) b(0(),a(1(),a(x,y))) -> b(1(),a(0(),a(x,y))) a(0(),a(x,y)) -> a(1(),a(1(),a(x,y))) Open