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 Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: p0() -> 5* s0() -> 3* f70() -> 2* a{#,0}(7,6) -> 1* f0() -> 7* a0(3,2) -> 4* a0(5,4) -> 6* 2 -> 6* problem: DPs: 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 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 Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: p0() -> 5* s0() -> 3* f140() -> 2* d0() -> 7* a{#,0}(7,6) -> 1* a0(3,2) -> 4* a0(5,4) -> 6* 2 -> 6* problem: DPs: 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 Qed