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

0 CpxTRS
    ↳1 CpxTrsMatchBoundsTAProof (⇔, 12 ms)
    ↳2 BOUNDS(1, n^1)
    ↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
        ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳6 CdtProblem
        ↳7 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳8 CdtProblem
        ↳9 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
        ↳10 CdtProblem
        ↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳12 CdtProblem
        ↳13 CdtUsableRulesProof (⇔, 0 ms)
        ↳14 CdtProblem
        ↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 74 ms)
        ↳16 CdtProblem
        ↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 20 ms)
        ↳18 CdtProblem
        ↳19 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳20 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:

compS_f#1(compS_f(x2), x1) → compS_f#1(x2, S(x1))
compS_f#1(id, x3) → S(x3)
iter#3(0) → id
iter#3(S(x6)) → compS_f(iter#3(x6))
main(0) → 0
main(S(x9)) → compS_f#1(iter#3(x9), 0)

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, 3]
transitions:
compS_f0(0) → 0
S0(0) → 0
id0() → 0
00() → 0
compS_f#10(0, 0) → 1
iter#30(0) → 2
main0(0) → 3
S1(0) → 4
compS_f#11(0, 4) → 1
S1(0) → 1
id1() → 2
iter#31(0) → 5
compS_f1(5) → 2
01() → 3
iter#31(0) → 6
01() → 7
compS_f#11(6, 7) → 3
S1(4) → 4
S1(4) → 1
id1() → 5
id1() → 6
compS_f1(5) → 5
compS_f1(5) → 6
S2(7) → 8
compS_f#12(5, 8) → 3
S2(7) → 3
S2(8) → 8
S2(8) → 3

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

compS_f#1(compS_f(z0), z1) → compS_f#1(z0, S(z1))
compS_f#1(id, z0) → S(z0)
iter#3(0) → id
iter#3(S(z0)) → compS_f(iter#3(z0))
main(0) → 0
main(S(z0)) → compS_f#1(iter#3(z0), 0)
Tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
COMPS_F#1(id, z0) → c1
ITER#3(0) → c2
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(0) → c4
MAIN(S(z0)) → c5(COMPS_F#1(iter#3(z0), 0), ITER#3(z0))
S tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
COMPS_F#1(id, z0) → c1
ITER#3(0) → c2
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(0) → c4
MAIN(S(z0)) → c5(COMPS_F#1(iter#3(z0), 0), ITER#3(z0))
K tuples:none
Defined Rule Symbols:

compS_f#1, iter#3, main

Defined Pair Symbols:

COMPS_F#1, ITER#3, MAIN

Compound Symbols:

c, c1, c2, c3, c4, c5

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

Removed 3 trailing nodes:

MAIN(0) → c4
ITER#3(0) → c2
COMPS_F#1(id, z0) → c1

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

compS_f#1(compS_f(z0), z1) → compS_f#1(z0, S(z1))
compS_f#1(id, z0) → S(z0)
iter#3(0) → id
iter#3(S(z0)) → compS_f(iter#3(z0))
main(0) → 0
main(S(z0)) → compS_f#1(iter#3(z0), 0)
Tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c5(COMPS_F#1(iter#3(z0), 0), ITER#3(z0))
S tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c5(COMPS_F#1(iter#3(z0), 0), ITER#3(z0))
K tuples:none
Defined Rule Symbols:

compS_f#1, iter#3, main

Defined Pair Symbols:

COMPS_F#1, ITER#3, MAIN

Compound Symbols:

c, c3, c5

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

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

compS_f#1(compS_f(z0), z1) → compS_f#1(z0, S(z1))
compS_f#1(id, z0) → S(z0)
iter#3(0) → id
iter#3(S(z0)) → compS_f(iter#3(z0))
main(0) → 0
main(S(z0)) → compS_f#1(iter#3(z0), 0)
Tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
MAIN(S(z0)) → c1(ITER#3(z0))
S tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
MAIN(S(z0)) → c1(ITER#3(z0))
K tuples:none
Defined Rule Symbols:

compS_f#1, iter#3, main

Defined Pair Symbols:

COMPS_F#1, ITER#3, MAIN

Compound Symbols:

c, c3, c1

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

MAIN(S(z0)) → c1(ITER#3(z0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

compS_f#1(compS_f(z0), z1) → compS_f#1(z0, S(z1))
compS_f#1(id, z0) → S(z0)
iter#3(0) → id
iter#3(S(z0)) → compS_f(iter#3(z0))
main(0) → 0
main(S(z0)) → compS_f#1(iter#3(z0), 0)
Tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
S tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
K tuples:none
Defined Rule Symbols:

compS_f#1, iter#3, main

Defined Pair Symbols:

COMPS_F#1, ITER#3, MAIN

Compound Symbols:

c, c3, c1

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

The following tuples could be moved from S to K by knowledge propagation:

MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

compS_f#1(compS_f(z0), z1) → compS_f#1(z0, S(z1))
compS_f#1(id, z0) → S(z0)
iter#3(0) → id
iter#3(S(z0)) → compS_f(iter#3(z0))
main(0) → 0
main(S(z0)) → compS_f#1(iter#3(z0), 0)
Tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
S tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
K tuples:

MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
Defined Rule Symbols:

compS_f#1, iter#3, main

Defined Pair Symbols:

COMPS_F#1, ITER#3, MAIN

Compound Symbols:

c, c3, c1

(13) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

compS_f#1(compS_f(z0), z1) → compS_f#1(z0, S(z1))
compS_f#1(id, z0) → S(z0)
main(0) → 0
main(S(z0)) → compS_f#1(iter#3(z0), 0)

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

iter#3(0) → id
iter#3(S(z0)) → compS_f(iter#3(z0))
Tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
S tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
K tuples:

MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
Defined Rule Symbols:

iter#3

Defined Pair Symbols:

COMPS_F#1, ITER#3, MAIN

Compound Symbols:

c, c3, c1

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

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

ITER#3(S(z0)) → c3(ITER#3(z0))
We considered the (Usable) Rules:none
And the Tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [3]   
POL(COMPS_F#1(x1, x2)) = [3]   
POL(ITER#3(x1)) = [2]x1   
POL(MAIN(x1)) = [2] + [2]x1   
POL(S(x1)) = [3] + x1   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c3(x1)) = x1   
POL(compS_f(x1)) = [3]   
POL(id) = [2]   
POL(iter#3(x1)) = [2] + [2]x1   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

iter#3(0) → id
iter#3(S(z0)) → compS_f(iter#3(z0))
Tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
S tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
K tuples:

MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
ITER#3(S(z0)) → c3(ITER#3(z0))
Defined Rule Symbols:

iter#3

Defined Pair Symbols:

COMPS_F#1, ITER#3, MAIN

Compound Symbols:

c, c3, c1

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

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

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
We considered the (Usable) Rules:

iter#3(S(z0)) → compS_f(iter#3(z0))
iter#3(0) → id
And the Tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]   
POL(COMPS_F#1(x1, x2)) = [1] + x1   
POL(ITER#3(x1)) = 0   
POL(MAIN(x1)) = [1] + x1   
POL(S(x1)) = [1] + x1   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c3(x1)) = x1   
POL(compS_f(x1)) = [1] + x1   
POL(id) = 0   
POL(iter#3(x1)) = x1   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

iter#3(0) → id
iter#3(S(z0)) → compS_f(iter#3(z0))
Tuples:

COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
ITER#3(S(z0)) → c3(ITER#3(z0))
MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
S tuples:none
K tuples:

MAIN(S(z0)) → c1(COMPS_F#1(iter#3(z0), 0))
ITER#3(S(z0)) → c3(ITER#3(z0))
COMPS_F#1(compS_f(z0), z1) → c(COMPS_F#1(z0, S(z1)))
Defined Rule Symbols:

iter#3

Defined Pair Symbols:

COMPS_F#1, ITER#3, MAIN

Compound Symbols:

c, c3, c1

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

The set S is empty

(20) BOUNDS(1, 1)