WORST_CASE(?,O(n^1))
proof of input_oDjZFXt0Uz.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) 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, 61 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:

   dx(X) -> one
   dx(a) -> zero
   dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA))
   dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
   dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA))
   dx(neg(ALPHA)) -> neg(dx(ALPHA))
   dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two))))
   dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)
   dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one)), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))

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:
   dx(z0) -> one
   dx(a) -> zero
   dx(plus(z0, z1)) -> plus(dx(z0), dx(z1))
   dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1)))
   dx(minus(z0, z1)) -> minus(dx(z0), dx(z1))
   dx(neg(z0)) -> neg(dx(z0))
   dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two))))
   dx(ln(z0)) -> div(dx(z0), z0)
   dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(z1))))
Tuples:
   DX(z0) -> c
   DX(a) -> c1
   DX(plus(z0, z1)) -> c2(DX(z0))
   DX(plus(z0, z1)) -> c3(DX(z1))
   DX(times(z0, z1)) -> c4(DX(z0))
   DX(times(z0, z1)) -> c5(DX(z1))
   DX(minus(z0, z1)) -> c6(DX(z0))
   DX(minus(z0, z1)) -> c7(DX(z1))
   DX(neg(z0)) -> c8(DX(z0))
   DX(div(z0, z1)) -> c9(DX(z0))
   DX(div(z0, z1)) -> c10(DX(z1))
   DX(ln(z0)) -> c11(DX(z0))
   DX(exp(z0, z1)) -> c12(DX(z0))
   DX(exp(z0, z1)) -> c13(DX(z1))
S tuples:
   DX(z0) -> c
   DX(a) -> c1
   DX(plus(z0, z1)) -> c2(DX(z0))
   DX(plus(z0, z1)) -> c3(DX(z1))
   DX(times(z0, z1)) -> c4(DX(z0))
   DX(times(z0, z1)) -> c5(DX(z1))
   DX(minus(z0, z1)) -> c6(DX(z0))
   DX(minus(z0, z1)) -> c7(DX(z1))
   DX(neg(z0)) -> c8(DX(z0))
   DX(div(z0, z1)) -> c9(DX(z0))
   DX(div(z0, z1)) -> c10(DX(z1))
   DX(ln(z0)) -> c11(DX(z0))
   DX(exp(z0, z1)) -> c12(DX(z0))
   DX(exp(z0, z1)) -> c13(DX(z1))
K tuples:none
Defined Rule Symbols:   dx_1

Defined Pair Symbols:   DX_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:
   DX(z0) -> c
   DX(a) -> c1

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   dx(z0) -> one
   dx(a) -> zero
   dx(plus(z0, z1)) -> plus(dx(z0), dx(z1))
   dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1)))
   dx(minus(z0, z1)) -> minus(dx(z0), dx(z1))
   dx(neg(z0)) -> neg(dx(z0))
   dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two))))
   dx(ln(z0)) -> div(dx(z0), z0)
   dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(z1))))
Tuples:
   DX(plus(z0, z1)) -> c2(DX(z0))
   DX(plus(z0, z1)) -> c3(DX(z1))
   DX(times(z0, z1)) -> c4(DX(z0))
   DX(times(z0, z1)) -> c5(DX(z1))
   DX(minus(z0, z1)) -> c6(DX(z0))
   DX(minus(z0, z1)) -> c7(DX(z1))
   DX(neg(z0)) -> c8(DX(z0))
   DX(div(z0, z1)) -> c9(DX(z0))
   DX(div(z0, z1)) -> c10(DX(z1))
   DX(ln(z0)) -> c11(DX(z0))
   DX(exp(z0, z1)) -> c12(DX(z0))
   DX(exp(z0, z1)) -> c13(DX(z1))
S tuples:
   DX(plus(z0, z1)) -> c2(DX(z0))
   DX(plus(z0, z1)) -> c3(DX(z1))
   DX(times(z0, z1)) -> c4(DX(z0))
   DX(times(z0, z1)) -> c5(DX(z1))
   DX(minus(z0, z1)) -> c6(DX(z0))
   DX(minus(z0, z1)) -> c7(DX(z1))
   DX(neg(z0)) -> c8(DX(z0))
   DX(div(z0, z1)) -> c9(DX(z0))
   DX(div(z0, z1)) -> c10(DX(z1))
   DX(ln(z0)) -> c11(DX(z0))
   DX(exp(z0, z1)) -> c12(DX(z0))
   DX(exp(z0, z1)) -> c13(DX(z1))
K tuples:none
Defined Rule Symbols:   dx_1

Defined Pair Symbols:   DX_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:
   dx(z0) -> one
   dx(a) -> zero
   dx(plus(z0, z1)) -> plus(dx(z0), dx(z1))
   dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1)))
   dx(minus(z0, z1)) -> minus(dx(z0), dx(z1))
   dx(neg(z0)) -> neg(dx(z0))
   dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two))))
   dx(ln(z0)) -> div(dx(z0), z0)
   dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(z1))))

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   DX(plus(z0, z1)) -> c2(DX(z0))
   DX(plus(z0, z1)) -> c3(DX(z1))
   DX(times(z0, z1)) -> c4(DX(z0))
   DX(times(z0, z1)) -> c5(DX(z1))
   DX(minus(z0, z1)) -> c6(DX(z0))
   DX(minus(z0, z1)) -> c7(DX(z1))
   DX(neg(z0)) -> c8(DX(z0))
   DX(div(z0, z1)) -> c9(DX(z0))
   DX(div(z0, z1)) -> c10(DX(z1))
   DX(ln(z0)) -> c11(DX(z0))
   DX(exp(z0, z1)) -> c12(DX(z0))
   DX(exp(z0, z1)) -> c13(DX(z1))
S tuples:
   DX(plus(z0, z1)) -> c2(DX(z0))
   DX(plus(z0, z1)) -> c3(DX(z1))
   DX(times(z0, z1)) -> c4(DX(z0))
   DX(times(z0, z1)) -> c5(DX(z1))
   DX(minus(z0, z1)) -> c6(DX(z0))
   DX(minus(z0, z1)) -> c7(DX(z1))
   DX(neg(z0)) -> c8(DX(z0))
   DX(div(z0, z1)) -> c9(DX(z0))
   DX(div(z0, z1)) -> c10(DX(z1))
   DX(ln(z0)) -> c11(DX(z0))
   DX(exp(z0, z1)) -> c12(DX(z0))
   DX(exp(z0, z1)) -> c13(DX(z1))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   DX_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:

   DX(plus(z0, z1)) -> c2(DX(z0))
   DX(plus(z0, z1)) -> c3(DX(z1))
   DX(times(z0, z1)) -> c4(DX(z0))
   DX(times(z0, z1)) -> c5(DX(z1))
   DX(minus(z0, z1)) -> c6(DX(z0))
   DX(minus(z0, z1)) -> c7(DX(z1))
   DX(neg(z0)) -> c8(DX(z0))
   DX(div(z0, z1)) -> c9(DX(z0))
   DX(div(z0, z1)) -> c10(DX(z1))
   DX(ln(z0)) -> c11(DX(z0))
   DX(exp(z0, z1)) -> c12(DX(z0))
   DX(exp(z0, z1)) -> c13(DX(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:

   DX(plus(z0, z1)) -> c2(DX(z0))
   DX(plus(z0, z1)) -> c3(DX(z1))
   DX(times(z0, z1)) -> c4(DX(z0))
   DX(times(z0, z1)) -> c5(DX(z1))
   DX(minus(z0, z1)) -> c6(DX(z0))
   DX(minus(z0, z1)) -> c7(DX(z1))
   DX(neg(z0)) -> c8(DX(z0))
   DX(div(z0, z1)) -> c9(DX(z0))
   DX(div(z0, z1)) -> c10(DX(z1))
   DX(ln(z0)) -> c11(DX(z0))
   DX(exp(z0, z1)) -> c12(DX(z0))
   DX(exp(z0, z1)) -> c13(DX(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: 
plus0(0, 0) -> 0
c20(0) -> 0
c30(0) -> 0
times0(0, 0) -> 0
c40(0) -> 0
c50(0) -> 0
minus0(0, 0) -> 0
c60(0) -> 0
c70(0) -> 0
neg0(0) -> 0
c80(0) -> 0
div0(0, 0) -> 0
c90(0) -> 0
c100(0) -> 0
ln0(0) -> 0
c110(0) -> 0
exp0(0, 0) -> 0
c120(0) -> 0
c130(0) -> 0
DX0(0) -> 1
DX1(0) -> 2
c21(2) -> 1
DX1(0) -> 3
c31(3) -> 1
DX1(0) -> 4
c41(4) -> 1
DX1(0) -> 5
c51(5) -> 1
DX1(0) -> 6
c61(6) -> 1
DX1(0) -> 7
c71(7) -> 1
DX1(0) -> 8
c81(8) -> 1
DX1(0) -> 9
c91(9) -> 1
DX1(0) -> 10
c101(10) -> 1
DX1(0) -> 11
c111(11) -> 1
DX1(0) -> 12
c121(12) -> 1
DX1(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)