YES Problem: sq(0(x1)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1))))))))))))))))) sq(s(x1)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(0(x1)) -> p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1))))))))))))))))))))))))))) twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) 0(x1) -> x1 Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [twice](x0) = x0, [p](x0) = x0, [s](x0) = x0, [sq](x0) = x0, [0](x0) = 1x0 orientation: sq(0(x1)) = 1x1 >= 1x1 = p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1))))))))))))))))) sq(s(x1)) = x1 >= x1 = s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(0(x1)) = 1x1 >= 1x1 = p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1))))))))))))))))))))))))))) twice(s(x1)) = x1 >= x1 = p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) = x1 >= x1 = p(x1) p(s(x1)) = x1 >= x1 = x1 p(0(x1)) = 1x1 >= 1x1 = 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) 0(x1) = 1x1 >= x1 = x1 problem: sq(0(x1)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1))))))))))))))))) sq(s(x1)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(0(x1)) -> p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1))))))))))))))))))))))))))) twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) Arctic Interpretation Processor: dimension: 1 interpretation: [twice](x0) = x0, [p](x0) = x0, [s](x0) = x0, [sq](x0) = 2x0, [0](x0) = 2x0 orientation: sq(0(x1)) = 4x1 >= 2x1 = p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1))))))))))))))))) sq(s(x1)) = 2x1 >= 2x1 = s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(0(x1)) = 2x1 >= 2x1 = p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1))))))))))))))))))))))))))) twice(s(x1)) = x1 >= x1 = p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) = x1 >= x1 = p(x1) p(s(x1)) = x1 >= x1 = x1 p(0(x1)) = 2x1 >= 2x1 = 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) problem: sq(s(x1)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(0(x1)) -> p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1))))))))))))))))))))))))))) twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) String Reversal Processor: s(sq(x1)) -> s(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))))))))))))))) 0(twice(x1)) -> s(p(s(p(s(p(s(s(p(p(s(s(s(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1))))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(s(s(s(0(x1)))))))))))) Matrix Interpretation Processor: dim=2 interpretation: [1 0] [0] [twice](x0) = [2 1]x0 + [1], [p](x0) = x0, [s](x0) = x0, [1 0] [0] [sq](x0) = [0 0]x0 + [2], [1 1] [0] [0](x0) = [0 2]x0 + [2] orientation: [1 0] [0] [1 0] [0] s(sq(x1)) = [0 0]x1 + [2] >= [0 0]x1 + [2] = s(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))))))))))))))) [3 1] [1] [1 1] [0] 0(twice(x1)) = [4 2]x1 + [4] >= [0 2]x1 + [2] = s(p(s(p(s(p(s(s(p(p(s(s(s(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1))))))))))))))))))))))))))) [1 0] [0] [1 0] [0] s(twice(x1)) = [2 1]x1 + [1] >= [2 1]x1 + [1] = s(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1))))))))))))))) s(p(p(x1))) = x1 >= x1 = p(x1) s(p(x1)) = x1 >= x1 = x1 [1 1] [0] [1 1] [0] 0(p(x1)) = [0 2]x1 + [2] >= [0 2]x1 + [2] = s(s(s(s(s(s(s(s(s(s(s(0(x1)))))))))))) problem: s(sq(x1)) -> s(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(s(s(s(0(x1)))))))))))) String Reversal Processor: sq(s(x1)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) DP Processor: DPs: sq#(s(x1)) -> p#(s(s(s(s(s(s(x1))))))) sq#(s(x1)) -> p#(p(s(s(s(s(s(s(x1)))))))) sq#(s(x1)) -> p#(p(p(s(s(s(s(s(s(x1))))))))) sq#(s(x1)) -> p#(p(p(p(s(s(s(s(s(s(x1)))))))))) sq#(s(x1)) -> p#(p(p(p(p(s(s(s(s(s(s(x1))))))))))) sq#(s(x1)) -> p#(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) sq#(s(x1)) -> p#(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))) sq#(s(x1)) -> p#(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))) sq#(s(x1)) -> p#(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))) sq#(s(x1)) -> p#(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))) sq#(s(x1)) -> p#(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) sq#(s(x1)) -> p#(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))) sq#(s(x1)) -> p#(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))) sq#(s(x1)) -> p#(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))) sq#(s(x1)) -> p#(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))) twice#(s(x1)) -> p#(s(x1)) twice#(s(x1)) -> p#(s(p(s(x1)))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) twice#(s(x1)) -> p#(s(s(s(twice(p(s(p(s(x1))))))))) twice#(s(x1)) -> p#(p(s(s(s(twice(p(s(p(s(x1)))))))))) twice#(s(x1)) -> p#(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))) twice#(s(x1)) -> p#(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p#(p(s(x1))) -> p#(x1) TRS: sq(s(x1)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) TDG Processor: DPs: sq#(s(x1)) -> p#(s(s(s(s(s(s(x1))))))) sq#(s(x1)) -> p#(p(s(s(s(s(s(s(x1)))))))) sq#(s(x1)) -> p#(p(p(s(s(s(s(s(s(x1))))))))) sq#(s(x1)) -> p#(p(p(p(s(s(s(s(s(s(x1)))))))))) sq#(s(x1)) -> p#(p(p(p(p(s(s(s(s(s(s(x1))))))))))) sq#(s(x1)) -> p#(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) sq#(s(x1)) -> p#(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))) sq#(s(x1)) -> p#(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))) sq#(s(x1)) -> p#(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))) sq#(s(x1)) -> p#(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))) sq#(s(x1)) -> p#(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) sq#(s(x1)) -> p#(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))) sq#(s(x1)) -> p#(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))) sq#(s(x1)) -> p#(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))) sq#(s(x1)) -> p#(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))) twice#(s(x1)) -> p#(s(x1)) twice#(s(x1)) -> p#(s(p(s(x1)))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) twice#(s(x1)) -> p#(s(s(s(twice(p(s(p(s(x1))))))))) twice#(s(x1)) -> p#(p(s(s(s(twice(p(s(p(s(x1)))))))))) twice#(s(x1)) -> p#(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))) twice#(s(x1)) -> p#(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p#(p(s(x1))) -> p#(x1) TRS: sq(s(x1)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) graph: twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(p(s(s(s(twice(p(s(p(s(x1)))))))))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(s(s(s(twice(p(s(p(s(x1))))))))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> twice#(p(s(p(s(x1))))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(s(p(s(x1)))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(s(x1)) twice#(s(x1)) -> p#(p(s(s(s(twice(p(s(p(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) twice#(s(x1)) -> p#(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) -> p#(p(s(x1))) -> p#(x1) twice#(s(x1)) -> p#(s(p(s(x1)))) -> p#(p(s(x1))) -> p#(x1) twice#(s(x1)) -> p#(s(s(s(twice(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) twice#(s(x1)) -> p#(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))) -> p#(p(s(x1))) -> p#(x1) twice#(s(x1)) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(p(s(s(s(twice(p(s(p(s(x1)))))))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(s(s(s(twice(p(s(p(s(x1))))))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> twice#(p(s(p(s(x1))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(s(p(s(x1)))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(s(x1)) sq#(s(x1)) -> p#(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(p(p(p(s(s(s(s(s(s(x1))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(p(p(s(s(s(s(s(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(p(s(s(s(s(s(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(s(s(s(s(s(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(s(s(s(s(s(s(x1))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(p(p(p(s(s(s(s(s(s(x1))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(p(p(s(s(s(s(s(s(x1)))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(p(s(s(s(s(s(s(x1))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(s(s(s(s(s(s(x1)))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(s(s(s(s(s(x1))))))) EDG Processor: DPs: sq#(s(x1)) -> p#(s(s(s(s(s(s(x1))))))) sq#(s(x1)) -> p#(p(s(s(s(s(s(s(x1)))))))) sq#(s(x1)) -> p#(p(p(s(s(s(s(s(s(x1))))))))) sq#(s(x1)) -> p#(p(p(p(s(s(s(s(s(s(x1)))))))))) sq#(s(x1)) -> p#(p(p(p(p(s(s(s(s(s(s(x1))))))))))) sq#(s(x1)) -> p#(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) sq#(s(x1)) -> p#(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))) sq#(s(x1)) -> p#(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))) sq#(s(x1)) -> p#(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))) sq#(s(x1)) -> p#(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))) sq#(s(x1)) -> p#(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) sq#(s(x1)) -> p#(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))) sq#(s(x1)) -> p#(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))) sq#(s(x1)) -> p#(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))) sq#(s(x1)) -> p#(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))) twice#(s(x1)) -> p#(s(x1)) twice#(s(x1)) -> p#(s(p(s(x1)))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) twice#(s(x1)) -> p#(s(s(s(twice(p(s(p(s(x1))))))))) twice#(s(x1)) -> p#(p(s(s(s(twice(p(s(p(s(x1)))))))))) twice#(s(x1)) -> p#(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))) twice#(s(x1)) -> p#(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p#(p(s(x1))) -> p#(x1) TRS: sq(s(x1)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) graph: twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(s(x1)) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(s(p(s(x1)))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> twice#(p(s(p(s(x1))))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(s(s(s(twice(p(s(p(s(x1))))))))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(p(s(s(s(twice(p(s(p(s(x1)))))))))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))) twice#(s(x1)) -> twice#(p(s(p(s(x1))))) -> twice#(s(x1)) -> p#(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) twice#(s(x1)) -> p#(p(s(s(s(twice(p(s(p(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) twice#(s(x1)) -> p#(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) -> p#(p(s(x1))) -> p#(x1) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(s(x1)) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(s(p(s(x1)))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> twice#(p(s(p(s(x1))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(s(s(s(twice(p(s(p(s(x1))))))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(p(s(s(s(twice(p(s(p(s(x1)))))))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))) sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) -> twice#(s(x1)) -> p#(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) sq#(s(x1)) -> p#(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(p(p(p(s(s(s(s(s(s(x1))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(p(p(s(s(s(s(s(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(p(s(s(s(s(s(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(s(s(s(s(s(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> p#(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(s(s(s(s(s(x1))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(s(s(s(s(s(s(x1)))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(p(s(s(s(s(s(s(x1))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(p(p(s(s(s(s(s(s(x1)))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(p(p(p(s(s(s(s(s(s(x1))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> twice#(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))) sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) -> sq#(s(x1)) -> p#(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))) SCC Processor: #sccs: 3 #rules: 3 #arcs: 42/625 DPs: sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) TRS: sq(s(x1)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) Usable Rule Processor: DPs: sq#(s(x1)) -> sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) TRS: p(s(x1)) -> x1 p(p(s(x1))) -> p(x1) p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) Arctic Interpretation Processor: dimension: 1 usable rules: p(s(x1)) -> x1 p(p(s(x1))) -> p(x1) p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) interpretation: [sq#](x0) = 8x0 + 0, [p](x0) = -2x0 + 8, [s](x0) = 2x0 + 9, [0](x0) = 0 orientation: sq#(s(x1)) = 10x1 + 17 >= 8x1 + 16 = sq#(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))) p(s(x1)) = x1 + 8 >= x1 = x1 p(p(s(x1))) = -2x1 + 8 >= -2x1 + 8 = p(x1) p(0(x1)) = 8 >= 0 = 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) problem: DPs: TRS: p(s(x1)) -> x1 p(p(s(x1))) -> p(x1) p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) Qed DPs: twice#(s(x1)) -> twice#(p(s(p(s(x1))))) TRS: sq(s(x1)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) Usable Rule Processor: DPs: twice#(s(x1)) -> twice#(p(s(p(s(x1))))) TRS: p(s(x1)) -> x1 Arctic Interpretation Processor: dimension: 4 usable rules: p(s(x1)) -> x1 interpretation: [twice#](x0) = [0 0 0 0]x0 + [0], [0 0 0 -&] [0] [0 0 0 -&] [0] [p](x0) = [0 0 0 -&]x0 + [0] [0 0 0 -&] [0], [0 0 0 0] [0] [0 0 0 0] [0] [s](x0) = [0 0 0 0]x0 + [0] [1 1 1 1] [1] orientation: twice#(s(x1)) = [1 1 1 1]x1 + [1] >= [0 0 0 0]x1 + [0] = twice#(p(s(p(s(x1))))) [0 0 0 0] [0] [0 0 0 0] [0] p(s(x1)) = [0 0 0 0]x1 + [0] >= x1 = x1 [0 0 0 0] [0] problem: DPs: TRS: p(s(x1)) -> x1 Qed DPs: p#(p(s(x1))) -> p#(x1) TRS: sq(s(x1)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) Usable Rule Processor: DPs: p#(p(s(x1))) -> p#(x1) TRS: Arctic Interpretation Processor: dimension: 4 usable rules: interpretation: [p#](x0) = [0 -& -& -&]x0, [1 -& 1 -&] [0 ] [1 -& 1 -&] [0 ] [p](x0) = [1 -& -& -&]x0 + [0 ] [0 -& -& 0 ] [-&], [0 -& 0 -&] [-&] [1 0 1 0 ] [1 ] [s](x0) = [-& 0 0 0 ]x0 + [0 ] [1 0 1 0 ] [-&] orientation: p#(p(s(x1))) = [1 1 1 1]x1 + [1] >= [0 -& -& -&]x1 = p#(x1) problem: DPs: TRS: Qed