WORST_CASE(?,O(n^1))
proof of input_TuiVMzWp8J.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) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 50 ms]
(8) CdtProblem
(9) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) 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:

   f(g(x)) -> f(a(g(g(f(x))), g(f(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:
   f(g(z0)) -> f(a(g(g(f(z0))), g(f(z0))))
Tuples:
   F(g(z0)) -> c(F(a(g(g(f(z0))), g(f(z0)))), F(z0))
   F(g(z0)) -> c1(F(a(g(g(f(z0))), g(f(z0)))), F(z0))
S tuples:
   F(g(z0)) -> c(F(a(g(g(f(z0))), g(f(z0)))), F(z0))
   F(g(z0)) -> c1(F(a(g(g(f(z0))), g(f(z0)))), F(z0))
K tuples:none
Defined Rule Symbols:   f_1

Defined Pair Symbols:   F_1

Compound Symbols:   c_2, c1_2


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

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing tuple parts
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(g(z0)) -> f(a(g(g(f(z0))), g(f(z0))))
Tuples:
   F(g(z0)) -> c(F(z0))
   F(g(z0)) -> c1(F(z0))
S tuples:
   F(g(z0)) -> c(F(z0))
   F(g(z0)) -> c1(F(z0))
K tuples:none
Defined Rule Symbols:   f_1

Defined Pair Symbols:   F_1

Compound Symbols:   c_1, c1_1


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

(5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   f(g(z0)) -> f(a(g(g(f(z0))), g(f(z0))))

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F(g(z0)) -> c(F(z0))
   F(g(z0)) -> c1(F(z0))
S tuples:
   F(g(z0)) -> c(F(z0))
   F(g(z0)) -> c1(F(z0))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   F_1

Compound Symbols:   c_1, c1_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.
   F(g(z0)) -> c(F(z0))
   F(g(z0)) -> c1(F(z0))
We considered the (Usable) Rules:none
And the Tuples:
   F(g(z0)) -> c(F(z0))
   F(g(z0)) -> c1(F(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(F(x_1)) = x_1
   POL(c(x_1)) = x_1
   POL(c1(x_1)) = x_1
   POL(g(x_1)) = [1] + x_1

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F(g(z0)) -> c(F(z0))
   F(g(z0)) -> c1(F(z0))
S tuples:none
K tuples:
   F(g(z0)) -> c(F(z0))
   F(g(z0)) -> c1(F(z0))
Defined Rule Symbols:none

Defined Pair Symbols:   F_1

Compound Symbols:   c_1, c1_1


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

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

(10)
BOUNDS(1, 1)