YES Problem: p(0(x1)) -> s(s(0(s(s(p(x1)))))) p(s(0(x1))) -> 0(x1) p(s(s(x1))) -> s(p(s(x1))) f(s(x1)) -> g(q(i(x1))) g(x1) -> f(p(p(x1))) q(i(x1)) -> q(s(x1)) q(s(x1)) -> s(s(x1)) i(x1) -> s(x1) Proof: String Reversal Processor: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) DP Processor: DPs: 0#(p(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(x1)) 0#(p(x1)) -> 0#(s(s(x1))) 0#(p(x1)) -> s#(0(s(s(x1)))) 0#(p(x1)) -> s#(s(0(s(s(x1))))) 0#(s(p(x1))) -> 0#(x1) s#(s(p(x1))) -> s#(x1) s#(s(p(x1))) -> s#(p(s(x1))) s#(f(x1)) -> g#(x1) s#(f(x1)) -> i#(q(g(x1))) i#(q(x1)) -> s#(q(x1)) s#(q(x1)) -> s#(x1) s#(q(x1)) -> s#(s(x1)) i#(x1) -> s#(x1) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) TDG Processor: DPs: 0#(p(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(x1)) 0#(p(x1)) -> 0#(s(s(x1))) 0#(p(x1)) -> s#(0(s(s(x1)))) 0#(p(x1)) -> s#(s(0(s(s(x1))))) 0#(s(p(x1))) -> 0#(x1) s#(s(p(x1))) -> s#(x1) s#(s(p(x1))) -> s#(p(s(x1))) s#(f(x1)) -> g#(x1) s#(f(x1)) -> i#(q(g(x1))) i#(q(x1)) -> s#(q(x1)) s#(q(x1)) -> s#(x1) s#(q(x1)) -> s#(s(x1)) i#(x1) -> s#(x1) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) graph: i#(q(x1)) -> s#(q(x1)) -> s#(q(x1)) -> s#(s(x1)) i#(q(x1)) -> s#(q(x1)) -> s#(q(x1)) -> s#(x1) i#(q(x1)) -> s#(q(x1)) -> s#(f(x1)) -> i#(q(g(x1))) i#(q(x1)) -> s#(q(x1)) -> s#(f(x1)) -> g#(x1) i#(q(x1)) -> s#(q(x1)) -> s#(s(p(x1))) -> s#(p(s(x1))) i#(q(x1)) -> s#(q(x1)) -> s#(s(p(x1))) -> s#(x1) i#(x1) -> s#(x1) -> s#(q(x1)) -> s#(s(x1)) i#(x1) -> s#(x1) -> s#(q(x1)) -> s#(x1) i#(x1) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) i#(x1) -> s#(x1) -> s#(f(x1)) -> g#(x1) i#(x1) -> s#(x1) -> s#(s(p(x1))) -> s#(p(s(x1))) i#(x1) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(s(x1)) -> s#(q(x1)) -> s#(s(x1)) s#(q(x1)) -> s#(s(x1)) -> s#(q(x1)) -> s#(x1) s#(q(x1)) -> s#(s(x1)) -> s#(f(x1)) -> i#(q(g(x1))) s#(q(x1)) -> s#(s(x1)) -> s#(f(x1)) -> g#(x1) s#(q(x1)) -> s#(s(x1)) -> s#(s(p(x1))) -> s#(p(s(x1))) s#(q(x1)) -> s#(s(x1)) -> s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) -> s#(q(x1)) -> s#(s(x1)) s#(q(x1)) -> s#(x1) -> s#(q(x1)) -> s#(x1) s#(q(x1)) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) s#(q(x1)) -> s#(x1) -> s#(f(x1)) -> g#(x1) s#(q(x1)) -> s#(x1) -> s#(s(p(x1))) -> s#(p(s(x1))) s#(q(x1)) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) s#(f(x1)) -> i#(q(g(x1))) -> i#(x1) -> s#(x1) s#(f(x1)) -> i#(q(g(x1))) -> i#(q(x1)) -> s#(q(x1)) s#(s(p(x1))) -> s#(p(s(x1))) -> s#(q(x1)) -> s#(s(x1)) s#(s(p(x1))) -> s#(p(s(x1))) -> s#(q(x1)) -> s#(x1) s#(s(p(x1))) -> s#(p(s(x1))) -> s#(f(x1)) -> i#(q(g(x1))) s#(s(p(x1))) -> s#(p(s(x1))) -> s#(f(x1)) -> g#(x1) s#(s(p(x1))) -> s#(p(s(x1))) -> s#(s(p(x1))) -> s#(p(s(x1))) s#(s(p(x1))) -> s#(p(s(x1))) -> s#(s(p(x1))) -> s#(x1) s#(s(p(x1))) -> s#(x1) -> s#(q(x1)) -> s#(s(x1)) s#(s(p(x1))) -> s#(x1) -> s#(q(x1)) -> s#(x1) s#(s(p(x1))) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) s#(s(p(x1))) -> s#(x1) -> s#(f(x1)) -> g#(x1) s#(s(p(x1))) -> s#(x1) -> s#(s(p(x1))) -> s#(p(s(x1))) s#(s(p(x1))) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) 0#(s(p(x1))) -> 0#(x1) -> 0#(s(p(x1))) -> 0#(x1) 0#(s(p(x1))) -> 0#(x1) -> 0#(p(x1)) -> s#(s(0(s(s(x1))))) 0#(s(p(x1))) -> 0#(x1) -> 0#(p(x1)) -> s#(0(s(s(x1)))) 0#(s(p(x1))) -> 0#(x1) -> 0#(p(x1)) -> 0#(s(s(x1))) 0#(s(p(x1))) -> 0#(x1) -> 0#(p(x1)) -> s#(s(x1)) 0#(s(p(x1))) -> 0#(x1) -> 0#(p(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(0(s(s(x1))))) -> s#(q(x1)) -> s#(s(x1)) 0#(p(x1)) -> s#(s(0(s(s(x1))))) -> s#(q(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(0(s(s(x1))))) -> s#(f(x1)) -> i#(q(g(x1))) 0#(p(x1)) -> s#(s(0(s(s(x1))))) -> s#(f(x1)) -> g#(x1) 0#(p(x1)) -> s#(s(0(s(s(x1))))) -> s#(s(p(x1))) -> s#(p(s(x1))) 0#(p(x1)) -> s#(s(0(s(s(x1))))) -> s#(s(p(x1))) -> s#(x1) 0#(p(x1)) -> s#(s(x1)) -> s#(q(x1)) -> s#(s(x1)) 0#(p(x1)) -> s#(s(x1)) -> s#(q(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(x1)) -> s#(f(x1)) -> i#(q(g(x1))) 0#(p(x1)) -> s#(s(x1)) -> s#(f(x1)) -> g#(x1) 0#(p(x1)) -> s#(s(x1)) -> s#(s(p(x1))) -> s#(p(s(x1))) 0#(p(x1)) -> s#(s(x1)) -> s#(s(p(x1))) -> s#(x1) 0#(p(x1)) -> s#(0(s(s(x1)))) -> s#(q(x1)) -> s#(s(x1)) 0#(p(x1)) -> s#(0(s(s(x1)))) -> s#(q(x1)) -> s#(x1) 0#(p(x1)) -> s#(0(s(s(x1)))) -> s#(f(x1)) -> i#(q(g(x1))) 0#(p(x1)) -> s#(0(s(s(x1)))) -> s#(f(x1)) -> g#(x1) 0#(p(x1)) -> s#(0(s(s(x1)))) -> s#(s(p(x1))) -> s#(p(s(x1))) 0#(p(x1)) -> s#(0(s(s(x1)))) -> s#(s(p(x1))) -> s#(x1) 0#(p(x1)) -> s#(x1) -> s#(q(x1)) -> s#(s(x1)) 0#(p(x1)) -> s#(x1) -> s#(q(x1)) -> s#(x1) 0#(p(x1)) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) 0#(p(x1)) -> s#(x1) -> s#(f(x1)) -> g#(x1) 0#(p(x1)) -> s#(x1) -> s#(s(p(x1))) -> s#(p(s(x1))) 0#(p(x1)) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(s(p(x1))) -> 0#(x1) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(p(x1)) -> s#(s(0(s(s(x1))))) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(p(x1)) -> s#(0(s(s(x1)))) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(p(x1)) -> 0#(s(s(x1))) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(p(x1)) -> s#(s(x1)) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(p(x1)) -> s#(x1) EDG Processor: DPs: 0#(p(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(x1)) 0#(p(x1)) -> 0#(s(s(x1))) 0#(p(x1)) -> s#(0(s(s(x1)))) 0#(p(x1)) -> s#(s(0(s(s(x1))))) 0#(s(p(x1))) -> 0#(x1) s#(s(p(x1))) -> s#(x1) s#(s(p(x1))) -> s#(p(s(x1))) s#(f(x1)) -> g#(x1) s#(f(x1)) -> i#(q(g(x1))) i#(q(x1)) -> s#(q(x1)) s#(q(x1)) -> s#(x1) s#(q(x1)) -> s#(s(x1)) i#(x1) -> s#(x1) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) graph: i#(q(x1)) -> s#(q(x1)) -> s#(q(x1)) -> s#(x1) i#(q(x1)) -> s#(q(x1)) -> s#(q(x1)) -> s#(s(x1)) i#(x1) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) i#(x1) -> s#(x1) -> s#(s(p(x1))) -> s#(p(s(x1))) i#(x1) -> s#(x1) -> s#(f(x1)) -> g#(x1) i#(x1) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) i#(x1) -> s#(x1) -> s#(q(x1)) -> s#(x1) i#(x1) -> s#(x1) -> s#(q(x1)) -> s#(s(x1)) s#(q(x1)) -> s#(s(x1)) -> s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(s(x1)) -> s#(s(p(x1))) -> s#(p(s(x1))) s#(q(x1)) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) -> s#(s(p(x1))) -> s#(p(s(x1))) s#(q(x1)) -> s#(x1) -> s#(f(x1)) -> g#(x1) s#(q(x1)) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) s#(q(x1)) -> s#(x1) -> s#(q(x1)) -> s#(x1) s#(q(x1)) -> s#(x1) -> s#(q(x1)) -> s#(s(x1)) s#(f(x1)) -> i#(q(g(x1))) -> i#(q(x1)) -> s#(q(x1)) s#(f(x1)) -> i#(q(g(x1))) -> i#(x1) -> s#(x1) s#(s(p(x1))) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) s#(s(p(x1))) -> s#(x1) -> s#(s(p(x1))) -> s#(p(s(x1))) s#(s(p(x1))) -> s#(x1) -> s#(f(x1)) -> g#(x1) s#(s(p(x1))) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) s#(s(p(x1))) -> s#(x1) -> s#(q(x1)) -> s#(x1) s#(s(p(x1))) -> s#(x1) -> s#(q(x1)) -> s#(s(x1)) 0#(s(p(x1))) -> 0#(x1) -> 0#(p(x1)) -> s#(x1) 0#(s(p(x1))) -> 0#(x1) -> 0#(p(x1)) -> s#(s(x1)) 0#(s(p(x1))) -> 0#(x1) -> 0#(p(x1)) -> 0#(s(s(x1))) 0#(s(p(x1))) -> 0#(x1) -> 0#(p(x1)) -> s#(0(s(s(x1)))) 0#(s(p(x1))) -> 0#(x1) -> 0#(p(x1)) -> s#(s(0(s(s(x1))))) 0#(s(p(x1))) -> 0#(x1) -> 0#(s(p(x1))) -> 0#(x1) 0#(p(x1)) -> s#(s(0(s(s(x1))))) -> s#(s(p(x1))) -> s#(x1) 0#(p(x1)) -> s#(s(0(s(s(x1))))) -> s#(s(p(x1))) -> s#(p(s(x1))) 0#(p(x1)) -> s#(s(x1)) -> s#(s(p(x1))) -> s#(x1) 0#(p(x1)) -> s#(s(x1)) -> s#(s(p(x1))) -> s#(p(s(x1))) 0#(p(x1)) -> s#(0(s(s(x1)))) -> s#(s(p(x1))) -> s#(x1) 0#(p(x1)) -> s#(0(s(s(x1)))) -> s#(s(p(x1))) -> s#(p(s(x1))) 0#(p(x1)) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) 0#(p(x1)) -> s#(x1) -> s#(s(p(x1))) -> s#(p(s(x1))) 0#(p(x1)) -> s#(x1) -> s#(f(x1)) -> g#(x1) 0#(p(x1)) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) 0#(p(x1)) -> s#(x1) -> s#(q(x1)) -> s#(x1) 0#(p(x1)) -> s#(x1) -> s#(q(x1)) -> s#(s(x1)) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(p(x1)) -> s#(x1) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(p(x1)) -> s#(s(x1)) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(p(x1)) -> 0#(s(s(x1))) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(p(x1)) -> s#(0(s(s(x1)))) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(p(x1)) -> s#(s(0(s(s(x1))))) 0#(p(x1)) -> 0#(s(s(x1))) -> 0#(s(p(x1))) -> 0#(x1) SCC Processor: #sccs: 2 #rules: 8 #arcs: 48/196 DPs: 0#(s(p(x1))) -> 0#(x1) 0#(p(x1)) -> 0#(s(s(x1))) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) Usable Rule Processor: DPs: 0#(s(p(x1))) -> 0#(x1) 0#(p(x1)) -> 0#(s(s(x1))) TRS: s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) s(q(x1)) -> s(s(x1)) i(q(x1)) -> s(q(x1)) i(x1) -> s(x1) g(x1) -> p(p(f(x1))) Arctic Interpretation Processor: dimension: 1 usable rules: s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) s(q(x1)) -> s(s(x1)) i(q(x1)) -> s(q(x1)) i(x1) -> s(x1) g(x1) -> p(p(f(x1))) interpretation: [0#](x0) = x0 + 0, [g](x0) = 15, [q](x0) = -4x0 + 0, [i](x0) = -7x0 + 4, [f](x0) = 1, [s](x0) = -7x0 + 4, [p](x0) = 7x0 + 5 orientation: 0#(s(p(x1))) = x1 + 4 >= x1 + 0 = 0#(x1) 0#(p(x1)) = 7x1 + 5 >= -14x1 + 4 = 0#(s(s(x1))) s(s(p(x1))) = -7x1 + 4 >= -7x1 + 4 = s(p(s(x1))) s(f(x1)) = 4 >= 4 = i(q(g(x1))) s(q(x1)) = -11x1 + 4 >= -14x1 + 4 = s(s(x1)) i(q(x1)) = -11x1 + 4 >= -11x1 + 4 = s(q(x1)) i(x1) = -7x1 + 4 >= -7x1 + 4 = s(x1) g(x1) = 15 >= 15 = p(p(f(x1))) problem: DPs: 0#(s(p(x1))) -> 0#(x1) TRS: s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) s(q(x1)) -> s(s(x1)) i(q(x1)) -> s(q(x1)) i(x1) -> s(x1) g(x1) -> p(p(f(x1))) Restore Modifier: DPs: 0#(s(p(x1))) -> 0#(x1) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) EDG Processor: DPs: 0#(s(p(x1))) -> 0#(x1) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) graph: 0#(s(p(x1))) -> 0#(x1) -> 0#(s(p(x1))) -> 0#(x1) CDG Processor: DPs: 0#(s(p(x1))) -> 0#(x1) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) graph: Qed DPs: i#(q(x1)) -> s#(q(x1)) s#(q(x1)) -> s#(s(x1)) s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) s#(f(x1)) -> i#(q(g(x1))) i#(x1) -> s#(x1) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) Usable Rule Processor: DPs: i#(q(x1)) -> s#(q(x1)) s#(q(x1)) -> s#(s(x1)) s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) s#(f(x1)) -> i#(q(g(x1))) i#(x1) -> s#(x1) TRS: s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) s(q(x1)) -> s(s(x1)) i(q(x1)) -> s(q(x1)) i(x1) -> s(x1) g(x1) -> p(p(f(x1))) Arctic Interpretation Processor: dimension: 1 usable rules: s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) s(q(x1)) -> s(s(x1)) i(q(x1)) -> s(q(x1)) i(x1) -> s(x1) g(x1) -> p(p(f(x1))) interpretation: [i#](x0) = 1x0 + 4, [s#](x0) = x0 + 2, [g](x0) = 10x0 + 2, [q](x0) = 1x0 + 2, [i](x0) = 1x0 + 4, [f](x0) = 12x0 + 4, [s](x0) = 1x0 + 0, [p](x0) = -1x0 + 0 orientation: i#(q(x1)) = 2x1 + 4 >= 1x1 + 2 = s#(q(x1)) s#(q(x1)) = 1x1 + 2 >= 1x1 + 2 = s#(s(x1)) s#(s(p(x1))) = x1 + 2 >= x1 + 2 = s#(x1) s#(q(x1)) = 1x1 + 2 >= x1 + 2 = s#(x1) s#(f(x1)) = 12x1 + 4 >= 12x1 + 4 = i#(q(g(x1))) i#(x1) = 1x1 + 4 >= x1 + 2 = s#(x1) s(s(p(x1))) = 1x1 + 2 >= 1x1 + 1 = s(p(s(x1))) s(f(x1)) = 13x1 + 5 >= 12x1 + 4 = i(q(g(x1))) s(q(x1)) = 2x1 + 3 >= 2x1 + 1 = s(s(x1)) i(q(x1)) = 2x1 + 4 >= 2x1 + 3 = s(q(x1)) i(x1) = 1x1 + 4 >= 1x1 + 0 = s(x1) g(x1) = 10x1 + 2 >= 10x1 + 2 = p(p(f(x1))) problem: DPs: s#(q(x1)) -> s#(s(x1)) s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) s#(f(x1)) -> i#(q(g(x1))) TRS: s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) s(q(x1)) -> s(s(x1)) i(q(x1)) -> s(q(x1)) i(x1) -> s(x1) g(x1) -> p(p(f(x1))) Restore Modifier: DPs: s#(q(x1)) -> s#(s(x1)) s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) s#(f(x1)) -> i#(q(g(x1))) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) EDG Processor: DPs: s#(q(x1)) -> s#(s(x1)) s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) s#(f(x1)) -> i#(q(g(x1))) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) graph: s#(q(x1)) -> s#(s(x1)) -> s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) -> s#(q(x1)) -> s#(s(x1)) s#(q(x1)) -> s#(x1) -> s#(q(x1)) -> s#(x1) s#(q(x1)) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) s#(q(x1)) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) s#(s(p(x1))) -> s#(x1) -> s#(q(x1)) -> s#(s(x1)) s#(s(p(x1))) -> s#(x1) -> s#(q(x1)) -> s#(x1) s#(s(p(x1))) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) s#(s(p(x1))) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) CDG Processor: DPs: s#(q(x1)) -> s#(s(x1)) s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) s#(f(x1)) -> i#(q(g(x1))) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) graph: s#(q(x1)) -> s#(s(x1)) -> s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) s#(q(x1)) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) s#(s(p(x1))) -> s#(x1) -> s#(s(p(x1))) -> s#(x1) s#(s(p(x1))) -> s#(x1) -> s#(f(x1)) -> i#(q(g(x1))) SCC Processor: #sccs: 1 #rules: 1 #arcs: 5/16 DPs: s#(s(p(x1))) -> s#(x1) TRS: 0(p(x1)) -> p(s(s(0(s(s(x1)))))) 0(s(p(x1))) -> 0(x1) s(s(p(x1))) -> s(p(s(x1))) s(f(x1)) -> i(q(g(x1))) g(x1) -> p(p(f(x1))) i(q(x1)) -> s(q(x1)) s(q(x1)) -> s(s(x1)) i(x1) -> s(x1) Usable Rule Processor: DPs: s#(s(p(x1))) -> s#(x1) TRS: Arctic Interpretation Processor: dimension: 4 usable rules: interpretation: [s#](x0) = [0 -& -& -&]x0, [1 -& 1 -&] [0 ] [1 -& 1 -&] [0 ] [s](x0) = [1 -& -& -&]x0 + [0 ] [0 -& -& 0 ] [-&], [0 -& 0 -&] [-&] [1 0 1 0 ] [1 ] [p](x0) = [-& 0 0 0 ]x0 + [0 ] [1 0 1 0 ] [-&] orientation: s#(s(p(x1))) = [1 1 1 1]x1 + [1] >= [0 -& -& -&]x1 = s#(x1) problem: DPs: TRS: Qed