WORST_CASE(Omega(n^1),O(n^1))
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 276 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (6) CdtProblem
    (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 25 ms]
    (10) CdtProblem
    (11) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) BOUNDS(1, 1)
(13) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxRelTRS
    (15) SlicingProof [LOWER BOUND(ID), 0 ms]
    (16) CpxRelTRS
    (17) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) typed CpxTrs
    (19) OrderProof [LOWER BOUND(ID), 5 ms]
    (20) typed CpxTrs
    (21) RewriteLemmaProof [LOWER BOUND(ID), 272 ms]
    (22) BEST
        (23) proven lower bound
            (24) LowerBoundPropagationProof [FINISHED, 0 ms]
            (25) BOUNDS(n^1, INF)
        (26) typed CpxTrs
            (27) RewriteLemmaProof [LOWER BOUND(ID), 53 ms]
            (28) typed CpxTrs
            (29) RewriteLemmaProof [LOWER BOUND(ID), 37 ms]
            (30) typed CpxTrs
            (31) RewriteLemmaProof [LOWER BOUND(ID), 37 ms]
            (32) BOUNDS(1, INF)


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

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   PLUS_X#1(0, z0) -> c
   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Nil) -> c2
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
   MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))

The (relative) TRS S consists of the following rules:

   plus_x#1(0, z0) -> z0
   plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
   map#2(plus_x(z0), Nil) -> Nil
   map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
   main(z0, z1) -> map#2(plus_x(z1), z0)

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   PLUS_X#1(0, z0) -> c
   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Nil) -> c2
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
   MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))

The (relative) TRS S consists of the following rules:

   plus_x#1(0, z0) -> z0
   plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
   map#2(plus_x(z0), Nil) -> Nil
   map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
   main(z0, z1) -> map#2(plus_x(z1), z0)

Rewrite Strategy: INNERMOST
----------------------------------------

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   plus_x#1(0, z0) -> z0
   plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
   map#2(plus_x(z0), Nil) -> Nil
   map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
   main(z0, z1) -> map#2(plus_x(z1), z0)
   PLUS_X#1(0, z0) -> c
   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Nil) -> c2
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
   MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))
