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

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 363 ms)
    ↳4 CdtProblem
    ↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 8 ms)
    ↳12 CdtProblem
    ↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳22 CdtProblem
    ↳23 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳24 CdtProblem
    ↳25 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳26 CdtProblem
↳27 CpxTrsMatchBoundsTAProof (⇔, 164 ms)
↳28 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(y, z)))))

Rewrite Strategy: INNERMOST

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

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3

(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
We considered the (Usable) Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
And the Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(L(x1)) = 0   
POL(MAX(x1)) = [2]x12   
POL(N(x1, x2)) = [1] + x2   
POL(c2(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(max(x1)) = 0   
POL(s(x1)) = 0   

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3

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

Use narrowing to replace MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2))) by

MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))), MAX(N(L(0), L(z0))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(z0), N(z1, z2)))) → c3(MAX(N(L(x0), L(max(N(L(z0), L(max(N(z1, z2)))))))), MAX(N(L(z0), N(z1, z2))))
MAX(N(L(x0), N(x1, x2))) → c3

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))), MAX(N(L(0), L(z0))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(z0), N(z1, z2)))) → c3(MAX(N(L(x0), L(max(N(L(z0), L(max(N(z1, z2)))))))), MAX(N(L(z0), N(z1, z2))))
MAX(N(L(x0), N(x1, x2))) → c3
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3, c3

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

Removed 1 trailing nodes:

MAX(N(L(x0), N(x1, x2))) → c3

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))), MAX(N(L(0), L(z0))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(z0), N(z1, z2)))) → c3(MAX(N(L(x0), L(max(N(L(z0), L(max(N(z1, z2)))))))), MAX(N(L(z0), N(z1, z2))))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))), MAX(N(L(0), L(z0)))) by

MAX(N(L(x0), N(L(0), L(x1)))) → c3(MAX(N(L(x0), L(x1))))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(z0), N(z1, z2)))) → c3(MAX(N(L(x0), L(max(N(L(z0), L(max(N(z1, z2)))))))), MAX(N(L(z0), N(z1, z2))))
MAX(N(L(x0), N(L(0), L(x1)))) → c3(MAX(N(L(x0), L(x1))))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3, c3

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MAX(N(L(x0), N(L(z0), N(z1, z2)))) → c3(MAX(N(L(x0), L(max(N(L(z0), L(max(N(z1, z2)))))))), MAX(N(L(z0), N(z1, z2)))) by

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(x2, x3)))) → c3

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(0), L(x1)))) → c3(MAX(N(L(x0), L(x1))))
MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(x2, x3)))) → c3
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3, c3, c3

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

Removed 1 trailing nodes:

MAX(N(L(x0), N(L(x1), N(x2, x3)))) → c3

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(0), L(x1)))) → c3(MAX(N(L(x0), L(x1))))
MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3, c3

(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1)))) by

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(0), L(x1)))) → c3(MAX(N(L(x0), L(x1))))
MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
S tuples:

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c3, c2

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1))))) by

MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c3(MAX(N(L(x0), L(s(z0)))), MAX(N(L(s(0)), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c3(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))), MAX(N(L(s(s(z0))), L(s(s(z1))))))
MAX(N(L(x0), N(L(s(x1)), L(s(x2))))) → c3

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), L(x1)))) → c3(MAX(N(L(x0), L(x1))))
MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c3(MAX(N(L(x0), L(s(z0)))), MAX(N(L(s(0)), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c3(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))), MAX(N(L(s(s(z0))), L(s(s(z1))))))
MAX(N(L(x0), N(L(s(x1)), L(s(x2))))) → c3
S tuples:

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c3, c2, c3

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

Removed 1 trailing nodes:

MAX(N(L(x0), N(L(s(x1)), L(s(x2))))) → c3

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), L(x1)))) → c3(MAX(N(L(x0), L(x1))))
MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c3(MAX(N(L(x0), L(s(z0)))), MAX(N(L(s(0)), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c3(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))), MAX(N(L(s(s(z0))), L(s(s(z1))))))
S tuples:

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c3, c2

(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(x0), N(L(0), L(x1)))) → c3(MAX(N(L(x0), L(x1)))) by

MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c3(MAX(N(L(x0), L(s(z0)))), MAX(N(L(s(0)), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c3(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))), MAX(N(L(s(s(z0))), L(s(s(z1))))))
MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))
S tuples:

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c2, c3

(23) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1))))) by

MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c3(MAX(N(L(x0), L(s(z0)))), MAX(N(L(s(0)), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c3(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))), MAX(N(L(s(s(z0))), L(s(s(z1))))))
MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
S tuples:

MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c3, c2

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c3(MAX(N(L(x0), L(s(z0)))), MAX(N(L(s(0)), L(s(z0))))) by

MAX(N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1))))))) → c3(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))), MAX(N(L(s(0)), L(s(s(s(y1)))))))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c3(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))), MAX(N(L(s(s(z0))), L(s(s(z1))))))
MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1))))))) → c3(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))), MAX(N(L(s(0)), L(s(s(s(y1)))))))
S tuples:

MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c3, c2

(27) 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 1.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
L0(0) → 0
N0(0, 0) → 0
00() → 0
s0(0) → 0
max0(0) → 1
L1(0) → 4
L1(0) → 5
N1(4, 5) → 3
max1(3) → 2
s1(2) → 1
N1(0, 0) → 8
max1(8) → 7
L1(7) → 6
N1(4, 6) → 3
max1(3) → 1
s1(2) → 7
max1(3) → 7
L1(2) → 5
0 → 1
0 → 7
0 → 2
7 → 1
7 → 2
2 → 1
2 → 7

(28) BOUNDS(O(1), O(n^1))