YES Problem: p(0(x1)) -> 0(s(s(p(x1)))) p(s(x1)) -> x1 p(p(s(x1))) -> p(x1) f(s(x1)) -> p(s(g(p(s(s(x1)))))) g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1))))))))))) j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1))))))))))) half(0(x1)) -> 0(s(s(half(p(s(p(s(x1)))))))) half(s(s(x1))) -> s(half(p(p(s(s(x1)))))) rd(0(x1)) -> 0(s(0(0(0(0(s(0(rd(x1))))))))) Proof: Matrix Interpretation Processor: dim=1 interpretation: [rd](x0) = 6x0 + 4, [half](x0) = 2x0 + 1, [j](x0) = x0, [g](x0) = x0, [f](x0) = x0, [s](x0) = x0, [p](x0) = x0, [0](x0) = x0 + 1 orientation: p(0(x1)) = x1 + 1 >= x1 + 1 = 0(s(s(p(x1)))) p(s(x1)) = x1 >= x1 = x1 p(p(s(x1))) = x1 >= x1 = p(x1) f(s(x1)) = x1 >= x1 = p(s(g(p(s(s(x1)))))) g(s(x1)) = x1 >= x1 = p(p(s(s(s(j(s(p(s(p(s(x1))))))))))) j(s(x1)) = x1 >= x1 = p(s(s(p(s(f(p(s(p(p(s(x1))))))))))) half(0(x1)) = 2x1 + 3 >= 2x1 + 2 = 0(s(s(half(p(s(p(s(x1)))))))) half(s(s(x1))) = 2x1 + 1 >= 2x1 + 1 = s(half(p(p(s(s(x1)))))) rd(0(x1)) = 6x1 + 10 >= 6x1 + 10 = 0(s(0(0(0(0(s(0(rd(x1))))))))) problem: p(0(x1)) -> 0(s(s(p(x1)))) p(s(x1)) -> x1 p(p(s(x1))) -> p(x1) f(s(x1)) -> p(s(g(p(s(s(x1)))))) g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1))))))))))) j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1))))))))))) half(s(s(x1))) -> s(half(p(p(s(s(x1)))))) rd(0(x1)) -> 0(s(0(0(0(0(s(0(rd(x1))))))))) Matrix Interpretation Processor: dim=1 interpretation: [rd](x0) = 9x0 + 12, [half](x0) = 8x0, [j](x0) = x0, [g](x0) = x0, [f](x0) = x0, [s](x0) = x0, [p](x0) = x0, [0](x0) = x0 + 2 orientation: p(0(x1)) = x1 + 2 >= x1 + 2 = 0(s(s(p(x1)))) p(s(x1)) = x1 >= x1 = x1 p(p(s(x1))) = x1 >= x1 = p(x1) f(s(x1)) = x1 >= x1 = p(s(g(p(s(s(x1)))))) g(s(x1)) = x1 >= x1 = p(p(s(s(s(j(s(p(s(p(s(x1))))))))))) j(s(x1)) = x1 >= x1 = p(s(s(p(s(f(p(s(p(p(s(x1))))))))))) half(s(s(x1))) = 8x1 >= 8x1 = s(half(p(p(s(s(x1)))))) rd(0(x1)) = 9x1 + 30 >= 9x1 + 24 = 0(s(0(0(0(0(s(0(rd(x1))))))))) problem: p(0(x1)) -> 0(s(s(p(x1)))) p(s(x1)) -> x1 p(p(s(x1))) -> p(x1) f(s(x1)) -> p(s(g(p(s(s(x1)))))) g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1))))))))))) j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1))))))))))) half(s(s(x1))) -> s(half(p(p(s(s(x1)))))) String Reversal Processor: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) DP Processor: DPs: 0#(p(x1)) -> 0#(x1) 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> s#(s(0(x1))) s#(f(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(j(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(s(p(x1))) s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) TDG Processor: DPs: 0#(p(x1)) -> 0#(x1) 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> s#(s(0(x1))) s#(f(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(j(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(s(p(x1))) s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) graph: s#(j(x1)) -> s#(s(p(x1))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(s(half(x1))) -> s#(x1) s#(j(x1)) -> s#(s(p(x1))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(j(x1)) -> s#(s(p(x1))) s#(j(x1)) -> s#(s(p(x1))) -> s#(j(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(p(p(x1))) s#(j(x1)) -> s#(s(p(x1))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(f(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(s(half(x1))) -> s#(x1) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(j(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) -> s#(f(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(s(half(x1))) -> s#(x1) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(j(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(j(x1)) -> s#(p(s(s(p(x1))))) -> s#(f(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(s(half(x1))) -> s#(x1) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(j(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) -> s#(f(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(p(x1)) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(j(x1)) -> s#(p(x1)) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(j(x1)) -> s#(p(x1)) -> s#(s(half(x1))) -> s#(x1) s#(j(x1)) -> s#(p(x1)) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(j(x1)) -> s#(p(x1)) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(j(x1)) -> s#(p(x1)) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(j(x1)) -> s#(p(x1)) -> s#(j(x1)) -> s#(s(p(x1))) s#(j(x1)) -> s#(p(x1)) -> s#(j(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(j(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(j(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(j(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(j(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(j(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(p(p(x1))) s#(j(x1)) -> s#(p(x1)) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(j(x1)) -> s#(p(x1)) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(j(x1)) -> s#(p(x1)) -> s#(f(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(j(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(f(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(j(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(f(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(j(x1)) -> s#(s(p(x1))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(j(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(f(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(j(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) -> s#(f(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(j(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) -> s#(f(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(p(p(x1))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(p(p(x1))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(j(x1)) -> s#(s(p(x1))) s#(g(x1)) -> s#(p(p(x1))) -> s#(j(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(p(p(x1))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(p(p(x1))) -> s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(p(p(x1))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(g(x1)) -> s#(p(p(x1))) -> s#(f(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(s(half(x1))) -> s#(x1) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(j(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(f(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(s(half(x1))) -> s#(x1) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(j(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(f(x1)) -> s#(p(g(s(p(x1))))) -> s#(f(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(p(x1)) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(f(x1)) -> s#(p(x1)) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(f(x1)) -> s#(p(x1)) -> s#(s(half(x1))) -> s#(x1) s#(f(x1)) -> s#(p(x1)) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(f(x1)) -> s#(p(x1)) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(f(x1)) -> s#(p(x1)) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(f(x1)) -> s#(p(x1)) -> s#(j(x1)) -> s#(s(p(x1))) s#(f(x1)) -> s#(p(x1)) -> s#(j(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(f(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(f(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(f(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(f(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(f(x1)) -> s#(p(x1)) -> s#(g(x1)) -> s#(p(p(x1))) s#(f(x1)) -> s#(p(x1)) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(f(x1)) -> s#(p(x1)) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(f(x1)) -> s#(p(x1)) -> s#(f(x1)) -> s#(p(x1)) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(j(x1)) -> s#(p(x1)) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(f(x1)) -> s#(p(x1)) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(j(x1)) -> s#(p(x1)) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(f(x1)) -> s#(p(x1)) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(x1) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(s(half(x1))) -> s#(x1) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(s(half(x1))) -> s#(x1) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(s(half(x1))) -> s#(x1) -> s#(j(x1)) -> s#(s(p(x1))) s#(s(half(x1))) -> s#(x1) -> s#(j(x1)) -> s#(p(x1)) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(p(p(x1))) s#(s(half(x1))) -> s#(x1) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(x1) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(s(half(x1))) -> s#(x1) -> s#(f(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(x1) 0#(p(x1)) -> s#(s(0(x1))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(j(x1)) -> s#(s(p(x1))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(j(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) 0#(p(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) 0#(p(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(x1) 0#(p(x1)) -> s#(0(x1)) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) 0#(p(x1)) -> s#(0(x1)) -> s#(j(x1)) -> s#(s(p(x1))) 0#(p(x1)) -> s#(0(x1)) -> s#(j(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(0(x1)) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) 0#(p(x1)) -> s#(0(x1)) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) 0#(p(x1)) -> s#(0(x1)) -> s#(f(x1)) -> s#(p(x1)) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(0(x1))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> 0#(x1) EDG Processor: DPs: 0#(p(x1)) -> 0#(x1) 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> s#(s(0(x1))) s#(f(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(j(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(s(p(x1))) s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) graph: s#(j(x1)) -> s#(s(p(x1))) -> s#(f(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(s(p(x1))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(p(p(x1))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(j(x1)) -> s#(p(x1)) s#(j(x1)) -> s#(s(p(x1))) -> s#(j(x1)) -> s#(s(p(x1))) s#(j(x1)) -> s#(s(p(x1))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(s(half(x1))) -> s#(x1) s#(j(x1)) -> s#(s(p(x1))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(j(x1)) -> s#(s(p(x1))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(j(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(f(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(j(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(f(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(p(p(x1))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(j(x1)) -> s#(p(x1)) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(j(x1)) -> s#(s(p(x1))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(g(x1)) -> s#(s(p(p(x1)))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(f(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(j(x1)) -> s#(p(x1)) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(s(half(x1))) -> s#(x1) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(f(x1)) -> s#(p(x1)) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(p(p(x1))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(j(x1)) -> s#(p(x1)) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(j(x1)) -> s#(s(p(x1))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(x1) -> s#(f(x1)) -> s#(p(x1)) s#(s(half(x1))) -> s#(x1) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) s#(s(half(x1))) -> s#(x1) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(p(p(x1))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(s(p(p(x1)))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s#(s(half(x1))) -> s#(x1) -> s#(j(x1)) -> s#(p(x1)) s#(s(half(x1))) -> s#(x1) -> s#(j(x1)) -> s#(s(p(x1))) s#(s(half(x1))) -> s#(x1) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) s#(s(half(x1))) -> s#(x1) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) s#(s(half(x1))) -> s#(x1) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(j(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(0(x1))) -> s#(j(x1)) -> s#(s(p(x1))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(x1) 0#(p(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) 0#(p(x1)) -> s#(0(x1)) -> s#(f(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(0(x1)) -> s#(f(x1)) -> s#(p(g(s(p(x1))))) 0#(p(x1)) -> s#(0(x1)) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(s(s(p(p(x1))))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(p(s(j(s(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(g(x1)) -> s#(p(s(p(s(j(s(s(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(j(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(0(x1)) -> s#(j(x1)) -> s#(s(p(x1))) 0#(p(x1)) -> s#(0(x1)) -> s#(j(x1)) -> s#(p(s(s(p(x1))))) 0#(p(x1)) -> s#(0(x1)) -> s#(j(x1)) -> s#(p(f(s(p(s(s(p(x1)))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(j(x1)) -> s#(p(p(s(p(f(s(p(s(s(p(x1))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(x1) 0#(p(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) 0#(p(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> 0#(x1) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(0(x1))) SCC Processor: #sccs: 2 #rules: 8 #arcs: 144/400 DPs: 0#(p(x1)) -> 0#(x1) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) Arctic Interpretation Processor: dimension: 2 interpretation: [0#](x0) = [0 1]x0, [1 ] [half](x0) = [-&], [1] [j](x0) = [2], [1] [g](x0) = [0], [1] [f](x0) = [0], [1 0 ] [0] [s](x0) = [0 -&]x0 + [0], [-& 0 ] [0] [p](x0) = [0 1 ]x0 + [1], [1 2] [2] [0](x0) = [2 3]x0 + [2] orientation: 0#(p(x1)) = [1 2]x1 + [2] >= [0 1]x1 = 0#(x1) [2 3] [3] [2 3] [3] 0(p(x1)) = [3 4]x1 + [4] >= [3 4]x1 + [4] = p(s(s(0(x1)))) [0 1 ] [1] s(p(x1)) = [-& 0 ]x1 + [0] >= x1 = x1 [1 2] [2] [-& 0 ] [0] s(p(p(x1))) = [0 1]x1 + [1] >= [0 1 ]x1 + [1] = p(x1) [2] [2] s(f(x1)) = [1] >= [1] = s(s(p(g(s(p(x1)))))) [2] [2] s(g(x1)) = [1] >= [1] = s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) [2] [2] s(j(x1)) = [1] >= [1] = s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) [3] [3] s(s(half(x1))) = [2] >= [2] = s(s(p(p(half(s(x1)))))) problem: DPs: TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) Qed DPs: s#(j(x1)) -> s#(s(p(x1))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) -> s#(s(s(p(p(x1))))) s#(g(x1)) -> s#(s(p(p(x1)))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) Arctic Interpretation Processor: dimension: 1 interpretation: [s#](x0) = 11x0 + 0, [half](x0) = x0, [j](x0) = 1x0 + 13, [g](x0) = 1x0 + 13, [f](x0) = 1x0 + 13, [s](x0) = x0, [p](x0) = x0, [0](x0) = 2x0 orientation: s#(j(x1)) = 12x1 + 24 >= 11x1 + 0 = s#(s(p(x1))) s#(s(half(x1))) = 11x1 + 0 >= 11x1 + 0 = s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) = 11x1 + 0 >= 11x1 + 0 = s#(x1) s#(g(x1)) = 12x1 + 24 >= 12x1 + 24 = s#(j(s(s(s(p(p(x1))))))) s#(g(x1)) = 12x1 + 24 >= 11x1 + 0 = s#(s(s(p(p(x1))))) s#(g(x1)) = 12x1 + 24 >= 11x1 + 0 = s#(s(p(p(x1)))) s#(f(x1)) = 12x1 + 24 >= 12x1 + 24 = s#(s(p(g(s(p(x1)))))) 0(p(x1)) = 2x1 >= 2x1 = p(s(s(0(x1)))) s(p(x1)) = x1 >= x1 = x1 s(p(p(x1))) = x1 >= x1 = p(x1) s(f(x1)) = 1x1 + 13 >= 1x1 + 13 = s(s(p(g(s(p(x1)))))) s(g(x1)) = 1x1 + 13 >= 1x1 + 13 = s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) = 1x1 + 13 >= 1x1 + 13 = s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) = x1 >= x1 = s(s(p(p(half(s(x1)))))) problem: DPs: s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) EDG Processor: DPs: s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(x1) s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) graph: s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(s(half(x1))) -> s#(x1) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(x1) -> s#(g(x1)) -> s#(j(s(s(s(p(p(x1))))))) s#(s(half(x1))) -> s#(x1) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) SCC Processor: #sccs: 1 #rules: 3 #arcs: 12/16 DPs: s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) Arctic Interpretation Processor: dimension: 1 interpretation: [s#](x0) = x0, [half](x0) = 2x0, [j](x0) = 8x0, [g](x0) = 8x0, [f](x0) = 8x0, [s](x0) = x0, [p](x0) = x0, [0](x0) = -7x0 + 0 orientation: s#(f(x1)) = 8x1 >= 8x1 = s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) = 2x1 >= x1 = s#(x1) s#(s(half(x1))) = 2x1 >= 2x1 = s#(s(p(p(half(s(x1)))))) 0(p(x1)) = -7x1 + 0 >= -7x1 + 0 = p(s(s(0(x1)))) s(p(x1)) = x1 >= x1 = x1 s(p(p(x1))) = x1 >= x1 = p(x1) s(f(x1)) = 8x1 >= 8x1 = s(s(p(g(s(p(x1)))))) s(g(x1)) = 8x1 >= 8x1 = s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) = 8x1 >= 8x1 = s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) = 2x1 >= 2x1 = s(s(p(p(half(s(x1)))))) problem: DPs: s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) EDG Processor: DPs: s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) graph: s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) CDG Processor: DPs: s#(f(x1)) -> s#(s(p(g(s(p(x1)))))) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) TRS: 0(p(x1)) -> p(s(s(0(x1)))) s(p(x1)) -> x1 s(p(p(x1))) -> p(x1) s(f(x1)) -> s(s(p(g(s(p(x1)))))) s(g(x1)) -> s(p(s(p(s(j(s(s(s(p(p(x1))))))))))) s(j(x1)) -> s(p(p(s(p(f(s(p(s(s(p(x1))))))))))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) graph: Qed