Tuples:
   PLUS_X#1'(0, z0) -> c6
   PLUS_X#1'(S(z0), z1) -> c7(PLUS_X#1'(z0, z1))
   MAP#2'(plus_x(z0), Nil) -> c8
   MAP#2'(plus_x(z0), Cons(z1, z2)) -> c9(PLUS_X#1'(z0, z1), MAP#2'(plus_x(z0), z2))
   MAIN'(z0, z1) -> c10(MAP#2'(plus_x(z1), z0))
   PLUS_X#1''(0, z0) -> c11
   PLUS_X#1''(S(z0), z1) -> c12(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Nil) -> c13
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c14(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c15(MAP#2''(plus_x(z0), z2))
   MAIN''(z0, z1) -> c16(MAP#2''(plus_x(z1), z0))
S tuples:
   PLUS_X#1''(0, z0) -> c11
   PLUS_X#1''(S(z0), z1) -> c12(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Nil) -> c13
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c14(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c15(MAP#2''(plus_x(z0), z2))
   MAIN''(z0, z1) -> c16(MAP#2''(plus_x(z1), z0))
K tuples:none
Defined Rule Symbols:   PLUS_X#1_2, MAP#2_2, MAIN_2, plus_x#1_2, map#2_2, main_2

Defined Pair Symbols:   PLUS_X#1'_2, MAP#2'_2, MAIN'_2, PLUS_X#1''_2, MAP#2''_2, MAIN''_2

Compound Symbols:   c6, c7_1, c8, c9_2, c10_1, c11, c12_1, c13, c14_1, c15_1, c16_1


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

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 2 leading nodes:
   MAIN'(z0, z1) -> c10(MAP#2'(plus_x(z1), z0))
   MAIN''(z0, z1) -> c16(MAP#2''(plus_x(z1), z0))
Removed 4 trailing nodes:
   PLUS_X#1''(0, z0) -> c11
   PLUS_X#1'(0, z0) -> c6
   MAP#2''(plus_x(z0), Nil) -> c13
   MAP#2'(plus_x(z0), Nil) -> c8

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   plus_x#1(0, z0) -> z0
   plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
   map#2(plus_x(z0), Nil) -> Nil
   map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
   main(z0, z1) -> map#2(plus_x(z1), z0)
   PLUS_X#1(0, z0) -> c
   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Nil) -> c2
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
   MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))
Tuples:
   PLUS_X#1'(S(z0), z1) -> c7(PLUS_X#1'(z0, z1))
   MAP#2'(plus_x(z0), Cons(z1, z2)) -> c9(PLUS_X#1'(z0, z1), MAP#2'(plus_x(z0), z2))
   PLUS_X#1''(S(z0), z1) -> c12(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c14(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c15(MAP#2''(plus_x(z0), z2))
S tuples:
   PLUS_X#1''(S(z0), z1) -> c12(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c14(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c15(MAP#2''(plus_x(z0), z2))
K tuples:none
Defined Rule Symbols:   PLUS_X#1_2, MAP#2_2, MAIN_2, plus_x#1_2, map#2_2, main_2

Defined Pair Symbols:   PLUS_X#1'_2, MAP#2'_2, PLUS_X#1''_2, MAP#2''_2

Compound Symbols:   c7_1, c9_2, c12_1, c14_1, c15_1


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

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   plus_x#1(0, z0) -> z0
   plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
   map#2(plus_x(z0), Nil) -> Nil
   map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
   main(z0, z1) -> map#2(plus_x(z1), z0)
   PLUS_X#1(0, z0) -> c
   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Nil) -> c2
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
   MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   PLUS_X#1'(S(z0), z1) -> c7(PLUS_X#1'(z0, z1))
   MAP#2'(plus_x(z0), Cons(z1, z2)) -> c9(PLUS_X#1'(z0, z1), MAP#2'(plus_x(z0), z2))
   PLUS_X#1''(S(z0), z1) -> c12(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c14(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c15(MAP#2''(plus_x(z0), z2))
S tuples:
   PLUS_X#1''(S(z0), z1) -> c12(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c14(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c15(MAP#2''(plus_x(z0), z2))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   PLUS_X#1'_2, MAP#2'_2, PLUS_X#1''_2, MAP#2''_2

Compound Symbols:   c7_1, c9_2, c12_1, c14_1, c15_1


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

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   PLUS_X#1''(S(z0), z1) -> c12(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c14(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c15(MAP#2''(plus_x(z0), z2))
We considered the (Usable) Rules:none
And the Tuples:
   PLUS_X#1'(S(z0), z1) -> c7(PLUS_X#1'(z0, z1))
   MAP#2'(plus_x(z0), Cons(z1, z2)) -> c9(PLUS_X#1'(z0, z1), MAP#2'(plus_x(z0), z2))
   PLUS_X#1''(S(z0), z1) -> c12(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c14(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c15(MAP#2''(plus_x(z0), z2))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(Cons(x_1, x_2)) = [1] + x_1 + x_2
   POL(MAP#2'(x_1, x_2)) = [3]x_2
   POL(MAP#2''(x_1, x_2)) = [1] + [2]x_1 + [3]x_2
   POL(PLUS_X#1'(x_1, x_2)) = [3] + [3]x_2
   POL(PLUS_X#1''(x_1, x_2)) = x_1 + [2]x_2
   POL(S(x_1)) = [3] + x_1
   POL(c12(x_1)) = x_1
   POL(c14(x_1)) = x_1
   POL(c15(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c9(x_1, x_2)) = x_1 + x_2
   POL(plus_x(x_1)) = [3] + x_1

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   PLUS_X#1'(S(z0), z1) -> c7(PLUS_X#1'(z0, z1))
   MAP#2'(plus_x(z0), Cons(z1, z2)) -> c9(PLUS_X#1'(z0, z1), MAP#2'(plus_x(z0), z2))
   PLUS_X#1''(S(z0), z1) -> c12(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c14(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c15(MAP#2''(plus_x(z0), z2))
S tuples:none
K tuples:
   PLUS_X#1''(S(z0), z1) -> c12(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c14(PLUS_X#1''(z0, z1))
   MAP#2''(plus_x(z0), Cons(z1, z2)) -> c15(MAP#2''(plus_x(z0), z2))
Defined Rule Symbols:none

Defined Pair Symbols:   PLUS_X#1'_2, MAP#2'_2, PLUS_X#1''_2, MAP#2''_2

Compound Symbols:   c7_1, c9_2, c12_1, c14_1, c15_1


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

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

(12)
BOUNDS(1, 1)

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

(13) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(14)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   PLUS_X#1(0', z0) -> c
   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Nil) -> c2
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1))
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
   MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))

The (relative) TRS S consists of the following rules:

   plus_x#1(0', z0) -> z0
   plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
   map#2(plus_x(z0), Nil) -> Nil
   map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
   main(z0, z1) -> map#2(plus_x(z1), z0)

Rewrite Strategy: INNERMOST
----------------------------------------

(15) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
PLUS_X#1/1

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

(16)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   PLUS_X#1(0') -> c
   PLUS_X#1(S(z0)) -> c1(PLUS_X#1(z0))
   MAP#2(plus_x(z0), Nil) -> c2
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0))
   MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
   MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))

