MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ active(U11(X1, X2, X3, X4)) -> U11(active(X1), X2, X3, X4)
, active(U11(tt(), N, X, XS)) -> mark(U12(splitAt(N, XS), X))
, active(U12(X1, X2)) -> U12(active(X1), X2)
, active(U12(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS))
, active(splitAt(X1, X2)) -> splitAt(X1, active(X2))
, active(splitAt(X1, X2)) -> splitAt(active(X1), X2)
, active(splitAt(s(N), cons(X, XS))) -> mark(U11(tt(), N, X, XS))
, active(splitAt(0(), XS)) -> mark(pair(nil(), XS))
, active(pair(X1, X2)) -> pair(X1, active(X2))
, active(pair(X1, X2)) -> pair(active(X1), X2)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, 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(snd(X)) -> snd(active(X))
, active(snd(pair(X, Y))) -> mark(Y)
, active(and(X1, X2)) -> and(active(X1), X2)
, active(and(tt(), X)) -> mark(X)
, active(fst(X)) -> fst(active(X))
, active(fst(pair(X, Y))) -> mark(X)
, 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(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(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)
, U11(mark(X1), X2, X3, X4) -> mark(U11(X1, X2, X3, X4))
, U11(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U11(X1, X2, X3, X4))
, U12(mark(X1), X2) -> mark(U12(X1, X2))
, U12(ok(X1), ok(X2)) -> ok(U12(X1, X2))
, 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))
, 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))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, 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))
, snd(mark(X)) -> mark(snd(X))
, snd(ok(X)) -> ok(snd(X))
, and(mark(X1), X2) -> mark(and(X1, X2))
, and(ok(X1), ok(X2)) -> ok(and(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))
, 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))
, 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))
, proper(U11(X1, X2, X3, X4)) ->
U11(proper(X1), proper(X2), proper(X3), proper(X4))
, proper(tt()) -> ok(tt())
, proper(U12(X1, X2)) -> U12(proper(X1), proper(X2))
, proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2))
, proper(pair(X1, X2)) -> pair(proper(X1), proper(X2))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2))
, proper(snd(X)) -> snd(proper(X))
, proper(and(X1, X2)) -> and(proper(X1), proper(X2))
, proper(fst(X)) -> fst(proper(X))
, proper(head(X)) -> head(proper(X))
, proper(natsFrom(X)) -> natsFrom(proper(X))
, proper(s(X)) -> s(proper(X))
, proper(sel(X1, X2)) -> sel(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(nil()) -> ok(nil())
, proper(tail(X)) -> tail(proper(X))
, proper(take(X1, X2)) -> take(proper(X1), proper(X2))
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X)) }
Obligation:
runtime complexity
Answer:
MAYBE
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
following reason:
Computation stopped due to timeout after 60.0 seconds.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
failed due to the following reason:
Computation stopped due to timeout after 30.0 seconds.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
to the following reason:
The processor is inapplicable, reason:
Processor only applicable for innermost runtime complexity analysis
2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
following reason:
The processor is inapplicable, reason:
Processor only applicable for innermost runtime complexity analysis
3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with minimal-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
due to the following reason:
We add the following weak dependency pairs:
Strict DPs:
{ active^#(U11(X1, X2, X3, X4)) ->
c_1(U11^#(active(X1), X2, X3, X4))
, active^#(U11(tt(), N, X, XS)) -> c_2(U12^#(splitAt(N, XS), X))
, active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2))
, active^#(U12(pair(YS, ZS), X)) -> c_4(pair^#(cons(X, YS), ZS))
, active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2)))
, active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2))
, active^#(splitAt(s(N), cons(X, XS))) ->
c_7(U11^#(tt(), N, X, XS))
, active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS))
, active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2)))
, active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2))
, active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2))
, active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS)))
, active^#(afterNth(X1, X2)) -> c_13(afterNth^#(X1, active(X2)))
, active^#(afterNth(X1, X2)) -> c_14(afterNth^#(active(X1), X2))
, active^#(snd(X)) -> c_15(snd^#(active(X)))
, active^#(snd(pair(X, Y))) -> c_16(Y)
, active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2))
, active^#(and(tt(), X)) -> c_18(X)
, active^#(fst(X)) -> c_19(fst^#(active(X)))
, active^#(fst(pair(X, Y))) -> c_20(X)
, active^#(head(X)) -> c_21(head^#(active(X)))
, active^#(head(cons(N, XS))) -> c_22(N)
, active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N))))
, active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X)))
, active^#(s(X)) -> c_25(s^#(active(X)))
, active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS)))
, active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2)))
, active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2))
, active^#(tail(X)) -> c_29(tail^#(active(X)))
, active^#(tail(cons(N, XS))) -> c_30(XS)
, active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS)))
, active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2)))
, active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2))
, U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4))
, U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4))
, U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2))
, U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2))
, 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))
, splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2))
, splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2))
, splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2))
, cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2))
, snd^#(mark(X)) -> c_49(snd^#(X))
, snd^#(ok(X)) -> c_50(snd^#(X))
, afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2))
, afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2))
, afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2))
, and^#(mark(X1), X2) -> c_51(and^#(X1, X2))
, and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2))
, fst^#(mark(X)) -> c_53(fst^#(X))
, fst^#(ok(X)) -> c_54(fst^#(X))
, head^#(mark(X)) -> c_55(head^#(X))
, head^#(ok(X)) -> c_56(head^#(X))
, natsFrom^#(mark(X)) -> c_57(natsFrom^#(X))
, natsFrom^#(ok(X)) -> c_58(natsFrom^#(X))
, 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))
, tail^#(mark(X)) -> c_64(tail^#(X))
, tail^#(ok(X)) -> c_65(tail^#(X))
, take^#(X1, mark(X2)) -> c_66(take^#(X1, X2))
, take^#(mark(X1), X2) -> c_67(take^#(X1, X2))
, take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2))
, proper^#(U11(X1, X2, X3, X4)) ->
c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4)))
, proper^#(tt()) -> c_70()
, proper^#(U12(X1, X2)) -> c_71(U12^#(proper(X1), proper(X2)))
, proper^#(splitAt(X1, X2)) ->
c_72(splitAt^#(proper(X1), proper(X2)))
, proper^#(pair(X1, X2)) -> c_73(pair^#(proper(X1), proper(X2)))
, proper^#(cons(X1, X2)) -> c_74(cons^#(proper(X1), proper(X2)))
, proper^#(afterNth(X1, X2)) ->
c_75(afterNth^#(proper(X1), proper(X2)))
, proper^#(snd(X)) -> c_76(snd^#(proper(X)))
, proper^#(and(X1, X2)) -> c_77(and^#(proper(X1), proper(X2)))
, proper^#(fst(X)) -> c_78(fst^#(proper(X)))
, proper^#(head(X)) -> c_79(head^#(proper(X)))
, proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X)))
, proper^#(s(X)) -> c_81(s^#(proper(X)))
, proper^#(sel(X1, X2)) -> c_82(sel^#(proper(X1), proper(X2)))
, proper^#(0()) -> c_83()
, proper^#(nil()) -> c_84()
, proper^#(tail(X)) -> c_85(tail^#(proper(X)))
, proper^#(take(X1, X2)) -> c_86(take^#(proper(X1), proper(X2)))
, top^#(mark(X)) -> c_87(top^#(proper(X)))
, top^#(ok(X)) -> c_88(top^#(active(X))) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ active^#(U11(X1, X2, X3, X4)) ->
c_1(U11^#(active(X1), X2, X3, X4))
, active^#(U11(tt(), N, X, XS)) -> c_2(U12^#(splitAt(N, XS), X))
, active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2))
, active^#(U12(pair(YS, ZS), X)) -> c_4(pair^#(cons(X, YS), ZS))
, active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2)))
, active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2))
, active^#(splitAt(s(N), cons(X, XS))) ->
c_7(U11^#(tt(), N, X, XS))
, active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS))
, active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2)))
, active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2))
, active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2))
, active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS)))
, active^#(afterNth(X1, X2)) -> c_13(afterNth^#(X1, active(X2)))
, active^#(afterNth(X1, X2)) -> c_14(afterNth^#(active(X1), X2))
, active^#(snd(X)) -> c_15(snd^#(active(X)))
, active^#(snd(pair(X, Y))) -> c_16(Y)
, active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2))
, active^#(and(tt(), X)) -> c_18(X)
, active^#(fst(X)) -> c_19(fst^#(active(X)))
, active^#(fst(pair(X, Y))) -> c_20(X)
, active^#(head(X)) -> c_21(head^#(active(X)))
, active^#(head(cons(N, XS))) -> c_22(N)
, active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N))))
, active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X)))
, active^#(s(X)) -> c_25(s^#(active(X)))
, active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS)))
, active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2)))
, active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2))
, active^#(tail(X)) -> c_29(tail^#(active(X)))
, active^#(tail(cons(N, XS))) -> c_30(XS)
, active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS)))
, active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2)))
, active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2))
, U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4))
, U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4))
, U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2))
, U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2))
, 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))
, splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2))
, splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2))
, splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2))
, cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2))
, snd^#(mark(X)) -> c_49(snd^#(X))
, snd^#(ok(X)) -> c_50(snd^#(X))
, afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2))
, afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2))
, afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2))
, and^#(mark(X1), X2) -> c_51(and^#(X1, X2))
, and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2))
, fst^#(mark(X)) -> c_53(fst^#(X))
, fst^#(ok(X)) -> c_54(fst^#(X))
, head^#(mark(X)) -> c_55(head^#(X))
, head^#(ok(X)) -> c_56(head^#(X))
, natsFrom^#(mark(X)) -> c_57(natsFrom^#(X))
, natsFrom^#(ok(X)) -> c_58(natsFrom^#(X))
, 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))
, tail^#(mark(X)) -> c_64(tail^#(X))
, tail^#(ok(X)) -> c_65(tail^#(X))
, take^#(X1, mark(X2)) -> c_66(take^#(X1, X2))
, take^#(mark(X1), X2) -> c_67(take^#(X1, X2))
, take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2))
, proper^#(U11(X1, X2, X3, X4)) ->
c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4)))
, proper^#(tt()) -> c_70()
, proper^#(U12(X1, X2)) -> c_71(U12^#(proper(X1), proper(X2)))
, proper^#(splitAt(X1, X2)) ->
c_72(splitAt^#(proper(X1), proper(X2)))
, proper^#(pair(X1, X2)) -> c_73(pair^#(proper(X1), proper(X2)))
, proper^#(cons(X1, X2)) -> c_74(cons^#(proper(X1), proper(X2)))
, proper^#(afterNth(X1, X2)) ->
c_75(afterNth^#(proper(X1), proper(X2)))
, proper^#(snd(X)) -> c_76(snd^#(proper(X)))
, proper^#(and(X1, X2)) -> c_77(and^#(proper(X1), proper(X2)))
, proper^#(fst(X)) -> c_78(fst^#(proper(X)))
, proper^#(head(X)) -> c_79(head^#(proper(X)))
, proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X)))
, proper^#(s(X)) -> c_81(s^#(proper(X)))
, proper^#(sel(X1, X2)) -> c_82(sel^#(proper(X1), proper(X2)))
, proper^#(0()) -> c_83()
, proper^#(nil()) -> c_84()
, proper^#(tail(X)) -> c_85(tail^#(proper(X)))
, proper^#(take(X1, X2)) -> c_86(take^#(proper(X1), proper(X2)))
, top^#(mark(X)) -> c_87(top^#(proper(X)))
, top^#(ok(X)) -> c_88(top^#(active(X))) }
Strict Trs:
{ active(U11(X1, X2, X3, X4)) -> U11(active(X1), X2, X3, X4)
, active(U11(tt(), N, X, XS)) -> mark(U12(splitAt(N, XS), X))
, active(U12(X1, X2)) -> U12(active(X1), X2)
, active(U12(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS))
, active(splitAt(X1, X2)) -> splitAt(X1, active(X2))
, active(splitAt(X1, X2)) -> splitAt(active(X1), X2)
, active(splitAt(s(N), cons(X, XS))) -> mark(U11(tt(), N, X, XS))
, active(splitAt(0(), XS)) -> mark(pair(nil(), XS))
, active(pair(X1, X2)) -> pair(X1, active(X2))
, active(pair(X1, X2)) -> pair(active(X1), X2)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, 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(snd(X)) -> snd(active(X))
, active(snd(pair(X, Y))) -> mark(Y)
, active(and(X1, X2)) -> and(active(X1), X2)
, active(and(tt(), X)) -> mark(X)
, active(fst(X)) -> fst(active(X))
, active(fst(pair(X, Y))) -> mark(X)
, 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(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(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)
, U11(mark(X1), X2, X3, X4) -> mark(U11(X1, X2, X3, X4))
, U11(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U11(X1, X2, X3, X4))
, U12(mark(X1), X2) -> mark(U12(X1, X2))
, U12(ok(X1), ok(X2)) -> ok(U12(X1, X2))
, 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))
, 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))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, 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))
, snd(mark(X)) -> mark(snd(X))
, snd(ok(X)) -> ok(snd(X))
, and(mark(X1), X2) -> mark(and(X1, X2))
, and(ok(X1), ok(X2)) -> ok(and(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))
, 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))
, 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))
, proper(U11(X1, X2, X3, X4)) ->
U11(proper(X1), proper(X2), proper(X3), proper(X4))
, proper(tt()) -> ok(tt())
, proper(U12(X1, X2)) -> U12(proper(X1), proper(X2))
, proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2))
, proper(pair(X1, X2)) -> pair(proper(X1), proper(X2))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2))
, proper(snd(X)) -> snd(proper(X))
, proper(and(X1, X2)) -> and(proper(X1), proper(X2))
, proper(fst(X)) -> fst(proper(X))
, proper(head(X)) -> head(proper(X))
, proper(natsFrom(X)) -> natsFrom(proper(X))
, proper(s(X)) -> s(proper(X))
, proper(sel(X1, X2)) -> sel(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(nil()) -> ok(nil())
, proper(tail(X)) -> tail(proper(X))
, proper(take(X1, X2)) -> take(proper(X1), proper(X2))
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X)) }
Obligation:
runtime complexity
Answer:
MAYBE
Consider the dependency graph:
1: active^#(U11(X1, X2, X3, X4)) ->
c_1(U11^#(active(X1), X2, X3, X4))
-->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4)) :35
-->_1 U11^#(mark(X1), X2, X3, X4) ->
c_34(U11^#(X1, X2, X3, X4)) :34
2: active^#(U11(tt(), N, X, XS)) -> c_2(U12^#(splitAt(N, XS), X))
-->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37
-->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36
3: active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2))
-->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37
-->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36
4: active^#(U12(pair(YS, ZS), X)) -> c_4(pair^#(cons(X, YS), ZS))
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
5: active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2)))
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
6: active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2))
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
7: active^#(splitAt(s(N), cons(X, XS))) ->
c_7(U11^#(tt(), N, X, XS))
8: active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS))
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
9: active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2)))
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
10: active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2))
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
11: active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2))
-->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45
-->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44
12: active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS)))
-->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47
-->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46
13: active^#(afterNth(X1, X2)) -> c_13(afterNth^#(X1, active(X2)))
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
14: active^#(afterNth(X1, X2)) -> c_14(afterNth^#(active(X1), X2))
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
15: active^#(snd(X)) -> c_15(snd^#(active(X)))
-->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47
-->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46
16: active^#(snd(pair(X, Y))) -> c_16(Y)
-->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88
-->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87
-->_1 proper^#(take(X1, X2)) ->
c_86(take^#(proper(X1), proper(X2))) :86
-->_1 proper^#(tail(X)) -> c_85(tail^#(proper(X))) :85
-->_1 proper^#(sel(X1, X2)) ->
c_82(sel^#(proper(X1), proper(X2))) :82
-->_1 proper^#(s(X)) -> c_81(s^#(proper(X))) :81
-->_1 proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) :80
-->_1 proper^#(head(X)) -> c_79(head^#(proper(X))) :79
-->_1 proper^#(fst(X)) -> c_78(fst^#(proper(X))) :78
-->_1 proper^#(and(X1, X2)) ->
c_77(and^#(proper(X1), proper(X2))) :77
-->_1 proper^#(snd(X)) -> c_76(snd^#(proper(X))) :76
-->_1 proper^#(afterNth(X1, X2)) ->
c_75(afterNth^#(proper(X1), proper(X2))) :75
-->_1 proper^#(cons(X1, X2)) ->
c_74(cons^#(proper(X1), proper(X2))) :74
-->_1 proper^#(pair(X1, X2)) ->
c_73(pair^#(proper(X1), proper(X2))) :73
-->_1 proper^#(splitAt(X1, X2)) ->
c_72(splitAt^#(proper(X1), proper(X2))) :72
-->_1 proper^#(U12(X1, X2)) ->
c_71(U12^#(proper(X1), proper(X2))) :71
-->_1 proper^#(U11(X1, X2, X3, X4)) ->
c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) :69
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
-->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65
-->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
-->_1 s^#(ok(X)) -> c_60(s^#(X)) :60
-->_1 s^#(mark(X)) -> c_59(s^#(X)) :59
-->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58
-->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57
-->_1 head^#(ok(X)) -> c_56(head^#(X)) :56
-->_1 head^#(mark(X)) -> c_55(head^#(X)) :55
-->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54
-->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53
-->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52
-->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
-->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47
-->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46
-->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45
-->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
-->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37
-->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36
-->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4)) :35
-->_1 U11^#(mark(X1), X2, X3, X4) ->
c_34(U11^#(X1, X2, X3, X4)) :34
-->_1 active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) :33
-->_1 active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) :32
-->_1 active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) :31
-->_1 active^#(tail(cons(N, XS))) -> c_30(XS) :30
-->_1 active^#(tail(X)) -> c_29(tail^#(active(X))) :29
-->_1 active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) :28
-->_1 active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) :27
-->_1 active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) :26
-->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25
-->_1 active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) :24
-->_1 active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) :23
-->_1 active^#(head(cons(N, XS))) -> c_22(N) :22
-->_1 active^#(head(X)) -> c_21(head^#(active(X))) :21
-->_1 active^#(fst(pair(X, Y))) -> c_20(X) :20
-->_1 active^#(fst(X)) -> c_19(fst^#(active(X))) :19
-->_1 active^#(and(tt(), X)) -> c_18(X) :18
-->_1 active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) :17
-->_1 proper^#(nil()) -> c_84() :84
-->_1 proper^#(0()) -> c_83() :83
-->_1 proper^#(tt()) -> c_70() :70
-->_1 active^#(snd(pair(X, Y))) -> c_16(Y) :16
-->_1 active^#(snd(X)) -> c_15(snd^#(active(X))) :15
-->_1 active^#(afterNth(X1, X2)) ->
c_14(afterNth^#(active(X1), X2)) :14
-->_1 active^#(afterNth(X1, X2)) ->
c_13(afterNth^#(X1, active(X2))) :13
-->_1 active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) :12
-->_1 active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) :11
-->_1 active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) :10
-->_1 active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) :9
-->_1 active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) :8
-->_1 active^#(splitAt(s(N), cons(X, XS))) ->
c_7(U11^#(tt(), N, X, XS)) :7
-->_1 active^#(splitAt(X1, X2)) ->
c_6(splitAt^#(active(X1), X2)) :6
-->_1 active^#(splitAt(X1, X2)) ->
c_5(splitAt^#(X1, active(X2))) :5
-->_1 active^#(U12(pair(YS, ZS), X)) ->
c_4(pair^#(cons(X, YS), ZS)) :4
-->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3
-->_1 active^#(U11(tt(), N, X, XS)) ->
c_2(U12^#(splitAt(N, XS), X)) :2
-->_1 active^#(U11(X1, X2, X3, X4)) ->
c_1(U11^#(active(X1), X2, X3, X4)) :1
17: active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2))
-->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52
-->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51
18: active^#(and(tt(), X)) -> c_18(X)
-->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88
-->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87
-->_1 proper^#(take(X1, X2)) ->
c_86(take^#(proper(X1), proper(X2))) :86
-->_1 proper^#(tail(X)) -> c_85(tail^#(proper(X))) :85
-->_1 proper^#(sel(X1, X2)) ->
c_82(sel^#(proper(X1), proper(X2))) :82
-->_1 proper^#(s(X)) -> c_81(s^#(proper(X))) :81
-->_1 proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) :80
-->_1 proper^#(head(X)) -> c_79(head^#(proper(X))) :79
-->_1 proper^#(fst(X)) -> c_78(fst^#(proper(X))) :78
-->_1 proper^#(and(X1, X2)) ->
c_77(and^#(proper(X1), proper(X2))) :77
-->_1 proper^#(snd(X)) -> c_76(snd^#(proper(X))) :76
-->_1 proper^#(afterNth(X1, X2)) ->
c_75(afterNth^#(proper(X1), proper(X2))) :75
-->_1 proper^#(cons(X1, X2)) ->
c_74(cons^#(proper(X1), proper(X2))) :74
-->_1 proper^#(pair(X1, X2)) ->
c_73(pair^#(proper(X1), proper(X2))) :73
-->_1 proper^#(splitAt(X1, X2)) ->
c_72(splitAt^#(proper(X1), proper(X2))) :72
-->_1 proper^#(U12(X1, X2)) ->
c_71(U12^#(proper(X1), proper(X2))) :71
-->_1 proper^#(U11(X1, X2, X3, X4)) ->
c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) :69
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
-->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65
-->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
-->_1 s^#(ok(X)) -> c_60(s^#(X)) :60
-->_1 s^#(mark(X)) -> c_59(s^#(X)) :59
-->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58
-->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57
-->_1 head^#(ok(X)) -> c_56(head^#(X)) :56
-->_1 head^#(mark(X)) -> c_55(head^#(X)) :55
-->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54
-->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53
-->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52
-->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
-->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47
-->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46
-->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45
-->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
-->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37
-->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36
-->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4)) :35
-->_1 U11^#(mark(X1), X2, X3, X4) ->
c_34(U11^#(X1, X2, X3, X4)) :34
-->_1 active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) :33
-->_1 active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) :32
-->_1 active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) :31
-->_1 active^#(tail(cons(N, XS))) -> c_30(XS) :30
-->_1 active^#(tail(X)) -> c_29(tail^#(active(X))) :29
-->_1 active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) :28
-->_1 active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) :27
-->_1 active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) :26
-->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25
-->_1 active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) :24
-->_1 active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) :23
-->_1 active^#(head(cons(N, XS))) -> c_22(N) :22
-->_1 active^#(head(X)) -> c_21(head^#(active(X))) :21
-->_1 active^#(fst(pair(X, Y))) -> c_20(X) :20
-->_1 active^#(fst(X)) -> c_19(fst^#(active(X))) :19
-->_1 proper^#(nil()) -> c_84() :84
-->_1 proper^#(0()) -> c_83() :83
-->_1 proper^#(tt()) -> c_70() :70
-->_1 active^#(and(tt(), X)) -> c_18(X) :18
-->_1 active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) :17
-->_1 active^#(snd(pair(X, Y))) -> c_16(Y) :16
-->_1 active^#(snd(X)) -> c_15(snd^#(active(X))) :15
-->_1 active^#(afterNth(X1, X2)) ->
c_14(afterNth^#(active(X1), X2)) :14
-->_1 active^#(afterNth(X1, X2)) ->
c_13(afterNth^#(X1, active(X2))) :13
-->_1 active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) :12
-->_1 active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) :11
-->_1 active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) :10
-->_1 active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) :9
-->_1 active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) :8
-->_1 active^#(splitAt(s(N), cons(X, XS))) ->
c_7(U11^#(tt(), N, X, XS)) :7
-->_1 active^#(splitAt(X1, X2)) ->
c_6(splitAt^#(active(X1), X2)) :6
-->_1 active^#(splitAt(X1, X2)) ->
c_5(splitAt^#(X1, active(X2))) :5
-->_1 active^#(U12(pair(YS, ZS), X)) ->
c_4(pair^#(cons(X, YS), ZS)) :4
-->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3
-->_1 active^#(U11(tt(), N, X, XS)) ->
c_2(U12^#(splitAt(N, XS), X)) :2
-->_1 active^#(U11(X1, X2, X3, X4)) ->
c_1(U11^#(active(X1), X2, X3, X4)) :1
19: active^#(fst(X)) -> c_19(fst^#(active(X)))
-->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54
-->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53
20: active^#(fst(pair(X, Y))) -> c_20(X)
-->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88
-->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87
-->_1 proper^#(take(X1, X2)) ->
c_86(take^#(proper(X1), proper(X2))) :86
-->_1 proper^#(tail(X)) -> c_85(tail^#(proper(X))) :85
-->_1 proper^#(sel(X1, X2)) ->
c_82(sel^#(proper(X1), proper(X2))) :82
-->_1 proper^#(s(X)) -> c_81(s^#(proper(X))) :81
-->_1 proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) :80
-->_1 proper^#(head(X)) -> c_79(head^#(proper(X))) :79
-->_1 proper^#(fst(X)) -> c_78(fst^#(proper(X))) :78
-->_1 proper^#(and(X1, X2)) ->
c_77(and^#(proper(X1), proper(X2))) :77
-->_1 proper^#(snd(X)) -> c_76(snd^#(proper(X))) :76
-->_1 proper^#(afterNth(X1, X2)) ->
c_75(afterNth^#(proper(X1), proper(X2))) :75
-->_1 proper^#(cons(X1, X2)) ->
c_74(cons^#(proper(X1), proper(X2))) :74
-->_1 proper^#(pair(X1, X2)) ->
c_73(pair^#(proper(X1), proper(X2))) :73
-->_1 proper^#(splitAt(X1, X2)) ->
c_72(splitAt^#(proper(X1), proper(X2))) :72
-->_1 proper^#(U12(X1, X2)) ->
c_71(U12^#(proper(X1), proper(X2))) :71
-->_1 proper^#(U11(X1, X2, X3, X4)) ->
c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) :69
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
-->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65
-->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
-->_1 s^#(ok(X)) -> c_60(s^#(X)) :60
-->_1 s^#(mark(X)) -> c_59(s^#(X)) :59
-->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58
-->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57
-->_1 head^#(ok(X)) -> c_56(head^#(X)) :56
-->_1 head^#(mark(X)) -> c_55(head^#(X)) :55
-->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54
-->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53
-->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52
-->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
-->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47
-->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46
-->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45
-->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
-->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37
-->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36
-->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4)) :35
-->_1 U11^#(mark(X1), X2, X3, X4) ->
c_34(U11^#(X1, X2, X3, X4)) :34
-->_1 active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) :33
-->_1 active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) :32
-->_1 active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) :31
-->_1 active^#(tail(cons(N, XS))) -> c_30(XS) :30
-->_1 active^#(tail(X)) -> c_29(tail^#(active(X))) :29
-->_1 active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) :28
-->_1 active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) :27
-->_1 active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) :26
-->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25
-->_1 active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) :24
-->_1 active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) :23
-->_1 active^#(head(cons(N, XS))) -> c_22(N) :22
-->_1 active^#(head(X)) -> c_21(head^#(active(X))) :21
-->_1 proper^#(nil()) -> c_84() :84
-->_1 proper^#(0()) -> c_83() :83
-->_1 proper^#(tt()) -> c_70() :70
-->_1 active^#(fst(pair(X, Y))) -> c_20(X) :20
-->_1 active^#(fst(X)) -> c_19(fst^#(active(X))) :19
-->_1 active^#(and(tt(), X)) -> c_18(X) :18
-->_1 active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) :17
-->_1 active^#(snd(pair(X, Y))) -> c_16(Y) :16
-->_1 active^#(snd(X)) -> c_15(snd^#(active(X))) :15
-->_1 active^#(afterNth(X1, X2)) ->
c_14(afterNth^#(active(X1), X2)) :14
-->_1 active^#(afterNth(X1, X2)) ->
c_13(afterNth^#(X1, active(X2))) :13
-->_1 active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) :12
-->_1 active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) :11
-->_1 active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) :10
-->_1 active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) :9
-->_1 active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) :8
-->_1 active^#(splitAt(s(N), cons(X, XS))) ->
c_7(U11^#(tt(), N, X, XS)) :7
-->_1 active^#(splitAt(X1, X2)) ->
c_6(splitAt^#(active(X1), X2)) :6
-->_1 active^#(splitAt(X1, X2)) ->
c_5(splitAt^#(X1, active(X2))) :5
-->_1 active^#(U12(pair(YS, ZS), X)) ->
c_4(pair^#(cons(X, YS), ZS)) :4
-->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3
-->_1 active^#(U11(tt(), N, X, XS)) ->
c_2(U12^#(splitAt(N, XS), X)) :2
-->_1 active^#(U11(X1, X2, X3, X4)) ->
c_1(U11^#(active(X1), X2, X3, X4)) :1
21: active^#(head(X)) -> c_21(head^#(active(X)))
-->_1 head^#(ok(X)) -> c_56(head^#(X)) :56
-->_1 head^#(mark(X)) -> c_55(head^#(X)) :55
22: active^#(head(cons(N, XS))) -> c_22(N)
-->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88
-->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87
-->_1 proper^#(take(X1, X2)) ->
c_86(take^#(proper(X1), proper(X2))) :86
-->_1 proper^#(tail(X)) -> c_85(tail^#(proper(X))) :85
-->_1 proper^#(sel(X1, X2)) ->
c_82(sel^#(proper(X1), proper(X2))) :82
-->_1 proper^#(s(X)) -> c_81(s^#(proper(X))) :81
-->_1 proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) :80
-->_1 proper^#(head(X)) -> c_79(head^#(proper(X))) :79
-->_1 proper^#(fst(X)) -> c_78(fst^#(proper(X))) :78
-->_1 proper^#(and(X1, X2)) ->
c_77(and^#(proper(X1), proper(X2))) :77
-->_1 proper^#(snd(X)) -> c_76(snd^#(proper(X))) :76
-->_1 proper^#(afterNth(X1, X2)) ->
c_75(afterNth^#(proper(X1), proper(X2))) :75
-->_1 proper^#(cons(X1, X2)) ->
c_74(cons^#(proper(X1), proper(X2))) :74
-->_1 proper^#(pair(X1, X2)) ->
c_73(pair^#(proper(X1), proper(X2))) :73
-->_1 proper^#(splitAt(X1, X2)) ->
c_72(splitAt^#(proper(X1), proper(X2))) :72
-->_1 proper^#(U12(X1, X2)) ->
c_71(U12^#(proper(X1), proper(X2))) :71
-->_1 proper^#(U11(X1, X2, X3, X4)) ->
c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) :69
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
-->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65
-->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
-->_1 s^#(ok(X)) -> c_60(s^#(X)) :60
-->_1 s^#(mark(X)) -> c_59(s^#(X)) :59
-->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58
-->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57
-->_1 head^#(ok(X)) -> c_56(head^#(X)) :56
-->_1 head^#(mark(X)) -> c_55(head^#(X)) :55
-->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54
-->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53
-->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52
-->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
-->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47
-->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46
-->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45
-->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
-->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37
-->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36
-->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4)) :35
-->_1 U11^#(mark(X1), X2, X3, X4) ->
c_34(U11^#(X1, X2, X3, X4)) :34
-->_1 active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) :33
-->_1 active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) :32
-->_1 active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) :31
-->_1 active^#(tail(cons(N, XS))) -> c_30(XS) :30
-->_1 active^#(tail(X)) -> c_29(tail^#(active(X))) :29
-->_1 active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) :28
-->_1 active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) :27
-->_1 active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) :26
-->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25
-->_1 active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) :24
-->_1 active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) :23
-->_1 proper^#(nil()) -> c_84() :84
-->_1 proper^#(0()) -> c_83() :83
-->_1 proper^#(tt()) -> c_70() :70
-->_1 active^#(head(cons(N, XS))) -> c_22(N) :22
-->_1 active^#(head(X)) -> c_21(head^#(active(X))) :21
-->_1 active^#(fst(pair(X, Y))) -> c_20(X) :20
-->_1 active^#(fst(X)) -> c_19(fst^#(active(X))) :19
-->_1 active^#(and(tt(), X)) -> c_18(X) :18
-->_1 active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) :17
-->_1 active^#(snd(pair(X, Y))) -> c_16(Y) :16
-->_1 active^#(snd(X)) -> c_15(snd^#(active(X))) :15
-->_1 active^#(afterNth(X1, X2)) ->
c_14(afterNth^#(active(X1), X2)) :14
-->_1 active^#(afterNth(X1, X2)) ->
c_13(afterNth^#(X1, active(X2))) :13
-->_1 active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) :12
-->_1 active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) :11
-->_1 active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) :10
-->_1 active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) :9
-->_1 active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) :8
-->_1 active^#(splitAt(s(N), cons(X, XS))) ->
c_7(U11^#(tt(), N, X, XS)) :7
-->_1 active^#(splitAt(X1, X2)) ->
c_6(splitAt^#(active(X1), X2)) :6
-->_1 active^#(splitAt(X1, X2)) ->
c_5(splitAt^#(X1, active(X2))) :5
-->_1 active^#(U12(pair(YS, ZS), X)) ->
c_4(pair^#(cons(X, YS), ZS)) :4
-->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3
-->_1 active^#(U11(tt(), N, X, XS)) ->
c_2(U12^#(splitAt(N, XS), X)) :2
-->_1 active^#(U11(X1, X2, X3, X4)) ->
c_1(U11^#(active(X1), X2, X3, X4)) :1
23: active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N))))
-->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45
-->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44
24: active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X)))
-->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58
-->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57
25: active^#(s(X)) -> c_25(s^#(active(X)))
-->_1 s^#(ok(X)) -> c_60(s^#(X)) :60
-->_1 s^#(mark(X)) -> c_59(s^#(X)) :59
26: active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS)))
-->_1 head^#(ok(X)) -> c_56(head^#(X)) :56
-->_1 head^#(mark(X)) -> c_55(head^#(X)) :55
27: active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2)))
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
28: active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2))
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
29: active^#(tail(X)) -> c_29(tail^#(active(X)))
-->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65
-->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64
30: active^#(tail(cons(N, XS))) -> c_30(XS)
-->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88
-->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87
-->_1 proper^#(take(X1, X2)) ->
c_86(take^#(proper(X1), proper(X2))) :86
-->_1 proper^#(tail(X)) -> c_85(tail^#(proper(X))) :85
-->_1 proper^#(sel(X1, X2)) ->
c_82(sel^#(proper(X1), proper(X2))) :82
-->_1 proper^#(s(X)) -> c_81(s^#(proper(X))) :81
-->_1 proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) :80
-->_1 proper^#(head(X)) -> c_79(head^#(proper(X))) :79
-->_1 proper^#(fst(X)) -> c_78(fst^#(proper(X))) :78
-->_1 proper^#(and(X1, X2)) ->
c_77(and^#(proper(X1), proper(X2))) :77
-->_1 proper^#(snd(X)) -> c_76(snd^#(proper(X))) :76
-->_1 proper^#(afterNth(X1, X2)) ->
c_75(afterNth^#(proper(X1), proper(X2))) :75
-->_1 proper^#(cons(X1, X2)) ->
c_74(cons^#(proper(X1), proper(X2))) :74
-->_1 proper^#(pair(X1, X2)) ->
c_73(pair^#(proper(X1), proper(X2))) :73
-->_1 proper^#(splitAt(X1, X2)) ->
c_72(splitAt^#(proper(X1), proper(X2))) :72
-->_1 proper^#(U12(X1, X2)) ->
c_71(U12^#(proper(X1), proper(X2))) :71
-->_1 proper^#(U11(X1, X2, X3, X4)) ->
c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) :69
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
-->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65
-->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
-->_1 s^#(ok(X)) -> c_60(s^#(X)) :60
-->_1 s^#(mark(X)) -> c_59(s^#(X)) :59
-->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58
-->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57
-->_1 head^#(ok(X)) -> c_56(head^#(X)) :56
-->_1 head^#(mark(X)) -> c_55(head^#(X)) :55
-->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54
-->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53
-->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52
-->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
-->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47
-->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46
-->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45
-->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
-->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37
-->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36
-->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4)) :35
-->_1 U11^#(mark(X1), X2, X3, X4) ->
c_34(U11^#(X1, X2, X3, X4)) :34
-->_1 active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) :33
-->_1 active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) :32
-->_1 active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) :31
-->_1 proper^#(nil()) -> c_84() :84
-->_1 proper^#(0()) -> c_83() :83
-->_1 proper^#(tt()) -> c_70() :70
-->_1 active^#(tail(cons(N, XS))) -> c_30(XS) :30
-->_1 active^#(tail(X)) -> c_29(tail^#(active(X))) :29
-->_1 active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) :28
-->_1 active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) :27
-->_1 active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) :26
-->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25
-->_1 active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) :24
-->_1 active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) :23
-->_1 active^#(head(cons(N, XS))) -> c_22(N) :22
-->_1 active^#(head(X)) -> c_21(head^#(active(X))) :21
-->_1 active^#(fst(pair(X, Y))) -> c_20(X) :20
-->_1 active^#(fst(X)) -> c_19(fst^#(active(X))) :19
-->_1 active^#(and(tt(), X)) -> c_18(X) :18
-->_1 active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) :17
-->_1 active^#(snd(pair(X, Y))) -> c_16(Y) :16
-->_1 active^#(snd(X)) -> c_15(snd^#(active(X))) :15
-->_1 active^#(afterNth(X1, X2)) ->
c_14(afterNth^#(active(X1), X2)) :14
-->_1 active^#(afterNth(X1, X2)) ->
c_13(afterNth^#(X1, active(X2))) :13
-->_1 active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) :12
-->_1 active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) :11
-->_1 active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) :10
-->_1 active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) :9
-->_1 active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) :8
-->_1 active^#(splitAt(s(N), cons(X, XS))) ->
c_7(U11^#(tt(), N, X, XS)) :7
-->_1 active^#(splitAt(X1, X2)) ->
c_6(splitAt^#(active(X1), X2)) :6
-->_1 active^#(splitAt(X1, X2)) ->
c_5(splitAt^#(X1, active(X2))) :5
-->_1 active^#(U12(pair(YS, ZS), X)) ->
c_4(pair^#(cons(X, YS), ZS)) :4
-->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3
-->_1 active^#(U11(tt(), N, X, XS)) ->
c_2(U12^#(splitAt(N, XS), X)) :2
-->_1 active^#(U11(X1, X2, X3, X4)) ->
c_1(U11^#(active(X1), X2, X3, X4)) :1
31: active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS)))
-->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54
-->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53
32: active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2)))
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
33: active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2))
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
34: U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4))
-->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4)) :35
-->_1 U11^#(mark(X1), X2, X3, X4) ->
c_34(U11^#(X1, X2, X3, X4)) :34
35: U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4))
-->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4)) :35
-->_1 U11^#(mark(X1), X2, X3, X4) ->
c_34(U11^#(X1, X2, X3, X4)) :34
36: U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2))
-->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37
-->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36
37: U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2))
-->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37
-->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36
38: pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2))
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
39: pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2))
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
40: pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2))
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
41: splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2))
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
42: splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2))
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
43: splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2))
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
44: cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2))
-->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45
-->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44
45: cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2))
-->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45
-->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44
46: snd^#(mark(X)) -> c_49(snd^#(X))
-->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47
-->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46
47: snd^#(ok(X)) -> c_50(snd^#(X))
-->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47
-->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46
48: afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2))
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
49: afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2))
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
50: afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2))
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
51: and^#(mark(X1), X2) -> c_51(and^#(X1, X2))
-->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52
-->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51
52: and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2))
-->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52
-->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51
53: fst^#(mark(X)) -> c_53(fst^#(X))
-->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54
-->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53
54: fst^#(ok(X)) -> c_54(fst^#(X))
-->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54
-->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53
55: head^#(mark(X)) -> c_55(head^#(X))
-->_1 head^#(ok(X)) -> c_56(head^#(X)) :56
-->_1 head^#(mark(X)) -> c_55(head^#(X)) :55
56: head^#(ok(X)) -> c_56(head^#(X))
-->_1 head^#(ok(X)) -> c_56(head^#(X)) :56
-->_1 head^#(mark(X)) -> c_55(head^#(X)) :55
57: natsFrom^#(mark(X)) -> c_57(natsFrom^#(X))
-->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58
-->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57
58: natsFrom^#(ok(X)) -> c_58(natsFrom^#(X))
-->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58
-->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57
59: s^#(mark(X)) -> c_59(s^#(X))
-->_1 s^#(ok(X)) -> c_60(s^#(X)) :60
-->_1 s^#(mark(X)) -> c_59(s^#(X)) :59
60: s^#(ok(X)) -> c_60(s^#(X))
-->_1 s^#(ok(X)) -> c_60(s^#(X)) :60
-->_1 s^#(mark(X)) -> c_59(s^#(X)) :59
61: sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2))
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
62: sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2))
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
63: sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2))
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
64: tail^#(mark(X)) -> c_64(tail^#(X))
-->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65
-->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64
65: tail^#(ok(X)) -> c_65(tail^#(X))
-->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65
-->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64
66: take^#(X1, mark(X2)) -> c_66(take^#(X1, X2))
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
67: take^#(mark(X1), X2) -> c_67(take^#(X1, X2))
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
68: take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2))
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
69: proper^#(U11(X1, X2, X3, X4)) ->
c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4)))
-->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4)) :35
-->_1 U11^#(mark(X1), X2, X3, X4) ->
c_34(U11^#(X1, X2, X3, X4)) :34
70: proper^#(tt()) -> c_70()
71: proper^#(U12(X1, X2)) -> c_71(U12^#(proper(X1), proper(X2)))
-->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37
-->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36
72: proper^#(splitAt(X1, X2)) ->
c_72(splitAt^#(proper(X1), proper(X2)))
-->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43
-->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42
-->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41
73: proper^#(pair(X1, X2)) -> c_73(pair^#(proper(X1), proper(X2)))
-->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40
-->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39
-->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38
74: proper^#(cons(X1, X2)) -> c_74(cons^#(proper(X1), proper(X2)))
-->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45
-->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44
75: proper^#(afterNth(X1, X2)) ->
c_75(afterNth^#(proper(X1), proper(X2)))
-->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50
-->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49
-->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48
76: proper^#(snd(X)) -> c_76(snd^#(proper(X)))
-->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47
-->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46
77: proper^#(and(X1, X2)) -> c_77(and^#(proper(X1), proper(X2)))
-->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52
-->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51
78: proper^#(fst(X)) -> c_78(fst^#(proper(X)))
-->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54
-->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53
79: proper^#(head(X)) -> c_79(head^#(proper(X)))
-->_1 head^#(ok(X)) -> c_56(head^#(X)) :56
-->_1 head^#(mark(X)) -> c_55(head^#(X)) :55
80: proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X)))
-->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58
-->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57
81: proper^#(s(X)) -> c_81(s^#(proper(X)))
-->_1 s^#(ok(X)) -> c_60(s^#(X)) :60
-->_1 s^#(mark(X)) -> c_59(s^#(X)) :59
82: proper^#(sel(X1, X2)) -> c_82(sel^#(proper(X1), proper(X2)))
-->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63
-->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62
-->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61
83: proper^#(0()) -> c_83()
84: proper^#(nil()) -> c_84()
85: proper^#(tail(X)) -> c_85(tail^#(proper(X)))
-->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65
-->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64
86: proper^#(take(X1, X2)) -> c_86(take^#(proper(X1), proper(X2)))
-->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68
-->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67
-->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66
87: top^#(mark(X)) -> c_87(top^#(proper(X)))
-->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88
-->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87
88: top^#(ok(X)) -> c_88(top^#(active(X)))
-->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88
-->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87
Only the nodes
{34,35,36,37,38,40,39,41,43,42,44,45,46,47,48,50,49,51,52,53,54,55,56,57,58,59,60,61,63,62,64,65,66,68,67,70,83,84,87,88}
are reachable from nodes
{34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,70,83,84,87,88}
that start derivation from marked basic terms. The nodes not
reachable are removed from the problem.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4))
, U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4))
, U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2))
, U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2))
, 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))
, splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2))
, splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2))
, splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2))
, cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2))
, snd^#(mark(X)) -> c_49(snd^#(X))
, snd^#(ok(X)) -> c_50(snd^#(X))
, afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2))
, afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2))
, afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2))
, and^#(mark(X1), X2) -> c_51(and^#(X1, X2))
, and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2))
, fst^#(mark(X)) -> c_53(fst^#(X))
, fst^#(ok(X)) -> c_54(fst^#(X))
, head^#(mark(X)) -> c_55(head^#(X))
, head^#(ok(X)) -> c_56(head^#(X))
, natsFrom^#(mark(X)) -> c_57(natsFrom^#(X))
, natsFrom^#(ok(X)) -> c_58(natsFrom^#(X))
, 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))
, tail^#(mark(X)) -> c_64(tail^#(X))
, tail^#(ok(X)) -> c_65(tail^#(X))
, take^#(X1, mark(X2)) -> c_66(take^#(X1, X2))
, take^#(mark(X1), X2) -> c_67(take^#(X1, X2))
, take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2))
, proper^#(tt()) -> c_70()
, proper^#(0()) -> c_83()
, proper^#(nil()) -> c_84()
, top^#(mark(X)) -> c_87(top^#(proper(X)))
, top^#(ok(X)) -> c_88(top^#(active(X))) }
Strict Trs:
{ active(U11(X1, X2, X3, X4)) -> U11(active(X1), X2, X3, X4)
, active(U11(tt(), N, X, XS)) -> mark(U12(splitAt(N, XS), X))
, active(U12(X1, X2)) -> U12(active(X1), X2)
, active(U12(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS))
, active(splitAt(X1, X2)) -> splitAt(X1, active(X2))
, active(splitAt(X1, X2)) -> splitAt(active(X1), X2)
, active(splitAt(s(N), cons(X, XS))) -> mark(U11(tt(), N, X, XS))
, active(splitAt(0(), XS)) -> mark(pair(nil(), XS))
, active(pair(X1, X2)) -> pair(X1, active(X2))
, active(pair(X1, X2)) -> pair(active(X1), X2)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, 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(snd(X)) -> snd(active(X))
, active(snd(pair(X, Y))) -> mark(Y)
, active(and(X1, X2)) -> and(active(X1), X2)
, active(and(tt(), X)) -> mark(X)
, active(fst(X)) -> fst(active(X))
, active(fst(pair(X, Y))) -> mark(X)
, 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(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(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)
, U11(mark(X1), X2, X3, X4) -> mark(U11(X1, X2, X3, X4))
, U11(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U11(X1, X2, X3, X4))
, U12(mark(X1), X2) -> mark(U12(X1, X2))
, U12(ok(X1), ok(X2)) -> ok(U12(X1, X2))
, 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))
, 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))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, 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))
, snd(mark(X)) -> mark(snd(X))
, snd(ok(X)) -> ok(snd(X))
, and(mark(X1), X2) -> mark(and(X1, X2))
, and(ok(X1), ok(X2)) -> ok(and(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))
, 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))
, 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))
, proper(U11(X1, X2, X3, X4)) ->
U11(proper(X1), proper(X2), proper(X3), proper(X4))
, proper(tt()) -> ok(tt())
, proper(U12(X1, X2)) -> U12(proper(X1), proper(X2))
, proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2))
, proper(pair(X1, X2)) -> pair(proper(X1), proper(X2))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2))
, proper(snd(X)) -> snd(proper(X))
, proper(and(X1, X2)) -> and(proper(X1), proper(X2))
, proper(fst(X)) -> fst(proper(X))
, proper(head(X)) -> head(proper(X))
, proper(natsFrom(X)) -> natsFrom(proper(X))
, proper(s(X)) -> s(proper(X))
, proper(sel(X1, X2)) -> sel(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(nil()) -> ok(nil())
, proper(tail(X)) -> tail(proper(X))
, proper(take(X1, X2)) -> take(proper(X1), proper(X2))
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X)) }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of {36,37,38} by applications
of Pre({36,37,38}) = {}. Here rules are labeled as follows:
DPs:
{ 1: U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4))
, 2: U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4))
, 3: U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2))
, 4: U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2))
, 5: pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2))
, 6: pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2))
, 7: pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2))
, 8: splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2))
, 9: splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2))
, 10: splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2))
, 11: cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2))
, 12: cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2))
, 13: snd^#(mark(X)) -> c_49(snd^#(X))
, 14: snd^#(ok(X)) -> c_50(snd^#(X))
, 15: afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2))
, 16: afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2))
, 17: afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2))
, 18: and^#(mark(X1), X2) -> c_51(and^#(X1, X2))
, 19: and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2))
, 20: fst^#(mark(X)) -> c_53(fst^#(X))
, 21: fst^#(ok(X)) -> c_54(fst^#(X))
, 22: head^#(mark(X)) -> c_55(head^#(X))
, 23: head^#(ok(X)) -> c_56(head^#(X))
, 24: natsFrom^#(mark(X)) -> c_57(natsFrom^#(X))
, 25: natsFrom^#(ok(X)) -> c_58(natsFrom^#(X))
, 26: s^#(mark(X)) -> c_59(s^#(X))
, 27: s^#(ok(X)) -> c_60(s^#(X))
, 28: sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2))
, 29: sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2))
, 30: sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2))
, 31: tail^#(mark(X)) -> c_64(tail^#(X))
, 32: tail^#(ok(X)) -> c_65(tail^#(X))
, 33: take^#(X1, mark(X2)) -> c_66(take^#(X1, X2))
, 34: take^#(mark(X1), X2) -> c_67(take^#(X1, X2))
, 35: take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2))
, 36: proper^#(tt()) -> c_70()
, 37: proper^#(0()) -> c_83()
, 38: proper^#(nil()) -> c_84()
, 39: top^#(mark(X)) -> c_87(top^#(proper(X)))
, 40: top^#(ok(X)) -> c_88(top^#(active(X))) }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4))
, U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) ->
c_35(U11^#(X1, X2, X3, X4))
, U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2))
, U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2))
, 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))
, splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2))
, splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2))
, splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2))
, cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2))
, snd^#(mark(X)) -> c_49(snd^#(X))
, snd^#(ok(X)) -> c_50(snd^#(X))
, afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2))
, afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2))
, afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2))
, and^#(mark(X1), X2) -> c_51(and^#(X1, X2))
, and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2))
, fst^#(mark(X)) -> c_53(fst^#(X))
, fst^#(ok(X)) -> c_54(fst^#(X))
, head^#(mark(X)) -> c_55(head^#(X))
, head^#(ok(X)) -> c_56(head^#(X))
, natsFrom^#(mark(X)) -> c_57(natsFrom^#(X))
, natsFrom^#(ok(X)) -> c_58(natsFrom^#(X))
, 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))
, tail^#(mark(X)) -> c_64(tail^#(X))
, tail^#(ok(X)) -> c_65(tail^#(X))
, take^#(X1, mark(X2)) -> c_66(take^#(X1, X2))
, take^#(mark(X1), X2) -> c_67(take^#(X1, X2))
, take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2))
, top^#(mark(X)) -> c_87(top^#(proper(X)))
, top^#(ok(X)) -> c_88(top^#(active(X))) }
Strict Trs:
{ active(U11(X1, X2, X3, X4)) -> U11(active(X1), X2, X3, X4)
, active(U11(tt(), N, X, XS)) -> mark(U12(splitAt(N, XS), X))
, active(U12(X1, X2)) -> U12(active(X1), X2)
, active(U12(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS))
, active(splitAt(X1, X2)) -> splitAt(X1, active(X2))
, active(splitAt(X1, X2)) -> splitAt(active(X1), X2)
, active(splitAt(s(N), cons(X, XS))) -> mark(U11(tt(), N, X, XS))
, active(splitAt(0(), XS)) -> mark(pair(nil(), XS))
, active(pair(X1, X2)) -> pair(X1, active(X2))
, active(pair(X1, X2)) -> pair(active(X1), X2)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, 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(snd(X)) -> snd(active(X))
, active(snd(pair(X, Y))) -> mark(Y)
, active(and(X1, X2)) -> and(active(X1), X2)
, active(and(tt(), X)) -> mark(X)
, active(fst(X)) -> fst(active(X))
, active(fst(pair(X, Y))) -> mark(X)
, 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(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(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)
, U11(mark(X1), X2, X3, X4) -> mark(U11(X1, X2, X3, X4))
, U11(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U11(X1, X2, X3, X4))
, U12(mark(X1), X2) -> mark(U12(X1, X2))
, U12(ok(X1), ok(X2)) -> ok(U12(X1, X2))
, 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))
, 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))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, 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))
, snd(mark(X)) -> mark(snd(X))
, snd(ok(X)) -> ok(snd(X))
, and(mark(X1), X2) -> mark(and(X1, X2))
, and(ok(X1), ok(X2)) -> ok(and(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))
, 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))
, 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))
, proper(U11(X1, X2, X3, X4)) ->
U11(proper(X1), proper(X2), proper(X3), proper(X4))
, proper(tt()) -> ok(tt())
, proper(U12(X1, X2)) -> U12(proper(X1), proper(X2))
, proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2))
, proper(pair(X1, X2)) -> pair(proper(X1), proper(X2))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2))
, proper(snd(X)) -> snd(proper(X))
, proper(and(X1, X2)) -> and(proper(X1), proper(X2))
, proper(fst(X)) -> fst(proper(X))
, proper(head(X)) -> head(proper(X))
, proper(natsFrom(X)) -> natsFrom(proper(X))
, proper(s(X)) -> s(proper(X))
, proper(sel(X1, X2)) -> sel(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(nil()) -> ok(nil())
, proper(tail(X)) -> tail(proper(X))
, proper(take(X1, X2)) -> take(proper(X1), proper(X2))
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X)) }
Weak DPs:
{ proper^#(tt()) -> c_70()
, proper^#(0()) -> c_83()
, proper^#(nil()) -> c_84() }
Obligation:
runtime complexity
Answer:
MAYBE
Empty strict component of the problem is NOT empty.
Arrrr..