WORST_CASE(?,O(n^1))
proof of input_wSuBQEvWQn.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 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 [ComplexityIfPolyImplication, 0 ms]
(4) CdtProblem
(5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 75 ms]
(8) CdtProblem
(9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 12 ms]
(10) CdtProblem
(11) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) 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:

   selects(x', revprefix, Cons(x, xs)) -> Cons(Cons(x', revapp(revprefix, Cons(x, xs))), selects(x, Cons(x', revprefix), xs))
   select(Cons(x, xs)) -> selects(x, Nil, xs)
   revapp(Cons(x, xs), rest) -> revapp(xs, Cons(x, rest))
   selects(x, revprefix, Nil) -> Cons(Cons(x, revapp(revprefix, Nil)), Nil)
   select(Nil) -> Nil
   revapp(Nil, rest) -> rest

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:
   selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3))
   selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil)
   select(Cons(z0, z1)) -> selects(z0, Nil, z1)
   select(Nil) -> Nil
   revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
   revapp(Nil, z0) -> z0
Tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1))
   SELECT(Nil) -> c4
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
   REVAPP(Nil, z0) -> c6
S tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1))
   SELECT(Nil) -> c4
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
   REVAPP(Nil, z0) -> c6
K tuples:none
Defined Rule Symbols:   selects_3, select_1, revapp_2

Defined Pair Symbols:   SELECTS_3, SELECT_1, REVAPP_2

Compound Symbols:   c_1, c1_1, c2_1, c3_1, c4, c5_1, c6


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

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1))
Removed 2 trailing nodes:
   REVAPP(Nil, z0) -> c6
   SELECT(Nil) -> c4

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3))
   selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil)
   select(Cons(z0, z1)) -> selects(z0, Nil, z1)
   select(Nil) -> Nil
   revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
   revapp(Nil, z0) -> z0
Tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
S tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
K tuples:none
Defined Rule Symbols:   selects_3, select_1, revapp_2

Defined Pair Symbols:   SELECTS_3, REVAPP_2

Compound Symbols:   c_1, c1_1, c2_1, c5_1


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

(5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3))
   selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil)
   select(Cons(z0, z1)) -> selects(z0, Nil, z1)
   select(Nil) -> Nil
   revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
   revapp(Nil, z0) -> z0

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
S tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   SELECTS_3, REVAPP_2

Compound Symbols:   c_1, c1_1, c2_1, c5_1


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

(7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
We considered the (Usable) Rules:none
And the Tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(Cons(x_1, x_2)) = [1] + x_1 + x_2
   POL(Nil) = [1]
   POL(REVAPP(x_1, x_2)) = [1] + x_1
   POL(SELECTS(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3
   POL(c(x_1)) = x_1
   POL(c1(x_1)) = x_1
   POL(c2(x_1)) = x_1
   POL(c5(x_1)) = x_1

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
S tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
K tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
Defined Rule Symbols:none

Defined Pair Symbols:   SELECTS_3, REVAPP_2

Compound Symbols:   c_1, c1_1, c2_1, c5_1


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

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
We considered the (Usable) Rules:none
And the Tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(Cons(x_1, x_2)) = [1] + x_1 + x_2
   POL(Nil) = [1]
   POL(REVAPP(x_1, x_2)) = [1]
   POL(SELECTS(x_1, x_2, x_3)) = x_1 + x_3
   POL(c(x_1)) = x_1
   POL(c1(x_1)) = x_1
   POL(c2(x_1)) = x_1
   POL(c5(x_1)) = x_1

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
S tuples:none
K tuples:
   SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3)))
   SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2)))
   SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3))
Defined Rule Symbols:none

Defined Pair Symbols:   SELECTS_3, REVAPP_2

Compound Symbols:   c_1, c1_1, c2_1, c5_1


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

(11) SIsEmptyProof (BOTH BOUNDS(ID, ID))
The set S is empty
----------------------------------------

(12)
BOUNDS(1, 1)