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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)),cons ( fstsplit ( m, app ( map_f(two(),head(in_2)),st_2)), in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) 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)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) 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))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_1) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_1) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) 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))) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,st_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_2) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_2) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> empty#(fstsplit(m,app(map_f(two(),head(in_2)),st_2))) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_5#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(in_2) 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) ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) 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))) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,st_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) if_7#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_3) 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) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(three(),head(in_3)),st_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> empty#(fstsplit(m,app(map_f(three(),head(in_3)),st_3))) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(three(),head(in_3)),st_3)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_9#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(in_3) 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) 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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) 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)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) 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))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_1) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_1) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) 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))) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,st_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_2) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_2) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> empty#(fstsplit(m,app(map_f(two(),head(in_2)),st_2))) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_5#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(in_2) 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) ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) 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))) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,st_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) if_7#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_3) 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) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(three(),head(in_3)),st_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> empty#(fstsplit(m,app(map_f(three(),head(in_3)),st_3))) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(three(),head(in_3)),st_3)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_9#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(in_3) 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) TRS: f47(x,y) -> x f47(x,y) -> y map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 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() sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,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) head(cons(h,t)) -> h app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) tail(cons(h,t)) -> 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)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) 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))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_1) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_1) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) 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))) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,st_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_2) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_2) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> empty#(fstsplit(m,app(map_f(two(),head(in_2)),st_2))) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_5#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(in_2) 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) ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) 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))) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,st_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) if_7#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_3) 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) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(three(),head(in_3)),st_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> empty#(fstsplit(m,app(map_f(three(),head(in_3)),st_3))) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(three(),head(in_3)),st_3)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_9#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(in_3) 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) TRS: f47(x,y) -> x f47(x,y) -> y map_f(pid,nil()) -> nil() map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 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() sndsplit(0(),x) -> x sndsplit(s(n),nil()) -> nil() sndsplit(s(n),cons(h,t)) -> sndsplit(n,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) head(cons(h,t)) -> h app(nil(),x) -> x app(cons(h,t),x) -> cons(h,app(t,x)) tail(cons(h,t)) -> t graph: 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) 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) -> 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))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) 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) -> 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))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) 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) -> 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))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> 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))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> 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))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> 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))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) -> map_f#(pid,cons(h,t)) -> map_f#(pid,t) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) -> map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(three(),head(in_3)),st_3)) -> sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) 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) -> 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))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) 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) -> 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))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) 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) -> 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))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_7#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_3) -> sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(three(),head(in_3)),st_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) -> map_f#(pid,cons(h,t)) -> map_f#(pid,t) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) -> map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(three(),head(in_3)),st_3)) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) -> if_7#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) -> 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) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_3) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) 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) -> 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))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) 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) -> 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))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) 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) -> 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))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) 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) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> 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))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> 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))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> 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))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) -> map_f#(pid,cons(h,t)) -> map_f#(pid,t) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) -> map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(two(),head(in_2)),st_2)) -> sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> 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))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> 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))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> 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))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_2) -> sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_2) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) -> if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) -> map_f#(pid,cons(h,t)) -> map_f#(pid,t) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) -> map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_2) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> 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))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> 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))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> 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))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) -> ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_1) -> sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_1) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(in_3) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) -> 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) 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))) -> if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_3) 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))) -> if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,st_3)) 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))) -> if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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))) -> if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3) 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))) -> if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) 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))) -> if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) 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))) -> if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(three(),head(in_3)),st_3)) 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))) -> if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> empty#(fstsplit(m,app(map_f(three(),head(in_3)),st_3))) 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))) -> if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(in_2) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) -> 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) 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))) -> if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_2) 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))) -> if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,st_2)) 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))) -> if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) 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))) -> if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_2) 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))) -> if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) 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))) -> if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) 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))) -> if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) 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))) -> if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> empty#(fstsplit(m,app(map_f(two(),head(in_2)),st_2))) 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))) -> if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) 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))) -> if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_1) 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))) -> if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_1) 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))) -> if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) -> map_f#(pid,cons(h,t)) -> map_f#(pid,t) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) -> map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) -> map_f#(pid,cons(h,t)) -> map_f#(pid,t) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) -> map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) -> length#(cons(h,t)) -> length#(t) ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) -> length#(cons(h,t)) -> length#(t) ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) -> leq#(s(n),s(m)) -> leq#(n,m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) -> leq#(s(n),s(m)) -> leq#(n,m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,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)) -> 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) 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)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1)) 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))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_1) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_1) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) 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))) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,st_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_2) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_2) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> empty#(fstsplit(m,app(map_f(two(),head(in_2)),st_2))) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(two(),head(in_2)),st_2)) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_2) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2))) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_5#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(in_2) 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) ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) 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))) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,st_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) if_7#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_3) 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) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(three(),head(in_3)),st_3)) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> empty#(fstsplit(m,app(map_f(three(),head(in_3)),st_3))) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(three(),head(in_3)),st_3)) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_3) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3) ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3))) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_9#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(in_3) 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) 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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3),st_3, m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) SCC Processor: #sccs: 7 #rules: 22 #arcs: 198/4489 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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x0 + 1, [if_9](x0, x1, x2, x3, x4, x5, x6) = 0, [if_8](x0, x1, x2, x3, x4, x5, x6) = 0, [three] = 0, [if_7](x0, x1, x2, x3, x4, x5, x6) = 0, [if_6](x0, x1, x2, x3, x4, x5, x6) = 0, [if_5](x0, x1, x2, x3, x4, x5, x6) = 0, [if_4](x0, x1, x2, x3, x4, x5, x6) = 0, [two] = 1, [if_3](x0, x1, x2, x3, x4, x5, x6) = 0, [if_2](x0, x1, x2, x3, x4, x5, x6) = 0, [if_1](x0, x1, x2, x3, x4, x5, x6) = 0, [ring](x0, x1, x2, x3, x4, x5) = 0, [tail](x0) = x0, [head](x0) = x0, [f](x0, x1) = 0, [map_f](x0, x1) = x0, [app](x0, x1) = x0 + x1, [length](x0) = 0, [leq](x0, x1) = 0, [false] = 0, [true] = 0, [empty](x0) = 0, [sndsplit](x0, x1) = x1, [cons](x0, x1) = x0 + x1 + 1, [s](x0) = 0, [nil] = 0, [fstsplit](x0, x1) = x1, [0] = 0 orientation: app#(cons(h,t),x) = h + 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)) = h + t + 1 >= h + 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)) = h + t + 1 >= t = 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)) = 0 >= 0 = s(length(t)) app(nil(),x) = x >= x = x app(cons(h,t),x) = h + t + x + 1 >= h + t + x + 1 = cons(h,app(t,x)) map_f(pid,nil()) = pid >= 0 = nil() map_f(pid,cons(h,t)) = pid >= pid = app(f(pid,h),map_f(pid,t)) head(cons(h,t)) = h + t + 1 >= h = h tail(cons(h,t)) = h + t + 1 >= t = t ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_1(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_2(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_2))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)),cons (fstsplit ( m, app ( map_f ( two(), head ( in_2)), st_2)), in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_5(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,tail(in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_6(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_3))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) if_7(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)), m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_9(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),st_3,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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) Qed DPs: 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) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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))) if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring#(st_1,in_2,st_2,in_3,st_3,m) -> if_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) 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))) if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring#(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) 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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) 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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) Matrix Interpretation Processor: dimension: 1 interpretation: [sndsplit#](x0, x1) = x1 + 1, [if_9](x0, x1, x2, x3, x4, x5, x6) = 0, [if_8](x0, x1, x2, x3, x4, x5, x6) = 0, [three] = 0, [if_7](x0, x1, x2, x3, x4, x5, x6) = 0, [if_6](x0, x1, x2, x3, x4, x5, x6) = 0, [if_5](x0, x1, x2, x3, x4, x5, x6) = 0, [if_4](x0, x1, x2, x3, x4, x5, x6) = 0, [two] = 0, [if_3](x0, x1, x2, x3, x4, x5, x6) = 0, [if_2](x0, x1, x2, x3, x4, x5, x6) = 0, [if_1](x0, x1, x2, x3, x4, x5, x6) = 0, [ring](x0, x1, x2, x3, x4, x5) = 0, [tail](x0) = x0, [head](x0) = x0, [f](x0, x1) = 0, [map_f](x0, x1) = 0, [app](x0, x1) = x0 + x1, [length](x0) = 1, [leq](x0, x1) = x0, [false] = 0, [true] = 0, [empty](x0) = x0, [sndsplit](x0, x1) = x1, [cons](x0, x1) = x0 + x1 + 1, [s](x0) = x0, [nil] = 0, [fstsplit](x0, x1) = x1, [0] = 1 orientation: sndsplit#(s(n),cons(h,t)) = h + t + 2 >= t + 1 = sndsplit#(n,t) fstsplit(0(),x) = x >= 0 = nil() fstsplit(s(n),nil()) = 0 >= 0 = nil() fstsplit(s(n),cons(h,t)) = h + t + 1 >= h + 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)) = h + t + 1 >= t = sndsplit(n,t) empty(nil()) = 0 >= 0 = true() empty(cons(h,t)) = h + t + 1 >= 0 = false() leq(0(),m) = 1 >= 0 = true() leq(s(n),0()) = n >= 0 = false() leq(s(n),s(m)) = n >= n = leq(n,m) length(nil()) = 1 >= 1 = 0() length(cons(h,t)) = 1 >= 1 = s(length(t)) app(nil(),x) = x >= x = x app(cons(h,t),x) = h + t + x + 1 >= h + 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)) head(cons(h,t)) = h + t + 1 >= h = h tail(cons(h,t)) = h + t + 1 >= t = t ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_1(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_2(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_2))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)),cons (fstsplit ( m, app ( map_f ( two(), head ( in_2)), st_2)), in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_5(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,tail(in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_6(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_3))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) if_7(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)), m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_9(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),st_3,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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) 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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) Matrix Interpretation Processor: dimension: 1 interpretation: [fstsplit#](x0, x1) = x1 + 1, [if_9](x0, x1, x2, x3, x4, x5, x6) = 0, [if_8](x0, x1, x2, x3, x4, x5, x6) = 0, [three] = 0, [if_7](x0, x1, x2, x3, x4, x5, x6) = 0, [if_6](x0, x1, x2, x3, x4, x5, x6) = 0, [if_5](x0, x1, x2, x3, x4, x5, x6) = 0, [if_4](x0, x1, x2, x3, x4, x5, x6) = 0, [two] = 0, [if_3](x0, x1, x2, x3, x4, x5, x6) = 0, [if_2](x0, x1, x2, x3, x4, x5, x6) = 0, [if_1](x0, x1, x2, x3, x4, x5, x6) = 0, [ring](x0, x1, x2, x3, x4, x5) = 0, [tail](x0) = x0, [head](x0) = x0, [f](x0, x1) = 0, [map_f](x0, x1) = 0, [app](x0, x1) = x0 + x1, [length](x0) = 1, [leq](x0, x1) = x0, [false] = 0, [true] = 0, [empty](x0) = x0, [sndsplit](x0, x1) = x1, [cons](x0, x1) = x0 + x1 + 1, [s](x0) = x0, [nil] = 0, [fstsplit](x0, x1) = x1, [0] = 1 orientation: fstsplit#(s(n),cons(h,t)) = h + t + 2 >= t + 1 = fstsplit#(n,t) fstsplit(0(),x) = x >= 0 = nil() fstsplit(s(n),nil()) = 0 >= 0 = nil() fstsplit(s(n),cons(h,t)) = h + t + 1 >= h + 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)) = h + t + 1 >= t = sndsplit(n,t) empty(nil()) = 0 >= 0 = true() empty(cons(h,t)) = h + t + 1 >= 0 = false() leq(0(),m) = 1 >= 0 = true() leq(s(n),0()) = n >= 0 = false() leq(s(n),s(m)) = n >= n = leq(n,m) length(nil()) = 1 >= 1 = 0() length(cons(h,t)) = 1 >= 1 = s(length(t)) app(nil(),x) = x >= x = x app(cons(h,t),x) = h + t + x + 1 >= h + 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)) head(cons(h,t)) = h + t + 1 >= h = h tail(cons(h,t)) = h + t + 1 >= t = t ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_1(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_2(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_2))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)),cons (fstsplit ( m, app ( map_f ( two(), head ( in_2)), st_2)), in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_5(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,tail(in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_6(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_3))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) if_7(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)), m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_9(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),st_3,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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) 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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) Matrix Interpretation Processor: dimension: 1 interpretation: [length#](x0) = x0 + 1, [if_9](x0, x1, x2, x3, x4, x5, x6) = 0, [if_8](x0, x1, x2, x3, x4, x5, x6) = 0, [three] = 0, [if_7](x0, x1, x2, x3, x4, x5, x6) = 0, [if_6](x0, x1, x2, x3, x4, x5, x6) = 0, [if_5](x0, x1, x2, x3, x4, x5, x6) = 0, [if_4](x0, x1, x2, x3, x4, x5, x6) = 0, [two] = 0, [if_3](x0, x1, x2, x3, x4, x5, x6) = 0, [if_2](x0, x1, x2, x3, x4, x5, x6) = 0, [if_1](x0, x1, x2, x3, x4, x5, x6) = 0, [ring](x0, x1, x2, x3, x4, x5) = 0, [tail](x0) = x0, [head](x0) = x0, [f](x0, x1) = x1 + 1, [map_f](x0, x1) = x1 + 1, [app](x0, x1) = x0 + x1, [length](x0) = x0, [leq](x0, x1) = 0, [false] = 0, [true] = 0, [empty](x0) = x0 + 1, [sndsplit](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [nil] = 1, [fstsplit](x0, x1) = x1 + 1, [0] = 1 orientation: length#(cons(h,t)) = h + t + 2 >= t + 1 = length#(t) fstsplit(0(),x) = x + 1 >= 1 = nil() fstsplit(s(n),nil()) = 2 >= 1 = nil() fstsplit(s(n),cons(h,t)) = h + t + 2 >= h + t + 2 = cons(h,fstsplit(n,t)) sndsplit(0(),x) = x + 2 >= x = x sndsplit(s(n),nil()) = n + 3 >= 1 = nil() sndsplit(s(n),cons(h,t)) = h + n + t + 3 >= n + t + 1 = sndsplit(n,t) empty(nil()) = 2 >= 0 = true() empty(cons(h,t)) = h + t + 2 >= 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()) = 1 >= 1 = 0() length(cons(h,t)) = h + t + 1 >= t + 1 = s(length(t)) app(nil(),x) = x + 1 >= x = x app(cons(h,t),x) = h + t + x + 1 >= h + t + x + 1 = cons(h,app(t,x)) map_f(pid,nil()) = 2 >= 1 = nil() map_f(pid,cons(h,t)) = h + t + 2 >= h + t + 2 = app(f(pid,h),map_f(pid,t)) head(cons(h,t)) = h + t + 1 >= h = h tail(cons(h,t)) = h + t + 1 >= t = t ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_1(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_2(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_2))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)),cons (fstsplit ( m, app ( map_f ( two(), head ( in_2)), st_2)), in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_5(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,tail(in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_6(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_3))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) if_7(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)), m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_9(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),st_3,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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) 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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) Matrix Interpretation Processor: dimension: 1 interpretation: [leq#](x0, x1) = x1 + 1, [if_9](x0, x1, x2, x3, x4, x5, x6) = 0, [if_8](x0, x1, x2, x3, x4, x5, x6) = 0, [three] = 0, [if_7](x0, x1, x2, x3, x4, x5, x6) = 0, [if_6](x0, x1, x2, x3, x4, x5, x6) = 0, [if_5](x0, x1, x2, x3, x4, x5, x6) = 0, [if_4](x0, x1, x2, x3, x4, x5, x6) = 0, [two] = 0, [if_3](x0, x1, x2, x3, x4, x5, x6) = 0, [if_2](x0, x1, x2, x3, x4, x5, x6) = 0, [if_1](x0, x1, x2, x3, x4, x5, x6) = 0, [ring](x0, x1, x2, x3, x4, x5) = 0, [tail](x0) = x0, [head](x0) = x0, [f](x0, x1) = x1 + 1, [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, [cons](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [nil] = 0, [fstsplit](x0, x1) = x1, [0] = 0 orientation: leq#(s(n),s(m)) = m + 2 >= m + 1 = leq#(n,m) fstsplit(0(),x) = x >= 0 = nil() fstsplit(s(n),nil()) = 0 >= 0 = nil() fstsplit(s(n),cons(h,t)) = h + t + 1 >= h + 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)) = h + t + 1 >= t = 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)) = h + t + 1 >= t + 1 = s(length(t)) app(nil(),x) = x >= x = x app(cons(h,t),x) = h + t + x + 1 >= h + t + x + 1 = cons(h,app(t,x)) map_f(pid,nil()) = 0 >= 0 = nil() map_f(pid,cons(h,t)) = h + t + 1 >= h + t + 1 = app(f(pid,h),map_f(pid,t)) head(cons(h,t)) = h + t + 1 >= h = h tail(cons(h,t)) = h + t + 1 >= t = t ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_1(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_2(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_2))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)),cons (fstsplit ( m, app ( map_f ( two(), head ( in_2)), st_2)), in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_5(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,tail(in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_6(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_3))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) if_7(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)), m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_9(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),st_3,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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) 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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) Matrix Interpretation Processor: dimension: 1 interpretation: [map_f#](x0, x1) = x1 + 1, [if_9](x0, x1, x2, x3, x4, x5, x6) = 0, [if_8](x0, x1, x2, x3, x4, x5, x6) = 0, [three] = 0, [if_7](x0, x1, x2, x3, x4, x5, x6) = 0, [if_6](x0, x1, x2, x3, x4, x5, x6) = 0, [if_5](x0, x1, x2, x3, x4, x5, x6) = 0, [if_4](x0, x1, x2, x3, x4, x5, x6) = 0, [two] = 1, [if_3](x0, x1, x2, x3, x4, x5, x6) = 0, [if_2](x0, x1, x2, x3, x4, x5, x6) = 0, [if_1](x0, x1, x2, x3, x4, x5, x6) = 0, [ring](x0, x1, x2, x3, x4, x5) = 0, [tail](x0) = x0, [head](x0) = x0, [f](x0, x1) = 0, [map_f](x0, x1) = x0, [app](x0, x1) = x0 + x1, [length](x0) = 0, [leq](x0, x1) = 0, [false] = 0, [true] = 0, [empty](x0) = 0, [sndsplit](x0, x1) = x1, [cons](x0, x1) = x0 + x1 + 1, [s](x0) = 0, [nil] = 0, [fstsplit](x0, x1) = x1, [0] = 0 orientation: map_f#(pid,cons(h,t)) = h + 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)) = h + t + 1 >= h + 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)) = h + t + 1 >= t = 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)) = 0 >= 0 = s(length(t)) app(nil(),x) = x >= x = x app(cons(h,t),x) = h + t + x + 1 >= h + t + x + 1 = cons(h,app(t,x)) map_f(pid,nil()) = pid >= 0 = nil() map_f(pid,cons(h,t)) = pid >= pid = app(f(pid,h),map_f(pid,t)) head(cons(h,t)) = h + t + 1 >= h = h tail(cons(h,t)) = h + t + 1 >= t = t ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_1(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_2(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_2))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)),cons (fstsplit ( m, app ( map_f ( two(), head ( in_2)), st_2)), in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) if_5(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,tail(in_2),st_2,in_3,st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_6(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_3))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) if_7(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)), m) ring(st_1,in_2,st_2,in_3,st_3,m) = 0 >= 0 = if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) if_9(st_1,in_2,st_2,in_3,st_3,m,true()) = 0 >= 0 = ring(st_1,in_2,st_2,tail(in_3),st_3,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)) head(cons(h,t)) -> h tail(cons(h,t)) -> t 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))) if_1(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) 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))) if_2(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2))) if_3(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) if_2(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_4(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two(),head(in_2)),st_2)), cons(fstsplit(m,app(map_f(two(),head(in_2)),st_2)),in_3), st_3,m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2)))) 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) 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))) if_6(st_1,in_2,st_2,in_3,st_3,m,true()) -> if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3))) 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) if_6(st_1,in_2,st_2,in_3,st_3,m,false()) -> 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)))) if_8(st_1,in_2,st_2,in_3,st_3,m,false()) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three(),head(in_3)),st_3)),m) ring(st_1,in_2,st_2,in_3,st_3,m) -> if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3)))) 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) Qed