YES Problem: p(0(x1)) -> 0(s(s(p(x1)))) p(s(x1)) -> x1 p(p(s(x1))) -> p(x1) f(s(x1)) -> g(s(x1)) g(x1) -> i(s(half(x1))) i(x1) -> f(p(x1)) half(0(x1)) -> 0(s(s(half(x1)))) half(s(s(x1))) -> s(half(p(p(s(s(x1)))))) 0(x1) -> x1 rd(0(x1)) -> 0(0(0(0(0(0(rd(x1))))))) Proof: Matrix Interpretation Processor: dim=1 interpretation: [rd](x0) = 6x0 + 14, [i](x0) = 4x0, [half](x0) = x0, [g](x0) = 4x0, [f](x0) = 4x0, [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)) = 4x1 >= 4x1 = g(s(x1)) g(x1) = 4x1 >= 4x1 = i(s(half(x1))) i(x1) = 4x1 >= 4x1 = f(p(x1)) half(0(x1)) = x1 + 1 >= x1 + 1 = 0(s(s(half(x1)))) half(s(s(x1))) = x1 >= x1 = s(half(p(p(s(s(x1)))))) 0(x1) = x1 + 1 >= x1 = x1 rd(0(x1)) = 6x1 + 20 >= 6x1 + 20 = 0(0(0(0(0(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)) -> g(s(x1)) g(x1) -> i(s(half(x1))) i(x1) -> f(p(x1)) half(0(x1)) -> 0(s(s(half(x1)))) half(s(s(x1))) -> s(half(p(p(s(s(x1)))))) rd(0(x1)) -> 0(0(0(0(0(0(rd(x1))))))) Matrix Interpretation Processor: dim=1 interpretation: [rd](x0) = 7x0, [i](x0) = x0, [half](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 = g(s(x1)) g(x1) = x1 >= x1 = i(s(half(x1))) i(x1) = x1 >= x1 = f(p(x1)) half(0(x1)) = x1 + 1 >= x1 + 1 = 0(s(s(half(x1)))) half(s(s(x1))) = x1 >= x1 = s(half(p(p(s(s(x1)))))) rd(0(x1)) = 7x1 + 7 >= 7x1 + 6 = 0(0(0(0(0(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)) -> g(s(x1)) g(x1) -> i(s(half(x1))) i(x1) -> f(p(x1)) half(0(x1)) -> 0(s(s(half(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(g(x1)) g(x1) -> half(s(i(x1))) i(x1) -> p(f(x1)) 0(half(x1)) -> half(s(s(0(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)) -> g#(x1) s#(f(x1)) -> s#(g(x1)) g#(x1) -> i#(x1) g#(x1) -> s#(i(x1)) 0#(half(x1)) -> 0#(x1) 0#(half(x1)) -> s#(0(x1)) 0#(half(x1)) -> s#(s(0(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(g(x1)) g(x1) -> half(s(i(x1))) i(x1) -> p(f(x1)) 0(half(x1)) -> half(s(s(0(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)) -> g#(x1) s#(f(x1)) -> s#(g(x1)) g#(x1) -> i#(x1) g#(x1) -> s#(i(x1)) 0#(half(x1)) -> 0#(x1) 0#(half(x1)) -> s#(0(x1)) 0#(half(x1)) -> s#(s(0(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(g(x1)) g(x1) -> half(s(i(x1))) i(x1) -> p(f(x1)) 0(half(x1)) -> half(s(s(0(x1)))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) graph: g#(x1) -> s#(i(x1)) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) g#(x1) -> s#(i(x1)) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) g#(x1) -> s#(i(x1)) -> s#(s(half(x1))) -> s#(x1) g#(x1) -> s#(i(x1)) -> s#(f(x1)) -> s#(g(x1)) g#(x1) -> s#(i(x1)) -> s#(f(x1)) -> g#(x1) s#(f(x1)) -> g#(x1) -> g#(x1) -> s#(i(x1)) s#(f(x1)) -> g#(x1) -> g#(x1) -> i#(x1) s#(f(x1)) -> s#(g(x1)) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(f(x1)) -> s#(g(x1)) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(f(x1)) -> s#(g(x1)) -> s#(s(half(x1))) -> s#(x1) s#(f(x1)) -> s#(g(x1)) -> s#(f(x1)) -> s#(g(x1)) s#(f(x1)) -> s#(g(x1)) -> s#(f(x1)) -> g#(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#(f(x1)) -> s#(g(x1)) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(f(x1)) -> g#(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#(f(x1)) -> s#(g(x1)) s#(s(half(x1))) -> s#(p(p(half(s(x1))))) -> s#(f(x1)) -> g#(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#(f(x1)) -> s#(g(x1)) s#(s(half(x1))) -> s#(x1) -> s#(f(x1)) -> g#(x1) 0#(half(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) 0#(half(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) 0#(half(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(x1) 0#(half(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> s#(g(x1)) 0#(half(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> g#(x1) 0#(half(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) 0#(half(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) 0#(half(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(x1) 0#(half(x1)) -> s#(0(x1)) -> s#(f(x1)) -> s#(g(x1)) 0#(half(x1)) -> s#(0(x1)) -> s#(f(x1)) -> g#(x1) 0#(half(x1)) -> 0#(x1) -> 0#(half(x1)) -> s#(s(0(x1))) 0#(half(x1)) -> 0#(x1) -> 0#(half(x1)) -> s#(0(x1)) 0#(half(x1)) -> 0#(x1) -> 0#(half(x1)) -> 0#(x1) 0#(half(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(0(x1))) 0#(half(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(0(x1)) 0#(half(x1)) -> 0#(x1) -> 0#(p(x1)) -> 0#(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#(f(x1)) -> s#(g(x1)) 0#(p(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> g#(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#(f(x1)) -> s#(g(x1)) 0#(p(x1)) -> s#(0(x1)) -> s#(f(x1)) -> g#(x1) 0#(p(x1)) -> 0#(x1) -> 0#(half(x1)) -> s#(s(0(x1))) 0#(p(x1)) -> 0#(x1) -> 0#(half(x1)) -> s#(0(x1)) 0#(p(x1)) -> 0#(x1) -> 0#(half(x1)) -> 0#(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)) -> g#(x1) s#(f(x1)) -> s#(g(x1)) g#(x1) -> i#(x1) g#(x1) -> s#(i(x1)) 0#(half(x1)) -> 0#(x1) 0#(half(x1)) -> s#(0(x1)) 0#(half(x1)) -> s#(s(0(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(g(x1)) g(x1) -> half(s(i(x1))) i(x1) -> p(f(x1)) 0(half(x1)) -> half(s(s(0(x1)))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) graph: g#(x1) -> s#(i(x1)) -> s#(f(x1)) -> g#(x1) g#(x1) -> s#(i(x1)) -> s#(f(x1)) -> s#(g(x1)) g#(x1) -> s#(i(x1)) -> s#(s(half(x1))) -> s#(x1) g#(x1) -> s#(i(x1)) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) g#(x1) -> s#(i(x1)) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) s#(f(x1)) -> g#(x1) -> g#(x1) -> i#(x1) s#(f(x1)) -> g#(x1) -> g#(x1) -> s#(i(x1)) s#(f(x1)) -> s#(g(x1)) -> s#(f(x1)) -> g#(x1) s#(f(x1)) -> s#(g(x1)) -> s#(f(x1)) -> s#(g(x1)) s#(f(x1)) -> s#(g(x1)) -> s#(s(half(x1))) -> s#(x1) s#(f(x1)) -> s#(g(x1)) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) s#(f(x1)) -> s#(g(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)) -> g#(x1) s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) -> s#(f(x1)) -> s#(g(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)) -> g#(x1) s#(s(half(x1))) -> s#(x1) -> s#(f(x1)) -> s#(g(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#(half(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> g#(x1) 0#(half(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> s#(g(x1)) 0#(half(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(x1) 0#(half(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) 0#(half(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) 0#(half(x1)) -> s#(0(x1)) -> s#(f(x1)) -> g#(x1) 0#(half(x1)) -> s#(0(x1)) -> s#(f(x1)) -> s#(g(x1)) 0#(half(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(x1) 0#(half(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) 0#(half(x1)) -> s#(0(x1)) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) 0#(half(x1)) -> 0#(x1) -> 0#(p(x1)) -> 0#(x1) 0#(half(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(0(x1)) 0#(half(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(0(x1))) 0#(half(x1)) -> 0#(x1) -> 0#(half(x1)) -> 0#(x1) 0#(half(x1)) -> 0#(x1) -> 0#(half(x1)) -> s#(0(x1)) 0#(half(x1)) -> 0#(x1) -> 0#(half(x1)) -> s#(s(0(x1))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> g#(x1) 0#(p(x1)) -> s#(s(0(x1))) -> s#(f(x1)) -> s#(g(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)) -> g#(x1) 0#(p(x1)) -> s#(0(x1)) -> s#(f(x1)) -> s#(g(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))) 0#(p(x1)) -> 0#(x1) -> 0#(half(x1)) -> 0#(x1) 0#(p(x1)) -> 0#(x1) -> 0#(half(x1)) -> s#(0(x1)) 0#(p(x1)) -> 0#(x1) -> 0#(half(x1)) -> s#(s(0(x1))) CDG Processor: DPs: 0#(p(x1)) -> 0#(x1) 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> s#(s(0(x1))) s#(f(x1)) -> g#(x1) s#(f(x1)) -> s#(g(x1)) g#(x1) -> i#(x1) g#(x1) -> s#(i(x1)) 0#(half(x1)) -> 0#(x1) 0#(half(x1)) -> s#(0(x1)) 0#(half(x1)) -> s#(s(0(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(g(x1)) g(x1) -> half(s(i(x1))) i(x1) -> p(f(x1)) 0(half(x1)) -> half(s(s(0(x1)))) s(s(half(x1))) -> s(s(p(p(half(s(x1)))))) graph: s#(f(x1)) -> g#(x1) -> g#(x1) -> s#(i(x1)) s#(f(x1)) -> g#(x1) -> g#(x1) -> i#(x1) 0#(half(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(s(p(p(half(s(x1)))))) 0#(half(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(p(p(half(s(x1))))) 0#(half(x1)) -> s#(s(0(x1))) -> s#(s(half(x1))) -> s#(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) SCC Processor: #sccs: 0 #rules: 0 #arcs: 8/169