The (relative) TRS S consists of the following rules:

   plus_x#1(0', z0) -> z0
   plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
   map#2(plus_x(z0), Nil) -> Nil
   map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
   main(z0, z1) -> map#2(plus_x(z1), z0)

Rewrite Strategy: INNERMOST
----------------------------------------

(17) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
PLUS_X#1(0') -> c
PLUS_X#1(S(z0)) -> c1(PLUS_X#1(z0))
MAP#2(plus_x(z0), Nil) -> c2
MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0))
MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))
plus_x#1(0', z0) -> z0
plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
map#2(plus_x(z0), Nil) -> Nil
map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
main(z0, z1) -> map#2(plus_x(z1), z0)

Types:
PLUS_X#1 :: 0':S -> c:c1
0' :: 0':S
c :: c:c1
S :: 0':S -> 0':S
c1 :: c:c1 -> c:c1
MAP#2 :: plus_x -> Nil:Cons -> c2:c3:c4
plus_x :: 0':S -> plus_x
Nil :: Nil:Cons
c2 :: c2:c3:c4
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
MAIN :: Nil:Cons -> 0':S -> c5
c5 :: c2:c3:c4 -> c5
plus_x#1 :: 0':S -> 0':S -> 0':S
map#2 :: plus_x -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> 0':S -> Nil:Cons
hole_c:c11_6 :: c:c1
hole_0':S2_6 :: 0':S
hole_c2:c3:c43_6 :: c2:c3:c4
hole_plus_x4_6 :: plus_x
hole_Nil:Cons5_6 :: Nil:Cons
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_0':S8_6 :: Nat -> 0':S
gen_c2:c3:c49_6 :: Nat -> c2:c3:c4
gen_Nil:Cons10_6 :: Nat -> Nil:Cons

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

(19) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
PLUS_X#1, MAP#2, plus_x#1, map#2

They will be analysed ascendingly in the following order:
PLUS_X#1 < MAP#2
plus_x#1 < map#2

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

(20)
Obligation:
Innermost TRS:
Rules:
PLUS_X#1(0') -> c
PLUS_X#1(S(z0)) -> c1(PLUS_X#1(z0))
MAP#2(plus_x(z0), Nil) -> c2
MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0))
MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))
plus_x#1(0', z0) -> z0
plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
map#2(plus_x(z0), Nil) -> Nil
map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
main(z0, z1) -> map#2(plus_x(z1), z0)

Types:
PLUS_X#1 :: 0':S -> c:c1
0' :: 0':S
c :: c:c1
S :: 0':S -> 0':S
c1 :: c:c1 -> c:c1
MAP#2 :: plus_x -> Nil:Cons -> c2:c3:c4
plus_x :: 0':S -> plus_x
Nil :: Nil:Cons
c2 :: c2:c3:c4
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
MAIN :: Nil:Cons -> 0':S -> c5
c5 :: c2:c3:c4 -> c5
plus_x#1 :: 0':S -> 0':S -> 0':S
map#2 :: plus_x -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> 0':S -> Nil:Cons
hole_c:c11_6 :: c:c1
hole_0':S2_6 :: 0':S
hole_c2:c3:c43_6 :: c2:c3:c4
hole_plus_x4_6 :: plus_x
hole_Nil:Cons5_6 :: Nil:Cons
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_0':S8_6 :: Nat -> 0':S
gen_c2:c3:c49_6 :: Nat -> c2:c3:c4
gen_Nil:Cons10_6 :: Nat -> Nil:Cons


Generator Equations:
gen_c:c17_6(0) <=> c
gen_c:c17_6(+(x, 1)) <=> c1(gen_c:c17_6(x))
gen_0':S8_6(0) <=> 0'
gen_0':S8_6(+(x, 1)) <=> S(gen_0':S8_6(x))
gen_c2:c3:c49_6(0) <=> c2
gen_c2:c3:c49_6(+(x, 1)) <=> c4(gen_c2:c3:c49_6(x))
gen_Nil:Cons10_6(0) <=> Nil
gen_Nil:Cons10_6(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_6(x))


The following defined symbols remain to be analysed:
PLUS_X#1, MAP#2, plus_x#1, map#2

They will be analysed ascendingly in the following order:
PLUS_X#1 < MAP#2
plus_x#1 < map#2

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS_X#1(gen_0':S8_6(n12_6)) -> gen_c:c17_6(n12_6), rt in Omega(1 + n12_6)

Induction Base:
PLUS_X#1(gen_0':S8_6(0)) ->_R^Omega(1)
c

Induction Step:
PLUS_X#1(gen_0':S8_6(+(n12_6, 1))) ->_R^Omega(1)
c1(PLUS_X#1(gen_0':S8_6(n12_6))) ->_IH
c1(gen_c:c17_6(c13_6))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(22)
Complex Obligation (BEST)

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

(23)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
PLUS_X#1(0') -> c
PLUS_X#1(S(z0)) -> c1(PLUS_X#1(z0))
MAP#2(plus_x(z0), Nil) -> c2
MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0))
MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))
plus_x#1(0', z0) -> z0
plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
map#2(plus_x(z0), Nil) -> Nil
map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
main(z0, z1) -> map#2(plus_x(z1), z0)

Types:
PLUS_X#1 :: 0':S -> c:c1
0' :: 0':S
c :: c:c1
S :: 0':S -> 0':S
c1 :: c:c1 -> c:c1
MAP#2 :: plus_x -> Nil:Cons -> c2:c3:c4
plus_x :: 0':S -> plus_x
Nil :: Nil:Cons
c2 :: c2:c3:c4
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
MAIN :: Nil:Cons -> 0':S -> c5
c5 :: c2:c3:c4 -> c5
plus_x#1 :: 0':S -> 0':S -> 0':S
map#2 :: plus_x -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> 0':S -> Nil:Cons
hole_c:c11_6 :: c:c1
hole_0':S2_6 :: 0':S
hole_c2:c3:c43_6 :: c2:c3:c4
hole_plus_x4_6 :: plus_x
hole_Nil:Cons5_6 :: Nil:Cons
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_0':S8_6 :: Nat -> 0':S
gen_c2:c3:c49_6 :: Nat -> c2:c3:c4
gen_Nil:Cons10_6 :: Nat -> Nil:Cons


Generator Equations:
gen_c:c17_6(0) <=> c
gen_c:c17_6(+(x, 1)) <=> c1(gen_c:c17_6(x))
gen_0':S8_6(0) <=> 0'
gen_0':S8_6(+(x, 1)) <=> S(gen_0':S8_6(x))
gen_c2:c3:c49_6(0) <=> c2
gen_c2:c3:c49_6(+(x, 1)) <=> c4(gen_c2:c3:c49_6(x))
gen_Nil:Cons10_6(0) <=> Nil
gen_Nil:Cons10_6(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_6(x))


The following defined symbols remain to be analysed:
PLUS_X#1, MAP#2, plus_x#1, map#2

They will be analysed ascendingly in the following order:
PLUS_X#1 < MAP#2
plus_x#1 < map#2

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

(24) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(25)
BOUNDS(n^1, INF)

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

(26)
Obligation:
Innermost TRS:
Rules:
PLUS_X#1(0') -> c
PLUS_X#1(S(z0)) -> c1(PLUS_X#1(z0))
MAP#2(plus_x(z0), Nil) -> c2
MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0))
MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))
plus_x#1(0', z0) -> z0
plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
map#2(plus_x(z0), Nil) -> Nil
map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
main(z0, z1) -> map#2(plus_x(z1), z0)

Types:
PLUS_X#1 :: 0':S -> c:c1
0' :: 0':S
c :: c:c1
S :: 0':S -> 0':S
c1 :: c:c1 -> c:c1
MAP#2 :: plus_x -> Nil:Cons -> c2:c3:c4
plus_x :: 0':S -> plus_x
Nil :: Nil:Cons
c2 :: c2:c3:c4
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
MAIN :: Nil:Cons -> 0':S -> c5
c5 :: c2:c3:c4 -> c5
plus_x#1 :: 0':S -> 0':S -> 0':S
map#2 :: plus_x -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> 0':S -> Nil:Cons
hole_c:c11_6 :: c:c1
hole_0':S2_6 :: 0':S
hole_c2:c3:c43_6 :: c2:c3:c4
hole_plus_x4_6 :: plus_x
hole_Nil:Cons5_6 :: Nil:Cons
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_0':S8_6 :: Nat -> 0':S
gen_c2:c3:c49_6 :: Nat -> c2:c3:c4
gen_Nil:Cons10_6 :: Nat -> Nil:Cons


Lemmas:
PLUS_X#1(gen_0':S8_6(n12_6)) -> gen_c:c17_6(n12_6), rt in Omega(1 + n12_6)


Generator Equations:
gen_c:c17_6(0) <=> c
gen_c:c17_6(+(x, 1)) <=> c1(gen_c:c17_6(x))
gen_0':S8_6(0) <=> 0'
gen_0':S8_6(+(x, 1)) <=> S(gen_0':S8_6(x))
gen_c2:c3:c49_6(0) <=> c2
gen_c2:c3:c49_6(+(x, 1)) <=> c4(gen_c2:c3:c49_6(x))
gen_Nil:Cons10_6(0) <=> Nil
gen_Nil:Cons10_6(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_6(x))


The following defined symbols remain to be analysed:
MAP#2, plus_x#1, map#2

They will be analysed ascendingly in the following order:
plus_x#1 < map#2

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MAP#2(plus_x(0'), gen_Nil:Cons10_6(n234_6)) -> gen_c2:c3:c49_6(n234_6), rt in Omega(1 + n234_6)

Induction Base:
MAP#2(plus_x(0'), gen_Nil:Cons10_6(0)) ->_R^Omega(1)
c2

Induction Step:
MAP#2(plus_x(0'), gen_Nil:Cons10_6(+(n234_6, 1))) ->_R^Omega(1)
c4(MAP#2(plus_x(0'), gen_Nil:Cons10_6(n234_6))) ->_IH
c4(gen_c2:c3:c49_6(c235_6))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(28)
Obligation:
Innermost TRS:
Rules:
PLUS_X#1(0') -> c
PLUS_X#1(S(z0)) -> c1(PLUS_X#1(z0))
MAP#2(plus_x(z0), Nil) -> c2
MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0))
MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))
plus_x#1(0', z0) -> z0
plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
map#2(plus_x(z0), Nil) -> Nil
map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
main(z0, z1) -> map#2(plus_x(z1), z0)

Types:
PLUS_X#1 :: 0':S -> c:c1
0' :: 0':S
c :: c:c1
S :: 0':S -> 0':S
c1 :: c:c1 -> c:c1
MAP#2 :: plus_x -> Nil:Cons -> c2:c3:c4
plus_x :: 0':S -> plus_x
Nil :: Nil:Cons
c2 :: c2:c3:c4
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
MAIN :: Nil:Cons -> 0':S -> c5
c5 :: c2:c3:c4 -> c5
plus_x#1 :: 0':S -> 0':S -> 0':S
map#2 :: plus_x -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> 0':S -> Nil:Cons
hole_c:c11_6 :: c:c1
hole_0':S2_6 :: 0':S
hole_c2:c3:c43_6 :: c2:c3:c4
hole_plus_x4_6 :: plus_x
hole_Nil:Cons5_6 :: Nil:Cons
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_0':S8_6 :: Nat -> 0':S
gen_c2:c3:c49_6 :: Nat -> c2:c3:c4
gen_Nil:Cons10_6 :: Nat -> Nil:Cons


Lemmas:
PLUS_X#1(gen_0':S8_6(n12_6)) -> gen_c:c17_6(n12_6), rt in Omega(1 + n12_6)
MAP#2(plus_x(0'), gen_Nil:Cons10_6(n234_6)) -> gen_c2:c3:c49_6(n234_6), rt in Omega(1 + n234_6)


Generator Equations:
gen_c:c17_6(0) <=> c
gen_c:c17_6(+(x, 1)) <=> c1(gen_c:c17_6(x))
gen_0':S8_6(0) <=> 0'
gen_0':S8_6(+(x, 1)) <=> S(gen_0':S8_6(x))
gen_c2:c3:c49_6(0) <=> c2
gen_c2:c3:c49_6(+(x, 1)) <=> c4(gen_c2:c3:c49_6(x))
gen_Nil:Cons10_6(0) <=> Nil
gen_Nil:Cons10_6(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_6(x))


