YES Problem: a(f(),0()) -> a(s(),0()) a(d(),0()) -> 0() a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x))))) a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x)))) a(p(),a(s(),x)) -> x Proof: DP Processor: DPs: a#(f(),0()) -> a#(s(),0()) a#(d(),a(s(),x)) -> a#(p(),a(s(),x)) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) a#(d(),a(s(),x)) -> a#(s(),a(d(),a(p(),a(s(),x)))) a#(d(),a(s(),x)) -> a#(s(),a(s(),a(d(),a(p(),a(s(),x))))) a#(f(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) TRS: a(f(),0()) -> a(s(),0()) a(d(),0()) -> 0() a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x))))) a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x)))) a(p(),a(s(),x)) -> x EDG Processor: DPs: a#(f(),0()) -> a#(s(),0()) a#(d(),a(s(),x)) -> a#(p(),a(s(),x)) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) a#(d(),a(s(),x)) -> a#(s(),a(d(),a(p(),a(s(),x)))) a#(d(),a(s(),x)) -> a#(s(),a(s(),a(d(),a(p(),a(s(),x))))) a#(f(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) TRS: a(f(),0()) -> a(s(),0()) a(d(),0()) -> 0() a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x))))) a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x)))) a(p(),a(s(),x)) -> x graph: a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) -> a#(d(),a(s(),x)) -> a#(p(),a(s(),x)) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) -> a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) -> a#(d(),a(s(),x)) -> a#(s(),a(d(),a(p(),a(s(),x)))) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) -> a#(d(),a(s(),x)) -> a#(s(),a(s(),a(d(),a(p(),a(s(),x))))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(s(),a(d(),a(p(),a(s(),x)))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(s(),a(s(),a(d(),a(p(),a(s(),x))))) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),0()) -> a#(s(),0()) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) SCC Processor: #sccs: 2 #rules: 2 #arcs: 12/64 DPs: a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) TRS: a(f(),0()) -> a(s(),0()) a(d(),0()) -> 0() a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x))))) a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x)))) a(p(),a(s(),x)) -> x Usable Rule Processor: DPs: a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) TRS: a(p(),a(s(),x)) -> x Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {6} transitions: a{#,0}(4,8) -> 6* f0() -> 4* a0(3,1) -> 3* a0(3,3) -> 3* a0(4,2) -> 3* a0(4,4) -> 3* a0(1,2) -> 3* a0(1,4) -> 3* a0(2,1) -> 3* a0(2,3) -> 3* a0(2,5) -> 7* a0(3,2) -> 3* a0(3,4) -> 3* a0(4,1) -> 3* a0(4,3) -> 3* a0(1,1) -> 3* a0(1,3) -> 3* a0(1,7) -> 8* a0(2,2) -> 3* a0(2,4) -> 3* s0() -> 2* p0() -> 1* a{#,1}(13,12) -> 6* f1() -> 13* a1(9,2) -> 10* a1(9,4) -> 10* a1(11,10) -> 12* a1(9,1) -> 10* a1(9,3) -> 10* p1() -> 11* s1() -> 9* 1 -> 12,3,5 2 -> 12,3,5 3 -> 12,5 4 -> 12,3,5 5 -> 8* problem: DPs: TRS: a(p(),a(s(),x)) -> x Qed DPs: a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) TRS: a(f(),0()) -> a(s(),0()) a(d(),0()) -> 0() a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x))))) a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x)))) a(p(),a(s(),x)) -> x Usable Rule Processor: DPs: a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) TRS: a(p(),a(s(),x)) -> x Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {6} transitions: a{#,0}(4,8) -> 6* a0(3,1) -> 3* a0(3,3) -> 3* a0(4,2) -> 3* a0(4,4) -> 3* a0(1,2) -> 3* a0(1,4) -> 3* a0(2,1) -> 3* a0(2,3) -> 3* a0(2,5) -> 7* a0(3,2) -> 3* a0(3,4) -> 3* a0(4,1) -> 3* a0(4,3) -> 3* a0(1,1) -> 3* a0(1,3) -> 3* a0(1,7) -> 8* a0(2,2) -> 3* a0(2,4) -> 3* s0() -> 2* p0() -> 1* a{#,1}(13,12) -> 6* a1(9,2) -> 10* a1(9,4) -> 10* a1(11,10) -> 12* a1(9,1) -> 10* a1(9,3) -> 10* p1() -> 11* s1() -> 9* d0() -> 4* d1() -> 13* 1 -> 12,3,5 2 -> 12,3,5 3 -> 12,5 4 -> 12,3,5 5 -> 8* problem: DPs: TRS: a(p(),a(s(),x)) -> x Qed