WORST_CASE(?,O(n^1))
proof of input_Wk0zx0tXX1.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 [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxTRS
(9) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(10) CpxTRS
(11) CpxTrsMatchBoundsTAProof [FINISHED, 72 ms]
(12) BOUNDS(1, n^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:

   D(t) -> 1
   D(constant) -> 0
   D(+(x, y)) -> +(D(x), D(y))
   D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
   D(-(x, y)) -> -(D(x), D(y))
   D(minus(x)) -> minus(D(x))
   D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2)))
   D(ln(x)) -> div(D(x), x)
   D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1))), D(x)), *(*(pow(x, y), ln(x)), D(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:
   D(t) -> 1
   D(constant) -> 0
   D(+(z0, z1)) -> +(D(z0), D(z1))
   D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1)))
   D(-(z0, z1)) -> -(D(z0), D(z1))
   D(minus(z0)) -> minus(D(z0))
   D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2)))
   D(ln(z0)) -> div(D(z0), z0)
   D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1)))
Tuples:
   D'(t) -> c
   D'(constant) -> c1
   D'(+(z0, z1)) -> c2(D'(z0))
   D'(+(z0, z1)) -> c3(D'(z1))
   D'(*(z0, z1)) -> c4(D'(z0))
   D'(*(z0, z1)) -> c5(D'(z1))
   D'(-(z0, z1)) -> c6(D'(z0))
   D'(-(z0, z1)) -> c7(D'(z1))
   D'(minus(z0)) -> c8(D'(z0))
   D'(div(z0, z1)) -> c9(D'(z0))
   D'(div(z0, z1)) -> c10(D'(z1))
   D'(ln(z0)) -> c11(D'(z0))
   D'(pow(z0, z1)) -> c12(D'(z0))
   D'(pow(z0, z1)) -> c13(D'(z1))
S tuples:
   D'(t) -> c
   D'(constant) -> c1
   D'(+(z0, z1)) -> c2(D'(z0))
   D'(+(z0, z1)) -> c3(D'(z1))
   D'(*(z0, z1)) -> c4(D'(z0))
   D'(*(z0, z1)) -> c5(D'(z1))
   D'(-(z0, z1)) -> c6(D'(z0))
   D'(-(z0, z1)) -> c7(D'(z1))
   D'(minus(z0)) -> c8(D'(z0))
   D'(div(z0, z1)) -> c9(D'(z0))
   D'(div(z0, z1)) -> c10(D'(z1))
   D'(ln(z0)) -> c11(D'(z0))
   D'(pow(z0, z1)) -> c12(D'(z0))
   D'(pow(z0, z1)) -> c13(D'(z1))
K tuples:none
Defined Rule Symbols:   D_1

Defined Pair Symbols:   D'_1

Compound Symbols:   c, c1, c2_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c13_1


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing nodes:
   D'(t) -> c
   D'(constant) -> c1

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   D(t) -> 1
   D(constant) -> 0
   D(+(z0, z1)) -> +(D(z0), D(z1))
   D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1)))
   D(-(z0, z1)) -> -(D(z0), D(z1))
   D(minus(z0)) -> minus(D(z0))
   D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2)))
   D(ln(z0)) -> div(D(z0), z0)
   D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1)))
Tuples:
   D'(+(z0, z1)) -> c2(D'(z0))
   D'(+(z0, z1)) -> c3(D'(z1))
   D'(*(z0, z1)) -> c4(D'(z0))
   D'(*(z0, z1)) -> c5(D'(z1))
   D'(-(z0, z1)) -> c6(D'(z0))
   D'(-(z0, z1)) -> c7(D'(z1))
   D'(minus(z0)) -> c8(D'(z0))
   D'(div(z0, z1)) -> c9(D'(z0))
   D'(div(z0, z1)) -> c10(D'(z1))
   D'(ln(z0)) -> c11(D'(z0))
   D'(pow(z0, z1)) -> c12(D'(z0))
   D'(pow(z0, z1)) -> c13(D'(z1))
S tuples:
   D'(+(z0, z1)) -> c2(D'(z0))
   D'(+(z0, z1)) -> c3(D'(z1))
   D'(*(z0, z1)) -> c4(D'(z0))
   D'(*(z0, z1)) -> c5(D'(z1))
   D'(-(z0, z1)) -> c6(D'(z0))
   D'(-(z0, z1)) -> c7(D'(z1))
   D'(minus(z0)) -> c8(D'(z0))
   D'(div(z0, z1)) -> c9(D'(z0))
   D'(div(z0, z1)) -> c10(D'(z1))
   D'(ln(z0)) -> c11(D'(z0))
   D'(pow(z0, z1)) -> c12(D'(z0))
   D'(pow(z0, z1)) -> c13(D'(z1))
K tuples:none
Defined Rule Symbols:   D_1

Defined Pair Symbols:   D'_1

Compound Symbols:   c2_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c13_1


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

(5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   D(t) -> 1
   D(constant) -> 0
   D(+(z0, z1)) -> +(D(z0), D(z1))
   D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1)))
   D(-(z0, z1)) -> -(D(z0), D(z1))
   D(minus(z0)) -> minus(D(z0))
   D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2)))
   D(ln(z0)) -> div(D(z0), z0)
   D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1)))

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   D'(+(z0, z1)) -> c2(D'(z0))
   D'(+(z0, z1)) -> c3(D'(z1))
   D'(*(z0, z1)) -> c4(D'(z0))
   D'(*(z0, z1)) -> c5(D'(z1))
   D'(-(z0, z1)) -> c6(D'(z0))
   D'(-(z0, z1)) -> c7(D'(z1))
   D'(minus(z0)) -> c8(D'(z0))
   D'(div(z0, z1)) -> c9(D'(z0))
   D'(div(z0, z1)) -> c10(D'(z1))
   D'(ln(z0)) -> c11(D'(z0))
   D'(pow(z0, z1)) -> c12(D'(z0))
   D'(pow(z0, z1)) -> c13(D'(z1))
S tuples:
   D'(+(z0, z1)) -> c2(D'(z0))
   D'(+(z0, z1)) -> c3(D'(z1))
   D'(*(z0, z1)) -> c4(D'(z0))
   D'(*(z0, z1)) -> c5(D'(z1))
   D'(-(z0, z1)) -> c6(D'(z0))
   D'(-(z0, z1)) -> c7(D'(z1))
   D'(minus(z0)) -> c8(D'(z0))
   D'(div(z0, z1)) -> c9(D'(z0))
   D'(div(z0, z1)) -> c10(D'(z1))
   D'(ln(z0)) -> c11(D'(z0))
   D'(pow(z0, z1)) -> c12(D'(z0))
   D'(pow(z0, z1)) -> c13(D'(z1))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   D'_1

Compound Symbols:   c2_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c13_1


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

(7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   D'(+(z0, z1)) -> c2(D'(z0))
   D'(+(z0, z1)) -> c3(D'(z1))
   D'(*(z0, z1)) -> c4(D'(z0))
   D'(*(z0, z1)) -> c5(D'(z1))
   D'(-(z0, z1)) -> c6(D'(z0))
   D'(-(z0, z1)) -> c7(D'(z1))
   D'(minus(z0)) -> c8(D'(z0))
   D'(div(z0, z1)) -> c9(D'(z0))
   D'(div(z0, z1)) -> c10(D'(z1))
   D'(ln(z0)) -> c11(D'(z0))
   D'(pow(z0, z1)) -> c12(D'(z0))
   D'(pow(z0, z1)) -> c13(D'(z1))

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

(9) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

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


The TRS R consists of the following rules:

   D'(+(z0, z1)) -> c2(D'(z0))
   D'(+(z0, z1)) -> c3(D'(z1))
   D'(*(z0, z1)) -> c4(D'(z0))
   D'(*(z0, z1)) -> c5(D'(z1))
   D'(-(z0, z1)) -> c6(D'(z0))
   D'(-(z0, z1)) -> c7(D'(z1))
   D'(minus(z0)) -> c8(D'(z0))
   D'(div(z0, z1)) -> c9(D'(z0))
   D'(div(z0, z1)) -> c10(D'(z1))
   D'(ln(z0)) -> c11(D'(z0))
   D'(pow(z0, z1)) -> c12(D'(z0))
   D'(pow(z0, z1)) -> c13(D'(z1))

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

