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


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 126 ms]
(8) CdtProblem
(9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^3)), 680 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(n^1, n^3).


The TRS R consists of the following rules:

   +(0, y) -> y
   +(s(x), y) -> s(+(x, y))
   +(p(x), y) -> p(+(x, y))
   minus(0) -> 0
   minus(s(x)) -> p(minus(x))
   minus(p(x)) -> s(minus(x))
   *(0, y) -> 0
   *(s(x), y) -> +(*(x, y), y)
   *(p(x), y) -> +(*(x, y), minus(y))

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:
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
Tuples:
   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))
S tuples:
   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))
K tuples:none
Defined Rule Symbols:   +_2, minus_1, *_2

Defined Pair Symbols:   +'_2, MINUS_1, *'_2

Compound Symbols:   c, c1_1, c2_1, c3, c4_1, c5_1, c6, c7_2, c8_2, c9_2


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 3 trailing nodes:
   *'(0, z0) -> c6
   +'(0, z0) -> c
   MINUS(0) -> c3

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
Tuples:
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))
S tuples:
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))
K tuples:none
Defined Rule Symbols:   +_2, minus_1, *_2

Defined Pair Symbols:   +'_2, MINUS_1, *'_2

Compound Symbols:   c1_1, c2_1, c4_1, c5_1, c7_2, c8_2, c9_2


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

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
Split RHS of tuples not part of any SCC
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
Tuples:
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c(+'(*(z0, z1), minus(z1)))
   *'(p(z0), z1) -> c(MINUS(z1))
S tuples:
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c(+'(*(z0, z1), minus(z1)))
   *'(p(z0), z1) -> c(MINUS(z1))
K tuples:none
Defined Rule Symbols:   +_2, minus_1, *_2

Defined Pair Symbols:   +'_2, MINUS_1, *'_2

Compound Symbols:   c1_1, c2_1, c4_1, c5_1, c7_2, c8_2, c_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.
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c(+'(*(z0, z1), minus(z1)))
   *'(p(z0), z1) -> c(MINUS(z1))
We considered the (Usable) Rules:none
And the Tuples:
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c(+'(*(z0, z1), minus(z1)))
   *'(p(z0), z1) -> c(MINUS(z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(*(x_1, x_2)) = [1] + x_1 + x_2
   POL(*'(x_1, x_2)) = [1] + x_1 + x_2
   POL(+(x_1, x_2)) = [1] + x_1 + x_2
   POL(+'(x_1, x_2)) = 0
   POL(0) = [1]
   POL(MINUS(x_1)) = x_1
   POL(c(x_1)) = x_1
   POL(c1(x_1)) = x_1
   POL(c2(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c5(x_1)) = x_1
   POL(c7(x_1, x_2)) = x_1 + x_2
   POL(c8(x_1, x_2)) = x_1 + x_2
   POL(minus(x_1)) = [1] + x_1
   POL(p(x_1)) = [1] + x_1
   POL(s(x_1)) = [1] + x_1

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
Tuples:
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c(+'(*(z0, z1), minus(z1)))
   *'(p(z0), z1) -> c(MINUS(z1))
S tuples:
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
K tuples:
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c(+'(*(z0, z1), minus(z1)))
   *'(p(z0), z1) -> c(MINUS(z1))
Defined Rule Symbols:   +_2, minus_1, *_2

Defined Pair Symbols:   +'_2, MINUS_1, *'_2

Compound Symbols:   c1_1, c2_1, c4_1, c5_1, c7_2, c8_2, c_1


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

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^3)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
We considered the (Usable) Rules:
   +(s(z0), z1) -> s(+(z0, z1))
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
   minus(0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   minus(s(z0)) -> p(minus(z0))
   +(p(z0), z1) -> p(+(z0, z1))
   +(0, z0) -> z0
And the Tuples:
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c(+'(*(z0, z1), minus(z1)))
   *'(p(z0), z1) -> c(MINUS(z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(*(x_1, x_2)) = x_1*x_2
   POL(*'(x_1, x_2)) = [1] + x_2 + x_2^2 + x_1^2*x_2 + x_2^3
   POL(+(x_1, x_2)) = x_1 + x_2
   POL(+'(x_1, x_2)) = x_1
   POL(0) = 0
   POL(MINUS(x_1)) = [1] + x_1 + x_1^2 + x_1^3
   POL(c(x_1)) = x_1
   POL(c1(x_1)) = x_1
   POL(c2(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c5(x_1)) = x_1
   POL(c7(x_1, x_2)) = x_1 + x_2
   POL(c8(x_1, x_2)) = x_1 + x_2
   POL(minus(x_1)) = x_1
   POL(p(x_1)) = [1] + x_1
   POL(s(x_1)) = [1] + x_1

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
Tuples:
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c(+'(*(z0, z1), minus(z1)))
   *'(p(z0), z1) -> c(MINUS(z1))
S tuples:none
K tuples:
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c(+'(*(z0, z1), minus(z1)))
   *'(p(z0), z1) -> c(MINUS(z1))
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
Defined Rule Symbols:   +_2, minus_1, *_2

Defined Pair Symbols:   +'_2, MINUS_1, *'_2

Compound Symbols:   c1_1, c2_1, c4_1, c5_1, c7_2, c8_2, c_1


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

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

(12)
BOUNDS(1, 1)