WORST_CASE(?,O(n^1))
proof of input_yIRrV4bBCV.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
(8) CdtProblem
(9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) CdtProblem
(11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 99 ms]
(12) CdtProblem
(13) CdtKnowledgeProof [FINISHED, 0 ms]
(14) BOUNDS(1, 1)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   U11(tt, N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X))
   U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
   afterNth(N, XS) -> snd(splitAt(N, XS))
   and(tt, X) -> activate(X)
   fst(pair(X, Y)) -> X
   head(cons(N, XS)) -> N
   natsFrom(N) -> cons(N, n__natsFrom(s(N)))
   sel(N, XS) -> head(afterNth(N, XS))
   snd(pair(X, Y)) -> Y
   splitAt(0, XS) -> pair(nil, XS)
   splitAt(s(N), cons(X, XS)) -> U11(tt, N, X, activate(XS))
   tail(cons(N, XS)) -> activate(XS)
   take(N, XS) -> fst(splitAt(N, XS))
   natsFrom(X) -> n__natsFrom(X)
   activate(n__natsFrom(X)) -> natsFrom(X)
   activate(X) -> X

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1))
   U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1)
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   and(tt, z0) -> activate(z0)
   fst(pair(z0, z1)) -> z0
   head(cons(z0, z1)) -> z0
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   sel(z0, z1) -> head(afterNth(z0, z1))
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2))
   tail(cons(z0, z1)) -> activate(z1)
   take(z0, z1) -> fst(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
Tuples:
   U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0))
   U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2))
   U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1))
   U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2))
   AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   AND(tt, z0) -> c5(ACTIVATE(z0))
   FST(pair(z0, z1)) -> c6
   HEAD(cons(z0, z1)) -> c7
   NATSFROM(z0) -> c8
   NATSFROM(z0) -> c9
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   SND(pair(z0, z1)) -> c11
   SPLITAT(0, z0) -> c12
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2))
   TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1))
   TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0))
   ACTIVATE(z0) -> c17
S tuples:
   U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0))
   U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2))
   U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1))
   U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2))
   AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   AND(tt, z0) -> c5(ACTIVATE(z0))
   FST(pair(z0, z1)) -> c6
   HEAD(cons(z0, z1)) -> c7
   NATSFROM(z0) -> c8
   NATSFROM(z0) -> c9
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   SND(pair(z0, z1)) -> c11
   SPLITAT(0, z0) -> c12
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2))
   TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1))
   TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0))
   ACTIVATE(z0) -> c17
K tuples:none
Defined Rule Symbols:   U11_4, U12_2, afterNth_2, and_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1

Defined Pair Symbols:   U11'_4, U12'_2, AFTERNTH_2, AND_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1

Compound Symbols:   c_3, c1_3, c2_2, c3_1, c4_2, c5_1, c6, c7, c8, c9, c10_2, c11, c12, c13_2, c14_1, c15_2, c16_1, c17


----------------------------------------

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 12 trailing nodes:
   TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1))
   SPLITAT(0, z0) -> c12
   FST(pair(z0, z1)) -> c6
   SND(pair(z0, z1)) -> c11
   U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2))
   NATSFROM(z0) -> c9
   HEAD(cons(z0, z1)) -> c7
   ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0))
   NATSFROM(z0) -> c8
   ACTIVATE(z0) -> c17
   AND(tt, z0) -> c5(ACTIVATE(z0))
   U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1))

----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1))
   U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1)
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   and(tt, z0) -> activate(z0)
   fst(pair(z0, z1)) -> z0
   head(cons(z0, z1)) -> z0
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   sel(z0, z1) -> head(afterNth(z0, z1))
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2))
   tail(cons(z0, z1)) -> activate(z1)
   take(z0, z1) -> fst(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
Tuples:
   U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0))
   U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2))
   AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2))
   TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
S tuples:
   U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0))
   U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2))
   AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2))
   TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
K tuples:none
Defined Rule Symbols:   U11_4, U12_2, afterNth_2, and_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1

Defined Pair Symbols:   U11'_4, AFTERNTH_2, SEL_2, SPLITAT_2, TAKE_2

Compound Symbols:   c_3, c1_3, c4_2, c10_2, c13_2, c15_2


----------------------------------------

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 8 trailing tuple parts
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1))
   U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1)
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   and(tt, z0) -> activate(z0)
   fst(pair(z0, z1)) -> z0
   head(cons(z0, z1)) -> z0
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   sel(z0, z1) -> head(afterNth(z0, z1))
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2))
   tail(cons(z0, z1)) -> activate(z1)
   take(z0, z1) -> fst(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
Tuples:
   U11'(tt, z0, z1, z2) -> c(SPLITAT(activate(z0), activate(z2)))
   U11'(tt, z0, z1, z2) -> c1(SPLITAT(activate(z0), activate(z2)))
   AFTERNTH(z0, z1) -> c4(SPLITAT(z0, z1))
   SEL(z0, z1) -> c10(AFTERNTH(z0, z1))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
   TAKE(z0, z1) -> c15(SPLITAT(z0, z1))
S tuples:
   U11'(tt, z0, z1, z2) -> c(SPLITAT(activate(z0), activate(z2)))
   U11'(tt, z0, z1, z2) -> c1(SPLITAT(activate(z0), activate(z2)))
   AFTERNTH(z0, z1) -> c4(SPLITAT(z0, z1))
   SEL(z0, z1) -> c10(AFTERNTH(z0, z1))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
   TAKE(z0, z1) -> c15(SPLITAT(z0, z1))
K tuples:none
Defined Rule Symbols:   U11_4, U12_2, afterNth_2, and_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1

Defined Pair Symbols:   U11'_4, AFTERNTH_2, SEL_2, SPLITAT_2, TAKE_2

Compound Symbols:   c_1, c1_1, c4_1, c10_1, c13_1, c15_1


----------------------------------------

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 3 leading nodes:
   SEL(z0, z1) -> c10(AFTERNTH(z0, z1))
   AFTERNTH(z0, z1) -> c4(SPLITAT(z0, z1))
   TAKE(z0, z1) -> c15(SPLITAT(z0, z1))

----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1))
   U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1)
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   and(tt, z0) -> activate(z0)
   fst(pair(z0, z1)) -> z0
   head(cons(z0, z1)) -> z0
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   sel(z0, z1) -> head(afterNth(z0, z1))
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2))
   tail(cons(z0, z1)) -> activate(z1)
   take(z0, z1) -> fst(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
Tuples:
   U11'(tt, z0, z1, z2) -> c(SPLITAT(activate(z0), activate(z2)))
   U11'(tt, z0, z1, z2) -> c1(SPLITAT(activate(z0), activate(z2)))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
S tuples:
   U11'(tt, z0, z1, z2) -> c(SPLITAT(activate(z0), activate(z2)))
   U11'(tt, z0, z1, z2) -> c1(SPLITAT(activate(z0), activate(z2)))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
K tuples:none
Defined Rule Symbols:   U11_4, U12_2, afterNth_2, and_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1

Defined Pair Symbols:   U11'_4, SPLITAT_2

Compound Symbols:   c_1, c1_1, c13_1


----------------------------------------

(9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1))
   U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1)
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   and(tt, z0) -> activate(z0)
   fst(pair(z0, z1)) -> z0
   head(cons(z0, z1)) -> z0
   sel(z0, z1) -> head(afterNth(z0, z1))
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2))
   tail(cons(z0, z1)) -> activate(z1)
   take(z0, z1) -> fst(splitAt(z0, z1))

----------------------------------------

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
Tuples:
   U11'(tt, z0, z1, z2) -> c(SPLITAT(activate(z0), activate(z2)))
   U11'(tt, z0, z1, z2) -> c1(SPLITAT(activate(z0), activate(z2)))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
S tuples:
   U11'(tt, z0, z1, z2) -> c(SPLITAT(activate(z0), activate(z2)))
   U11'(tt, z0, z1, z2) -> c1(SPLITAT(activate(z0), activate(z2)))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
K tuples:none
Defined Rule Symbols:   activate_1, natsFrom_1

Defined Pair Symbols:   U11'_4, SPLITAT_2

Compound Symbols:   c_1, c1_1, c13_1


----------------------------------------

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
We considered the (Usable) Rules:
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   natsFrom(z0) -> n__natsFrom(z0)
And the Tuples:
   U11'(tt, z0, z1, z2) -> c(SPLITAT(activate(z0), activate(z2)))
   U11'(tt, z0, z1, z2) -> c1(SPLITAT(activate(z0), activate(z2)))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(SPLITAT(x_1, x_2)) = [1] + x_1 + x_2
   POL(U11'(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_4
   POL(activate(x_1)) = x_1
   POL(c(x_1)) = x_1
   POL(c1(x_1)) = x_1
   POL(c13(x_1)) = x_1
   POL(cons(x_1, x_2)) = x_2
   POL(n__natsFrom(x_1)) = [1]
   POL(natsFrom(x_1)) = [1]
   POL(s(x_1)) = [1] + x_1
   POL(tt) = [1]

----------------------------------------

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
Tuples:
   U11'(tt, z0, z1, z2) -> c(SPLITAT(activate(z0), activate(z2)))
   U11'(tt, z0, z1, z2) -> c1(SPLITAT(activate(z0), activate(z2)))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
S tuples:
   U11'(tt, z0, z1, z2) -> c(SPLITAT(activate(z0), activate(z2)))
   U11'(tt, z0, z1, z2) -> c1(SPLITAT(activate(z0), activate(z2)))
K tuples:
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
Defined Rule Symbols:   activate_1, natsFrom_1

Defined Pair Symbols:   U11'_4, SPLITAT_2

Compound Symbols:   c_1, c1_1, c13_1


----------------------------------------

(13) CdtKnowledgeProof (FINISHED)
The following tuples could be moved from S to K by knowledge propagation:
   U11'(tt, z0, z1, z2) -> c(SPLITAT(activate(z0), activate(z2)))
   U11'(tt, z0, z1, z2) -> c1(SPLITAT(activate(z0), activate(z2)))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
   SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)))
Now S is empty
----------------------------------------

(14)
BOUNDS(1, 1)