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: 1 enrichment: match-dp automaton: final states: {8} transitions: a{#,0}(4,10) -> 8* f0() -> 4* a0(3,1) -> 3* a0(3,3) -> 3* a0(3,5) -> 3* a0(4,2) -> 3* a0(4,4) -> 3* a0(4,6) -> 3* a0(5,1) -> 3* a0(5,3) -> 3* a0(5,5) -> 3* a0(6,2) -> 3* a0(1,2) -> 3* a0(6,4) -> 3* a0(1,4) -> 3* a0(6,6) -> 3* a0(1,6) -> 3* a0(2,1) -> 3* a0(2,3) -> 3* a0(2,5) -> 3* a0(2,7) -> 9* a0(3,2) -> 3* a0(3,4) -> 3* a0(3,6) -> 3* a0(4,1) -> 3* a0(4,3) -> 3* a0(4,5) -> 3* a0(5,2) -> 3* a0(5,4) -> 3* a0(5,6) -> 3* a0(6,1) -> 3* a0(1,1) -> 3* a0(6,3) -> 3* a0(1,3) -> 3* a0(6,5) -> 3* a0(1,5) -> 3* a0(1,9) -> 10* a0(2,2) -> 3* a0(2,4) -> 3* a0(2,6) -> 3* s0() -> 2* p0() -> 1* 00() -> 3,5 d0() -> 6* a{#,1}(20,19) -> 8* f1() -> 20* a1(18,17) -> 19* a1(16,2) -> 17* a1(16,4) -> 17* a1(16,6) -> 17* a1(16,1) -> 17* a1(16,3) -> 17* a1(16,5) -> 17* p1() -> 18* s1() -> 16* 1 -> 19,3,7 2 -> 19,3,7 3 -> 19,7 4 -> 19,3,7 5 -> 3,7 6 -> 19,3,7 7 -> 10* 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: 1 enrichment: match-dp automaton: final states: {8} transitions: a{#,0}(4,10) -> 8* f0() -> 5* a0(3,1) -> 3* a0(3,3) -> 3* a0(3,5) -> 3* a0(4,2) -> 3* a0(4,4) -> 3* a0(4,6) -> 3* a0(5,1) -> 3* a0(5,3) -> 3* a0(5,5) -> 3* a0(6,2) -> 3* a0(1,2) -> 3* a0(6,4) -> 3* a0(1,4) -> 3* a0(6,6) -> 3* a0(1,6) -> 3* a0(2,1) -> 3* a0(2,3) -> 3* a0(2,5) -> 3* a0(2,7) -> 9* a0(3,2) -> 3* a0(3,4) -> 3* a0(3,6) -> 3* a0(4,1) -> 3* a0(4,3) -> 3* a0(4,5) -> 3* a0(5,2) -> 3* a0(5,4) -> 3* a0(5,6) -> 3* a0(6,1) -> 3* a0(1,1) -> 3* a0(6,3) -> 3* a0(1,3) -> 3* a0(6,5) -> 3* a0(1,5) -> 3* a0(1,9) -> 10* a0(2,2) -> 3* a0(2,4) -> 3* a0(2,6) -> 3* s0() -> 2* p0() -> 1* 00() -> 3,6 d0() -> 4* a{#,1}(20,19) -> 8* a1(18,17) -> 19* a1(16,2) -> 17* a1(16,4) -> 17* a1(16,6) -> 17* a1(16,1) -> 17* a1(16,3) -> 17* a1(16,5) -> 17* p1() -> 18* s1() -> 16* d1() -> 20* 1 -> 19,3,7 2 -> 19,3,7 3 -> 19,7 4 -> 19,3,7 5 -> 3,7 6 -> 19,3,7 7 -> 10* 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