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) Usable Rule 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: f30(x,y) -> x f30(x,y) -> y map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) empty(nil()) -> true() empty(cons(h,t)) -> false() app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 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: f30(x,y) -> x f30(x,y) -> y map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) empty(nil()) -> true() empty(cons(h,t)) -> false() app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 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) EDG 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: f30(x,y) -> x f30(x,y) -> y map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) empty(nil()) -> true() empty(cons(h,t)) -> false() app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) graph: if3#(store,m,false()) -> process#(sndsplit(m,app(map_f(self(),nil()),store)),m) -> process#(store,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) -> if1#(store,m,leq(m,length(store))) 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) -> 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) -> if1#(store,m,leq(m,length(store))) 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()) -> map_f#(self(),nil()) 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()) -> 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()) -> process#(sndsplit(m,app(map_f(self(),nil()),store)),m) 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()) -> 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()) -> app#(map_f(self(),nil()),sndsplit(m,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,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,true()) -> 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()) -> if2#(store,m,empty(fstsplit(m,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,false()) -> 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()) -> empty#(fstsplit(m,app(map_f(self(),nil()),store))) 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) -> 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)) -> 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) 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) CDG 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: f30(x,y) -> x f30(x,y) -> y map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) length(nil()) -> 0() length(cons(h,t)) -> s(length(t)) leq(0(),m) -> true() leq(s(n),0()) -> false() leq(s(n),s(m)) -> leq(n,m) fstsplit(0(),x) -> nil() fstsplit(s(n),nil()) -> nil() fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) empty(nil()) -> true() empty(cons(h,t)) -> false() app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 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()) -> 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()) -> 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()) -> 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) 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) Restore Modifier: 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) SCC Processor: #sccs: 7 #rules: 11 #arcs: 35/676 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) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x0 + 1, [if3](x0, x1, x2) = 0, [self] = 0, [if2](x0, x1, x2) = 0, [if1](x0, x1, x2) = 0, [process](x0, x1) = 0, [f](x0, x1) = 0, [map_f](x0, x1) = 0, [app](x0, x1) = x0 + x1, [length](x0) = x0 + 1, [leq](x0, x1) = x1 + 1, [false] = 0, [true] = 1, [empty](x0) = 1, [sndsplit](x0, x1) = x1, [cons](x0, x1) = x1 + 1, [s](x0) = x0, [nil] = 0, [fstsplit](x0, x1) = x1, [0] = 1 orientation: app#(cons(h,t),x) = t + 2 >= t + 1 = app#(t,x) fstsplit(0(),x) = x >= 0 = nil() fstsplit(s(n),nil()) = 0 >= 0 = nil() fstsplit(s(n),cons(h,t)) = t + 1 >= t + 1 = cons(h,fstsplit(n,t)) sndsplit(0(),x) = x >= x = x sndsplit(s(n),nil()) = 0 >= 0 = nil() sndsplit(s(n),cons(h,t)) = t + 1 >= t = sndsplit(n,t) empty(nil()) = 1 >= 1 = true() empty(cons(h,t)) = 1 >= 0 = false() leq(0(),m) = m + 1 >= 1 = true() leq(s(n),0()) = 2 >= 0 = false() leq(s(n),s(m)) = m + 1 >= m + 1 = leq(n,m) length(nil()) = 1 >= 1 = 0() length(cons(h,t)) = t + 2 >= t + 1 = s(length(t)) app(nil(),x) = x >= x = x app(cons(h,t),x) = t + x + 1 >= t + x + 1 = cons(h,app(t,x)) map_f(pid,nil()) = 0 >= 0 = nil() map_f(pid,cons(h,t)) = 0 >= 0 = app(f(pid,h),map_f(pid,t)) process(store,m) = 0 >= 0 = if1(store,m,leq(m,length(store))) if1(store,m,true()) = 0 >= 0 = if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) = 0 >= 0 = if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) if2(store,m,false()) = 0 >= 0 = process(app(map_f(self(),nil()),sndsplit(m,store)),m) if3(store,m,false()) = 0 >= 0 = process(sndsplit(m,app(map_f(self(),nil()),store)),m) 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: 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) Matrix Interpretation Processor: dimension: 1 interpretation: [map_f#](x0, x1) = x1 + 1, [if3](x0, x1, x2) = 0, [self] = 0, [if2](x0, x1, x2) = 0, [if1](x0, x1, x2) = 0, [process](x0, x1) = 0, [f](x0, x1) = 0, [map_f](x0, x1) = 0, [app](x0, x1) = x0 + x1, [length](x0) = x0 + 1, [leq](x0, x1) = x1 + 1, [false] = 0, [true] = 1, [empty](x0) = 1, [sndsplit](x0, x1) = x1, [cons](x0, x1) = x1 + 1, [s](x0) = x0, [nil] = 0, [fstsplit](x0, x1) = x1, [0] = 1 orientation: map_f#(pid,cons(h,t)) = t + 2 >= t + 1 = map_f#(pid,t) fstsplit(0(),x) = x >= 0 = nil() fstsplit(s(n),nil()) = 0 >= 0 = nil() fstsplit(s(n),cons(h,t)) = t + 1 >= t + 1 = cons(h,fstsplit(n,t)) sndsplit(0(),x) = x >= x = x sndsplit(s(n),nil()) = 0 >= 0 = nil() sndsplit(s(n),cons(h,t)) = t + 1 >= t = sndsplit(n,t) empty(nil()) = 1 >= 1 = true() empty(cons(h,t)) = 1 >= 0 = false() leq(0(),m) = m + 1 >= 1 = true() leq(s(n),0()) = 2 >= 0 = false() leq(s(n),s(m)) = m + 1 >= m + 1 = leq(n,m) length(nil()) = 1 >= 1 = 0() length(cons(h,t)) = t + 2 >= t + 1 = s(length(t)) app(nil(),x) = x >= x = x app(cons(h,t),x) = t + x + 1 >= t + x + 1 = cons(h,app(t,x)) map_f(pid,nil()) = 0 >= 0 = nil() map_f(pid,cons(h,t)) = 0 >= 0 = app(f(pid,h),map_f(pid,t)) process(store,m) = 0 >= 0 = if1(store,m,leq(m,length(store))) if1(store,m,true()) = 0 >= 0 = if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) = 0 >= 0 = if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) if2(store,m,false()) = 0 >= 0 = process(app(map_f(self(),nil()),sndsplit(m,store)),m) if3(store,m,false()) = 0 >= 0 = process(sndsplit(m,app(map_f(self(),nil()),store)),m) 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: 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: 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) Matrix Interpretation Processor: dimension: 1 interpretation: [sndsplit#](x0, x1) = x0, [if3](x0, x1, x2) = 0, [self] = 0, [if2](x0, x1, x2) = 0, [if1](x0, x1, x2) = 0, [process](x0, x1) = 0, [f](x0, x1) = 0, [map_f](x0, x1) = x1, [app](x0, x1) = x0 + x1, [length](x0) = x0 + 1, [leq](x0, x1) = x1, [false] = 0, [true] = 0, [empty](x0) = 0, [sndsplit](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x1 + 1, [s](x0) = x0 + 1, [nil] = 0, [fstsplit](x0, x1) = x0, [0] = 0 orientation: sndsplit#(s(n),cons(h,t)) = n + 1 >= n = sndsplit#(n,t) fstsplit(0(),x) = 0 >= 0 = nil() fstsplit(s(n),nil()) = n + 1 >= 0 = nil() fstsplit(s(n),cons(h,t)) = n + 1 >= n + 1 = cons(h,fstsplit(n,t)) sndsplit(0(),x) = x + 1 >= x = x sndsplit(s(n),nil()) = n + 2 >= 0 = nil() sndsplit(s(n),cons(h,t)) = n + t + 3 >= n + t + 1 = sndsplit(n,t) empty(nil()) = 0 >= 0 = true() empty(cons(h,t)) = 0 >= 0 = false() leq(0(),m) = m >= 0 = true() leq(s(n),0()) = 0 >= 0 = false() leq(s(n),s(m)) = m + 1 >= m = leq(n,m) length(nil()) = 1 >= 0 = 0() length(cons(h,t)) = t + 2 >= t + 2 = s(length(t)) app(nil(),x) = x >= x = x app(cons(h,t),x) = t + x + 1 >= t + x + 1 = cons(h,app(t,x)) map_f(pid,nil()) = 0 >= 0 = nil() map_f(pid,cons(h,t)) = t + 1 >= t = app(f(pid,h),map_f(pid,t)) process(store,m) = 0 >= 0 = if1(store,m,leq(m,length(store))) if1(store,m,true()) = 0 >= 0 = if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) = 0 >= 0 = if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) if2(store,m,false()) = 0 >= 0 = process(app(map_f(self(),nil()),sndsplit(m,store)),m) if3(store,m,false()) = 0 >= 0 = process(sndsplit(m,app(map_f(self(),nil()),store)),m) 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) Matrix Interpretation Processor: dimension: 1 interpretation: [fstsplit#](x0, x1) = x0, [if3](x0, x1, x2) = 0, [self] = 0, [if2](x0, x1, x2) = 0, [if1](x0, x1, x2) = 0, [process](x0, x1) = 0, [f](x0, x1) = 0, [map_f](x0, x1) = x1, [app](x0, x1) = x0 + x1, [length](x0) = x0 + 1, [leq](x0, x1) = x1, [false] = 0, [true] = 0, [empty](x0) = 0, [sndsplit](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x1 + 1, [s](x0) = x0 + 1, [nil] = 0, [fstsplit](x0, x1) = x0, [0] = 0 orientation: fstsplit#(s(n),cons(h,t)) = n + 1 >= n = fstsplit#(n,t) fstsplit(0(),x) = 0 >= 0 = nil() fstsplit(s(n),nil()) = n + 1 >= 0 = nil() fstsplit(s(n),cons(h,t)) = n + 1 >= n + 1 = cons(h,fstsplit(n,t)) sndsplit(0(),x) = x + 1 >= x = x sndsplit(s(n),nil()) = n + 2 >= 0 = nil() sndsplit(s(n),cons(h,t)) = n + t + 3 >= n + t + 1 = sndsplit(n,t) empty(nil()) = 0 >= 0 = true() empty(cons(h,t)) = 0 >= 0 = false() leq(0(),m) = m >= 0 = true() leq(s(n),0()) = 0 >= 0 = false() leq(s(n),s(m)) = m + 1 >= m = leq(n,m) length(nil()) = 1 >= 0 = 0() length(cons(h,t)) = t + 2 >= t + 2 = s(length(t)) app(nil(),x) = x >= x = x app(cons(h,t),x) = t + x + 1 >= t + x + 1 = cons(h,app(t,x)) map_f(pid,nil()) = 0 >= 0 = nil() map_f(pid,cons(h,t)) = t + 1 >= t = app(f(pid,h),map_f(pid,t)) process(store,m) = 0 >= 0 = if1(store,m,leq(m,length(store))) if1(store,m,true()) = 0 >= 0 = if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) = 0 >= 0 = if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) if2(store,m,false()) = 0 >= 0 = process(app(map_f(self(),nil()),sndsplit(m,store)),m) if3(store,m,false()) = 0 >= 0 = process(sndsplit(m,app(map_f(self(),nil()),store)),m) 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) Matrix Interpretation Processor: dimension: 1 interpretation: [leq#](x0, x1) = x1, [if3](x0, x1, x2) = x1, [self] = 0, [if2](x0, x1, x2) = x1, [if1](x0, x1, x2) = x1, [process](x0, x1) = x1, [f](x0, x1) = 0, [map_f](x0, x1) = x1, [app](x0, x1) = x0 + x1, [length](x0) = x0, [leq](x0, x1) = 0, [false] = 0, [true] = 0, [empty](x0) = 0, [sndsplit](x0, x1) = x1 + 1, [cons](x0, x1) = x1 + 1, [s](x0) = x0 + 1, [nil] = 0, [fstsplit](x0, x1) = x0 + 1, [0] = 0 orientation: leq#(s(n),s(m)) = m + 1 >= m = leq#(n,m) fstsplit(0(),x) = 1 >= 0 = nil() fstsplit(s(n),nil()) = n + 2 >= 0 = nil() fstsplit(s(n),cons(h,t)) = n + 2 >= n + 2 = cons(h,fstsplit(n,t)) sndsplit(0(),x) = x + 1 >= x = x sndsplit(s(n),nil()) = 1 >= 0 = nil() sndsplit(s(n),cons(h,t)) = t + 2 >= t + 1 = sndsplit(n,t) empty(nil()) = 0 >= 0 = true() empty(cons(h,t)) = 0 >= 0 = false() leq(0(),m) = 0 >= 0 = true() leq(s(n),0()) = 0 >= 0 = false() leq(s(n),s(m)) = 0 >= 0 = leq(n,m) length(nil()) = 0 >= 0 = 0() length(cons(h,t)) = t + 1 >= t + 1 = s(length(t)) app(nil(),x) = x >= x = x app(cons(h,t),x) = t + x + 1 >= t + x + 1 = cons(h,app(t,x)) map_f(pid,nil()) = 0 >= 0 = nil() map_f(pid,cons(h,t)) = t + 1 >= t = app(f(pid,h),map_f(pid,t)) process(store,m) = m >= m = if1(store,m,leq(m,length(store))) if1(store,m,true()) = m >= m = if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) = m >= m = if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) if2(store,m,false()) = m >= m = process(app(map_f(self(),nil()),sndsplit(m,store)),m) if3(store,m,false()) = m >= m = process(sndsplit(m,app(map_f(self(),nil()),store)),m) 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) Matrix Interpretation Processor: dimension: 1 interpretation: [length#](x0) = x0, [if3](x0, x1, x2) = 0, [self] = 0, [if2](x0, x1, x2) = 0, [if1](x0, x1, x2) = 0, [process](x0, x1) = 0, [f](x0, x1) = 0, [map_f](x0, x1) = x1, [app](x0, x1) = x0 + x1, [length](x0) = 1, [leq](x0, x1) = x1 + 1, [false] = 0, [true] = 0, [empty](x0) = x0, [sndsplit](x0, x1) = x1, [cons](x0, x1) = x1 + 1, [s](x0) = x0, [nil] = 1, [fstsplit](x0, x1) = x0 + x1, [0] = 1 orientation: length#(cons(h,t)) = t + 1 >= t = length#(t) fstsplit(0(),x) = x + 1 >= 1 = nil() fstsplit(s(n),nil()) = n + 1 >= 1 = nil() fstsplit(s(n),cons(h,t)) = n + t + 1 >= n + t + 1 = cons(h,fstsplit(n,t)) sndsplit(0(),x) = x >= x = x sndsplit(s(n),nil()) = 1 >= 1 = nil() sndsplit(s(n),cons(h,t)) = t + 1 >= t = sndsplit(n,t) empty(nil()) = 1 >= 0 = true() empty(cons(h,t)) = t + 1 >= 0 = false() leq(0(),m) = m + 1 >= 0 = true() leq(s(n),0()) = 2 >= 0 = false() leq(s(n),s(m)) = m + 1 >= m + 1 = leq(n,m) length(nil()) = 1 >= 1 = 0() length(cons(h,t)) = 1 >= 1 = s(length(t)) app(nil(),x) = x + 1 >= x = x app(cons(h,t),x) = t + x + 1 >= t + x + 1 = cons(h,app(t,x)) map_f(pid,nil()) = 1 >= 1 = nil() map_f(pid,cons(h,t)) = t + 1 >= t = app(f(pid,h),map_f(pid,t)) process(store,m) = 0 >= 0 = if1(store,m,leq(m,length(store))) if1(store,m,true()) = 0 >= 0 = if2(store,m,empty(fstsplit(m,store))) if1(store,m,false()) = 0 >= 0 = if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) if2(store,m,false()) = 0 >= 0 = process(app(map_f(self(),nil()),sndsplit(m,store)),m) if3(store,m,false()) = 0 >= 0 = process(sndsplit(m,app(map_f(self(),nil()),store)),m) 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