YES Problem: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x Proof: DP Processor: DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) f#(c(s(x),y)) -> f#(c(x,s(y))) f#(f(x)) -> f#(d(f(x))) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x EDG Processor: DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) f#(c(s(x),y)) -> f#(c(x,s(y))) f#(f(x)) -> f#(d(f(x))) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x graph: f#(c(s(x),y)) -> f#(c(x,s(y))) -> f#(c(s(x),y)) -> f#(c(x,s(y))) g#(c(x,s(y))) -> g#(c(s(x),y)) -> g#(c(x,s(y))) -> g#(c(s(x),y)) SCC Processor: #sccs: 2 #rules: 2 #arcs: 2/9 DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x Usable Rule Processor: DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) TRS: Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {4} transitions: s1(5) -> 7* s1(7) -> 7* g{#,0}(6) -> 4* c0(5,3) -> 6* c0(1,2) -> 2* c0(2,1) -> 2* c0(1,1) -> 2* c0(2,2) -> 2* s0(2) -> 1* s0(1) -> 1* s0(3) -> 5* g{#,1}(8) -> 4* c1(7,1) -> 8* c1(7,2) -> 8* 1 -> 3* 2 -> 3* problem: DPs: TRS: Qed DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0) = x0, [d](x0) = x0, [f](x0) = x0, [g](x0) = 0, [c](x0, x1) = x0, [s](x0) = x0 + 1 orientation: f#(c(s(x),y)) = x + 1 >= x = f#(c(x,s(y))) g(c(x,s(y))) = 0 >= 0 = g(c(s(x),y)) f(c(s(x),y)) = x + 1 >= x = f(c(x,s(y))) f(f(x)) = x >= x = f(d(f(x))) f(x) = x >= x = x problem: DPs: TRS: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x Qed