MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: app(cons(h,t),x) -> cons(h,app(t,x)) app(nil(),x) -> x empty(cons(h,t)) -> false() empty(nil()) -> true() fstsplit(0(),x) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) fstsplit(s(n),nil()) -> nil() if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if2(store,m,false()) -> process(app(map_f(self(),nil()),sndsplit(m,store)),m) if3(store,m,false()) -> process(sndsplit(m,app(map_f(self(),nil()),store)),m) length(cons(h,t)) -> s(length(t)) length(nil()) -> 0() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) map_f(pid,nil()) -> nil() process(store,m) -> if1(store,m,leq(m,length(store))) sndsplit(0(),x) -> x sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) sndsplit(s(n),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} / {0/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} and constructors {0,cons,f,false,nil,s,self,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs app#(cons(h,t),x) -> c_1(app#(t,x)) app#(nil(),x) -> c_2() empty#(cons(h,t)) -> c_3() empty#(nil()) -> c_4() fstsplit#(0(),x) -> c_5() fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) fstsplit#(s(n),nil()) -> c_7() if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)) if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)) if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) length#(cons(h,t)) -> c_12(length#(t)) length#(nil()) -> c_13() leq#(0(),m) -> c_14() leq#(s(n),0()) -> c_15() leq#(s(n),s(m)) -> c_16(leq#(n,m)) map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)) map_f#(pid,nil()) -> c_18() process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) sndsplit#(0(),x) -> c_20() sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) sndsplit#(s(n),nil()) -> c_22() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: app#(cons(h,t),x) -> c_1(app#(t,x)) app#(nil(),x) -> c_2() empty#(cons(h,t)) -> c_3() empty#(nil()) -> c_4() fstsplit#(0(),x) -> c_5() fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) fstsplit#(s(n),nil()) -> c_7() if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)) if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)) if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) length#(cons(h,t)) -> c_12(length#(t)) length#(nil()) -> c_13() leq#(0(),m) -> c_14() leq#(s(n),0()) -> c_15() leq#(s(n),s(m)) -> c_16(leq#(n,m)) map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)) map_f#(pid,nil()) -> c_18() process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) sndsplit#(0(),x) -> c_20() sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) sndsplit#(s(n),nil()) -> c_22() - Weak TRS: app(cons(h,t),x) -> cons(h,app(t,x)) app(nil(),x) -> x empty(cons(h,t)) -> false() empty(nil()) -> true() fstsplit(0(),x) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) fstsplit(s(n),nil()) -> nil() if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if2(store,m,false()) -> process(app(map_f(self(),nil()),sndsplit(m,store)),m) if3(store,m,false()) -> process(sndsplit(m,app(map_f(self(),nil()),store)),m) length(cons(h,t)) -> s(length(t)) length(nil()) -> 0() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) map_f(pid,nil()) -> nil() process(store,m) -> if1(store,m,leq(m,length(store))) sndsplit(0(),x) -> x sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) sndsplit(s(n),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,cons/2,f/2 ,false/0,nil/0,s/1,self/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/5,c_9/3,c_10/4,c_11/4,c_12/1 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/2,c_18/0,c_19/3,c_20/0,c_21/1,c_22/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,empty#,fstsplit#,if1#,if2#,if3#,length#,leq#,map_f# ,process#,sndsplit#} and constructors {0,cons,f,false,nil,s,self,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: app(cons(h,t),x) -> cons(h,app(t,x)) app(nil(),x) -> x empty(cons(h,t)) -> false() empty(nil()) -> true() fstsplit(0(),x) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) fstsplit(s(n),nil()) -> nil() length(cons(h,t)) -> s(length(t)) length(nil()) -> 0() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) map_f(pid,nil()) -> nil() sndsplit(0(),x) -> x sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) sndsplit(s(n),nil()) -> nil() app#(cons(h,t),x) -> c_1(app#(t,x)) app#(nil(),x) -> c_2() empty#(cons(h,t)) -> c_3() empty#(nil()) -> c_4() fstsplit#(0(),x) -> c_5() fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) fstsplit#(s(n),nil()) -> c_7() if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)) if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)) if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) length#(cons(h,t)) -> c_12(length#(t)) length#(nil()) -> c_13() leq#(0(),m) -> c_14() leq#(s(n),0()) -> c_15() leq#(s(n),s(m)) -> c_16(leq#(n,m)) map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)) map_f#(pid,nil()) -> c_18() process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) sndsplit#(0(),x) -> c_20() sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) sndsplit#(s(n),nil()) -> c_22() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: app#(cons(h,t),x) -> c_1(app#(t,x)) app#(nil(),x) -> c_2() empty#(cons(h,t)) -> c_3() empty#(nil()) -> c_4() fstsplit#(0(),x) -> c_5() fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) fstsplit#(s(n),nil()) -> c_7() if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)) if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)) if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) length#(cons(h,t)) -> c_12(length#(t)) length#(nil()) -> c_13() leq#(0(),m) -> c_14() leq#(s(n),0()) -> c_15() leq#(s(n),s(m)) -> c_16(leq#(n,m)) map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)) map_f#(pid,nil()) -> c_18() process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) sndsplit#(0(),x) -> c_20() sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) sndsplit#(s(n),nil()) -> c_22() - Weak TRS: app(cons(h,t),x) -> cons(h,app(t,x)) app(nil(),x) -> x empty(cons(h,t)) -> false() empty(nil()) -> true() fstsplit(0(),x) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) fstsplit(s(n),nil()) -> nil() length(cons(h,t)) -> s(length(t)) length(nil()) -> 0() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) map_f(pid,nil()) -> nil() sndsplit(0(),x) -> x sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) sndsplit(s(n),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,cons/2,f/2 ,false/0,nil/0,s/1,self/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/5,c_9/3,c_10/4,c_11/4,c_12/1 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/2,c_18/0,c_19/3,c_20/0,c_21/1,c_22/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,empty#,fstsplit#,if1#,if2#,if3#,length#,leq#,map_f# ,process#,sndsplit#} and constructors {0,cons,f,false,nil,s,self,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,4,5,7,13,14,15,18,20,22} by application of Pre({2,3,4,5,7,13,14,15,18,20,22}) = {1,6,8,9,10,11,12,16,17,19,21}. Here rules are labelled as follows: 1: app#(cons(h,t),x) -> c_1(app#(t,x)) 2: app#(nil(),x) -> c_2() 3: empty#(cons(h,t)) -> c_3() 4: empty#(nil()) -> c_4() 5: fstsplit#(0(),x) -> c_5() 6: fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) 7: fstsplit#(s(n),nil()) -> c_7() 8: if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) 9: if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)) 10: if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)) 11: if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) 12: length#(cons(h,t)) -> c_12(length#(t)) 13: length#(nil()) -> c_13() 14: leq#(0(),m) -> c_14() 15: leq#(s(n),0()) -> c_15() 16: leq#(s(n),s(m)) -> c_16(leq#(n,m)) 17: map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)) 18: map_f#(pid,nil()) -> c_18() 19: process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) 20: sndsplit#(0(),x) -> c_20() 21: sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) 22: sndsplit#(s(n),nil()) -> c_22() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: app#(cons(h,t),x) -> c_1(app#(t,x)) fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)) if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)) if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) length#(cons(h,t)) -> c_12(length#(t)) leq#(s(n),s(m)) -> c_16(leq#(n,m)) map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)) process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) - Weak DPs: app#(nil(),x) -> c_2() empty#(cons(h,t)) -> c_3() empty#(nil()) -> c_4() fstsplit#(0(),x) -> c_5() fstsplit#(s(n),nil()) -> c_7() length#(nil()) -> c_13() leq#(0(),m) -> c_14() leq#(s(n),0()) -> c_15() map_f#(pid,nil()) -> c_18() sndsplit#(0(),x) -> c_20() sndsplit#(s(n),nil()) -> c_22() - Weak TRS: app(cons(h,t),x) -> cons(h,app(t,x)) app(nil(),x) -> x empty(cons(h,t)) -> false() empty(nil()) -> true() fstsplit(0(),x) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) fstsplit(s(n),nil()) -> nil() length(cons(h,t)) -> s(length(t)) length(nil()) -> 0() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) map_f(pid,nil()) -> nil() sndsplit(0(),x) -> x sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) sndsplit(s(n),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,cons/2,f/2 ,false/0,nil/0,s/1,self/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/5,c_9/3,c_10/4,c_11/4,c_12/1 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/2,c_18/0,c_19/3,c_20/0,c_21/1,c_22/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,empty#,fstsplit#,if1#,if2#,if3#,length#,leq#,map_f# ,process#,sndsplit#} and constructors {0,cons,f,false,nil,s,self,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:app#(cons(h,t),x) -> c_1(app#(t,x)) -->_1 app#(nil(),x) -> c_2():12 -->_1 app#(cons(h,t),x) -> c_1(app#(t,x)):1 2:S:fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) -->_1 fstsplit#(s(n),nil()) -> c_7():16 -->_1 fstsplit#(0(),x) -> c_5():15 -->_1 fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)):2 3:S:if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) -->_1 if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())):6 -->_5 map_f#(pid,nil()) -> c_18():20 -->_3 fstsplit#(s(n),nil()) -> c_7():16 -->_3 fstsplit#(0(),x) -> c_5():15 -->_2 empty#(nil()) -> c_4():14 -->_2 empty#(cons(h,t)) -> c_3():13 -->_4 app#(nil(),x) -> c_2():12 -->_3 fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)):2 -->_4 app#(cons(h,t),x) -> c_1(app#(t,x)):1 4:S:if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)) -->_1 if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)):5 -->_3 fstsplit#(s(n),nil()) -> c_7():16 -->_3 fstsplit#(0(),x) -> c_5():15 -->_2 empty#(nil()) -> c_4():14 -->_2 empty#(cons(h,t)) -> c_3():13 -->_3 fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)):2 5:S:if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)) -->_4 sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)):11 -->_1 process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)):10 -->_4 sndsplit#(s(n),nil()) -> c_22():22 -->_4 sndsplit#(0(),x) -> c_20():21 -->_3 map_f#(pid,nil()) -> c_18():20 -->_2 app#(nil(),x) -> c_2():12 -->_2 app#(cons(h,t),x) -> c_1(app#(t,x)):1 6:S:if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) -->_2 sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)):11 -->_1 process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)):10 -->_2 sndsplit#(s(n),nil()) -> c_22():22 -->_2 sndsplit#(0(),x) -> c_20():21 -->_4 map_f#(pid,nil()) -> c_18():20 -->_3 app#(nil(),x) -> c_2():12 -->_3 app#(cons(h,t),x) -> c_1(app#(t,x)):1 7:S:length#(cons(h,t)) -> c_12(length#(t)) -->_1 length#(nil()) -> c_13():17 -->_1 length#(cons(h,t)) -> c_12(length#(t)):7 8:S:leq#(s(n),s(m)) -> c_16(leq#(n,m)) -->_1 leq#(s(n),0()) -> c_15():19 -->_1 leq#(0(),m) -> c_14():18 -->_1 leq#(s(n),s(m)) -> c_16(leq#(n,m)):8 9:S:map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)) -->_2 map_f#(pid,nil()) -> c_18():20 -->_2 map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)):9 10:S:process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) -->_2 leq#(s(n),0()) -> c_15():19 -->_2 leq#(0(),m) -> c_14():18 -->_3 length#(nil()) -> c_13():17 -->_2 leq#(s(n),s(m)) -> c_16(leq#(n,m)):8 -->_3 length#(cons(h,t)) -> c_12(length#(t)):7 -->_1 if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)):4 -->_1 if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())):3 11:S:sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) -->_1 sndsplit#(s(n),nil()) -> c_22():22 -->_1 sndsplit#(0(),x) -> c_20():21 -->_1 sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)):11 12:W:app#(nil(),x) -> c_2() 13:W:empty#(cons(h,t)) -> c_3() 14:W:empty#(nil()) -> c_4() 15:W:fstsplit#(0(),x) -> c_5() 16:W:fstsplit#(s(n),nil()) -> c_7() 17:W:length#(nil()) -> c_13() 18:W:leq#(0(),m) -> c_14() 19:W:leq#(s(n),0()) -> c_15() 20:W:map_f#(pid,nil()) -> c_18() 21:W:sndsplit#(0(),x) -> c_20() 22:W:sndsplit#(s(n),nil()) -> c_22() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: empty#(cons(h,t)) -> c_3() 14: empty#(nil()) -> c_4() 20: map_f#(pid,nil()) -> c_18() 17: length#(nil()) -> c_13() 18: leq#(0(),m) -> c_14() 19: leq#(s(n),0()) -> c_15() 21: sndsplit#(0(),x) -> c_20() 22: sndsplit#(s(n),nil()) -> c_22() 15: fstsplit#(0(),x) -> c_5() 16: fstsplit#(s(n),nil()) -> c_7() 12: app#(nil(),x) -> c_2() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: app#(cons(h,t),x) -> c_1(app#(t,x)) fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)) if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)) if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) length#(cons(h,t)) -> c_12(length#(t)) leq#(s(n),s(m)) -> c_16(leq#(n,m)) map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)) process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) - Weak TRS: app(cons(h,t),x) -> cons(h,app(t,x)) app(nil(),x) -> x empty(cons(h,t)) -> false() empty(nil()) -> true() fstsplit(0(),x) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) fstsplit(s(n),nil()) -> nil() length(cons(h,t)) -> s(length(t)) length(nil()) -> 0() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) map_f(pid,nil()) -> nil() sndsplit(0(),x) -> x sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) sndsplit(s(n),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,cons/2,f/2 ,false/0,nil/0,s/1,self/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/5,c_9/3,c_10/4,c_11/4,c_12/1 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/2,c_18/0,c_19/3,c_20/0,c_21/1,c_22/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,empty#,fstsplit#,if1#,if2#,if3#,length#,leq#,map_f# ,process#,sndsplit#} and constructors {0,cons,f,false,nil,s,self,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:app#(cons(h,t),x) -> c_1(app#(t,x)) -->_1 app#(cons(h,t),x) -> c_1(app#(t,x)):1 2:S:fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) -->_1 fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)):2 3:S:if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) -->_1 if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())):6 -->_3 fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)):2 -->_4 app#(cons(h,t),x) -> c_1(app#(t,x)):1 4:S:if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)) -->_1 if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)):5 -->_3 fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)):2 5:S:if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,map_f#(self(),nil()) ,sndsplit#(m,store)) -->_4 sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)):11 -->_1 process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)):10 -->_2 app#(cons(h,t),x) -> c_1(app#(t,x)):1 6:S:if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())) -->_2 sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)):11 -->_1 process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)):10 -->_3 app#(cons(h,t),x) -> c_1(app#(t,x)):1 7:S:length#(cons(h,t)) -> c_12(length#(t)) -->_1 length#(cons(h,t)) -> c_12(length#(t)):7 8:S:leq#(s(n),s(m)) -> c_16(leq#(n,m)) -->_1 leq#(s(n),s(m)) -> c_16(leq#(n,m)):8 9:S:map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)) -->_2 map_f#(pid,cons(h,t)) -> c_17(app#(f(pid,h),map_f(pid,t)),map_f#(pid,t)):9 10:S:process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) -->_2 leq#(s(n),s(m)) -> c_16(leq#(n,m)):8 -->_3 length#(cons(h,t)) -> c_12(length#(t)):7 -->_1 if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))) ,empty#(fstsplit(m,store)) ,fstsplit#(m,store)):4 -->_1 if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,empty#(fstsplit(m,app(map_f(self(),nil()),store))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store) ,map_f#(self(),nil())):3 11:S:sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) -->_1 sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)):11 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store)) if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))),fstsplit#(m,store)) if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,sndsplit#(m,store)) if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store)) map_f#(pid,cons(h,t)) -> c_17(map_f#(pid,t)) * Step 6: UsableRules MAYBE + Considered Problem: - Strict DPs: app#(cons(h,t),x) -> c_1(app#(t,x)) fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store)) if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))),fstsplit#(m,store)) if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,sndsplit#(m,store)) if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store)) length#(cons(h,t)) -> c_12(length#(t)) leq#(s(n),s(m)) -> c_16(leq#(n,m)) map_f#(pid,cons(h,t)) -> c_17(map_f#(pid,t)) process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) - Weak TRS: app(cons(h,t),x) -> cons(h,app(t,x)) app(nil(),x) -> x empty(cons(h,t)) -> false() empty(nil()) -> true() fstsplit(0(),x) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) fstsplit(s(n),nil()) -> nil() length(cons(h,t)) -> s(length(t)) length(nil()) -> 0() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) map_f(pid,nil()) -> nil() sndsplit(0(),x) -> x sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) sndsplit(s(n),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,cons/2,f/2 ,false/0,nil/0,s/1,self/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/3,c_9/2,c_10/3,c_11/3,c_12/1 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/0,c_19/3,c_20/0,c_21/1,c_22/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,empty#,fstsplit#,if1#,if2#,if3#,length#,leq#,map_f# ,process#,sndsplit#} and constructors {0,cons,f,false,nil,s,self,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: app(cons(h,t),x) -> cons(h,app(t,x)) app(nil(),x) -> x empty(cons(h,t)) -> false() empty(nil()) -> true() fstsplit(0(),x) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) fstsplit(s(n),nil()) -> nil() length(cons(h,t)) -> s(length(t)) length(nil()) -> 0() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) map_f(pid,nil()) -> nil() sndsplit(0(),x) -> x sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) sndsplit(s(n),nil()) -> nil() app#(cons(h,t),x) -> c_1(app#(t,x)) fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store)) if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))),fstsplit#(m,store)) if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,sndsplit#(m,store)) if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store)) length#(cons(h,t)) -> c_12(length#(t)) leq#(s(n),s(m)) -> c_16(leq#(n,m)) map_f#(pid,cons(h,t)) -> c_17(map_f#(pid,t)) process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: app#(cons(h,t),x) -> c_1(app#(t,x)) fstsplit#(s(n),cons(h,t)) -> c_6(fstsplit#(n,t)) if1#(store,m,false()) -> c_8(if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) ,fstsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store)) if1#(store,m,true()) -> c_9(if2#(store,m,empty(fstsplit(m,store))),fstsplit#(m,store)) if2#(store,m,false()) -> c_10(process#(app(map_f(self(),nil()),sndsplit(m,store)),m) ,app#(map_f(self(),nil()),sndsplit(m,store)) ,sndsplit#(m,store)) if3#(store,m,false()) -> c_11(process#(sndsplit(m,app(map_f(self(),nil()),store)),m) ,sndsplit#(m,app(map_f(self(),nil()),store)) ,app#(map_f(self(),nil()),store)) length#(cons(h,t)) -> c_12(length#(t)) leq#(s(n),s(m)) -> c_16(leq#(n,m)) map_f#(pid,cons(h,t)) -> c_17(map_f#(pid,t)) process#(store,m) -> c_19(if1#(store,m,leq(m,length(store))),leq#(m,length(store)),length#(store)) sndsplit#(s(n),cons(h,t)) -> c_21(sndsplit#(n,t)) - Weak TRS: app(cons(h,t),x) -> cons(h,app(t,x)) app(nil(),x) -> x empty(cons(h,t)) -> false() empty(nil()) -> true() fstsplit(0(),x) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) fstsplit(s(n),nil()) -> nil() length(cons(h,t)) -> s(length(t)) length(nil()) -> 0() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) map_f(pid,nil()) -> nil() sndsplit(0(),x) -> x sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) sndsplit(s(n),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,cons/2,f/2 ,false/0,nil/0,s/1,self/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/3,c_9/2,c_10/3,c_11/3,c_12/1 ,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/0,c_19/3,c_20/0,c_21/1,c_22/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,empty#,fstsplit#,if1#,if2#,if3#,length#,leq#,map_f# ,process#,sndsplit#} and constructors {0,cons,f,false,nil,s,self,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE