YES Problem: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) -> 0() app(app(times(),app(s(),x)),y) -> app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) -> app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) -> app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) Proof: DP Processor: DPs: app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(times(),app(s(),x)),y) -> app#(times(),x) app#(app(times(),app(s(),x)),y) -> app#(app(times(),x),y) app#(app(times(),app(s(),x)),y) -> app#(plus(),app(app(times(),x),y)) app#(app(times(),app(s(),x)),y) -> app#(app(plus(),app(app(times(),x),y)),y) app#(inc(),xs) -> app#(s(),0()) app#(inc(),xs) -> app#(plus(),app(s(),0())) app#(inc(),xs) -> app#(map(),app(plus(),app(s(),0()))) app#(inc(),xs) -> app#(app(map(),app(plus(),app(s(),0()))),xs) app#(double(),xs) -> app#(s(),0()) app#(double(),xs) -> app#(s(),app(s(),0())) app#(double(),xs) -> app#(times(),app(s(),app(s(),0()))) app#(double(),xs) -> app#(map(),app(times(),app(s(),app(s(),0())))) app#(double(),xs) -> app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) -> 0() app(app(times(),app(s(),x)),y) -> app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) -> app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) -> app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) EDG Processor: DPs: app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(times(),app(s(),x)),y) -> app#(times(),x) app#(app(times(),app(s(),x)),y) -> app#(app(times(),x),y) app#(app(times(),app(s(),x)),y) -> app#(plus(),app(app(times(),x),y)) app#(app(times(),app(s(),x)),y) -> app#(app(plus(),app(app(times(),x),y)),y) app#(inc(),xs) -> app#(s(),0()) app#(inc(),xs) -> app#(plus(),app(s(),0())) app#(inc(),xs) -> app#(map(),app(plus(),app(s(),0()))) app#(inc(),xs) -> app#(app(map(),app(plus(),app(s(),0()))),xs) app#(double(),xs) -> app#(s(),0()) app#(double(),xs) -> app#(s(),app(s(),0())) app#(double(),xs) -> app#(times(),app(s(),app(s(),0()))) app#(double(),xs) -> app#(map(),app(times(),app(s(),app(s(),0())))) app#(double(),xs) -> app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) -> 0() app(app(times(),app(s(),x)),y) -> app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) -> app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) -> app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) graph: app#(double(),xs) -> app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(double(),xs) -> app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(double(),xs) -> app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(double(),xs) -> app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(inc(),xs) -> app#(app(map(),app(plus(),app(s(),0()))),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(inc(),xs) -> app#(app(map(),app(plus(),app(s(),0()))),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(inc(),xs) -> app#(app(map(),app(plus(),app(s(),0()))),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(inc(),xs) -> app#(app(map(),app(plus(),app(s(),0()))),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(times(),app(s(),x)),y) -> app#(times(),x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(times(),app(s(),x)),y) -> app#(app(times(),x),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(times(),app(s(),x)),y) -> app#(plus(),app(app(times(),x),y)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(times(),app(s(),x)),y) -> app#(app(plus(),app(app(times(),x),y)),y) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(inc(),xs) -> app#(s(),0()) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(inc(),xs) -> app#(plus(),app(s(),0())) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(inc(),xs) -> app#(map(),app(plus(),app(s(),0()))) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(inc(),xs) -> app#(app(map(),app(plus(),app(s(),0()))),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),xs) -> app#(s(),0()) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),xs) -> app#(s(),app(s(),0())) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),xs) -> app#(times(),app(s(),app(s(),0()))) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),xs) -> app#(map(),app(times(),app(s(),app(s(),0())))) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(double(),xs) -> app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) -> app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) app#(app(times(),app(s(),x)),y) -> app#(app(times(),x),y) -> app#(app(times(),app(s(),x)),y) -> app#(times(),x) app#(app(times(),app(s(),x)),y) -> app#(app(times(),x),y) -> app#(app(times(),app(s(),x)),y) -> app#(app(times(),x),y) app#(app(times(),app(s(),x)),y) -> app#(app(times(),x),y) -> app#(app(times(),app(s(),x)),y) -> app#(plus(),app(app(times(),x),y)) app#(app(times(),app(s(),x)),y) -> app#(app(times(),x),y) -> app#(app(times(),app(s(),x)),y) -> app#(app(plus(),app(app(times(),x),y)),y) app#(app(times(),app(s(),x)),y) -> app#(app(plus(),app(app(times(),x),y)),y) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(times(),app(s(),x)),y) -> app#(app(plus(),app(app(times(),x),y)),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(times(),app(s(),x)),y) -> app#(app(plus(),app(app(times(),x),y)),y) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) SCC Processor: #sccs: 3 #rules: 6 #arcs: 42/400 DPs: app#(double(),xs) -> app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) app#(inc(),xs) -> app#(app(map(),app(plus(),app(s(),0()))),xs) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) -> 0() app(app(times(),app(s(),x)),y) -> app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) -> app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) -> app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) Subterm Criterion Processor: simple projection: pi(app#) = 1 problem: DPs: app#(double(),xs) -> app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) app#(inc(),xs) -> app#(app(map(),app(plus(),app(s(),0()))),xs) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) -> 0() app(app(times(),app(s(),x)),y) -> app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) -> app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) -> app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x0, [cons] = 0, [nil] = 0, [double] = 0, [map] = 0, [inc] = 1, [times] = 0, [s] = 0, [app](x0, x1) = x1, [0] = 0, [plus] = 0 orientation: app#(double(),xs) = 0 >= 0 = app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) app#(inc(),xs) = 1 >= 0 = app#(app(map(),app(plus(),app(s(),0()))),xs) app(app(plus(),0()),y) = y >= y = y app(app(plus(),app(s(),x)),y) = y >= y = app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) = y >= 0 = 0() app(app(times(),app(s(),x)),y) = y >= y = app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) = xs >= xs = app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) = xs >= xs = app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) = 0 >= 0 = nil() app(app(map(),f),app(app(cons(),x),xs)) = xs >= xs = app(app(cons(),app(f,x)),app(app(map(),f),xs)) problem: DPs: app#(double(),xs) -> app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) -> 0() app(app(times(),app(s(),x)),y) -> app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) -> app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) -> app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x0, [cons] = 0, [nil] = 0, [double] = 1, [map] = 0, [inc] = 0, [times] = 0, [s] = 0, [app](x0, x1) = x1, [0] = 0, [plus] = 0 orientation: app#(double(),xs) = 1 >= 0 = app#(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(plus(),0()),y) = y >= y = y app(app(plus(),app(s(),x)),y) = y >= y = app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) = y >= 0 = 0() app(app(times(),app(s(),x)),y) = y >= y = app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) = xs >= xs = app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) = xs >= xs = app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) = 0 >= 0 = nil() app(app(map(),f),app(app(cons(),x),xs)) = xs >= xs = app(app(cons(),app(f,x)),app(app(map(),f),xs)) problem: DPs: TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) -> 0() app(app(times(),app(s(),x)),y) -> app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) -> app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) -> app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) Qed DPs: app#(app(times(),app(s(),x)),y) -> app#(app(times(),x),y) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) -> 0() app(app(times(),app(s(),x)),y) -> app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) -> app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) -> app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) Usable Rule Processor: DPs: app#(app(times(),app(s(),x)),y) -> app#(app(times(),x),y) TRS: Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {5} transitions: app1(7,1) -> 8* app1(7,3) -> 8* app1(7,2) -> 8* times1() -> 7* app{#,0}(6,4) -> 5* app0(3,1) -> 3* app0(3,3) -> 3* app0(1,2) -> 3* app0(2,1) -> 3* app0(2,3) -> 3* app0(3,2) -> 3* app0(1,1) -> 3* app0(1,3) -> 3* app0(2,2) -> 3* app0(2,4) -> 6* times0() -> 2* s0() -> 1* app{#,1}(8,4) -> 5* 1 -> 4* 2 -> 4* 3 -> 4* problem: DPs: TRS: Qed DPs: app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(times(),0()),y) -> 0() app(app(times(),app(s(),x)),y) -> app(app(plus(),app(app(times(),x),y)),y) app(inc(),xs) -> app(app(map(),app(plus(),app(s(),0()))),xs) app(double(),xs) -> app(app(map(),app(times(),app(s(),app(s(),0())))),xs) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) Usable Rule Processor: DPs: app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) TRS: Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {5} transitions: app1(7,1) -> 8* app1(7,3) -> 8* app1(7,2) -> 8* plus0() -> 2* plus1() -> 7* app{#,0}(6,4) -> 5* app0(3,1) -> 3* app0(3,3) -> 3* app0(1,2) -> 3* app0(2,1) -> 3* app0(2,3) -> 3* app0(3,2) -> 3* app0(1,1) -> 3* app0(1,3) -> 3* app0(2,2) -> 3* app0(2,4) -> 6* s0() -> 1* app{#,1}(8,4) -> 5* 1 -> 4* 2 -> 4* 3 -> 4* problem: DPs: TRS: Qed