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

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

rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

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

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4]
transitions:
Cons0(0, 0) → 0
rev_l0() → 0
step_x_f0(0, 0, 0) → 0
fleft_op_e_xs_10() → 0
Nil0() → 0
rev_l#20(0, 0) → 1
step_x_f#10(0, 0, 0, 0) → 2
foldr#30(0) → 3
main0(0) → 4
Cons1(0, 0) → 1
rev_l#21(0, 0) → 5
step_x_f#11(0, 0, 0, 5) → 2
rev_l#21(0, 0) → 2
fleft_op_e_xs_11() → 3
rev_l1() → 6
foldr#31(0) → 7
step_x_f1(6, 0, 7) → 3
Nil1() → 4
rev_l1() → 8
foldr#31(0) → 9
Nil1() → 10
step_x_f#11(8, 0, 9, 10) → 4
Cons2(0, 0) → 2
Cons2(0, 0) → 5
rev_l#21(5, 0) → 5
rev_l#21(5, 0) → 2
fleft_op_e_xs_11() → 7
fleft_op_e_xs_11() → 9
step_x_f1(6, 0, 7) → 7
step_x_f1(6, 0, 7) → 9
Cons2(0, 5) → 2
Cons2(0, 5) → 5
rev_l#22(10, 0) → 11
step_x_f#12(6, 0, 7, 11) → 4
rev_l#22(10, 0) → 4
Cons3(0, 10) → 4
Cons3(0, 10) → 11
rev_l#22(11, 0) → 11
rev_l#22(11, 0) → 4
Cons3(0, 11) → 4
Cons3(0, 11) → 11

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

rev_l#2(z0, z1) → Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) → rev_l#2(z1, z0)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) → step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) → Nil
main(Cons(z0, z1)) → step_x_f#1(rev_l, z0, foldr#3(z1), Nil)
Tuples:

REV_L#2(z0, z1) → c
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) → c2(REV_L#2(z1, z0))
FOLDR#3(Nil) → c3
FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
MAIN(Nil) → c5
MAIN(Cons(z0, z1)) → c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
S tuples:

REV_L#2(z0, z1) → c
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) → c2(REV_L#2(z1, z0))
FOLDR#3(Nil) → c3
FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
MAIN(Nil) → c5
MAIN(Cons(z0, z1)) → c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
K tuples:none
Defined Rule Symbols:

rev_l#2, step_x_f#1, foldr#3, main

Defined Pair Symbols:

REV_L#2, STEP_X_F#1, FOLDR#3, MAIN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6

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

Removed 4 trailing nodes:

MAIN(Nil) → c5
REV_L#2(z0, z1) → c
STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) → c2(REV_L#2(z1, z0))
FOLDR#3(Nil) → c3

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

rev_l#2(z0, z1) → Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) → rev_l#2(z1, z0)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) → step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) → Nil
main(Cons(z0, z1)) → step_x_f#1(rev_l, z0, foldr#3(z1), Nil)
Tuples:

STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
MAIN(Cons(z0, z1)) → c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
S tuples:

STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
MAIN(Cons(z0, z1)) → c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
K tuples:none
Defined Rule Symbols:

rev_l#2, step_x_f#1, foldr#3, main

Defined Pair Symbols:

STEP_X_F#1, FOLDR#3, MAIN

Compound Symbols:

c1, c4, c6

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

Removed 1 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

rev_l#2(z0, z1) → Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) → rev_l#2(z1, z0)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) → step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) → Nil
main(Cons(z0, z1)) → step_x_f#1(rev_l, z0, foldr#3(z1), Nil)
Tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
MAIN(Cons(z0, z1)) → c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
S tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
MAIN(Cons(z0, z1)) → c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
K tuples:none
Defined Rule Symbols:

rev_l#2, step_x_f#1, foldr#3, main

Defined Pair Symbols:

FOLDR#3, MAIN, STEP_X_F#1

Compound Symbols:

c4, c6, c1

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

Split RHS of tuples not part of any SCC

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

rev_l#2(z0, z1) → Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) → rev_l#2(z1, z0)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) → step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) → Nil
main(Cons(z0, z1)) → step_x_f#1(rev_l, z0, foldr#3(z1), Nil)
Tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
MAIN(Cons(z0, z1)) → c(FOLDR#3(z1))
S tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
MAIN(Cons(z0, z1)) → c(FOLDR#3(z1))
K tuples:none
Defined Rule Symbols:

rev_l#2, step_x_f#1, foldr#3, main

Defined Pair Symbols:

FOLDR#3, STEP_X_F#1, MAIN

Compound Symbols:

c4, c1, c

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

MAIN(Cons(z0, z1)) → c(FOLDR#3(z1))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

rev_l#2(z0, z1) → Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) → rev_l#2(z1, z0)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) → step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) → Nil
main(Cons(z0, z1)) → step_x_f#1(rev_l, z0, foldr#3(z1), Nil)
Tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
S tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
K tuples:none
Defined Rule Symbols:

rev_l#2, step_x_f#1, foldr#3, main

Defined Pair Symbols:

FOLDR#3, STEP_X_F#1, MAIN

Compound Symbols:

c4, c1, c

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

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

MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

rev_l#2(z0, z1) → Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) → rev_l#2(z1, z0)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) → step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) → Nil
main(Cons(z0, z1)) → step_x_f#1(rev_l, z0, foldr#3(z1), Nil)
Tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
S tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
K tuples:

MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
Defined Rule Symbols:

rev_l#2, step_x_f#1, foldr#3, main

Defined Pair Symbols:

FOLDR#3, STEP_X_F#1, MAIN

Compound Symbols:

c4, c1, c

(15) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) → rev_l#2(z1, z0)
main(Nil) → Nil
main(Cons(z0, z1)) → step_x_f#1(rev_l, z0, foldr#3(z1), Nil)

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

rev_l#2(z0, z1) → Cons(z1, z0)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) → step_x_f(rev_l, z0, foldr#3(z1))
Tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
S tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
K tuples:

MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
Defined Rule Symbols:

rev_l#2, foldr#3

Defined Pair Symbols:

FOLDR#3, STEP_X_F#1, MAIN

Compound Symbols:

c4, c1, c

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

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
We considered the (Usable) Rules:none
And the Tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(Cons(x1, x2)) = [1] + x2   
POL(FOLDR#3(x1)) = x1   
POL(MAIN(x1)) = [1]   
POL(Nil) = 0   
POL(STEP_X_F#1(x1, x2, x3, x4)) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c4(x1)) = x1   
POL(fleft_op_e_xs_1) = 0   
POL(foldr#3(x1)) = 0   
POL(rev_l) = 0   
POL(rev_l#2(x1, x2)) = 0   
POL(step_x_f(x1, x2, x3)) = 0   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

rev_l#2(z0, z1) → Cons(z1, z0)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) → step_x_f(rev_l, z0, foldr#3(z1))
Tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
S tuples:

STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
K tuples:

MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
Defined Rule Symbols:

rev_l#2, foldr#3

Defined Pair Symbols:

FOLDR#3, STEP_X_F#1, MAIN

Compound Symbols:

c4, c1, c

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

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

STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
We considered the (Usable) Rules:

foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) → step_x_f(rev_l, z0, foldr#3(z1))
And the Tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(Cons(x1, x2)) = [1] + x1 + x2   
POL(FOLDR#3(x1)) = 0   
POL(MAIN(x1)) = [1] + x1   
POL(Nil) = 0   
POL(STEP_X_F#1(x1, x2, x3, x4)) = x1 + x2 + x3   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c4(x1)) = x1   
POL(fleft_op_e_xs_1) = 0   
POL(foldr#3(x1)) = x1   
POL(rev_l) = [1]   
POL(rev_l#2(x1, x2)) = 0   
POL(step_x_f(x1, x2, x3)) = x1 + x2 + x3   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

rev_l#2(z0, z1) → Cons(z1, z0)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) → step_x_f(rev_l, z0, foldr#3(z1))
Tuples:

FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
S tuples:none
K tuples:

MAIN(Cons(z0, z1)) → c(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil))
FOLDR#3(Cons(z0, z1)) → c4(FOLDR#3(z1))
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) → c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)))
Defined Rule Symbols:

rev_l#2, foldr#3

Defined Pair Symbols:

FOLDR#3, STEP_X_F#1, MAIN

Compound Symbols:

c4, c1, c

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

The set S is empty

(22) BOUNDS(1, 1)