MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a() -> b() a() -> c() double(0()) -> 0() double(s(x)) -> s(s(double(x))) droplast(cons(x,cons(y,xs))) -> cons(x,droplast(cons(y,xs))) droplast(cons(x,nil())) -> nil() droplast(nil()) -> nil() if(false(),x,y,z) -> loop(x,double(y),s(z)) if(true(),x,y,z) -> z ifmap(false(),xs,ys) -> mapIter(droplast(xs),cons(log(last(xs)),ys)) ifmap(true(),xs,ys) -> ys isempty(cons(x,xs)) -> false() isempty(nil()) -> true() last(cons(x,cons(y,xs))) -> last(cons(y,xs)) last(cons(x,nil())) -> x last(nil()) -> error() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) log(0()) -> logError() log(s(x)) -> loop(s(x),s(0()),0()) loop(x,s(y),z) -> if(le(x,s(y)),x,s(y),z) mapIter(xs,ys) -> ifmap(isempty(xs),xs,ys) maplog(xs) -> mapIter(xs,nil()) - Signature: {a/0,double/1,droplast/1,if/4,ifmap/3,isempty/1,last/1,le/2,log/1,loop/3,mapIter/2,maplog/1} / {0/0,b/0,c/0 ,cons/2,error/0,false/0,logError/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a,double,droplast,if,ifmap,isempty,last,le,log,loop ,mapIter,maplog} and constructors {0,b,c,cons,error,false,logError,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a#() -> c_1() a#() -> c_2() double#(0()) -> c_3() double#(s(x)) -> c_4(double#(x)) droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) droplast#(cons(x,nil())) -> c_6() droplast#(nil()) -> c_7() if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) if#(true(),x,y,z) -> c_9() ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) ifmap#(true(),xs,ys) -> c_11() isempty#(cons(x,xs)) -> c_12() isempty#(nil()) -> c_13() last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) last#(cons(x,nil())) -> c_15() last#(nil()) -> c_16() le#(0(),y) -> c_17() le#(s(x),0()) -> c_18() le#(s(x),s(y)) -> c_19(le#(x,y)) log#(0()) -> c_20() log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)) maplog#(xs) -> c_24(mapIter#(xs,nil())) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: a#() -> c_1() a#() -> c_2() double#(0()) -> c_3() double#(s(x)) -> c_4(double#(x)) droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) droplast#(cons(x,nil())) -> c_6() droplast#(nil()) -> c_7() if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) if#(true(),x,y,z) -> c_9() ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) ifmap#(true(),xs,ys) -> c_11() isempty#(cons(x,xs)) -> c_12() isempty#(nil()) -> c_13() last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) last#(cons(x,nil())) -> c_15() last#(nil()) -> c_16() le#(0(),y) -> c_17() le#(s(x),0()) -> c_18() le#(s(x),s(y)) -> c_19(le#(x,y)) log#(0()) -> c_20() log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)) maplog#(xs) -> c_24(mapIter#(xs,nil())) - Weak TRS: a() -> b() a() -> c() double(0()) -> 0() double(s(x)) -> s(s(double(x))) droplast(cons(x,cons(y,xs))) -> cons(x,droplast(cons(y,xs))) droplast(cons(x,nil())) -> nil() droplast(nil()) -> nil() if(false(),x,y,z) -> loop(x,double(y),s(z)) if(true(),x,y,z) -> z ifmap(false(),xs,ys) -> mapIter(droplast(xs),cons(log(last(xs)),ys)) ifmap(true(),xs,ys) -> ys isempty(cons(x,xs)) -> false() isempty(nil()) -> true() last(cons(x,cons(y,xs))) -> last(cons(y,xs)) last(cons(x,nil())) -> x last(nil()) -> error() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) log(0()) -> logError() log(s(x)) -> loop(s(x),s(0()),0()) loop(x,s(y),z) -> if(le(x,s(y)),x,s(y),z) mapIter(xs,ys) -> ifmap(isempty(xs),xs,ys) maplog(xs) -> mapIter(xs,nil()) - Signature: {a/0,double/1,droplast/1,if/4,ifmap/3,isempty/1,last/1,le/2,log/1,loop/3,mapIter/2,maplog/1,a#/0,double#/1 ,droplast#/1,if#/4,ifmap#/3,isempty#/1,last#/1,le#/2,log#/1,loop#/3,mapIter#/2,maplog#/1} / {0/0,b/0,c/0 ,cons/2,error/0,false/0,logError/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/2,c_9/0 ,c_10/4,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/1,c_22/2,c_23/2,c_24/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,double#,droplast#,if#,ifmap#,isempty#,last#,le#,log# ,loop#,mapIter#,maplog#} and constructors {0,b,c,cons,error,false,logError,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: double(0()) -> 0() double(s(x)) -> s(s(double(x))) droplast(cons(x,cons(y,xs))) -> cons(x,droplast(cons(y,xs))) droplast(cons(x,nil())) -> nil() droplast(nil()) -> nil() if(false(),x,y,z) -> loop(x,double(y),s(z)) if(true(),x,y,z) -> z isempty(cons(x,xs)) -> false() isempty(nil()) -> true() last(cons(x,cons(y,xs))) -> last(cons(y,xs)) last(cons(x,nil())) -> x last(nil()) -> error() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) log(0()) -> logError() log(s(x)) -> loop(s(x),s(0()),0()) loop(x,s(y),z) -> if(le(x,s(y)),x,s(y),z) a#() -> c_1() a#() -> c_2() double#(0()) -> c_3() double#(s(x)) -> c_4(double#(x)) droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) droplast#(cons(x,nil())) -> c_6() droplast#(nil()) -> c_7() if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) if#(true(),x,y,z) -> c_9() ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) ifmap#(true(),xs,ys) -> c_11() isempty#(cons(x,xs)) -> c_12() isempty#(nil()) -> c_13() last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) last#(cons(x,nil())) -> c_15() last#(nil()) -> c_16() le#(0(),y) -> c_17() le#(s(x),0()) -> c_18() le#(s(x),s(y)) -> c_19(le#(x,y)) log#(0()) -> c_20() log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)) maplog#(xs) -> c_24(mapIter#(xs,nil())) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a#() -> c_1() a#() -> c_2() double#(0()) -> c_3() double#(s(x)) -> c_4(double#(x)) droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) droplast#(cons(x,nil())) -> c_6() droplast#(nil()) -> c_7() if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) if#(true(),x,y,z) -> c_9() ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) ifmap#(true(),xs,ys) -> c_11() isempty#(cons(x,xs)) -> c_12() isempty#(nil()) -> c_13() last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) last#(cons(x,nil())) -> c_15() last#(nil()) -> c_16() le#(0(),y) -> c_17() le#(s(x),0()) -> c_18() le#(s(x),s(y)) -> c_19(le#(x,y)) log#(0()) -> c_20() log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)) maplog#(xs) -> c_24(mapIter#(xs,nil())) - Weak TRS: double(0()) -> 0() double(s(x)) -> s(s(double(x))) droplast(cons(x,cons(y,xs))) -> cons(x,droplast(cons(y,xs))) droplast(cons(x,nil())) -> nil() droplast(nil()) -> nil() if(false(),x,y,z) -> loop(x,double(y),s(z)) if(true(),x,y,z) -> z isempty(cons(x,xs)) -> false() isempty(nil()) -> true() last(cons(x,cons(y,xs))) -> last(cons(y,xs)) last(cons(x,nil())) -> x last(nil()) -> error() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) log(0()) -> logError() log(s(x)) -> loop(s(x),s(0()),0()) loop(x,s(y),z) -> if(le(x,s(y)),x,s(y),z) - Signature: {a/0,double/1,droplast/1,if/4,ifmap/3,isempty/1,last/1,le/2,log/1,loop/3,mapIter/2,maplog/1,a#/0,double#/1 ,droplast#/1,if#/4,ifmap#/3,isempty#/1,last#/1,le#/2,log#/1,loop#/3,mapIter#/2,maplog#/1} / {0/0,b/0,c/0 ,cons/2,error/0,false/0,logError/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/2,c_9/0 ,c_10/4,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/1,c_22/2,c_23/2,c_24/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,double#,droplast#,if#,ifmap#,isempty#,last#,le#,log# ,loop#,mapIter#,maplog#} and constructors {0,b,c,cons,error,false,logError,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,6,7,9,11,12,13,15,16,17,18,20} by application of Pre({1,2,3,6,7,9,11,12,13,15,16,17,18,20}) = {4,5,8,10,14,19,22,23}. Here rules are labelled as follows: 1: a#() -> c_1() 2: a#() -> c_2() 3: double#(0()) -> c_3() 4: double#(s(x)) -> c_4(double#(x)) 5: droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) 6: droplast#(cons(x,nil())) -> c_6() 7: droplast#(nil()) -> c_7() 8: if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) 9: if#(true(),x,y,z) -> c_9() 10: ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) 11: ifmap#(true(),xs,ys) -> c_11() 12: isempty#(cons(x,xs)) -> c_12() 13: isempty#(nil()) -> c_13() 14: last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) 15: last#(cons(x,nil())) -> c_15() 16: last#(nil()) -> c_16() 17: le#(0(),y) -> c_17() 18: le#(s(x),0()) -> c_18() 19: le#(s(x),s(y)) -> c_19(le#(x,y)) 20: log#(0()) -> c_20() 21: log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) 22: loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) 23: mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)) 24: maplog#(xs) -> c_24(mapIter#(xs,nil())) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: double#(s(x)) -> c_4(double#(x)) droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) le#(s(x),s(y)) -> c_19(le#(x,y)) log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)) maplog#(xs) -> c_24(mapIter#(xs,nil())) - Weak DPs: a#() -> c_1() a#() -> c_2() double#(0()) -> c_3() droplast#(cons(x,nil())) -> c_6() droplast#(nil()) -> c_7() if#(true(),x,y,z) -> c_9() ifmap#(true(),xs,ys) -> c_11() isempty#(cons(x,xs)) -> c_12() isempty#(nil()) -> c_13() last#(cons(x,nil())) -> c_15() last#(nil()) -> c_16() le#(0(),y) -> c_17() le#(s(x),0()) -> c_18() log#(0()) -> c_20() - Weak TRS: double(0()) -> 0() double(s(x)) -> s(s(double(x))) droplast(cons(x,cons(y,xs))) -> cons(x,droplast(cons(y,xs))) droplast(cons(x,nil())) -> nil() droplast(nil()) -> nil() if(false(),x,y,z) -> loop(x,double(y),s(z)) if(true(),x,y,z) -> z isempty(cons(x,xs)) -> false() isempty(nil()) -> true() last(cons(x,cons(y,xs))) -> last(cons(y,xs)) last(cons(x,nil())) -> x last(nil()) -> error() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) log(0()) -> logError() log(s(x)) -> loop(s(x),s(0()),0()) loop(x,s(y),z) -> if(le(x,s(y)),x,s(y),z) - Signature: {a/0,double/1,droplast/1,if/4,ifmap/3,isempty/1,last/1,le/2,log/1,loop/3,mapIter/2,maplog/1,a#/0,double#/1 ,droplast#/1,if#/4,ifmap#/3,isempty#/1,last#/1,le#/2,log#/1,loop#/3,mapIter#/2,maplog#/1} / {0/0,b/0,c/0 ,cons/2,error/0,false/0,logError/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/2,c_9/0 ,c_10/4,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/1,c_22/2,c_23/2,c_24/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,double#,droplast#,if#,ifmap#,isempty#,last#,le#,log# ,loop#,mapIter#,maplog#} and constructors {0,b,c,cons,error,false,logError,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:double#(s(x)) -> c_4(double#(x)) -->_1 double#(0()) -> c_3():13 -->_1 double#(s(x)) -> c_4(double#(x)):1 2:S:droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) -->_1 droplast#(cons(x,nil())) -> c_6():14 -->_1 droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))):2 3:S:if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) -->_1 loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))):8 -->_2 double#(0()) -> c_3():13 -->_2 double#(s(x)) -> c_4(double#(x)):1 4:S:ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) -->_1 mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)):9 -->_3 log#(s(x)) -> c_21(loop#(s(x),s(0()),0())):7 -->_4 last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))):5 -->_3 log#(0()) -> c_20():24 -->_4 last#(nil()) -> c_16():21 -->_4 last#(cons(x,nil())) -> c_15():20 -->_2 droplast#(nil()) -> c_7():15 -->_2 droplast#(cons(x,nil())) -> c_6():14 -->_2 droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))):2 5:S:last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) -->_1 last#(cons(x,nil())) -> c_15():20 -->_1 last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))):5 6:S:le#(s(x),s(y)) -> c_19(le#(x,y)) -->_1 le#(s(x),0()) -> c_18():23 -->_1 le#(0(),y) -> c_17():22 -->_1 le#(s(x),s(y)) -> c_19(le#(x,y)):6 7:S:log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) -->_1 loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))):8 8:S:loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) -->_2 le#(0(),y) -> c_17():22 -->_1 if#(true(),x,y,z) -> c_9():16 -->_2 le#(s(x),s(y)) -> c_19(le#(x,y)):6 -->_1 if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)):3 9:S:mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)) -->_2 isempty#(nil()) -> c_13():19 -->_2 isempty#(cons(x,xs)) -> c_12():18 -->_1 ifmap#(true(),xs,ys) -> c_11():17 -->_1 ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)):4 10:S:maplog#(xs) -> c_24(mapIter#(xs,nil())) -->_1 mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)):9 11:W:a#() -> c_1() 12:W:a#() -> c_2() 13:W:double#(0()) -> c_3() 14:W:droplast#(cons(x,nil())) -> c_6() 15:W:droplast#(nil()) -> c_7() 16:W:if#(true(),x,y,z) -> c_9() 17:W:ifmap#(true(),xs,ys) -> c_11() 18:W:isempty#(cons(x,xs)) -> c_12() 19:W:isempty#(nil()) -> c_13() 20:W:last#(cons(x,nil())) -> c_15() 21:W:last#(nil()) -> c_16() 22:W:le#(0(),y) -> c_17() 23:W:le#(s(x),0()) -> c_18() 24:W:log#(0()) -> c_20() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: a#() -> c_2() 11: a#() -> c_1() 15: droplast#(nil()) -> c_7() 21: last#(nil()) -> c_16() 24: log#(0()) -> c_20() 20: last#(cons(x,nil())) -> c_15() 17: ifmap#(true(),xs,ys) -> c_11() 18: isempty#(cons(x,xs)) -> c_12() 19: isempty#(nil()) -> c_13() 23: le#(s(x),0()) -> c_18() 16: if#(true(),x,y,z) -> c_9() 22: le#(0(),y) -> c_17() 14: droplast#(cons(x,nil())) -> c_6() 13: double#(0()) -> c_3() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: double#(s(x)) -> c_4(double#(x)) droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) le#(s(x),s(y)) -> c_19(le#(x,y)) log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)) maplog#(xs) -> c_24(mapIter#(xs,nil())) - Weak TRS: double(0()) -> 0() double(s(x)) -> s(s(double(x))) droplast(cons(x,cons(y,xs))) -> cons(x,droplast(cons(y,xs))) droplast(cons(x,nil())) -> nil() droplast(nil()) -> nil() if(false(),x,y,z) -> loop(x,double(y),s(z)) if(true(),x,y,z) -> z isempty(cons(x,xs)) -> false() isempty(nil()) -> true() last(cons(x,cons(y,xs))) -> last(cons(y,xs)) last(cons(x,nil())) -> x last(nil()) -> error() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) log(0()) -> logError() log(s(x)) -> loop(s(x),s(0()),0()) loop(x,s(y),z) -> if(le(x,s(y)),x,s(y),z) - Signature: {a/0,double/1,droplast/1,if/4,ifmap/3,isempty/1,last/1,le/2,log/1,loop/3,mapIter/2,maplog/1,a#/0,double#/1 ,droplast#/1,if#/4,ifmap#/3,isempty#/1,last#/1,le#/2,log#/1,loop#/3,mapIter#/2,maplog#/1} / {0/0,b/0,c/0 ,cons/2,error/0,false/0,logError/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/2,c_9/0 ,c_10/4,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/1,c_22/2,c_23/2,c_24/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,double#,droplast#,if#,ifmap#,isempty#,last#,le#,log# ,loop#,mapIter#,maplog#} and constructors {0,b,c,cons,error,false,logError,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:double#(s(x)) -> c_4(double#(x)) -->_1 double#(s(x)) -> c_4(double#(x)):1 2:S:droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) -->_1 droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))):2 3:S:if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) -->_1 loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))):8 -->_2 double#(s(x)) -> c_4(double#(x)):1 4:S:ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) -->_1 mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)):9 -->_3 log#(s(x)) -> c_21(loop#(s(x),s(0()),0())):7 -->_4 last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))):5 -->_2 droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))):2 5:S:last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) -->_1 last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))):5 6:S:le#(s(x),s(y)) -> c_19(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_19(le#(x,y)):6 7:S:log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) -->_1 loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))):8 8:S:loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) -->_2 le#(s(x),s(y)) -> c_19(le#(x,y)):6 -->_1 if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)):3 9:S:mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)) -->_1 ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)):4 10:S:maplog#(xs) -> c_24(mapIter#(xs,nil())) -->_1 mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys),isempty#(xs)):9 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys)) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: double#(s(x)) -> c_4(double#(x)) droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) le#(s(x),s(y)) -> c_19(le#(x,y)) log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys)) maplog#(xs) -> c_24(mapIter#(xs,nil())) - Weak TRS: double(0()) -> 0() double(s(x)) -> s(s(double(x))) droplast(cons(x,cons(y,xs))) -> cons(x,droplast(cons(y,xs))) droplast(cons(x,nil())) -> nil() droplast(nil()) -> nil() if(false(),x,y,z) -> loop(x,double(y),s(z)) if(true(),x,y,z) -> z isempty(cons(x,xs)) -> false() isempty(nil()) -> true() last(cons(x,cons(y,xs))) -> last(cons(y,xs)) last(cons(x,nil())) -> x last(nil()) -> error() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) log(0()) -> logError() log(s(x)) -> loop(s(x),s(0()),0()) loop(x,s(y),z) -> if(le(x,s(y)),x,s(y),z) - Signature: {a/0,double/1,droplast/1,if/4,ifmap/3,isempty/1,last/1,le/2,log/1,loop/3,mapIter/2,maplog/1,a#/0,double#/1 ,droplast#/1,if#/4,ifmap#/3,isempty#/1,last#/1,le#/2,log#/1,loop#/3,mapIter#/2,maplog#/1} / {0/0,b/0,c/0 ,cons/2,error/0,false/0,logError/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/2,c_9/0 ,c_10/4,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/1,c_22/2,c_23/1,c_24/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,double#,droplast#,if#,ifmap#,isempty#,last#,le#,log# ,loop#,mapIter#,maplog#} and constructors {0,b,c,cons,error,false,logError,nil,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:double#(s(x)) -> c_4(double#(x)) -->_1 double#(s(x)) -> c_4(double#(x)):1 2:S:droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) -->_1 droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))):2 3:S:if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) -->_1 loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))):8 -->_2 double#(s(x)) -> c_4(double#(x)):1 4:S:ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) -->_1 mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys)):9 -->_3 log#(s(x)) -> c_21(loop#(s(x),s(0()),0())):7 -->_4 last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))):5 -->_2 droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))):2 5:S:last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) -->_1 last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))):5 6:S:le#(s(x),s(y)) -> c_19(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_19(le#(x,y)):6 7:S:log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) -->_1 loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))):8 8:S:loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) -->_2 le#(s(x),s(y)) -> c_19(le#(x,y)):6 -->_1 if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)):3 9:S:mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys)) -->_1 ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)):4 10:S:maplog#(xs) -> c_24(mapIter#(xs,nil())) -->_1 mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys)):9 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(10,maplog#(xs) -> c_24(mapIter#(xs,nil())))] * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: double#(s(x)) -> c_4(double#(x)) droplast#(cons(x,cons(y,xs))) -> c_5(droplast#(cons(y,xs))) if#(false(),x,y,z) -> c_8(loop#(x,double(y),s(z)),double#(y)) ifmap#(false(),xs,ys) -> c_10(mapIter#(droplast(xs),cons(log(last(xs)),ys)) ,droplast#(xs) ,log#(last(xs)) ,last#(xs)) last#(cons(x,cons(y,xs))) -> c_14(last#(cons(y,xs))) le#(s(x),s(y)) -> c_19(le#(x,y)) log#(s(x)) -> c_21(loop#(s(x),s(0()),0())) loop#(x,s(y),z) -> c_22(if#(le(x,s(y)),x,s(y),z),le#(x,s(y))) mapIter#(xs,ys) -> c_23(ifmap#(isempty(xs),xs,ys)) - Weak TRS: double(0()) -> 0() double(s(x)) -> s(s(double(x))) droplast(cons(x,cons(y,xs))) -> cons(x,droplast(cons(y,xs))) droplast(cons(x,nil())) -> nil() droplast(nil()) -> nil() if(false(),x,y,z) -> loop(x,double(y),s(z)) if(true(),x,y,z) -> z isempty(cons(x,xs)) -> false() isempty(nil()) -> true() last(cons(x,cons(y,xs))) -> last(cons(y,xs)) last(cons(x,nil())) -> x last(nil()) -> error() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) log(0()) -> logError() log(s(x)) -> loop(s(x),s(0()),0()) loop(x,s(y),z) -> if(le(x,s(y)),x,s(y),z) - Signature: {a/0,double/1,droplast/1,if/4,ifmap/3,isempty/1,last/1,le/2,log/1,loop/3,mapIter/2,maplog/1,a#/0,double#/1 ,droplast#/1,if#/4,ifmap#/3,isempty#/1,last#/1,le#/2,log#/1,loop#/3,mapIter#/2,maplog#/1} / {0/0,b/0,c/0 ,cons/2,error/0,false/0,logError/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/2,c_9/0 ,c_10/4,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/1,c_22/2,c_23/1,c_24/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,double#,droplast#,if#,ifmap#,isempty#,last#,le#,log# ,loop#,mapIter#,maplog#} and constructors {0,b,c,cons,error,false,logError,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE