tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APP(cons(z0,z1),z2) -> c14(APP(z1,z2)) APP(nil(),z0) -> c13() EMPTY(cons(z0,z1)) -> c7() EMPTY(nil()) -> c6() FSTSPLIT(0(),z0) -> c() FSTSPLIT(s(z0),cons(z1,z2)) -> c2(FSTSPLIT(z0,z2)) FSTSPLIT(s(z0),nil()) -> c1() IF1(z0,z1,false()) -> c19(IF3(z0,z1,empty(fstsplit(z1,app(map_f(self(),nil()),z0)))) ,EMPTY(fstsplit(z1,app(map_f(self(),nil()),z0))) ,FSTSPLIT(z1,app(map_f(self(),nil()),z0)) ,APP(map_f(self(),nil()),z0) ,MAP_F(self(),nil())) IF1(z0,z1,true()) -> c18(IF2(z0,z1,empty(fstsplit(z1,z0))),EMPTY(fstsplit(z1,z0)),FSTSPLIT(z1,z0)) IF2(z0,z1,false()) -> c20(PROCESS(app(map_f(self(),nil()),sndsplit(z1,z0)),z1) ,APP(map_f(self(),nil()),sndsplit(z1,z0)) ,MAP_F(self(),nil())) IF2(z0,z1,false()) -> c21(PROCESS(app(map_f(self(),nil()),sndsplit(z1,z0)),z1) ,APP(map_f(self(),nil()),sndsplit(z1,z0)) ,SNDSPLIT(z1,z0)) IF3(z0,z1,false()) -> c22(PROCESS(sndsplit(z1,app(map_f(self(),nil()),z0)),z1) ,SNDSPLIT(z1,app(map_f(self(),nil()),z0)) ,APP(map_f(self(),nil()),z0) ,MAP_F(self(),nil())) LENGTH(cons(z0,z1)) -> c12(LENGTH(z1)) LENGTH(nil()) -> c11() LEQ(0(),z0) -> c8() LEQ(s(z0),0()) -> c9() LEQ(s(z0),s(z1)) -> c10(LEQ(z0,z1)) MAP_F(z0,cons(z1,z2)) -> c16(APP(f(z0,z1),map_f(z0,z2)),MAP_F(z0,z2)) MAP_F(z0,nil()) -> c15() PROCESS(z0,z1) -> c17(IF1(z0,z1,leq(z1,length(z0))),LEQ(z1,length(z0)),LENGTH(z0)) SNDSPLIT(0(),z0) -> c3() SNDSPLIT(s(z0),cons(z1,z2)) -> c5(SNDSPLIT(z0,z2)) SNDSPLIT(s(z0),nil()) -> c4() - Weak TRS: app(cons(z0,z1),z2) -> cons(z0,app(z1,z2)) app(nil(),z0) -> z0 empty(cons(z0,z1)) -> false() empty(nil()) -> true() fstsplit(0(),z0) -> nil() fstsplit(s(z0),cons(z1,z2)) -> cons(z1,fstsplit(z0,z2)) fstsplit(s(z0),nil()) -> nil() if1(z0,z1,false()) -> if3(z0,z1,empty(fstsplit(z1,app(map_f(self(),nil()),z0)))) if1(z0,z1,true()) -> if2(z0,z1,empty(fstsplit(z1,z0))) if2(z0,z1,false()) -> process(app(map_f(self(),nil()),sndsplit(z1,z0)),z1) if3(z0,z1,false()) -> process(sndsplit(z1,app(map_f(self(),nil()),z0)),z1) length(cons(z0,z1)) -> s(length(z1)) length(nil()) -> 0() leq(0(),z0) -> true() leq(s(z0),0()) -> false() leq(s(z0),s(z1)) -> leq(z0,z1) map_f(z0,cons(z1,z2)) -> app(f(z0,z1),map_f(z0,z2)) map_f(z0,nil()) -> nil() process(z0,z1) -> if1(z0,z1,leq(z1,length(z0))) sndsplit(0(),z0) -> z0 sndsplit(s(z0),cons(z1,z2)) -> sndsplit(z0,z2) sndsplit(s(z0),nil()) -> nil() - Signature: {APP/2,EMPTY/1,FSTSPLIT/2,IF1/3,IF2/3,IF3/3,LENGTH/1,LEQ/2,MAP_F/2,PROCESS/2,SNDSPLIT/2,app/2,empty/1 ,fstsplit/2,if1/3,if2/3,if3/3,length/1,leq/2,map_f/2,process/2,sndsplit/2} / {0/0,c/0,c1/0,c10/1,c11/0,c12/1 ,c13/0,c14/1,c15/0,c16/2,c17/3,c18/3,c19/5,c2/1,c20/3,c21/3,c22/4,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,cons/2 ,f/2,false/0,nil/0,s/1,self/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,EMPTY,FSTSPLIT,IF1,IF2,IF3,LENGTH,LEQ,MAP_F,PROCESS ,SNDSPLIT,app,empty,fstsplit,if1,if2,if3,length,leq,map_f,process,sndsplit} and constructors {0,c,c1,c10,c11 ,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c3,c4,c5,c6,c7,c8,c9,cons,f,false,nil,s,self,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APP(cons(z0,z1),z2) -> c14(APP(z1,z2)) APP(nil(),z0) -> c13() EMPTY(cons(z0,z1)) -> c7() EMPTY(nil()) -> c6() FSTSPLIT(0(),z0) -> c() FSTSPLIT(s(z0),cons(z1,z2)) -> c2(FSTSPLIT(z0,z2)) FSTSPLIT(s(z0),nil()) -> c1() IF1(z0,z1,false()) -> c19(IF3(z0,z1,empty(fstsplit(z1,app(map_f(self(),nil()),z0)))) ,EMPTY(fstsplit(z1,app(map_f(self(),nil()),z0))) ,FSTSPLIT(z1,app(map_f(self(),nil()),z0)) ,APP(map_f(self(),nil()),z0) ,MAP_F(self(),nil())) IF1(z0,z1,true()) -> c18(IF2(z0,z1,empty(fstsplit(z1,z0))),EMPTY(fstsplit(z1,z0)),FSTSPLIT(z1,z0)) IF2(z0,z1,false()) -> c20(PROCESS(app(map_f(self(),nil()),sndsplit(z1,z0)),z1) ,APP(map_f(self(),nil()),sndsplit(z1,z0)) ,MAP_F(self(),nil())) IF2(z0,z1,false()) -> c21(PROCESS(app(map_f(self(),nil()),sndsplit(z1,z0)),z1) ,APP(map_f(self(),nil()),sndsplit(z1,z0)) ,SNDSPLIT(z1,z0)) IF3(z0,z1,false()) -> c22(PROCESS(sndsplit(z1,app(map_f(self(),nil()),z0)),z1) ,SNDSPLIT(z1,app(map_f(self(),nil()),z0)) ,APP(map_f(self(),nil()),z0) ,MAP_F(self(),nil())) LENGTH(cons(z0,z1)) -> c12(LENGTH(z1)) LENGTH(nil()) -> c11() LEQ(0(),z0) -> c8() LEQ(s(z0),0()) -> c9() LEQ(s(z0),s(z1)) -> c10(LEQ(z0,z1)) MAP_F(z0,cons(z1,z2)) -> c16(APP(f(z0,z1),map_f(z0,z2)),MAP_F(z0,z2)) MAP_F(z0,nil()) -> c15() PROCESS(z0,z1) -> c17(IF1(z0,z1,leq(z1,length(z0))),LEQ(z1,length(z0)),LENGTH(z0)) SNDSPLIT(0(),z0) -> c3() SNDSPLIT(s(z0),cons(z1,z2)) -> c5(SNDSPLIT(z0,z2)) SNDSPLIT(s(z0),nil()) -> c4() - Weak TRS: app(cons(z0,z1),z2) -> cons(z0,app(z1,z2)) app(nil(),z0) -> z0 empty(cons(z0,z1)) -> false() empty(nil()) -> true() fstsplit(0(),z0) -> nil() fstsplit(s(z0),cons(z1,z2)) -> cons(z1,fstsplit(z0,z2)) fstsplit(s(z0),nil()) -> nil() if1(z0,z1,false()) -> if3(z0,z1,empty(fstsplit(z1,app(map_f(self(),nil()),z0)))) if1(z0,z1,true()) -> if2(z0,z1,empty(fstsplit(z1,z0))) if2(z0,z1,false()) -> process(app(map_f(self(),nil()),sndsplit(z1,z0)),z1) if3(z0,z1,false()) -> process(sndsplit(z1,app(map_f(self(),nil()),z0)),z1) length(cons(z0,z1)) -> s(length(z1)) length(nil()) -> 0() leq(0(),z0) -> true() leq(s(z0),0()) -> false() leq(s(z0),s(z1)) -> leq(z0,z1) map_f(z0,cons(z1,z2)) -> app(f(z0,z1),map_f(z0,z2)) map_f(z0,nil()) -> nil() process(z0,z1) -> if1(z0,z1,leq(z1,length(z0))) sndsplit(0(),z0) -> z0 sndsplit(s(z0),cons(z1,z2)) -> sndsplit(z0,z2) sndsplit(s(z0),nil()) -> nil() - Signature: {APP/2,EMPTY/1,FSTSPLIT/2,IF1/3,IF2/3,IF3/3,LENGTH/1,LEQ/2,MAP_F/2,PROCESS/2,SNDSPLIT/2,app/2,empty/1 ,fstsplit/2,if1/3,if2/3,if3/3,length/1,leq/2,map_f/2,process/2,sndsplit/2} / {0/0,c/0,c1/0,c10/1,c11/0,c12/1 ,c13/0,c14/1,c15/0,c16/2,c17/3,c18/3,c19/5,c2/1,c20/3,c21/3,c22/4,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,cons/2 ,f/2,false/0,nil/0,s/1,self/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,EMPTY,FSTSPLIT,IF1,IF2,IF3,LENGTH,LEQ,MAP_F,PROCESS ,SNDSPLIT,app,empty,fstsplit,if1,if2,if3,length,leq,map_f,process,sndsplit} and constructors {0,c,c1,c10,c11 ,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c3,c4,c5,c6,c7,c8,c9,cons,f,false,nil,s,self,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APP(cons(z0,z1),z2) -> c14(APP(z1,z2)) APP(nil(),z0) -> c13() EMPTY(cons(z0,z1)) -> c7() EMPTY(nil()) -> c6() FSTSPLIT(0(),z0) -> c() FSTSPLIT(s(z0),cons(z1,z2)) -> c2(FSTSPLIT(z0,z2)) FSTSPLIT(s(z0),nil()) -> c1() IF1(z0,z1,false()) -> c19(IF3(z0,z1,empty(fstsplit(z1,app(map_f(self(),nil()),z0)))) ,EMPTY(fstsplit(z1,app(map_f(self(),nil()),z0))) ,FSTSPLIT(z1,app(map_f(self(),nil()),z0)) ,APP(map_f(self(),nil()),z0) ,MAP_F(self(),nil())) IF1(z0,z1,true()) -> c18(IF2(z0,z1,empty(fstsplit(z1,z0))),EMPTY(fstsplit(z1,z0)),FSTSPLIT(z1,z0)) IF2(z0,z1,false()) -> c20(PROCESS(app(map_f(self(),nil()),sndsplit(z1,z0)),z1) ,APP(map_f(self(),nil()),sndsplit(z1,z0)) ,MAP_F(self(),nil())) IF2(z0,z1,false()) -> c21(PROCESS(app(map_f(self(),nil()),sndsplit(z1,z0)),z1) ,APP(map_f(self(),nil()),sndsplit(z1,z0)) ,SNDSPLIT(z1,z0)) IF3(z0,z1,false()) -> c22(PROCESS(sndsplit(z1,app(map_f(self(),nil()),z0)),z1) ,SNDSPLIT(z1,app(map_f(self(),nil()),z0)) ,APP(map_f(self(),nil()),z0) ,MAP_F(self(),nil())) LENGTH(cons(z0,z1)) -> c12(LENGTH(z1)) LENGTH(nil()) -> c11() LEQ(0(),z0) -> c8() LEQ(s(z0),0()) -> c9() LEQ(s(z0),s(z1)) -> c10(LEQ(z0,z1)) MAP_F(z0,cons(z1,z2)) -> c16(APP(f(z0,z1),map_f(z0,z2)),MAP_F(z0,z2)) MAP_F(z0,nil()) -> c15() PROCESS(z0,z1) -> c17(IF1(z0,z1,leq(z1,length(z0))),LEQ(z1,length(z0)),LENGTH(z0)) SNDSPLIT(0(),z0) -> c3() SNDSPLIT(s(z0),cons(z1,z2)) -> c5(SNDSPLIT(z0,z2)) SNDSPLIT(s(z0),nil()) -> c4() - Weak TRS: app(cons(z0,z1),z2) -> cons(z0,app(z1,z2)) app(nil(),z0) -> z0 empty(cons(z0,z1)) -> false() empty(nil()) -> true() fstsplit(0(),z0) -> nil() fstsplit(s(z0),cons(z1,z2)) -> cons(z1,fstsplit(z0,z2)) fstsplit(s(z0),nil()) -> nil() if1(z0,z1,false()) -> if3(z0,z1,empty(fstsplit(z1,app(map_f(self(),nil()),z0)))) if1(z0,z1,true()) -> if2(z0,z1,empty(fstsplit(z1,z0))) if2(z0,z1,false()) -> process(app(map_f(self(),nil()),sndsplit(z1,z0)),z1) if3(z0,z1,false()) -> process(sndsplit(z1,app(map_f(self(),nil()),z0)),z1) length(cons(z0,z1)) -> s(length(z1)) length(nil()) -> 0() leq(0(),z0) -> true() leq(s(z0),0()) -> false() leq(s(z0),s(z1)) -> leq(z0,z1) map_f(z0,cons(z1,z2)) -> app(f(z0,z1),map_f(z0,z2)) map_f(z0,nil()) -> nil() process(z0,z1) -> if1(z0,z1,leq(z1,length(z0))) sndsplit(0(),z0) -> z0 sndsplit(s(z0),cons(z1,z2)) -> sndsplit(z0,z2) sndsplit(s(z0),nil()) -> nil() - Signature: {APP/2,EMPTY/1,FSTSPLIT/2,IF1/3,IF2/3,IF3/3,LENGTH/1,LEQ/2,MAP_F/2,PROCESS/2,SNDSPLIT/2,app/2,empty/1 ,fstsplit/2,if1/3,if2/3,if3/3,length/1,leq/2,map_f/2,process/2,sndsplit/2} / {0/0,c/0,c1/0,c10/1,c11/0,c12/1 ,c13/0,c14/1,c15/0,c16/2,c17/3,c18/3,c19/5,c2/1,c20/3,c21/3,c22/4,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,cons/2 ,f/2,false/0,nil/0,s/1,self/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,EMPTY,FSTSPLIT,IF1,IF2,IF3,LENGTH,LEQ,MAP_F,PROCESS ,SNDSPLIT,app,empty,fstsplit,if1,if2,if3,length,leq,map_f,process,sndsplit} and constructors {0,c,c1,c10,c11 ,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c3,c4,c5,c6,c7,c8,c9,cons,f,false,nil,s,self,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: APP(y,z){y -> cons(x,y)} = APP(cons(x,y),z) ->^+ c14(APP(y,z)) = C[APP(y,z) = APP(y,z){}] WORST_CASE(Omega(n^1),?)