The following defined symbols remain to be analysed:
plus_x#1, map#2

They will be analysed ascendingly in the following order:
plus_x#1 < map#2

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus_x#1(gen_0':S8_6(n748_6), gen_0':S8_6(b)) -> gen_0':S8_6(+(n748_6, b)), rt in Omega(0)

Induction Base:
plus_x#1(gen_0':S8_6(0), gen_0':S8_6(b)) ->_R^Omega(0)
gen_0':S8_6(b)

Induction Step:
plus_x#1(gen_0':S8_6(+(n748_6, 1)), gen_0':S8_6(b)) ->_R^Omega(0)
S(plus_x#1(gen_0':S8_6(n748_6), gen_0':S8_6(b))) ->_IH
S(gen_0':S8_6(+(b, c749_6)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(30)
Obligation:
Innermost TRS:
Rules:
PLUS_X#1(0') -> c
PLUS_X#1(S(z0)) -> c1(PLUS_X#1(z0))
MAP#2(plus_x(z0), Nil) -> c2
MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0))
MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2))
MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))
plus_x#1(0', z0) -> z0
plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1))
map#2(plus_x(z0), Nil) -> Nil
map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2))
main(z0, z1) -> map#2(plus_x(z1), z0)

Types:
PLUS_X#1 :: 0':S -> c:c1
0' :: 0':S
c :: c:c1
S :: 0':S -> 0':S
c1 :: c:c1 -> c:c1
MAP#2 :: plus_x -> Nil:Cons -> c2:c3:c4
plus_x :: 0':S -> plus_x
Nil :: Nil:Cons
c2 :: c2:c3:c4
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
MAIN :: Nil:Cons -> 0':S -> c5
c5 :: c2:c3:c4 -> c5
plus_x#1 :: 0':S -> 0':S -> 0':S
map#2 :: plus_x -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> 0':S -> Nil:Cons
hole_c:c11_6 :: c:c1
hole_0':S2_6 :: 0':S
hole_c2:c3:c43_6 :: c2:c3:c4
hole_plus_x4_6 :: plus_x
hole_Nil:Cons5_6 :: Nil:Cons
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_0':S8_6 :: Nat -> 0':S
gen_c2:c3:c49_6 :: Nat -> c2:c3:c4
gen_Nil:Cons10_6 :: Nat -> Nil:Cons


Lemmas:
PLUS_X#1(gen_0':S8_6(n12_6)) -> gen_c:c17_6(n12_6), rt in Omega(1 + n12_6)
MAP#2(plus_x(0'), gen_Nil:Cons10_6(n234_6)) -> gen_c2:c3:c49_6(n234_6), rt in Omega(1 + n234_6)
plus_x#1(gen_0':S8_6(n748_6), gen_0':S8_6(b)) -> gen_0':S8_6(+(n748_6, b)), rt in Omega(0)


Generator Equations:
gen_c:c17_6(0) <=> c
gen_c:c17_6(+(x, 1)) <=> c1(gen_c:c17_6(x))
gen_0':S8_6(0) <=> 0'
gen_0':S8_6(+(x, 1)) <=> S(gen_0':S8_6(x))
gen_c2:c3:c49_6(0) <=> c2
gen_c2:c3:c49_6(+(x, 1)) <=> c4(gen_c2:c3:c49_6(x))
gen_Nil:Cons10_6(0) <=> Nil
gen_Nil:Cons10_6(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_6(x))


The following defined symbols remain to be analysed:
map#2
----------------------------------------

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
map#2(plus_x(0'), gen_Nil:Cons10_6(n1731_6)) -> gen_Nil:Cons10_6(n1731_6), rt in Omega(0)

Induction Base:
map#2(plus_x(0'), gen_Nil:Cons10_6(0)) ->_R^Omega(0)
Nil

Induction Step:
map#2(plus_x(0'), gen_Nil:Cons10_6(+(n1731_6, 1))) ->_R^Omega(0)
Cons(plus_x#1(0', 0'), map#2(plus_x(0'), gen_Nil:Cons10_6(n1731_6))) ->_L^Omega(0)
Cons(gen_0':S8_6(+(0, 0)), map#2(plus_x(0'), gen_Nil:Cons10_6(n1731_6))) ->_IH
Cons(gen_0':S8_6(0), gen_Nil:Cons10_6(c1732_6))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(32)
BOUNDS(1, INF)