MAYBE 0.07/0.19 MAYBE 0.07/0.19 0.07/0.19 Problem: 0.07/0.19 fstsplit(0(),x) -> nil() 0.07/0.19 fstsplit(s(n),nil()) -> nil() 0.07/0.19 fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) 0.07/0.19 sndsplit(0(),x) -> x 0.07/0.19 sndsplit(s(n),nil()) -> nil() 0.07/0.19 sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 0.07/0.19 empty(nil()) -> true() 0.07/0.19 empty(cons(h,t)) -> false() 0.07/0.19 leq(0(),m) -> true() 0.07/0.19 leq(s(n),0()) -> false() 0.07/0.19 leq(s(n),s(m)) -> leq(n,m) 0.07/0.19 length(nil()) -> 0() 0.07/0.19 length(cons(h,t)) -> s(length(t)) 0.07/0.19 app(nil(),x) -> x 0.07/0.19 app(cons(h,t),x) -> cons(h,app(t,x)) 0.07/0.19 map_f(pid,nil()) -> nil() 0.07/0.19 map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 0.07/0.19 process(store,m) -> if1(store,m,leq(m,length(store))) 0.07/0.19 if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store))) 0.07/0.19 if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store)))) 0.07/0.19 if2(store,m,false()) -> process(app(map_f(self(),nil()),sndsplit(m,store)),m) 0.07/0.19 if3(store,m,false()) -> process(sndsplit(m,app(map_f(self(),nil()),store)),m) 0.07/0.19 0.07/0.19 Proof: 0.07/0.19 Open 0.07/0.19 EOF