MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: active(afterNth(N,XS)) -> mark(snd(splitAt(N,XS))) active(afterNth(X1,X2)) -> afterNth(X1,active(X2)) active(afterNth(X1,X2)) -> afterNth(active(X1),X2) active(cons(X1,X2)) -> cons(active(X1),X2) active(fst(X)) -> fst(active(X)) active(fst(pair(XS,YS))) -> mark(XS) active(head(X)) -> head(active(X)) active(head(cons(N,XS))) -> mark(N) active(natsFrom(N)) -> mark(cons(N,natsFrom(s(N)))) active(natsFrom(X)) -> natsFrom(active(X)) active(pair(X1,X2)) -> pair(X1,active(X2)) active(pair(X1,X2)) -> pair(active(X1),X2) active(s(X)) -> s(active(X)) active(sel(N,XS)) -> mark(head(afterNth(N,XS))) active(sel(X1,X2)) -> sel(X1,active(X2)) active(sel(X1,X2)) -> sel(active(X1),X2) active(snd(X)) -> snd(active(X)) active(snd(pair(XS,YS))) -> mark(YS) active(splitAt(X1,X2)) -> splitAt(X1,active(X2)) active(splitAt(X1,X2)) -> splitAt(active(X1),X2) active(splitAt(0(),XS)) -> mark(pair(nil(),XS)) active(splitAt(s(N),cons(X,XS))) -> mark(u(splitAt(N,XS),N,X,XS)) active(tail(X)) -> tail(active(X)) active(tail(cons(N,XS))) -> mark(XS) active(take(N,XS)) -> mark(fst(splitAt(N,XS))) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(u(X1,X2,X3,X4)) -> u(active(X1),X2,X3,X4) active(u(pair(YS,ZS),N,X,XS)) -> mark(pair(cons(X,YS),ZS)) afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2)) afterNth(mark(X1),X2) -> mark(afterNth(X1,X2)) afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) fst(mark(X)) -> mark(fst(X)) fst(ok(X)) -> ok(fst(X)) head(mark(X)) -> mark(head(X)) head(ok(X)) -> ok(head(X)) natsFrom(mark(X)) -> mark(natsFrom(X)) natsFrom(ok(X)) -> ok(natsFrom(X)) pair(X1,mark(X2)) -> mark(pair(X1,X2)) pair(mark(X1),X2) -> mark(pair(X1,X2)) pair(ok(X1),ok(X2)) -> ok(pair(X1,X2)) proper(0()) -> ok(0()) proper(afterNth(X1,X2)) -> afterNth(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(fst(X)) -> fst(proper(X)) proper(head(X)) -> head(proper(X)) proper(natsFrom(X)) -> natsFrom(proper(X)) proper(nil()) -> ok(nil()) proper(pair(X1,X2)) -> pair(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(snd(X)) -> snd(proper(X)) proper(splitAt(X1,X2)) -> splitAt(proper(X1),proper(X2)) proper(tail(X)) -> tail(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(u(X1,X2,X3,X4)) -> u(proper(X1),proper(X2),proper(X3),proper(X4)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) snd(mark(X)) -> mark(snd(X)) snd(ok(X)) -> ok(snd(X)) splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2)) splitAt(mark(X1),X2) -> mark(splitAt(X1,X2)) splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2)) tail(mark(X)) -> mark(tail(X)) tail(ok(X)) -> ok(tail(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) u(mark(X1),X2,X3,X4) -> mark(u(X1,X2,X3,X4)) u(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(u(X1,X2,X3,X4)) - Signature: {active/1,afterNth/2,cons/2,fst/1,head/1,natsFrom/1,pair/2,proper/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2 ,top/1,u/4} / {0/0,mark/1,nil/0,ok/1} - Obligation: innermost runtime complexity wrt. defined symbols {active,afterNth,cons,fst,head,natsFrom,pair,proper,s,sel ,snd,splitAt,tail,take,top,u} and constructors {0,mark,nil,ok} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)) active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)) active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)) active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)) active#(fst(X)) -> c_5(fst#(active(X)),active#(X)) active#(fst(pair(XS,YS))) -> c_6() active#(head(X)) -> c_7(head#(active(X)),active#(X)) active#(head(cons(N,XS))) -> c_8() active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)) active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)) active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)) active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)) active#(s(X)) -> c_13(s#(active(X)),active#(X)) active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)) active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)) active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)) active#(snd(X)) -> c_17(snd#(active(X)),active#(X)) active#(snd(pair(XS,YS))) -> c_18() active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)) active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)) active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)) active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)) active#(tail(X)) -> c_23(tail#(active(X)),active#(X)) active#(tail(cons(N,XS))) -> c_24() active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)) active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)) active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)) active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)) afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)) afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)) afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)) cons#(mark(X1),X2) -> c_33(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)) fst#(mark(X)) -> c_35(fst#(X)) fst#(ok(X)) -> c_36(fst#(X)) head#(mark(X)) -> c_37(head#(X)) head#(ok(X)) -> c_38(head#(X)) natsFrom#(mark(X)) -> c_39(natsFrom#(X)) natsFrom#(ok(X)) -> c_40(natsFrom#(X)) pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)) pair#(mark(X1),X2) -> c_42(pair#(X1,X2)) pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)) proper#(0()) -> c_44() proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)) proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)) proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)) proper#(nil()) -> c_50() proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)) proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)) proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)) s#(mark(X)) -> c_59(s#(X)) s#(ok(X)) -> c_60(s#(X)) sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)) sel#(mark(X1),X2) -> c_62(sel#(X1,X2)) sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)) snd#(mark(X)) -> c_64(snd#(X)) snd#(ok(X)) -> c_65(snd#(X)) splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)) splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)) splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)) tail#(mark(X)) -> c_69(tail#(X)) tail#(ok(X)) -> c_70(tail#(X)) take#(X1,mark(X2)) -> c_71(take#(X1,X2)) take#(mark(X1),X2) -> c_72(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)) top#(mark(X)) -> c_74(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_75(top#(active(X)),active#(X)) u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)) u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)) active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)) active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)) active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)) active#(fst(X)) -> c_5(fst#(active(X)),active#(X)) active#(fst(pair(XS,YS))) -> c_6() active#(head(X)) -> c_7(head#(active(X)),active#(X)) active#(head(cons(N,XS))) -> c_8() active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)) active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)) active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)) active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)) active#(s(X)) -> c_13(s#(active(X)),active#(X)) active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)) active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)) active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)) active#(snd(X)) -> c_17(snd#(active(X)),active#(X)) active#(snd(pair(XS,YS))) -> c_18() active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)) active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)) active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)) active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)) active#(tail(X)) -> c_23(tail#(active(X)),active#(X)) active#(tail(cons(N,XS))) -> c_24() active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)) active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)) active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)) active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)) afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)) afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)) afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)) cons#(mark(X1),X2) -> c_33(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)) fst#(mark(X)) -> c_35(fst#(X)) fst#(ok(X)) -> c_36(fst#(X)) head#(mark(X)) -> c_37(head#(X)) head#(ok(X)) -> c_38(head#(X)) natsFrom#(mark(X)) -> c_39(natsFrom#(X)) natsFrom#(ok(X)) -> c_40(natsFrom#(X)) pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)) pair#(mark(X1),X2) -> c_42(pair#(X1,X2)) pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)) proper#(0()) -> c_44() proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)) proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)) proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)) proper#(nil()) -> c_50() proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)) proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)) proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)) s#(mark(X)) -> c_59(s#(X)) s#(ok(X)) -> c_60(s#(X)) sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)) sel#(mark(X1),X2) -> c_62(sel#(X1,X2)) sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)) snd#(mark(X)) -> c_64(snd#(X)) snd#(ok(X)) -> c_65(snd#(X)) splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)) splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)) splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)) tail#(mark(X)) -> c_69(tail#(X)) tail#(ok(X)) -> c_70(tail#(X)) take#(X1,mark(X2)) -> c_71(take#(X1,X2)) take#(mark(X1),X2) -> c_72(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)) top#(mark(X)) -> c_74(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_75(top#(active(X)),active#(X)) u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)) u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)) - Weak TRS: active(afterNth(N,XS)) -> mark(snd(splitAt(N,XS))) active(afterNth(X1,X2)) -> afterNth(X1,active(X2)) active(afterNth(X1,X2)) -> afterNth(active(X1),X2) active(cons(X1,X2)) -> cons(active(X1),X2) active(fst(X)) -> fst(active(X)) active(fst(pair(XS,YS))) -> mark(XS) active(head(X)) -> head(active(X)) active(head(cons(N,XS))) -> mark(N) active(natsFrom(N)) -> mark(cons(N,natsFrom(s(N)))) active(natsFrom(X)) -> natsFrom(active(X)) active(pair(X1,X2)) -> pair(X1,active(X2)) active(pair(X1,X2)) -> pair(active(X1),X2) active(s(X)) -> s(active(X)) active(sel(N,XS)) -> mark(head(afterNth(N,XS))) active(sel(X1,X2)) -> sel(X1,active(X2)) active(sel(X1,X2)) -> sel(active(X1),X2) active(snd(X)) -> snd(active(X)) active(snd(pair(XS,YS))) -> mark(YS) active(splitAt(X1,X2)) -> splitAt(X1,active(X2)) active(splitAt(X1,X2)) -> splitAt(active(X1),X2) active(splitAt(0(),XS)) -> mark(pair(nil(),XS)) active(splitAt(s(N),cons(X,XS))) -> mark(u(splitAt(N,XS),N,X,XS)) active(tail(X)) -> tail(active(X)) active(tail(cons(N,XS))) -> mark(XS) active(take(N,XS)) -> mark(fst(splitAt(N,XS))) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(u(X1,X2,X3,X4)) -> u(active(X1),X2,X3,X4) active(u(pair(YS,ZS),N,X,XS)) -> mark(pair(cons(X,YS),ZS)) afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2)) afterNth(mark(X1),X2) -> mark(afterNth(X1,X2)) afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) fst(mark(X)) -> mark(fst(X)) fst(ok(X)) -> ok(fst(X)) head(mark(X)) -> mark(head(X)) head(ok(X)) -> ok(head(X)) natsFrom(mark(X)) -> mark(natsFrom(X)) natsFrom(ok(X)) -> ok(natsFrom(X)) pair(X1,mark(X2)) -> mark(pair(X1,X2)) pair(mark(X1),X2) -> mark(pair(X1,X2)) pair(ok(X1),ok(X2)) -> ok(pair(X1,X2)) proper(0()) -> ok(0()) proper(afterNth(X1,X2)) -> afterNth(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(fst(X)) -> fst(proper(X)) proper(head(X)) -> head(proper(X)) proper(natsFrom(X)) -> natsFrom(proper(X)) proper(nil()) -> ok(nil()) proper(pair(X1,X2)) -> pair(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(snd(X)) -> snd(proper(X)) proper(splitAt(X1,X2)) -> splitAt(proper(X1),proper(X2)) proper(tail(X)) -> tail(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(u(X1,X2,X3,X4)) -> u(proper(X1),proper(X2),proper(X3),proper(X4)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) snd(mark(X)) -> mark(snd(X)) snd(ok(X)) -> ok(snd(X)) splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2)) splitAt(mark(X1),X2) -> mark(splitAt(X1,X2)) splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2)) tail(mark(X)) -> mark(tail(X)) tail(ok(X)) -> ok(tail(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) u(mark(X1),X2,X3,X4) -> mark(u(X1,X2,X3,X4)) u(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(u(X1,X2,X3,X4)) - Signature: {active/1,afterNth/2,cons/2,fst/1,head/1,natsFrom/1,pair/2,proper/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2 ,top/1,u/4,active#/1,afterNth#/2,cons#/2,fst#/1,head#/1,natsFrom#/1,pair#/2,proper#/1,s#/1,sel#/2,snd#/1 ,splitAt#/2,tail#/1,take#/2,top#/1,u#/4} / {0/0,mark/1,nil/0,ok/1,c_1/2,c_2/2,c_3/2,c_4/2,c_5/2,c_6/0,c_7/2 ,c_8/0,c_9/3,c_10/2,c_11/2,c_12/2,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/0,c_19/2,c_20/2,c_21/1,c_22/2 ,c_23/2,c_24/0,c_25/2,c_26/2,c_27/2,c_28/2,c_29/2,c_30/1,c_31/1,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/1 ,c_38/1,c_39/1,c_40/1,c_41/1,c_42/1,c_43/1,c_44/0,c_45/3,c_46/3,c_47/2,c_48/2,c_49/2,c_50/0,c_51/3,c_52/2 ,c_53/3,c_54/2,c_55/3,c_56/2,c_57/3,c_58/5,c_59/1,c_60/1,c_61/1,c_62/1,c_63/1,c_64/1,c_65/1,c_66/1,c_67/1 ,c_68/1,c_69/1,c_70/1,c_71/1,c_72/1,c_73/1,c_74/2,c_75/2,c_76/1,c_77/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,afterNth#,cons#,fst#,head#,natsFrom#,pair# ,proper#,s#,sel#,snd#,splitAt#,tail#,take#,top#,u#} and constructors {0,mark,nil,ok} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: active(afterNth(N,XS)) -> mark(snd(splitAt(N,XS))) active(afterNth(X1,X2)) -> afterNth(X1,active(X2)) active(afterNth(X1,X2)) -> afterNth(active(X1),X2) active(cons(X1,X2)) -> cons(active(X1),X2) active(fst(X)) -> fst(active(X)) active(fst(pair(XS,YS))) -> mark(XS) active(head(X)) -> head(active(X)) active(head(cons(N,XS))) -> mark(N) active(natsFrom(N)) -> mark(cons(N,natsFrom(s(N)))) active(natsFrom(X)) -> natsFrom(active(X)) active(pair(X1,X2)) -> pair(X1,active(X2)) active(pair(X1,X2)) -> pair(active(X1),X2) active(s(X)) -> s(active(X)) active(sel(N,XS)) -> mark(head(afterNth(N,XS))) active(sel(X1,X2)) -> sel(X1,active(X2)) active(sel(X1,X2)) -> sel(active(X1),X2) active(snd(X)) -> snd(active(X)) active(snd(pair(XS,YS))) -> mark(YS) active(splitAt(X1,X2)) -> splitAt(X1,active(X2)) active(splitAt(X1,X2)) -> splitAt(active(X1),X2) active(splitAt(0(),XS)) -> mark(pair(nil(),XS)) active(splitAt(s(N),cons(X,XS))) -> mark(u(splitAt(N,XS),N,X,XS)) active(tail(X)) -> tail(active(X)) active(tail(cons(N,XS))) -> mark(XS) active(take(N,XS)) -> mark(fst(splitAt(N,XS))) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(u(X1,X2,X3,X4)) -> u(active(X1),X2,X3,X4) active(u(pair(YS,ZS),N,X,XS)) -> mark(pair(cons(X,YS),ZS)) afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2)) afterNth(mark(X1),X2) -> mark(afterNth(X1,X2)) afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) fst(mark(X)) -> mark(fst(X)) fst(ok(X)) -> ok(fst(X)) head(mark(X)) -> mark(head(X)) head(ok(X)) -> ok(head(X)) natsFrom(mark(X)) -> mark(natsFrom(X)) natsFrom(ok(X)) -> ok(natsFrom(X)) pair(X1,mark(X2)) -> mark(pair(X1,X2)) pair(mark(X1),X2) -> mark(pair(X1,X2)) pair(ok(X1),ok(X2)) -> ok(pair(X1,X2)) proper(0()) -> ok(0()) proper(afterNth(X1,X2)) -> afterNth(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(fst(X)) -> fst(proper(X)) proper(head(X)) -> head(proper(X)) proper(natsFrom(X)) -> natsFrom(proper(X)) proper(nil()) -> ok(nil()) proper(pair(X1,X2)) -> pair(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(snd(X)) -> snd(proper(X)) proper(splitAt(X1,X2)) -> splitAt(proper(X1),proper(X2)) proper(tail(X)) -> tail(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(u(X1,X2,X3,X4)) -> u(proper(X1),proper(X2),proper(X3),proper(X4)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) snd(mark(X)) -> mark(snd(X)) snd(ok(X)) -> ok(snd(X)) splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2)) splitAt(mark(X1),X2) -> mark(splitAt(X1,X2)) splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2)) tail(mark(X)) -> mark(tail(X)) tail(ok(X)) -> ok(tail(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) u(mark(X1),X2,X3,X4) -> mark(u(X1,X2,X3,X4)) u(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(u(X1,X2,X3,X4)) active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)) active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)) active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)) active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)) active#(fst(X)) -> c_5(fst#(active(X)),active#(X)) active#(fst(pair(XS,YS))) -> c_6() active#(head(X)) -> c_7(head#(active(X)),active#(X)) active#(head(cons(N,XS))) -> c_8() active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)) active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)) active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)) active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)) active#(s(X)) -> c_13(s#(active(X)),active#(X)) active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)) active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)) active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)) active#(snd(X)) -> c_17(snd#(active(X)),active#(X)) active#(snd(pair(XS,YS))) -> c_18() active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)) active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)) active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)) active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)) active#(tail(X)) -> c_23(tail#(active(X)),active#(X)) active#(tail(cons(N,XS))) -> c_24() active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)) active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)) active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)) active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)) afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)) afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)) afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)) cons#(mark(X1),X2) -> c_33(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)) fst#(mark(X)) -> c_35(fst#(X)) fst#(ok(X)) -> c_36(fst#(X)) head#(mark(X)) -> c_37(head#(X)) head#(ok(X)) -> c_38(head#(X)) natsFrom#(mark(X)) -> c_39(natsFrom#(X)) natsFrom#(ok(X)) -> c_40(natsFrom#(X)) pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)) pair#(mark(X1),X2) -> c_42(pair#(X1,X2)) pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)) proper#(0()) -> c_44() proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)) proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)) proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)) proper#(nil()) -> c_50() proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)) proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)) proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)) s#(mark(X)) -> c_59(s#(X)) s#(ok(X)) -> c_60(s#(X)) sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)) sel#(mark(X1),X2) -> c_62(sel#(X1,X2)) sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)) snd#(mark(X)) -> c_64(snd#(X)) snd#(ok(X)) -> c_65(snd#(X)) splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)) splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)) splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)) tail#(mark(X)) -> c_69(tail#(X)) tail#(ok(X)) -> c_70(tail#(X)) take#(X1,mark(X2)) -> c_71(take#(X1,X2)) take#(mark(X1),X2) -> c_72(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)) top#(mark(X)) -> c_74(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_75(top#(active(X)),active#(X)) u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)) u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)) active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)) active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)) active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)) active#(fst(X)) -> c_5(fst#(active(X)),active#(X)) active#(fst(pair(XS,YS))) -> c_6() active#(head(X)) -> c_7(head#(active(X)),active#(X)) active#(head(cons(N,XS))) -> c_8() active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)) active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)) active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)) active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)) active#(s(X)) -> c_13(s#(active(X)),active#(X)) active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)) active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)) active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)) active#(snd(X)) -> c_17(snd#(active(X)),active#(X)) active#(snd(pair(XS,YS))) -> c_18() active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)) active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)) active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)) active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)) active#(tail(X)) -> c_23(tail#(active(X)),active#(X)) active#(tail(cons(N,XS))) -> c_24() active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)) active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)) active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)) active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)) afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)) afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)) afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)) cons#(mark(X1),X2) -> c_33(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)) fst#(mark(X)) -> c_35(fst#(X)) fst#(ok(X)) -> c_36(fst#(X)) head#(mark(X)) -> c_37(head#(X)) head#(ok(X)) -> c_38(head#(X)) natsFrom#(mark(X)) -> c_39(natsFrom#(X)) natsFrom#(ok(X)) -> c_40(natsFrom#(X)) pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)) pair#(mark(X1),X2) -> c_42(pair#(X1,X2)) pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)) proper#(0()) -> c_44() proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)) proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)) proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)) proper#(nil()) -> c_50() proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)) proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)) proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)) s#(mark(X)) -> c_59(s#(X)) s#(ok(X)) -> c_60(s#(X)) sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)) sel#(mark(X1),X2) -> c_62(sel#(X1,X2)) sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)) snd#(mark(X)) -> c_64(snd#(X)) snd#(ok(X)) -> c_65(snd#(X)) splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)) splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)) splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)) tail#(mark(X)) -> c_69(tail#(X)) tail#(ok(X)) -> c_70(tail#(X)) take#(X1,mark(X2)) -> c_71(take#(X1,X2)) take#(mark(X1),X2) -> c_72(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)) top#(mark(X)) -> c_74(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_75(top#(active(X)),active#(X)) u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)) u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)) - Weak TRS: active(afterNth(N,XS)) -> mark(snd(splitAt(N,XS))) active(afterNth(X1,X2)) -> afterNth(X1,active(X2)) active(afterNth(X1,X2)) -> afterNth(active(X1),X2) active(cons(X1,X2)) -> cons(active(X1),X2) active(fst(X)) -> fst(active(X)) active(fst(pair(XS,YS))) -> mark(XS) active(head(X)) -> head(active(X)) active(head(cons(N,XS))) -> mark(N) active(natsFrom(N)) -> mark(cons(N,natsFrom(s(N)))) active(natsFrom(X)) -> natsFrom(active(X)) active(pair(X1,X2)) -> pair(X1,active(X2)) active(pair(X1,X2)) -> pair(active(X1),X2) active(s(X)) -> s(active(X)) active(sel(N,XS)) -> mark(head(afterNth(N,XS))) active(sel(X1,X2)) -> sel(X1,active(X2)) active(sel(X1,X2)) -> sel(active(X1),X2) active(snd(X)) -> snd(active(X)) active(snd(pair(XS,YS))) -> mark(YS) active(splitAt(X1,X2)) -> splitAt(X1,active(X2)) active(splitAt(X1,X2)) -> splitAt(active(X1),X2) active(splitAt(0(),XS)) -> mark(pair(nil(),XS)) active(splitAt(s(N),cons(X,XS))) -> mark(u(splitAt(N,XS),N,X,XS)) active(tail(X)) -> tail(active(X)) active(tail(cons(N,XS))) -> mark(XS) active(take(N,XS)) -> mark(fst(splitAt(N,XS))) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(u(X1,X2,X3,X4)) -> u(active(X1),X2,X3,X4) active(u(pair(YS,ZS),N,X,XS)) -> mark(pair(cons(X,YS),ZS)) afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2)) afterNth(mark(X1),X2) -> mark(afterNth(X1,X2)) afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) fst(mark(X)) -> mark(fst(X)) fst(ok(X)) -> ok(fst(X)) head(mark(X)) -> mark(head(X)) head(ok(X)) -> ok(head(X)) natsFrom(mark(X)) -> mark(natsFrom(X)) natsFrom(ok(X)) -> ok(natsFrom(X)) pair(X1,mark(X2)) -> mark(pair(X1,X2)) pair(mark(X1),X2) -> mark(pair(X1,X2)) pair(ok(X1),ok(X2)) -> ok(pair(X1,X2)) proper(0()) -> ok(0()) proper(afterNth(X1,X2)) -> afterNth(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(fst(X)) -> fst(proper(X)) proper(head(X)) -> head(proper(X)) proper(natsFrom(X)) -> natsFrom(proper(X)) proper(nil()) -> ok(nil()) proper(pair(X1,X2)) -> pair(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(snd(X)) -> snd(proper(X)) proper(splitAt(X1,X2)) -> splitAt(proper(X1),proper(X2)) proper(tail(X)) -> tail(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(u(X1,X2,X3,X4)) -> u(proper(X1),proper(X2),proper(X3),proper(X4)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) snd(mark(X)) -> mark(snd(X)) snd(ok(X)) -> ok(snd(X)) splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2)) splitAt(mark(X1),X2) -> mark(splitAt(X1,X2)) splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2)) tail(mark(X)) -> mark(tail(X)) tail(ok(X)) -> ok(tail(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) u(mark(X1),X2,X3,X4) -> mark(u(X1,X2,X3,X4)) u(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(u(X1,X2,X3,X4)) - Signature: {active/1,afterNth/2,cons/2,fst/1,head/1,natsFrom/1,pair/2,proper/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2 ,top/1,u/4,active#/1,afterNth#/2,cons#/2,fst#/1,head#/1,natsFrom#/1,pair#/2,proper#/1,s#/1,sel#/2,snd#/1 ,splitAt#/2,tail#/1,take#/2,top#/1,u#/4} / {0/0,mark/1,nil/0,ok/1,c_1/2,c_2/2,c_3/2,c_4/2,c_5/2,c_6/0,c_7/2 ,c_8/0,c_9/3,c_10/2,c_11/2,c_12/2,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/0,c_19/2,c_20/2,c_21/1,c_22/2 ,c_23/2,c_24/0,c_25/2,c_26/2,c_27/2,c_28/2,c_29/2,c_30/1,c_31/1,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/1 ,c_38/1,c_39/1,c_40/1,c_41/1,c_42/1,c_43/1,c_44/0,c_45/3,c_46/3,c_47/2,c_48/2,c_49/2,c_50/0,c_51/3,c_52/2 ,c_53/3,c_54/2,c_55/3,c_56/2,c_57/3,c_58/5,c_59/1,c_60/1,c_61/1,c_62/1,c_63/1,c_64/1,c_65/1,c_66/1,c_67/1 ,c_68/1,c_69/1,c_70/1,c_71/1,c_72/1,c_73/1,c_74/2,c_75/2,c_76/1,c_77/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,afterNth#,cons#,fst#,head#,natsFrom#,pair# ,proper#,s#,sel#,snd#,splitAt#,tail#,take#,top#,u#} and constructors {0,mark,nil,ok} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {6,8,18,24,44,50} by application of Pre({6,8,18,24,44,50}) = {2,3,4,5,7,10,11,12,13,15,16,17,19,20,23,26,27,28,45,46,47,48,49,51,52,53,54,55 ,56,57,58,74,75}. Here rules are labelled as follows: 1: active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)) 2: active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)) 3: active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)) 4: active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)) 5: active#(fst(X)) -> c_5(fst#(active(X)),active#(X)) 6: active#(fst(pair(XS,YS))) -> c_6() 7: active#(head(X)) -> c_7(head#(active(X)),active#(X)) 8: active#(head(cons(N,XS))) -> c_8() 9: active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)) 10: active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)) 11: active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)) 12: active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)) 13: active#(s(X)) -> c_13(s#(active(X)),active#(X)) 14: active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)) 15: active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)) 16: active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)) 17: active#(snd(X)) -> c_17(snd#(active(X)),active#(X)) 18: active#(snd(pair(XS,YS))) -> c_18() 19: active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)) 20: active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)) 21: active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)) 22: active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)) 23: active#(tail(X)) -> c_23(tail#(active(X)),active#(X)) 24: active#(tail(cons(N,XS))) -> c_24() 25: active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)) 26: active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)) 27: active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)) 28: active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)) 29: active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)) 30: afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)) 31: afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)) 32: afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)) 33: cons#(mark(X1),X2) -> c_33(cons#(X1,X2)) 34: cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)) 35: fst#(mark(X)) -> c_35(fst#(X)) 36: fst#(ok(X)) -> c_36(fst#(X)) 37: head#(mark(X)) -> c_37(head#(X)) 38: head#(ok(X)) -> c_38(head#(X)) 39: natsFrom#(mark(X)) -> c_39(natsFrom#(X)) 40: natsFrom#(ok(X)) -> c_40(natsFrom#(X)) 41: pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)) 42: pair#(mark(X1),X2) -> c_42(pair#(X1,X2)) 43: pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)) 44: proper#(0()) -> c_44() 45: proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 46: proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 47: proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)) 48: proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)) 49: proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)) 50: proper#(nil()) -> c_50() 51: proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 52: proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)) 53: proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 54: proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)) 55: proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 56: proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)) 57: proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 58: proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)) 59: s#(mark(X)) -> c_59(s#(X)) 60: s#(ok(X)) -> c_60(s#(X)) 61: sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)) 62: sel#(mark(X1),X2) -> c_62(sel#(X1,X2)) 63: sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)) 64: snd#(mark(X)) -> c_64(snd#(X)) 65: snd#(ok(X)) -> c_65(snd#(X)) 66: splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)) 67: splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)) 68: splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)) 69: tail#(mark(X)) -> c_69(tail#(X)) 70: tail#(ok(X)) -> c_70(tail#(X)) 71: take#(X1,mark(X2)) -> c_71(take#(X1,X2)) 72: take#(mark(X1),X2) -> c_72(take#(X1,X2)) 73: take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)) 74: top#(mark(X)) -> c_74(top#(proper(X)),proper#(X)) 75: top#(ok(X)) -> c_75(top#(active(X)),active#(X)) 76: u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)) 77: u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)) active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)) active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)) active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)) active#(fst(X)) -> c_5(fst#(active(X)),active#(X)) active#(head(X)) -> c_7(head#(active(X)),active#(X)) active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)) active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)) active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)) active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)) active#(s(X)) -> c_13(s#(active(X)),active#(X)) active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)) active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)) active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)) active#(snd(X)) -> c_17(snd#(active(X)),active#(X)) active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)) active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)) active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)) active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)) active#(tail(X)) -> c_23(tail#(active(X)),active#(X)) active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)) active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)) active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)) active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)) afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)) afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)) afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)) cons#(mark(X1),X2) -> c_33(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)) fst#(mark(X)) -> c_35(fst#(X)) fst#(ok(X)) -> c_36(fst#(X)) head#(mark(X)) -> c_37(head#(X)) head#(ok(X)) -> c_38(head#(X)) natsFrom#(mark(X)) -> c_39(natsFrom#(X)) natsFrom#(ok(X)) -> c_40(natsFrom#(X)) pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)) pair#(mark(X1),X2) -> c_42(pair#(X1,X2)) pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)) proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)) proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)) proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)) proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)) proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)) proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)) s#(mark(X)) -> c_59(s#(X)) s#(ok(X)) -> c_60(s#(X)) sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)) sel#(mark(X1),X2) -> c_62(sel#(X1,X2)) sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)) snd#(mark(X)) -> c_64(snd#(X)) snd#(ok(X)) -> c_65(snd#(X)) splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)) splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)) splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)) tail#(mark(X)) -> c_69(tail#(X)) tail#(ok(X)) -> c_70(tail#(X)) take#(X1,mark(X2)) -> c_71(take#(X1,X2)) take#(mark(X1),X2) -> c_72(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)) top#(mark(X)) -> c_74(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_75(top#(active(X)),active#(X)) u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)) u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)) - Weak DPs: active#(fst(pair(XS,YS))) -> c_6() active#(head(cons(N,XS))) -> c_8() active#(snd(pair(XS,YS))) -> c_18() active#(tail(cons(N,XS))) -> c_24() proper#(0()) -> c_44() proper#(nil()) -> c_50() - Weak TRS: active(afterNth(N,XS)) -> mark(snd(splitAt(N,XS))) active(afterNth(X1,X2)) -> afterNth(X1,active(X2)) active(afterNth(X1,X2)) -> afterNth(active(X1),X2) active(cons(X1,X2)) -> cons(active(X1),X2) active(fst(X)) -> fst(active(X)) active(fst(pair(XS,YS))) -> mark(XS) active(head(X)) -> head(active(X)) active(head(cons(N,XS))) -> mark(N) active(natsFrom(N)) -> mark(cons(N,natsFrom(s(N)))) active(natsFrom(X)) -> natsFrom(active(X)) active(pair(X1,X2)) -> pair(X1,active(X2)) active(pair(X1,X2)) -> pair(active(X1),X2) active(s(X)) -> s(active(X)) active(sel(N,XS)) -> mark(head(afterNth(N,XS))) active(sel(X1,X2)) -> sel(X1,active(X2)) active(sel(X1,X2)) -> sel(active(X1),X2) active(snd(X)) -> snd(active(X)) active(snd(pair(XS,YS))) -> mark(YS) active(splitAt(X1,X2)) -> splitAt(X1,active(X2)) active(splitAt(X1,X2)) -> splitAt(active(X1),X2) active(splitAt(0(),XS)) -> mark(pair(nil(),XS)) active(splitAt(s(N),cons(X,XS))) -> mark(u(splitAt(N,XS),N,X,XS)) active(tail(X)) -> tail(active(X)) active(tail(cons(N,XS))) -> mark(XS) active(take(N,XS)) -> mark(fst(splitAt(N,XS))) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(u(X1,X2,X3,X4)) -> u(active(X1),X2,X3,X4) active(u(pair(YS,ZS),N,X,XS)) -> mark(pair(cons(X,YS),ZS)) afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2)) afterNth(mark(X1),X2) -> mark(afterNth(X1,X2)) afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) fst(mark(X)) -> mark(fst(X)) fst(ok(X)) -> ok(fst(X)) head(mark(X)) -> mark(head(X)) head(ok(X)) -> ok(head(X)) natsFrom(mark(X)) -> mark(natsFrom(X)) natsFrom(ok(X)) -> ok(natsFrom(X)) pair(X1,mark(X2)) -> mark(pair(X1,X2)) pair(mark(X1),X2) -> mark(pair(X1,X2)) pair(ok(X1),ok(X2)) -> ok(pair(X1,X2)) proper(0()) -> ok(0()) proper(afterNth(X1,X2)) -> afterNth(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(fst(X)) -> fst(proper(X)) proper(head(X)) -> head(proper(X)) proper(natsFrom(X)) -> natsFrom(proper(X)) proper(nil()) -> ok(nil()) proper(pair(X1,X2)) -> pair(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(snd(X)) -> snd(proper(X)) proper(splitAt(X1,X2)) -> splitAt(proper(X1),proper(X2)) proper(tail(X)) -> tail(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(u(X1,X2,X3,X4)) -> u(proper(X1),proper(X2),proper(X3),proper(X4)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) snd(mark(X)) -> mark(snd(X)) snd(ok(X)) -> ok(snd(X)) splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2)) splitAt(mark(X1),X2) -> mark(splitAt(X1,X2)) splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2)) tail(mark(X)) -> mark(tail(X)) tail(ok(X)) -> ok(tail(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) u(mark(X1),X2,X3,X4) -> mark(u(X1,X2,X3,X4)) u(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(u(X1,X2,X3,X4)) - Signature: {active/1,afterNth/2,cons/2,fst/1,head/1,natsFrom/1,pair/2,proper/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2 ,top/1,u/4,active#/1,afterNth#/2,cons#/2,fst#/1,head#/1,natsFrom#/1,pair#/2,proper#/1,s#/1,sel#/2,snd#/1 ,splitAt#/2,tail#/1,take#/2,top#/1,u#/4} / {0/0,mark/1,nil/0,ok/1,c_1/2,c_2/2,c_3/2,c_4/2,c_5/2,c_6/0,c_7/2 ,c_8/0,c_9/3,c_10/2,c_11/2,c_12/2,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/0,c_19/2,c_20/2,c_21/1,c_22/2 ,c_23/2,c_24/0,c_25/2,c_26/2,c_27/2,c_28/2,c_29/2,c_30/1,c_31/1,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/1 ,c_38/1,c_39/1,c_40/1,c_41/1,c_42/1,c_43/1,c_44/0,c_45/3,c_46/3,c_47/2,c_48/2,c_49/2,c_50/0,c_51/3,c_52/2 ,c_53/3,c_54/2,c_55/3,c_56/2,c_57/3,c_58/5,c_59/1,c_60/1,c_61/1,c_62/1,c_63/1,c_64/1,c_65/1,c_66/1,c_67/1 ,c_68/1,c_69/1,c_70/1,c_71/1,c_72/1,c_73/1,c_74/2,c_75/2,c_76/1,c_77/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,afterNth#,cons#,fst#,head#,natsFrom#,pair# ,proper#,s#,sel#,snd#,splitAt#,tail#,take#,top#,u#} and constructors {0,mark,nil,ok} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)) -->_2 splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)):62 -->_2 splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)):61 -->_2 splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)):60 -->_1 snd#(ok(X)) -> c_65(snd#(X)):59 -->_1 snd#(mark(X)) -> c_64(snd#(X)):58 2:S:active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)) -->_1 afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)):28 -->_1 afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)):27 -->_1 afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)):26 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 3:S:active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)) -->_1 afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)):28 -->_1 afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)):27 -->_1 afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)):26 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 4:S:active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)) -->_1 cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)):30 -->_1 cons#(mark(X1),X2) -> c_33(cons#(X1,X2)):29 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 5:S:active#(fst(X)) -> c_5(fst#(active(X)),active#(X)) -->_1 fst#(ok(X)) -> c_36(fst#(X)):32 -->_1 fst#(mark(X)) -> c_35(fst#(X)):31 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 6:S:active#(head(X)) -> c_7(head#(active(X)),active#(X)) -->_1 head#(ok(X)) -> c_38(head#(X)):34 -->_1 head#(mark(X)) -> c_37(head#(X)):33 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 7:S:active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)) -->_3 s#(ok(X)) -> c_60(s#(X)):54 -->_3 s#(mark(X)) -> c_59(s#(X)):53 -->_2 natsFrom#(ok(X)) -> c_40(natsFrom#(X)):36 -->_2 natsFrom#(mark(X)) -> c_39(natsFrom#(X)):35 -->_1 cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)):30 -->_1 cons#(mark(X1),X2) -> c_33(cons#(X1,X2)):29 8:S:active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)) -->_1 natsFrom#(ok(X)) -> c_40(natsFrom#(X)):36 -->_1 natsFrom#(mark(X)) -> c_39(natsFrom#(X)):35 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 9:S:active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)) -->_1 pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)):39 -->_1 pair#(mark(X1),X2) -> c_42(pair#(X1,X2)):38 -->_1 pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)):37 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 10:S:active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)) -->_1 pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)):39 -->_1 pair#(mark(X1),X2) -> c_42(pair#(X1,X2)):38 -->_1 pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)):37 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 11:S:active#(s(X)) -> c_13(s#(active(X)),active#(X)) -->_1 s#(ok(X)) -> c_60(s#(X)):54 -->_1 s#(mark(X)) -> c_59(s#(X)):53 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 12:S:active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)) -->_1 head#(ok(X)) -> c_38(head#(X)):34 -->_1 head#(mark(X)) -> c_37(head#(X)):33 -->_2 afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)):28 -->_2 afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)):27 -->_2 afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)):26 13:S:active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)) -->_1 sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)):57 -->_1 sel#(mark(X1),X2) -> c_62(sel#(X1,X2)):56 -->_1 sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)):55 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 14:S:active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)) -->_1 sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)):57 -->_1 sel#(mark(X1),X2) -> c_62(sel#(X1,X2)):56 -->_1 sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)):55 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 15:S:active#(snd(X)) -> c_17(snd#(active(X)),active#(X)) -->_1 snd#(ok(X)) -> c_65(snd#(X)):59 -->_1 snd#(mark(X)) -> c_64(snd#(X)):58 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 16:S:active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)) -->_1 splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)):62 -->_1 splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)):61 -->_1 splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)):60 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 17:S:active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)) -->_1 splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)):62 -->_1 splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)):61 -->_1 splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)):60 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 18:S:active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)) -->_1 pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)):37 19:S:active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)) -->_1 u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)):71 -->_1 u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)):70 -->_2 splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)):62 -->_2 splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)):61 -->_2 splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)):60 20:S:active#(tail(X)) -> c_23(tail#(active(X)),active#(X)) -->_1 tail#(ok(X)) -> c_70(tail#(X)):64 -->_1 tail#(mark(X)) -> c_69(tail#(X)):63 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 21:S:active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)) -->_2 splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)):62 -->_2 splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)):61 -->_2 splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)):60 -->_1 fst#(ok(X)) -> c_36(fst#(X)):32 -->_1 fst#(mark(X)) -> c_35(fst#(X)):31 22:S:active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)) -->_1 take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)):67 -->_1 take#(mark(X1),X2) -> c_72(take#(X1,X2)):66 -->_1 take#(X1,mark(X2)) -> c_71(take#(X1,X2)):65 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 23:S:active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)) -->_1 take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)):67 -->_1 take#(mark(X1),X2) -> c_72(take#(X1,X2)):66 -->_1 take#(X1,mark(X2)) -> c_71(take#(X1,X2)):65 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 24:S:active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)) -->_1 u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)):71 -->_1 u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)):70 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 25:S:active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)) -->_1 pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)):39 -->_1 pair#(mark(X1),X2) -> c_42(pair#(X1,X2)):38 -->_1 pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)):37 -->_2 cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)):30 -->_2 cons#(mark(X1),X2) -> c_33(cons#(X1,X2)):29 26:S:afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)) -->_1 afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)):28 -->_1 afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)):27 -->_1 afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)):26 27:S:afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)) -->_1 afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)):28 -->_1 afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)):27 -->_1 afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)):26 28:S:afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)) -->_1 afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)):28 -->_1 afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)):27 -->_1 afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)):26 29:S:cons#(mark(X1),X2) -> c_33(cons#(X1,X2)) -->_1 cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)):30 -->_1 cons#(mark(X1),X2) -> c_33(cons#(X1,X2)):29 30:S:cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)) -->_1 cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)):30 -->_1 cons#(mark(X1),X2) -> c_33(cons#(X1,X2)):29 31:S:fst#(mark(X)) -> c_35(fst#(X)) -->_1 fst#(ok(X)) -> c_36(fst#(X)):32 -->_1 fst#(mark(X)) -> c_35(fst#(X)):31 32:S:fst#(ok(X)) -> c_36(fst#(X)) -->_1 fst#(ok(X)) -> c_36(fst#(X)):32 -->_1 fst#(mark(X)) -> c_35(fst#(X)):31 33:S:head#(mark(X)) -> c_37(head#(X)) -->_1 head#(ok(X)) -> c_38(head#(X)):34 -->_1 head#(mark(X)) -> c_37(head#(X)):33 34:S:head#(ok(X)) -> c_38(head#(X)) -->_1 head#(ok(X)) -> c_38(head#(X)):34 -->_1 head#(mark(X)) -> c_37(head#(X)):33 35:S:natsFrom#(mark(X)) -> c_39(natsFrom#(X)) -->_1 natsFrom#(ok(X)) -> c_40(natsFrom#(X)):36 -->_1 natsFrom#(mark(X)) -> c_39(natsFrom#(X)):35 36:S:natsFrom#(ok(X)) -> c_40(natsFrom#(X)) -->_1 natsFrom#(ok(X)) -> c_40(natsFrom#(X)):36 -->_1 natsFrom#(mark(X)) -> c_39(natsFrom#(X)):35 37:S:pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)) -->_1 pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)):39 -->_1 pair#(mark(X1),X2) -> c_42(pair#(X1,X2)):38 -->_1 pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)):37 38:S:pair#(mark(X1),X2) -> c_42(pair#(X1,X2)) -->_1 pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)):39 -->_1 pair#(mark(X1),X2) -> c_42(pair#(X1,X2)):38 -->_1 pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)):37 39:S:pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)) -->_1 pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)):39 -->_1 pair#(mark(X1),X2) -> c_42(pair#(X1,X2)):38 -->_1 pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)):37 40:S:proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_3 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_3 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_3 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_3 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_3 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_3 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_3 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_3 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_3 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_3 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_3 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_3 proper#(nil()) -> c_50():77 -->_2 proper#(nil()) -> c_50():77 -->_3 proper#(0()) -> c_44():76 -->_2 proper#(0()) -> c_44():76 -->_3 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_1 afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)):28 -->_1 afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)):27 -->_1 afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)):26 41:S:proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_3 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_3 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_3 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_3 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_3 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_3 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_3 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_3 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_3 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_3 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_3 proper#(nil()) -> c_50():77 -->_2 proper#(nil()) -> c_50():77 -->_3 proper#(0()) -> c_44():76 -->_2 proper#(0()) -> c_44():76 -->_3 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_3 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_1 cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)):30 -->_1 cons#(mark(X1),X2) -> c_33(cons#(X1,X2)):29 42:S:proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)) -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(nil()) -> c_50():77 -->_2 proper#(0()) -> c_44():76 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_1 fst#(ok(X)) -> c_36(fst#(X)):32 -->_1 fst#(mark(X)) -> c_35(fst#(X)):31 43:S:proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)) -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(nil()) -> c_50():77 -->_2 proper#(0()) -> c_44():76 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_1 head#(ok(X)) -> c_38(head#(X)):34 -->_1 head#(mark(X)) -> c_37(head#(X)):33 44:S:proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)) -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(nil()) -> c_50():77 -->_2 proper#(0()) -> c_44():76 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_1 natsFrom#(ok(X)) -> c_40(natsFrom#(X)):36 -->_1 natsFrom#(mark(X)) -> c_39(natsFrom#(X)):35 45:S:proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_3 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_3 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_3 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_3 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_3 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_3 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_3 proper#(nil()) -> c_50():77 -->_2 proper#(nil()) -> c_50():77 -->_3 proper#(0()) -> c_44():76 -->_2 proper#(0()) -> c_44():76 -->_3 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_3 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_3 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_3 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_3 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_3 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_1 pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)):39 -->_1 pair#(mark(X1),X2) -> c_42(pair#(X1,X2)):38 -->_1 pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)):37 46:S:proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)) -->_1 s#(ok(X)) -> c_60(s#(X)):54 -->_1 s#(mark(X)) -> c_59(s#(X)):53 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(nil()) -> c_50():77 -->_2 proper#(0()) -> c_44():76 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 47:S:proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_1 sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)):57 -->_1 sel#(mark(X1),X2) -> c_62(sel#(X1,X2)):56 -->_1 sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)):55 -->_3 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_3 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_3 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_3 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_3 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_3 proper#(nil()) -> c_50():77 -->_2 proper#(nil()) -> c_50():77 -->_3 proper#(0()) -> c_44():76 -->_2 proper#(0()) -> c_44():76 -->_3 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_3 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_3 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_3 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_3 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_3 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_3 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_3 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 48:S:proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)) -->_1 snd#(ok(X)) -> c_65(snd#(X)):59 -->_1 snd#(mark(X)) -> c_64(snd#(X)):58 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(nil()) -> c_50():77 -->_2 proper#(0()) -> c_44():76 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 49:S:proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_1 splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)):62 -->_1 splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)):61 -->_1 splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)):60 -->_3 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_3 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_3 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_3 proper#(nil()) -> c_50():77 -->_2 proper#(nil()) -> c_50():77 -->_3 proper#(0()) -> c_44():76 -->_2 proper#(0()) -> c_44():76 -->_3 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_3 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_3 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_3 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_3 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_3 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_3 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_3 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_3 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_3 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 50:S:proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)) -->_1 tail#(ok(X)) -> c_70(tail#(X)):64 -->_1 tail#(mark(X)) -> c_69(tail#(X)):63 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(nil()) -> c_50():77 -->_2 proper#(0()) -> c_44():76 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 51:S:proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_1 take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)):67 -->_1 take#(mark(X1),X2) -> c_72(take#(X1,X2)):66 -->_1 take#(X1,mark(X2)) -> c_71(take#(X1,X2)):65 -->_3 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_3 proper#(nil()) -> c_50():77 -->_2 proper#(nil()) -> c_50():77 -->_3 proper#(0()) -> c_44():76 -->_2 proper#(0()) -> c_44():76 -->_3 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_3 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_3 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_3 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_3 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_3 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_3 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_3 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_3 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_3 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_3 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_3 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 52:S:proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)) -->_1 u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)):71 -->_1 u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)):70 -->_5 proper#(nil()) -> c_50():77 -->_4 proper#(nil()) -> c_50():77 -->_3 proper#(nil()) -> c_50():77 -->_2 proper#(nil()) -> c_50():77 -->_5 proper#(0()) -> c_44():76 -->_4 proper#(0()) -> c_44():76 -->_3 proper#(0()) -> c_44():76 -->_2 proper#(0()) -> c_44():76 -->_5 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_4 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_3 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_5 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_4 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_3 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_5 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_4 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_3 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_5 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_4 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_3 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_5 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_4 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_3 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_5 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_4 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_3 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_5 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_4 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_3 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_5 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_4 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_3 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_5 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_4 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_3 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_5 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_4 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_3 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_5 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_4 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_3 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_5 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_4 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_3 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_5 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_4 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_3 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 53:S:s#(mark(X)) -> c_59(s#(X)) -->_1 s#(ok(X)) -> c_60(s#(X)):54 -->_1 s#(mark(X)) -> c_59(s#(X)):53 54:S:s#(ok(X)) -> c_60(s#(X)) -->_1 s#(ok(X)) -> c_60(s#(X)):54 -->_1 s#(mark(X)) -> c_59(s#(X)):53 55:S:sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)) -->_1 sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)):57 -->_1 sel#(mark(X1),X2) -> c_62(sel#(X1,X2)):56 -->_1 sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)):55 56:S:sel#(mark(X1),X2) -> c_62(sel#(X1,X2)) -->_1 sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)):57 -->_1 sel#(mark(X1),X2) -> c_62(sel#(X1,X2)):56 -->_1 sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)):55 57:S:sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)) -->_1 sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)):57 -->_1 sel#(mark(X1),X2) -> c_62(sel#(X1,X2)):56 -->_1 sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)):55 58:S:snd#(mark(X)) -> c_64(snd#(X)) -->_1 snd#(ok(X)) -> c_65(snd#(X)):59 -->_1 snd#(mark(X)) -> c_64(snd#(X)):58 59:S:snd#(ok(X)) -> c_65(snd#(X)) -->_1 snd#(ok(X)) -> c_65(snd#(X)):59 -->_1 snd#(mark(X)) -> c_64(snd#(X)):58 60:S:splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)) -->_1 splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)):62 -->_1 splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)):61 -->_1 splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)):60 61:S:splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)) -->_1 splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)):62 -->_1 splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)):61 -->_1 splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)):60 62:S:splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)) -->_1 splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)):62 -->_1 splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)):61 -->_1 splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)):60 63:S:tail#(mark(X)) -> c_69(tail#(X)) -->_1 tail#(ok(X)) -> c_70(tail#(X)):64 -->_1 tail#(mark(X)) -> c_69(tail#(X)):63 64:S:tail#(ok(X)) -> c_70(tail#(X)) -->_1 tail#(ok(X)) -> c_70(tail#(X)):64 -->_1 tail#(mark(X)) -> c_69(tail#(X)):63 65:S:take#(X1,mark(X2)) -> c_71(take#(X1,X2)) -->_1 take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)):67 -->_1 take#(mark(X1),X2) -> c_72(take#(X1,X2)):66 -->_1 take#(X1,mark(X2)) -> c_71(take#(X1,X2)):65 66:S:take#(mark(X1),X2) -> c_72(take#(X1,X2)) -->_1 take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)):67 -->_1 take#(mark(X1),X2) -> c_72(take#(X1,X2)):66 -->_1 take#(X1,mark(X2)) -> c_71(take#(X1,X2)):65 67:S:take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)) -->_1 take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)):67 -->_1 take#(mark(X1),X2) -> c_72(take#(X1,X2)):66 -->_1 take#(X1,mark(X2)) -> c_71(take#(X1,X2)):65 68:S:top#(mark(X)) -> c_74(top#(proper(X)),proper#(X)) -->_1 top#(ok(X)) -> c_75(top#(active(X)),active#(X)):69 -->_2 proper#(nil()) -> c_50():77 -->_2 proper#(0()) -> c_44():76 -->_1 top#(mark(X)) -> c_74(top#(proper(X)),proper#(X)):68 -->_2 proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)):52 -->_2 proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):51 -->_2 proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)):50 -->_2 proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):49 -->_2 proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)):48 -->_2 proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):47 -->_2 proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)):46 -->_2 proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):45 -->_2 proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)):44 -->_2 proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)):43 -->_2 proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)):42 -->_2 proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):41 -->_2 proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):40 69:S:top#(ok(X)) -> c_75(top#(active(X)),active#(X)) -->_2 active#(tail(cons(N,XS))) -> c_24():75 -->_2 active#(snd(pair(XS,YS))) -> c_18():74 -->_2 active#(head(cons(N,XS))) -> c_8():73 -->_2 active#(fst(pair(XS,YS))) -> c_6():72 -->_1 top#(ok(X)) -> c_75(top#(active(X)),active#(X)):69 -->_1 top#(mark(X)) -> c_74(top#(proper(X)),proper#(X)):68 -->_2 active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)):25 -->_2 active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)):24 -->_2 active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)):23 -->_2 active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)):22 -->_2 active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)):21 -->_2 active#(tail(X)) -> c_23(tail#(active(X)),active#(X)):20 -->_2 active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)):19 -->_2 active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)):18 -->_2 active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)):17 -->_2 active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)):16 -->_2 active#(snd(X)) -> c_17(snd#(active(X)),active#(X)):15 -->_2 active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)):14 -->_2 active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)):13 -->_2 active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)):12 -->_2 active#(s(X)) -> c_13(s#(active(X)),active#(X)):11 -->_2 active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)):10 -->_2 active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)):9 -->_2 active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)):8 -->_2 active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)):7 -->_2 active#(head(X)) -> c_7(head#(active(X)),active#(X)):6 -->_2 active#(fst(X)) -> c_5(fst#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)):3 -->_2 active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)):2 -->_2 active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)):1 70:S:u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)) -->_1 u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)):71 -->_1 u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)):70 71:S:u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)) -->_1 u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)):71 -->_1 u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)):70 72:W:active#(fst(pair(XS,YS))) -> c_6() 73:W:active#(head(cons(N,XS))) -> c_8() 74:W:active#(snd(pair(XS,YS))) -> c_18() 75:W:active#(tail(cons(N,XS))) -> c_24() 76:W:proper#(0()) -> c_44() 77:W:proper#(nil()) -> c_50() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 76: proper#(0()) -> c_44() 77: proper#(nil()) -> c_50() 72: active#(fst(pair(XS,YS))) -> c_6() 73: active#(head(cons(N,XS))) -> c_8() 74: active#(snd(pair(XS,YS))) -> c_18() 75: active#(tail(cons(N,XS))) -> c_24() * Step 5: Failure MAYBE + Considered Problem: - Strict DPs: active#(afterNth(N,XS)) -> c_1(snd#(splitAt(N,XS)),splitAt#(N,XS)) active#(afterNth(X1,X2)) -> c_2(afterNth#(X1,active(X2)),active#(X2)) active#(afterNth(X1,X2)) -> c_3(afterNth#(active(X1),X2),active#(X1)) active#(cons(X1,X2)) -> c_4(cons#(active(X1),X2),active#(X1)) active#(fst(X)) -> c_5(fst#(active(X)),active#(X)) active#(head(X)) -> c_7(head#(active(X)),active#(X)) active#(natsFrom(N)) -> c_9(cons#(N,natsFrom(s(N))),natsFrom#(s(N)),s#(N)) active#(natsFrom(X)) -> c_10(natsFrom#(active(X)),active#(X)) active#(pair(X1,X2)) -> c_11(pair#(X1,active(X2)),active#(X2)) active#(pair(X1,X2)) -> c_12(pair#(active(X1),X2),active#(X1)) active#(s(X)) -> c_13(s#(active(X)),active#(X)) active#(sel(N,XS)) -> c_14(head#(afterNth(N,XS)),afterNth#(N,XS)) active#(sel(X1,X2)) -> c_15(sel#(X1,active(X2)),active#(X2)) active#(sel(X1,X2)) -> c_16(sel#(active(X1),X2),active#(X1)) active#(snd(X)) -> c_17(snd#(active(X)),active#(X)) active#(splitAt(X1,X2)) -> c_19(splitAt#(X1,active(X2)),active#(X2)) active#(splitAt(X1,X2)) -> c_20(splitAt#(active(X1),X2),active#(X1)) active#(splitAt(0(),XS)) -> c_21(pair#(nil(),XS)) active#(splitAt(s(N),cons(X,XS))) -> c_22(u#(splitAt(N,XS),N,X,XS),splitAt#(N,XS)) active#(tail(X)) -> c_23(tail#(active(X)),active#(X)) active#(take(N,XS)) -> c_25(fst#(splitAt(N,XS)),splitAt#(N,XS)) active#(take(X1,X2)) -> c_26(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_27(take#(active(X1),X2),active#(X1)) active#(u(X1,X2,X3,X4)) -> c_28(u#(active(X1),X2,X3,X4),active#(X1)) active#(u(pair(YS,ZS),N,X,XS)) -> c_29(pair#(cons(X,YS),ZS),cons#(X,YS)) afterNth#(X1,mark(X2)) -> c_30(afterNth#(X1,X2)) afterNth#(mark(X1),X2) -> c_31(afterNth#(X1,X2)) afterNth#(ok(X1),ok(X2)) -> c_32(afterNth#(X1,X2)) cons#(mark(X1),X2) -> c_33(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_34(cons#(X1,X2)) fst#(mark(X)) -> c_35(fst#(X)) fst#(ok(X)) -> c_36(fst#(X)) head#(mark(X)) -> c_37(head#(X)) head#(ok(X)) -> c_38(head#(X)) natsFrom#(mark(X)) -> c_39(natsFrom#(X)) natsFrom#(ok(X)) -> c_40(natsFrom#(X)) pair#(X1,mark(X2)) -> c_41(pair#(X1,X2)) pair#(mark(X1),X2) -> c_42(pair#(X1,X2)) pair#(ok(X1),ok(X2)) -> c_43(pair#(X1,X2)) proper#(afterNth(X1,X2)) -> c_45(afterNth#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_46(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(fst(X)) -> c_47(fst#(proper(X)),proper#(X)) proper#(head(X)) -> c_48(head#(proper(X)),proper#(X)) proper#(natsFrom(X)) -> c_49(natsFrom#(proper(X)),proper#(X)) proper#(pair(X1,X2)) -> c_51(pair#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_52(s#(proper(X)),proper#(X)) proper#(sel(X1,X2)) -> c_53(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(snd(X)) -> c_54(snd#(proper(X)),proper#(X)) proper#(splitAt(X1,X2)) -> c_55(splitAt#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(tail(X)) -> c_56(tail#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_57(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(u(X1,X2,X3,X4)) -> c_58(u#(proper(X1),proper(X2),proper(X3),proper(X4)) ,proper#(X1) ,proper#(X2) ,proper#(X3) ,proper#(X4)) s#(mark(X)) -> c_59(s#(X)) s#(ok(X)) -> c_60(s#(X)) sel#(X1,mark(X2)) -> c_61(sel#(X1,X2)) sel#(mark(X1),X2) -> c_62(sel#(X1,X2)) sel#(ok(X1),ok(X2)) -> c_63(sel#(X1,X2)) snd#(mark(X)) -> c_64(snd#(X)) snd#(ok(X)) -> c_65(snd#(X)) splitAt#(X1,mark(X2)) -> c_66(splitAt#(X1,X2)) splitAt#(mark(X1),X2) -> c_67(splitAt#(X1,X2)) splitAt#(ok(X1),ok(X2)) -> c_68(splitAt#(X1,X2)) tail#(mark(X)) -> c_69(tail#(X)) tail#(ok(X)) -> c_70(tail#(X)) take#(X1,mark(X2)) -> c_71(take#(X1,X2)) take#(mark(X1),X2) -> c_72(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_73(take#(X1,X2)) top#(mark(X)) -> c_74(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_75(top#(active(X)),active#(X)) u#(mark(X1),X2,X3,X4) -> c_76(u#(X1,X2,X3,X4)) u#(ok(X1),ok(X2),ok(X3),ok(X4)) -> c_77(u#(X1,X2,X3,X4)) - Weak TRS: active(afterNth(N,XS)) -> mark(snd(splitAt(N,XS))) active(afterNth(X1,X2)) -> afterNth(X1,active(X2)) active(afterNth(X1,X2)) -> afterNth(active(X1),X2) active(cons(X1,X2)) -> cons(active(X1),X2) active(fst(X)) -> fst(active(X)) active(fst(pair(XS,YS))) -> mark(XS) active(head(X)) -> head(active(X)) active(head(cons(N,XS))) -> mark(N) active(natsFrom(N)) -> mark(cons(N,natsFrom(s(N)))) active(natsFrom(X)) -> natsFrom(active(X)) active(pair(X1,X2)) -> pair(X1,active(X2)) active(pair(X1,X2)) -> pair(active(X1),X2) active(s(X)) -> s(active(X)) active(sel(N,XS)) -> mark(head(afterNth(N,XS))) active(sel(X1,X2)) -> sel(X1,active(X2)) active(sel(X1,X2)) -> sel(active(X1),X2) active(snd(X)) -> snd(active(X)) active(snd(pair(XS,YS))) -> mark(YS) active(splitAt(X1,X2)) -> splitAt(X1,active(X2)) active(splitAt(X1,X2)) -> splitAt(active(X1),X2) active(splitAt(0(),XS)) -> mark(pair(nil(),XS)) active(splitAt(s(N),cons(X,XS))) -> mark(u(splitAt(N,XS),N,X,XS)) active(tail(X)) -> tail(active(X)) active(tail(cons(N,XS))) -> mark(XS) active(take(N,XS)) -> mark(fst(splitAt(N,XS))) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(u(X1,X2,X3,X4)) -> u(active(X1),X2,X3,X4) active(u(pair(YS,ZS),N,X,XS)) -> mark(pair(cons(X,YS),ZS)) afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2)) afterNth(mark(X1),X2) -> mark(afterNth(X1,X2)) afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) fst(mark(X)) -> mark(fst(X)) fst(ok(X)) -> ok(fst(X)) head(mark(X)) -> mark(head(X)) head(ok(X)) -> ok(head(X)) natsFrom(mark(X)) -> mark(natsFrom(X)) natsFrom(ok(X)) -> ok(natsFrom(X)) pair(X1,mark(X2)) -> mark(pair(X1,X2)) pair(mark(X1),X2) -> mark(pair(X1,X2)) pair(ok(X1),ok(X2)) -> ok(pair(X1,X2)) proper(0()) -> ok(0()) proper(afterNth(X1,X2)) -> afterNth(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(fst(X)) -> fst(proper(X)) proper(head(X)) -> head(proper(X)) proper(natsFrom(X)) -> natsFrom(proper(X)) proper(nil()) -> ok(nil()) proper(pair(X1,X2)) -> pair(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(snd(X)) -> snd(proper(X)) proper(splitAt(X1,X2)) -> splitAt(proper(X1),proper(X2)) proper(tail(X)) -> tail(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(u(X1,X2,X3,X4)) -> u(proper(X1),proper(X2),proper(X3),proper(X4)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) snd(mark(X)) -> mark(snd(X)) snd(ok(X)) -> ok(snd(X)) splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2)) splitAt(mark(X1),X2) -> mark(splitAt(X1,X2)) splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2)) tail(mark(X)) -> mark(tail(X)) tail(ok(X)) -> ok(tail(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) u(mark(X1),X2,X3,X4) -> mark(u(X1,X2,X3,X4)) u(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(u(X1,X2,X3,X4)) - Signature: {active/1,afterNth/2,cons/2,fst/1,head/1,natsFrom/1,pair/2,proper/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2 ,top/1,u/4,active#/1,afterNth#/2,cons#/2,fst#/1,head#/1,natsFrom#/1,pair#/2,proper#/1,s#/1,sel#/2,snd#/1 ,splitAt#/2,tail#/1,take#/2,top#/1,u#/4} / {0/0,mark/1,nil/0,ok/1,c_1/2,c_2/2,c_3/2,c_4/2,c_5/2,c_6/0,c_7/2 ,c_8/0,c_9/3,c_10/2,c_11/2,c_12/2,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/0,c_19/2,c_20/2,c_21/1,c_22/2 ,c_23/2,c_24/0,c_25/2,c_26/2,c_27/2,c_28/2,c_29/2,c_30/1,c_31/1,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/1 ,c_38/1,c_39/1,c_40/1,c_41/1,c_42/1,c_43/1,c_44/0,c_45/3,c_46/3,c_47/2,c_48/2,c_49/2,c_50/0,c_51/3,c_52/2 ,c_53/3,c_54/2,c_55/3,c_56/2,c_57/3,c_58/5,c_59/1,c_60/1,c_61/1,c_62/1,c_63/1,c_64/1,c_65/1,c_66/1,c_67/1 ,c_68/1,c_69/1,c_70/1,c_71/1,c_72/1,c_73/1,c_74/2,c_75/2,c_76/1,c_77/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,afterNth#,cons#,fst#,head#,natsFrom#,pair# ,proper#,s#,sel#,snd#,splitAt#,tail#,take#,top#,u#} and constructors {0,mark,nil,ok} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE