YES Problem: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y Proof: DP Processor: DPs: c#(c(c(y))) -> c#(a(y,0())) c#(c(c(y))) -> c#(c(a(y,0()))) c#(a(a(0(),x),y)) -> c#(0()) c#(a(a(0(),x),y)) -> c#(c(0())) c#(a(a(0(),x),y)) -> c#(c(c(0()))) TRS: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y EDG Processor: DPs: c#(c(c(y))) -> c#(a(y,0())) c#(c(c(y))) -> c#(c(a(y,0()))) c#(a(a(0(),x),y)) -> c#(0()) c#(a(a(0(),x),y)) -> c#(c(0())) c#(a(a(0(),x),y)) -> c#(c(c(0()))) TRS: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y graph: c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(c(c(y))) -> c#(a(y,0())) c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(c(c(y))) -> c#(c(a(y,0()))) c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(a(a(0(),x),y)) -> c#(0()) c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(a(a(0(),x),y)) -> c#(c(0())) c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(a(a(0(),x),y)) -> c#(c(c(0()))) c#(a(a(0(),x),y)) -> c#(c(c(0()))) -> c#(c(c(y))) -> c#(a(y,0())) c#(a(a(0(),x),y)) -> c#(c(c(0()))) -> c#(c(c(y))) -> c#(c(a(y,0()))) c#(a(a(0(),x),y)) -> c#(c(c(0()))) -> c#(a(a(0(),x),y)) -> c#(0()) c#(a(a(0(),x),y)) -> c#(c(c(0()))) -> c#(a(a(0(),x),y)) -> c#(c(0())) c#(a(a(0(),x),y)) -> c#(c(c(0()))) -> c#(a(a(0(),x),y)) -> c#(c(c(0()))) c#(c(c(y))) -> c#(a(y,0())) -> c#(a(a(0(),x),y)) -> c#(0()) c#(c(c(y))) -> c#(a(y,0())) -> c#(a(a(0(),x),y)) -> c#(c(0())) c#(c(c(y))) -> c#(a(y,0())) -> c#(a(a(0(),x),y)) -> c#(c(c(0()))) c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(c(c(y))) -> c#(a(y,0())) c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(c(c(y))) -> c#(c(a(y,0()))) c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(a(a(0(),x),y)) -> c#(0()) c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(a(a(0(),x),y)) -> c#(c(0())) c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(a(a(0(),x),y)) -> c#(c(c(0()))) SCC Processor: #sccs: 1 #rules: 4 #arcs: 18/25 DPs: c#(a(a(0(),x),y)) -> c#(c(0())) c#(a(a(0(),x),y)) -> c#(c(c(0()))) c#(c(c(y))) -> c#(c(a(y,0()))) c#(c(c(y))) -> c#(a(y,0())) TRS: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {2} transitions: 00() -> 3* c0(3) -> 4* c{#,0}(4) -> 2* 3 -> 4* problem: DPs: c#(a(a(0(),x),y)) -> c#(c(c(0()))) c#(c(c(y))) -> c#(c(a(y,0()))) c#(c(c(y))) -> c#(a(y,0())) TRS: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {2} transitions: 00() -> 3* c0(4) -> 5* c0(3) -> 4* c{#,0}(5) -> 2* c{#,0}(4) -> 2* a0(3,3) -> 4* 3 -> 4* 4 -> 5* problem: DPs: c#(c(c(y))) -> c#(c(a(y,0()))) c#(c(c(y))) -> c#(a(y,0())) TRS: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y Matrix Interpretation Processor: dimension: 1 interpretation: [c#](x0) = x0 + 1, [a](x0, x1) = 1, [0] = 0, [c](x0) = x0 + 1 orientation: c#(c(c(y))) = y + 3 >= 3 = c#(c(a(y,0()))) c#(c(c(y))) = y + 3 >= 2 = c#(a(y,0())) c(c(c(y))) = y + 3 >= 3 = c(c(a(y,0()))) c(a(a(0(),x),y)) = 2 >= 1 = a(c(c(c(0()))),y) c(y) = y + 1 >= y = y problem: DPs: c#(c(c(y))) -> c#(c(a(y,0()))) TRS: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y Matrix Interpretation Processor: dimension: 1 interpretation: [c#](x0) = x0, [a](x0, x1) = 0, [0] = 0, [c](x0) = x0 + 1 orientation: c#(c(c(y))) = y + 2 >= 1 = c#(c(a(y,0()))) c(c(c(y))) = y + 3 >= 2 = c(c(a(y,0()))) c(a(a(0(),x),y)) = 1 >= 0 = a(c(c(c(0()))),y) c(y) = y + 1 >= y = y problem: DPs: TRS: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y Qed