(11) CpxTrsMatchBoundsTAProof (FINISHED)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1. 

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: 
final states : [1]
transitions: 
+0(0, 0) -> 0
c20(0) -> 0
c30(0) -> 0
*0(0, 0) -> 0
c40(0) -> 0
c50(0) -> 0
-0(0, 0) -> 0
c60(0) -> 0
c70(0) -> 0
minus0(0) -> 0
c80(0) -> 0
div0(0, 0) -> 0
c90(0) -> 0
c100(0) -> 0
ln0(0) -> 0
c110(0) -> 0
pow0(0, 0) -> 0
c120(0) -> 0
c130(0) -> 0
D'0(0) -> 1
D'1(0) -> 2
c21(2) -> 1
D'1(0) -> 3
c31(3) -> 1
D'1(0) -> 4
c41(4) -> 1
D'1(0) -> 5
c51(5) -> 1
D'1(0) -> 6
c61(6) -> 1
D'1(0) -> 7
c71(7) -> 1
D'1(0) -> 8
c81(8) -> 1
D'1(0) -> 9
c91(9) -> 1
D'1(0) -> 10
c101(10) -> 1
D'1(0) -> 11
c111(11) -> 1
D'1(0) -> 12
c121(12) -> 1
D'1(0) -> 13
c131(13) -> 1
c21(2) -> 2
c21(2) -> 3
c21(2) -> 4
c21(2) -> 5
c21(2) -> 6
c21(2) -> 7
c21(2) -> 8
c21(2) -> 9
c21(2) -> 10
c21(2) -> 11
c21(2) -> 12
c21(2) -> 13
c31(3) -> 2
c31(3) -> 3
c31(3) -> 4
c31(3) -> 5
c31(3) -> 6
c31(3) -> 7
c31(3) -> 8
c31(3) -> 9
c31(3) -> 10
c31(3) -> 11
c31(3) -> 12
c31(3) -> 13
c41(4) -> 2
c41(4) -> 3
c41(4) -> 4
c41(4) -> 5
c41(4) -> 6
c41(4) -> 7
c41(4) -> 8
c41(4) -> 9
c41(4) -> 10
c41(4) -> 11
c41(4) -> 12
c41(4) -> 13
c51(5) -> 2
c51(5) -> 3
c51(5) -> 4
c51(5) -> 5
c51(5) -> 6
c51(5) -> 7
c51(5) -> 8
c51(5) -> 9
c51(5) -> 10
c51(5) -> 11
c51(5) -> 12
c51(5) -> 13
c61(6) -> 2
c61(6) -> 3
c61(6) -> 4
c61(6) -> 5
c61(6) -> 6
c61(6) -> 7
c61(6) -> 8
c61(6) -> 9
c61(6) -> 10
c61(6) -> 11
c61(6) -> 12
c61(6) -> 13
c71(7) -> 2
c71(7) -> 3
c71(7) -> 4
c71(7) -> 5
c71(7) -> 6
c71(7) -> 7
c71(7) -> 8
c71(7) -> 9
c71(7) -> 10
c71(7) -> 11
c71(7) -> 12
c71(7) -> 13
c81(8) -> 2
c81(8) -> 3
c81(8) -> 4
c81(8) -> 5
c81(8) -> 6
c81(8) -> 7
c81(8) -> 8
c81(8) -> 9
c81(8) -> 10
c81(8) -> 11
c81(8) -> 12
c81(8) -> 13
c91(9) -> 2
c91(9) -> 3
c91(9) -> 4
c91(9) -> 5
c91(9) -> 6
c91(9) -> 7
c91(9) -> 8
c91(9) -> 9
c91(9) -> 10
c91(9) -> 11
c91(9) -> 12
c91(9) -> 13
c101(10) -> 2
c101(10) -> 3
c101(10) -> 4
c101(10) -> 5
c101(10) -> 6
c101(10) -> 7
c101(10) -> 8
c101(10) -> 9
c101(10) -> 10
c101(10) -> 11
c101(10) -> 12
c101(10) -> 13
c111(11) -> 2
c111(11) -> 3
c111(11) -> 4
c111(11) -> 5
c111(11) -> 6
c111(11) -> 7
c111(11) -> 8
c111(11) -> 9
c111(11) -> 10
c111(11) -> 11
c111(11) -> 12
c111(11) -> 13
c121(12) -> 2
c121(12) -> 3
c121(12) -> 4
c121(12) -> 5
c121(12) -> 6
c121(12) -> 7
c121(12) -> 8
c121(12) -> 9
c121(12) -> 10
c121(12) -> 11
c121(12) -> 12
c121(12) -> 13
c131(13) -> 2
c131(13) -> 3
c131(13) -> 4
c131(13) -> 5
c131(13) -> 6
c131(13) -> 7
c131(13) -> 8
c131(13) -> 9
c131(13) -> 10
c131(13) -> 11
c131(13) -> 12
c131(13) -> 13

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

(12)
BOUNDS(1, n^1)