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 automaton: final states: {7} transitions: s0() -> 6* p0() -> 6* a{#,1}(17,16) -> 7* f1() -> 17* a1(13,6) -> 14* a1(15,14) -> 16* p1() -> 15* s1() -> 13* a{#,0}(6,6) -> 7* f0() -> 6* a0(6,6) -> 6* 6 -> 16* 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 automaton: final states: {7} transitions: s0() -> 6* p0() -> 6* a{#,1}(17,16) -> 7* a1(13,6) -> 14* a1(15,14) -> 16* p1() -> 15* s1() -> 13* d0() -> 6* a{#,0}(6,6) -> 7* d1() -> 17* a0(6,6) -> 6* 6 -> 16* problem: DPs: TRS: a(p(),a(s(),x)) -> x Qed