MAYBE Problem: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Proof: DP Processor: DPs: fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) leq#(s(n),s(m)) -> leq#(n,m) length#(cons(h,t)) -> length#(t) app#(cons(h,t),x) -> app#(t,x) map_f#(pid,cons(h,t)) -> map_f#(pid,t) map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) process#(store,m) -> length#(store) process#(store,m) -> leq#(m,length(store)) process#(store,m) -> if1#(store,m,leq(m,length(store))) if1#(store,m,true()) -> fstsplit#(m,store) if1#(store,m,true()) -> empty#(fstsplit(m,store)) if1#(store,m,true()) -> if2#(store,m,empty(fstsplit(m,store))) if1#(store,m,false()) -> map_f#(self(),nil()) if1#(store,m,false()) -> app#(map_f(self(),nil()),store) if1#(store,m,false()) -> fstsplit#(m,app(map_f(self(),nil()),store)) if1#(store,m,false()) -> empty#(fstsplit(m,app(map_f(self(),nil()),store))) if1#(store,m,false()) -> if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) if2#(store,m,false()) -> sndsplit#(m,store) if2#(store,m,false()) -> map_f#(self(),nil()) if2#(store,m,false()) -> app#(map_f(self(),nil()),sndsplit(m,store)) if2#(store,m,false()) -> process#(app(map_f(self(),nil()),sndsplit(m,store)),m) if3#(store,m,false()) -> map_f#(self(),nil()) if3#(store,m,false()) -> app#(map_f(self(),nil()),store) if3#(store,m,false()) -> sndsplit#(m,app(map_f(self(),nil()),store)) if3#(store,m,false()) -> process#(sndsplit(m,app(map_f(self(),nil()),store)),m) TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) TDG Processor: DPs: fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) leq#(s(n),s(m)) -> leq#(n,m) length#(cons(h,t)) -> length#(t) app#(cons(h,t),x) -> app#(t,x) map_f#(pid,cons(h,t)) -> map_f#(pid,t) map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) process#(store,m) -> length#(store) process#(store,m) -> leq#(m,length(store)) process#(store,m) -> if1#(store,m,leq(m,length(store))) if1#(store,m,true()) -> fstsplit#(m,store) if1#(store,m,true()) -> empty#(fstsplit(m,store)) if1#(store,m,true()) -> if2#(store,m,empty(fstsplit(m,store))) if1#(store,m,false()) -> map_f#(self(),nil()) if1#(store,m,false()) -> app#(map_f(self(),nil()),store) if1#(store,m,false()) -> fstsplit#(m,app(map_f(self(),nil()),store)) if1#(store,m,false()) -> empty#(fstsplit(m,app(map_f(self(),nil()),store))) if1#(store,m,false()) -> if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) if2#(store,m,false()) -> sndsplit#(m,store) if2#(store,m,false()) -> map_f#(self(),nil()) if2#(store,m,false()) -> app#(map_f(self(),nil()),sndsplit(m,store)) if2#(store,m,false()) -> process#(app(map_f(self(),nil()),sndsplit(m,store)),m) if3#(store,m,false()) -> map_f#(self(),nil()) if3#(store,m,false()) -> app#(map_f(self(),nil()),store) if3#(store,m,false()) -> sndsplit#(m,app(map_f(self(),nil()),store)) if3#(store,m,false()) -> process#(sndsplit(m,app(map_f(self(),nil()),store)),m) TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) graph: if3#(store,m,false()) -> process#(sndsplit(m,app(map_f(self(),nil()),store)),m) -> process#(store,m) -> if1#(store,m,leq(m,length(store))) if3#(store,m,false()) -> process#(sndsplit(m,app(map_f(self(),nil()),store)),m) -> process#(store,m) -> leq#(m,length(store)) if3#(store,m,false()) -> process#(sndsplit(m,app(map_f(self(),nil()),store)),m) -> process#(store,m) -> length#(store) if3#(store,m,false()) -> map_f#(self(),nil()) -> map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) if3#(store,m,false()) -> map_f#(self(),nil()) -> map_f#(pid,cons(h,t)) -> map_f#(pid,t) if3#(store,m,false()) -> app#(map_f(self(),nil()),store) -> app#(cons(h,t),x) -> app#(t,x) if3#(store,m,false()) -> sndsplit#(m,app(map_f(self(),nil()),store)) -> sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) if2#(store,m,false()) -> process#(app(map_f(self(),nil()),sndsplit(m,store)),m) -> process#(store,m) -> if1#(store,m,leq(m,length(store))) if2#(store,m,false()) -> process#(app(map_f(self(),nil()),sndsplit(m,store)),m) -> process#(store,m) -> leq#(m,length(store)) if2#(store,m,false()) -> process#(app(map_f(self(),nil()),sndsplit(m,store)),m) -> process#(store,m) -> length#(store) if2#(store,m,false()) -> map_f#(self(),nil()) -> map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) if2#(store,m,false()) -> map_f#(self(),nil()) -> map_f#(pid,cons(h,t)) -> map_f#(pid,t) if2#(store,m,false()) -> app#(map_f(self(),nil()),sndsplit(m,store)) -> app#(cons(h,t),x) -> app#(t,x) if2#(store,m,false()) -> sndsplit#(m,store) -> sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) if1#(store,m,false()) -> if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) -> if3#(store,m,false()) -> process#(sndsplit(m,app(map_f(self(),nil()),store)),m) if1#(store,m,false()) -> if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) -> if3#(store,m,false()) -> sndsplit#(m,app(map_f(self(),nil()),store)) if1#(store,m,false()) -> if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) -> if3#(store,m,false()) -> app#(map_f(self(),nil()),store) if1#(store,m,false()) -> if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) -> if3#(store,m,false()) -> map_f#(self(),nil()) if1#(store,m,false()) -> map_f#(self(),nil()) -> map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) if1#(store,m,false()) -> map_f#(self(),nil()) -> map_f#(pid,cons(h,t)) -> map_f#(pid,t) if1#(store,m,false()) -> app#(map_f(self(),nil()),store) -> app#(cons(h,t),x) -> app#(t,x) if1#(store,m,false()) -> fstsplit#(m,app(map_f(self(),nil()),store)) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) 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) if1#(store,m,true()) -> if2#(store,m,empty(fstsplit(m,store))) -> if2#(store,m,false()) -> app#(map_f(self(),nil()),sndsplit(m,store)) if1#(store,m,true()) -> if2#(store,m,empty(fstsplit(m,store))) -> if2#(store,m,false()) -> map_f#(self(),nil()) if1#(store,m,true()) -> if2#(store,m,empty(fstsplit(m,store))) -> if2#(store,m,false()) -> sndsplit#(m,store) if1#(store,m,true()) -> fstsplit#(m,store) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) process#(store,m) -> if1#(store,m,leq(m,length(store))) -> if1#(store,m,false()) -> if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) process#(store,m) -> if1#(store,m,leq(m,length(store))) -> if1#(store,m,false()) -> empty#(fstsplit(m,app(map_f(self(),nil()),store))) process#(store,m) -> if1#(store,m,leq(m,length(store))) -> if1#(store,m,false()) -> fstsplit#(m,app(map_f(self(),nil()),store)) process#(store,m) -> if1#(store,m,leq(m,length(store))) -> if1#(store,m,false()) -> app#(map_f(self(),nil()),store) process#(store,m) -> if1#(store,m,leq(m,length(store))) -> if1#(store,m,false()) -> map_f#(self(),nil()) process#(store,m) -> if1#(store,m,leq(m,length(store))) -> if1#(store,m,true()) -> if2#(store,m,empty(fstsplit(m,store))) process#(store,m) -> if1#(store,m,leq(m,length(store))) -> if1#(store,m,true()) -> empty#(fstsplit(m,store)) process#(store,m) -> if1#(store,m,leq(m,length(store))) -> if1#(store,m,true()) -> fstsplit#(m,store) process#(store,m) -> length#(store) -> length#(cons(h,t)) -> length#(t) process#(store,m) -> leq#(m,length(store)) -> leq#(s(n),s(m)) -> leq#(n,m) map_f#(pid,cons(h,t)) -> map_f#(pid,t) -> map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) map_f#(pid,cons(h,t)) -> map_f#(pid,t) -> map_f#(pid,cons(h,t)) -> map_f#(pid,t) map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) -> app#(cons(h,t),x) -> app#(t,x) app#(cons(h,t),x) -> app#(t,x) -> app#(cons(h,t),x) -> app#(t,x) length#(cons(h,t)) -> length#(t) -> length#(cons(h,t)) -> length#(t) leq#(s(n),s(m)) -> leq#(n,m) -> leq#(s(n),s(m)) -> leq#(n,m) sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) -> sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) SCC Processor: #sccs: 7 #rules: 11 #arcs: 45/676 DPs: if3#(store,m,false()) -> process#(sndsplit(m,app(map_f(self(),nil()),store)),m) process#(store,m) -> if1#(store,m,leq(m,length(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) if1#(store,m,false()) -> if3#(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Open DPs: map_f#(pid,cons(h,t)) -> map_f#(pid,t) TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Subterm Criterion Processor: simple projection: pi(map_f#) = 1 problem: DPs: TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Qed DPs: app#(cons(h,t),x) -> app#(t,x) TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Subterm Criterion Processor: simple projection: pi(app#) = 0 problem: DPs: TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Qed DPs: sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Subterm Criterion Processor: simple projection: pi(sndsplit#) = 1 problem: DPs: TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Qed DPs: fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Subterm Criterion Processor: simple projection: pi(fstsplit#) = 1 problem: DPs: TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Qed DPs: leq#(s(n),s(m)) -> leq#(n,m) TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Subterm Criterion Processor: simple projection: pi(leq#) = 1 problem: DPs: TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Qed DPs: length#(cons(h,t)) -> length#(t) TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Subterm Criterion Processor: simple projection: pi(length#) = 0 problem: DPs: TRS: fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) empty(nil()) -> true() empty(cons(h,t)) -> false() leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) process(store,m) -> if1(store,m,leq(m,length(store))) if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),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) Qed