WORST_CASE(Omega(n^1),O(n^1))
proof of input_PumuKDnCIH.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (4) CdtProblem
    (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxTRS
    (9) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
    (10) CpxTRS
    (11) CpxTrsMatchBoundsTAProof [FINISHED, 14 ms]
    (12) BOUNDS(1, n^1)
(13) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CdtProblem
    (15) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) CpxRelTRS
    (17) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) CpxRelTRS
    (19) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (20) typed CpxTrs
    (21) OrderProof [LOWER BOUND(ID), 12 ms]
    (22) typed CpxTrs
    (23) RewriteLemmaProof [LOWER BOUND(ID), 317 ms]
    (24) BEST
        (25) proven lower bound
            (26) LowerBoundPropagationProof [FINISHED, 0 ms]
            (27) BOUNDS(n^1, INF)
        (28) typed CpxTrs
            (29) RewriteLemmaProof [LOWER BOUND(ID), 105 ms]
            (30) typed CpxTrs
            (31) RewriteLemmaProof [LOWER BOUND(ID), 71 ms]
            (32) typed CpxTrs
            (33) RewriteLemmaProof [LOWER BOUND(ID), 34 ms]
            (34) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   plus_x#1(0, x8) -> x8
   plus_x#1(S(x12), x14) -> S(plus_x#1(x12, x14))
   map#2(plus_x(x2), Nil) -> Nil
   map#2(plus_x(x6), Cons(x4, x2)) -> Cons(plus_x#1(x6, x4), map#2(plus_x(x6), x2))
   main(x5, x12) -> map#2(plus_x(x12), x5)

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
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)
Tuples:
   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))
S tuples:
   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))
K tuples:none
Defined Rule Symbols:   plus_x#1_2, map#2_2, main_2

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

Compound Symbols:   c, c1_1, c2, c3_1, c4_1, c5_1


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

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0))
Removed 2 trailing nodes:
   MAP#2(plus_x(z0), Nil) -> c2
   PLUS_X#1(0, z0) -> c

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

(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)
Tuples:
   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   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))
S tuples:
   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   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))
K tuples:none
Defined Rule Symbols:   plus_x#1_2, map#2_2, main_2

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

Compound Symbols:   c1_1, c3_1, c4_1


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

(5) 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)

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   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))
S tuples:
   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   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))
K tuples:none
Defined Rule Symbols:none

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

Compound Symbols:   c1_1, c3_1, c4_1


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

(7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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

   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   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))

S is empty.
Rewrite Strategy: INNERMOST
----------------------------------------

(9) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

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

   PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1))
   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))

S is empty.
Rewrite Strategy: INNERMOST
----------------------------------------

(11) CpxTrsMatchBoundsTAProof (FINISHED)
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, 2]
transitions: 
S0(0) -> 0
c10(0) -> 0
plus_x0(0) -> 0
Cons0(0, 0) -> 0
c30(0) -> 0
c40(0) -> 0
PLUS_X#10(0, 0) -> 1
MAP#20(0, 0) -> 2
PLUS_X#11(0, 0) -> 3
c11(3) -> 1
PLUS_X#11(0, 0) -> 4
c31(4) -> 2
plus_x1(0) -> 6
MAP#21(6, 0) -> 5
c41(5) -> 2
c11(3) -> 3
c11(3) -> 4
c31(4) -> 5
c41(5) -> 5

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

(12)
BOUNDS(1, n^1)

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

(13) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(14)
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)
Tuples:
   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))
S tuples:
   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))
K tuples:none
Defined Rule Symbols:   plus_x#1_2, map#2_2, main_2

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

Compound Symbols:   c, c1_1, c2, c3_1, c4_1, c5_1


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

(15) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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

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

(18)
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
----------------------------------------

(19) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(20)
Obligation:
Innermost TRS:
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))
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 -> 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

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

(21) 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

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

(22)
Obligation:
Innermost TRS:
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))
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 -> 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

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

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

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

Induction Step:
PLUS_X#1(gen_0':S8_6(+(n12_6, 1)), gen_0':S8_6(b)) ->_R^Omega(1)
c1(PLUS_X#1(gen_0':S8_6(n12_6), gen_0':S8_6(b))) ->_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).
----------------------------------------

(24)
Complex Obligation (BEST)

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

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

Innermost TRS:
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))
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 -> 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

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

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

(27)
BOUNDS(n^1, INF)

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

(28)
Obligation:
Innermost TRS:
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))
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 -> 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_0':S8_6(b)) -> 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

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MAP#2(plus_x(0'), gen_Nil:Cons10_6(n404_6)) -> gen_c2:c3:c49_6(n404_6), rt in Omega(1 + n404_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(+(n404_6, 1))) ->_R^Omega(1)
c4(MAP#2(plus_x(0'), gen_Nil:Cons10_6(n404_6))) ->_IH
c4(gen_c2:c3:c49_6(c405_6))

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

(30)
Obligation:
Innermost TRS:
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))
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 -> 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_0':S8_6(b)) -> gen_c:c17_6(n12_6), rt in Omega(1 + n12_6)
MAP#2(plus_x(0'), gen_Nil:Cons10_6(n404_6)) -> gen_c2:c3:c49_6(n404_6), rt in Omega(1 + n404_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

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus_x#1(gen_0':S8_6(n919_6), gen_0':S8_6(b)) -> gen_0':S8_6(+(n919_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(+(n919_6, 1)), gen_0':S8_6(b)) ->_R^Omega(0)
S(plus_x#1(gen_0':S8_6(n919_6), gen_0':S8_6(b))) ->_IH
S(gen_0':S8_6(+(b, c920_6)))

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

(32)
Obligation:
Innermost TRS:
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))
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 -> 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_0':S8_6(b)) -> gen_c:c17_6(n12_6), rt in Omega(1 + n12_6)
MAP#2(plus_x(0'), gen_Nil:Cons10_6(n404_6)) -> gen_c2:c3:c49_6(n404_6), rt in Omega(1 + n404_6)
plus_x#1(gen_0':S8_6(n919_6), gen_0':S8_6(b)) -> gen_0':S8_6(+(n919_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
----------------------------------------

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
map#2(plus_x(0'), gen_Nil:Cons10_6(n1902_6)) -> gen_Nil:Cons10_6(n1902_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(+(n1902_6, 1))) ->_R^Omega(0)
Cons(plus_x#1(0', 0'), map#2(plus_x(0'), gen_Nil:Cons10_6(n1902_6))) ->_L^Omega(0)
Cons(gen_0':S8_6(+(0, 0)), map#2(plus_x(0'), gen_Nil:Cons10_6(n1902_6))) ->_IH
Cons(gen_0':S8_6(0), gen_Nil:Cons10_6(c1903_6))

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

(34)
BOUNDS(1, INF)