MAYBE
0.18/0.23	MAYBE
0.18/0.23	
0.18/0.23	Problem:
0.18/0.23	 fstsplit(0(),x) -> nil()
0.18/0.23	 fstsplit(s(n),nil()) -> nil()
0.18/0.23	 fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t))
0.18/0.23	 sndsplit(0(),x) -> x
0.18/0.23	 sndsplit(s(n),nil()) -> nil()
0.18/0.23	 sndsplit(s(n),cons(h,t)) -> sndsplit(n,t)
0.18/0.23	 empty(nil()) -> true()
0.18/0.23	 empty(cons(h,t)) -> false()
0.18/0.23	 leq(0(),m) -> true()
0.18/0.23	 leq(s(n),0()) -> false()
0.18/0.23	 leq(s(n),s(m)) -> leq(n,m)
0.18/0.23	 length(nil()) -> 0()
0.18/0.23	 length(cons(h,t)) -> s(length(t))
0.18/0.23	 app(nil(),x) -> x
0.18/0.23	 app(cons(h,t),x) -> cons(h,app(t,x))
0.18/0.23	 map_f(pid,nil()) -> nil()
0.18/0.23	 map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t))
0.18/0.23	 head(cons(h,t)) -> h
0.18/0.23	 tail(cons(h,t)) -> t
0.18/0.23	 ring(st_1,in_2,st_2,in_3,st_3,m) -> if_1(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1)))
0.18/0.23	 if_1(st_1,in_2,st_2,in_3,st_3,m,false()) ->
0.18/0.23	 ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m)
0.18/0.23	 ring(st_1,in_2,st_2,in_3,st_3,m) -> if_2(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_2)))
0.18/0.23	 if_2(st_1,in_2,st_2,in_3,st_3,m,true()) ->
0.18/0.23	 if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2)))
0.18/0.23	 if_3(st_1,in_2,st_2,in_3,st_3,m,false()) ->
0.18/0.24	 ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m)
0.18/0.24	 if_2(st_1,in_2,st_2,in_3,st_3,m,false()) ->
0.18/0.24	 if_4(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,app(map_f(two(),head(in_2)),st_2))))
0.18/0.24	 if_4(st_1,in_2,st_2,in_3,st_3,m,false()) ->
0.18/0.24	 ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)),cons
0.18/0.24	                                                                    (
0.18/0.24	                                                                    fstsplit
0.18/0.24	                                                                    (
0.18/0.24	                                                                    m,
0.18/0.24	                                                                    app
0.18/0.24	                                                                    (
0.18/0.24	                                                                    map_f(two(),head(in_2)),st_2)),
0.18/0.24	                                                                    in_3),
0.18/0.24	      st_3,m)
0.18/0.24	 ring(st_1,in_2,st_2,in_3,st_3,m) ->
0.18/0.24	 if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2))))
0.18/0.24	 if_5(st_1,in_2,st_2,in_3,st_3,m,true()) -> ring(st_1,tail(in_2),st_2,in_3,st_3,m)
0.18/0.24	 ring(st_1,in_2,st_2,in_3,st_3,m) -> if_6(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_3)))
0.18/0.24	 if_6(st_1,in_2,st_2,in_3,st_3,m,true()) ->
0.18/0.24	 if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3)))
0.18/0.24	 if_7(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m)
0.18/0.24	 if_6(st_1,in_2,st_2,in_3,st_3,m,false()) ->
0.18/0.24	 if_8(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,app(map_f(three(),head(in_3)),st_3))))
0.18/0.24	 if_8(st_1,in_2,st_2,in_3,st_3,m,false()) ->
0.18/0.24	 ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m)
0.18/0.24	 ring(st_1,in_2,st_2,in_3,st_3,m) ->
0.18/0.24	 if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3))))
0.18/0.24	 if_9(st_1,in_2,st_2,in_3,st_3,m,true()) -> ring(st_1,in_2,st_2,tail(in_3),st_3,m)
0.18/0.24	
0.18/0.24	Proof:
0.18/0.24	 Open
0.18/0.24	EOF