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

0 CpxTRS
    ↳1 CpxTrsMatchBoundsTAProof (⇔, 4 ms)
    ↳2 BOUNDS(1, n^1)
    ↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 21 ms)
    ↳4 CdtProblem
        ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳6 CdtProblem
        ↳7 CdtUsableRulesProof (⇔, 0 ms)
        ↳8 CdtProblem
        ↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 117 ms)
        ↳10 CdtProblem
        ↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 71 ms)
        ↳12 CdtProblem
        ↳13 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳14 BOUNDS(1, 1)

(0) 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:

concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
lessleaves(X, leaf) → false
lessleaves(leaf, cons(W, Z)) → true
lessleaves(cons(U, V), cons(W, Z)) → lessleaves(concat(U, V), concat(W, Z))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

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 2.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
leaf0() → 0
cons0(0, 0) → 0
false0() → 0
true0() → 0
concat0(0, 0) → 1
lessleaves0(0, 0) → 2
concat1(0, 0) → 3
cons1(0, 3) → 1
false1() → 2
true1() → 2
concat1(0, 0) → 4
concat1(0, 0) → 5
lessleaves1(4, 5) → 2
cons1(0, 3) → 3
cons1(0, 3) → 4
cons1(0, 3) → 5
concat1(0, 3) → 5
concat1(0, 3) → 4
concat2(0, 3) → 6
concat2(0, 3) → 7
lessleaves2(6, 7) → 2
concat1(0, 3) → 3
0 → 1
0 → 3
0 → 4
0 → 5
3 → 4
3 → 5
3 → 6
3 → 7

(2) BOUNDS(1, n^1)

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

concat(leaf, z0) → z0
concat(cons(z0, z1), z2) → cons(z0, concat(z1, z2))
lessleaves(z0, leaf) → false
lessleaves(leaf, cons(z0, z1)) → true
lessleaves(cons(z0, z1), cons(z2, z3)) → lessleaves(concat(z0, z1), concat(z2, z3))
Tuples:

CONCAT(leaf, z0) → c
CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
LESSLEAVES(z0, leaf) → c2
LESSLEAVES(leaf, cons(z0, z1)) → c3
LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
S tuples:

CONCAT(leaf, z0) → c
CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
LESSLEAVES(z0, leaf) → c2
LESSLEAVES(leaf, cons(z0, z1)) → c3
LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
K tuples:none
Defined Rule Symbols:

concat, lessleaves

Defined Pair Symbols:

CONCAT, LESSLEAVES

Compound Symbols:

c, c1, c2, c3, c4

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 3 trailing nodes:

LESSLEAVES(leaf, cons(z0, z1)) → c3
CONCAT(leaf, z0) → c
LESSLEAVES(z0, leaf) → c2

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

concat(leaf, z0) → z0
concat(cons(z0, z1), z2) → cons(z0, concat(z1, z2))
lessleaves(z0, leaf) → false
lessleaves(leaf, cons(z0, z1)) → true
lessleaves(cons(z0, z1), cons(z2, z3)) → lessleaves(concat(z0, z1), concat(z2, z3))
Tuples:

CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
S tuples:

CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
K tuples:none
Defined Rule Symbols:

concat, lessleaves

Defined Pair Symbols:

CONCAT, LESSLEAVES

Compound Symbols:

c1, c4

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

lessleaves(z0, leaf) → false
lessleaves(leaf, cons(z0, z1)) → true
lessleaves(cons(z0, z1), cons(z2, z3)) → lessleaves(concat(z0, z1), concat(z2, z3))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

concat(leaf, z0) → z0
concat(cons(z0, z1), z2) → cons(z0, concat(z1, z2))
Tuples:

CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
S tuples:

CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
K tuples:none
Defined Rule Symbols:

concat

Defined Pair Symbols:

CONCAT, LESSLEAVES

Compound Symbols:

c1, c4

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
We considered the (Usable) Rules:

concat(leaf, z0) → z0
concat(cons(z0, z1), z2) → cons(z0, concat(z1, z2))
And the Tuples:

CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x1, x2)) = 0   
POL(LESSLEAVES(x1, x2)) = x2   
POL(c1(x1)) = x1   
POL(c4(x1, x2, x3)) = x1 + x2 + x3   
POL(concat(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = [2] + x1 + x2   
POL(leaf) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

concat(leaf, z0) → z0
concat(cons(z0, z1), z2) → cons(z0, concat(z1, z2))
Tuples:

CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
S tuples:

CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
K tuples:

LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
Defined Rule Symbols:

concat

Defined Pair Symbols:

CONCAT, LESSLEAVES

Compound Symbols:

c1, c4

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
We considered the (Usable) Rules:

concat(leaf, z0) → z0
concat(cons(z0, z1), z2) → cons(z0, concat(z1, z2))
And the Tuples:

CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x1, x2)) = [2]x1 + x2   
POL(LESSLEAVES(x1, x2)) = x22 + x12   
POL(c1(x1)) = x1   
POL(c4(x1, x2, x3)) = x1 + x2 + x3   
POL(concat(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = [1] + x1 + x2   
POL(leaf) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

concat(leaf, z0) → z0
concat(cons(z0, z1), z2) → cons(z0, concat(z1, z2))
Tuples:

CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
S tuples:none
K tuples:

LESSLEAVES(cons(z0, z1), cons(z2, z3)) → c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1), CONCAT(z2, z3))
CONCAT(cons(z0, z1), z2) → c1(CONCAT(z1, z2))
Defined Rule Symbols:

concat

Defined Pair Symbols:

CONCAT, LESSLEAVES

Compound Symbols:

c1, c4

(13) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(14) BOUNDS(1, 1)