WORST_CASE(Omega(n^1),?)
proof of input_eUxEpFSws0.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 44 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 399 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 84 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 148 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 47 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 100 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 64 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 114 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 57 ms]
        (30) typed CpxTrs
        (31) RewriteLemmaProof [LOWER BOUND(ID), 32 ms]
        (32) typed CpxTrs
        (33) RewriteLemmaProof [LOWER BOUND(ID), 48 ms]
        (34) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   cond_scanr_f_z_xs_1(Cons(0, x11), 0) -> Cons(0, Cons(0, x11))
   cond_scanr_f_z_xs_1(Cons(S(x2), x11), 0) -> Cons(S(x2), Cons(S(x2), x11))
   cond_scanr_f_z_xs_1(Cons(0, x11), M(x2)) -> Cons(0, Cons(0, x11))
   cond_scanr_f_z_xs_1(Cons(S(x40), x23), M(0)) -> Cons(S(x40), Cons(S(x40), x23))
   cond_scanr_f_z_xs_1(Cons(S(x8), x23), M(S(x4))) -> Cons(minus#2(x8, x4), Cons(S(x8), x23))
   cond_scanr_f_z_xs_1(Cons(0, x11), S(x2)) -> Cons(S(x2), Cons(0, x11))
   cond_scanr_f_z_xs_1(Cons(S(x2), x11), S(x4)) -> Cons(plus#2(S(x4), S(x2)), Cons(S(x2), x11))
   scanr#3(Nil) -> Cons(0, Nil)
   scanr#3(Cons(x4, x2)) -> cond_scanr_f_z_xs_1(scanr#3(x2), x4)
   foldl#3(x2, Nil) -> x2
   foldl#3(x6, Cons(x4, x2)) -> foldl#3(max#2(x6, x4), x2)
   minus#2(0, x16) -> 0
   minus#2(S(x20), 0) -> S(x20)
   minus#2(S(x4), S(x2)) -> minus#2(x4, x2)
   plus#2(0, S(x2)) -> S(x2)
   plus#2(S(x4), S(x2)) -> S(plus#2(x4, S(x2)))
   max#2(0, x8) -> x8
   max#2(S(x12), 0) -> S(x12)
   max#2(S(x4), S(x2)) -> S(max#2(x4, x2))
   main(x1) -> foldl#3(0, scanr#3(x1))

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

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   cond_scanr_f_z_xs_1(Cons(0, z0), 0) -> Cons(0, Cons(0, z0))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0) -> Cons(S(z0), Cons(S(z0), z1))
   cond_scanr_f_z_xs_1(Cons(0, z0), M(z1)) -> Cons(0, Cons(0, z0))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0)) -> Cons(S(z0), Cons(S(z0), z1))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
   cond_scanr_f_z_xs_1(Cons(0, z0), S(z1)) -> Cons(S(z1), Cons(0, z0))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
   scanr#3(Nil) -> Cons(0, Nil)
   scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
   foldl#3(z0, Nil) -> z0
   foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
   minus#2(0, z0) -> 0
   minus#2(S(z0), 0) -> S(z0)
   minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
   plus#2(0, S(z0)) -> S(z0)
   plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
   max#2(0, z0) -> z0
   max#2(S(z0), 0) -> S(z0)
   max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
   main(z0) -> foldl#3(0, scanr#3(z0))
Tuples:
   COND_SCANR_F_Z_XS_1(Cons(0, z0), 0) -> c
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0) -> c1
   COND_SCANR_F_Z_XS_1(Cons(0, z0), M(z1)) -> c2
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0)) -> c3
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
   COND_SCANR_F_Z_XS_1(Cons(0, z0), S(z1)) -> c5
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
   SCANR#3(Nil) -> c7
   SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
   FOLDL#3(z0, Nil) -> c9
   FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
   MINUS#2(0, z0) -> c11
   MINUS#2(S(z0), 0) -> c12
   MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
   PLUS#2(0, S(z0)) -> c14
   PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
   MAX#2(0, z0) -> c16
   MAX#2(S(z0), 0) -> c17
   MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
   MAIN(z0) -> c19(FOLDL#3(0, scanr#3(z0)), SCANR#3(z0))
S tuples:
   COND_SCANR_F_Z_XS_1(Cons(0, z0), 0) -> c
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0) -> c1
   COND_SCANR_F_Z_XS_1(Cons(0, z0), M(z1)) -> c2
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0)) -> c3
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
   COND_SCANR_F_Z_XS_1(Cons(0, z0), S(z1)) -> c5
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
   SCANR#3(Nil) -> c7
   SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
   FOLDL#3(z0, Nil) -> c9
   FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
   MINUS#2(0, z0) -> c11
   MINUS#2(S(z0), 0) -> c12
   MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
   PLUS#2(0, S(z0)) -> c14
   PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
   MAX#2(0, z0) -> c16
   MAX#2(S(z0), 0) -> c17
   MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
   MAIN(z0) -> c19(FOLDL#3(0, scanr#3(z0)), SCANR#3(z0))
K tuples:none
Defined Rule Symbols:   cond_scanr_f_z_xs_1_2, scanr#3_1, foldl#3_2, minus#2_2, plus#2_2, max#2_2, main_1

Defined Pair Symbols:   COND_SCANR_F_Z_XS_1_2, SCANR#3_1, FOLDL#3_2, MINUS#2_2, PLUS#2_2, MAX#2_2, MAIN_1

Compound Symbols:   c, c1, c2, c3, c4_1, c5, c6_1, c7, c8_2, c9, c10_2, c11, c12, c13_1, c14, c15_1, c16, c17, c18_1, c19_2


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

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

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

   COND_SCANR_F_Z_XS_1(Cons(0, z0), 0) -> c
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0) -> c1
   COND_SCANR_F_Z_XS_1(Cons(0, z0), M(z1)) -> c2
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0)) -> c3
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
   COND_SCANR_F_Z_XS_1(Cons(0, z0), S(z1)) -> c5
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
   SCANR#3(Nil) -> c7
   SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
   FOLDL#3(z0, Nil) -> c9
   FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
   MINUS#2(0, z0) -> c11
   MINUS#2(S(z0), 0) -> c12
   MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
   PLUS#2(0, S(z0)) -> c14
   PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
   MAX#2(0, z0) -> c16
   MAX#2(S(z0), 0) -> c17
   MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
   MAIN(z0) -> c19(FOLDL#3(0, scanr#3(z0)), SCANR#3(z0))

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

   cond_scanr_f_z_xs_1(Cons(0, z0), 0) -> Cons(0, Cons(0, z0))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0) -> Cons(S(z0), Cons(S(z0), z1))
   cond_scanr_f_z_xs_1(Cons(0, z0), M(z1)) -> Cons(0, Cons(0, z0))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0)) -> Cons(S(z0), Cons(S(z0), z1))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
   cond_scanr_f_z_xs_1(Cons(0, z0), S(z1)) -> Cons(S(z1), Cons(0, z0))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
   scanr#3(Nil) -> Cons(0, Nil)
   scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
   foldl#3(z0, Nil) -> z0
   foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
   minus#2(0, z0) -> 0
   minus#2(S(z0), 0) -> S(z0)
   minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
   plus#2(0, S(z0)) -> S(z0)
   plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
   max#2(0, z0) -> z0
   max#2(S(z0), 0) -> S(z0)
   max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
   main(z0) -> foldl#3(0, scanr#3(z0))

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

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

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

   COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
   COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
   COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
   COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
   SCANR#3(Nil) -> c7
   SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
   FOLDL#3(z0, Nil) -> c9
   FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
   MINUS#2(0', z0) -> c11
   MINUS#2(S(z0), 0') -> c12
   MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
   PLUS#2(0', S(z0)) -> c14
   PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
   MAX#2(0', z0) -> c16
   MAX#2(S(z0), 0') -> c17
   MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
   MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))

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

   cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
   cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
   cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
   cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
   scanr#3(Nil) -> Cons(0', Nil)
   scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
   foldl#3(z0, Nil) -> z0
   foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
   minus#2(0', z0) -> 0'
   minus#2(S(z0), 0') -> S(z0)
   minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
   plus#2(0', S(z0)) -> S(z0)
   plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
   max#2(0', z0) -> z0
   max#2(S(z0), 0') -> S(z0)
   max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
   main(z0) -> foldl#3(0', scanr#3(z0))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MINUS#2, PLUS#2, SCANR#3, scanr#3, FOLDL#3, max#2, MAX#2, minus#2, plus#2, foldl#3

They will be analysed ascendingly in the following order:
scanr#3 < SCANR#3
max#2 < FOLDL#3
MAX#2 < FOLDL#3
max#2 < foldl#3

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

(10)
Obligation:
Innermost TRS:
Rules:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
MINUS#2, PLUS#2, SCANR#3, scanr#3, FOLDL#3, max#2, MAX#2, minus#2, plus#2, foldl#3

They will be analysed ascendingly in the following order:
scanr#3 < SCANR#3
max#2 < FOLDL#3
MAX#2 < FOLDL#3
max#2 < foldl#3

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20)) -> gen_c11:c12:c1312_20(n18_20), rt in Omega(1 + n18_20)

Induction Base:
MINUS#2(gen_0':S:M11_20(0), gen_0':S:M11_20(0)) ->_R^Omega(1)
c11

Induction Step:
MINUS#2(gen_0':S:M11_20(+(n18_20, 1)), gen_0':S:M11_20(+(n18_20, 1))) ->_R^Omega(1)
c13(MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20))) ->_IH
c13(gen_c11:c12:c1312_20(c19_20))

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

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
MINUS#2, PLUS#2, SCANR#3, scanr#3, FOLDL#3, max#2, MAX#2, minus#2, plus#2, foldl#3

They will be analysed ascendingly in the following order:
scanr#3 < SCANR#3
max#2 < FOLDL#3
MAX#2 < FOLDL#3
max#2 < foldl#3

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Lemmas:
MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20)) -> gen_c11:c12:c1312_20(n18_20), rt in Omega(1 + n18_20)


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
PLUS#2, SCANR#3, scanr#3, FOLDL#3, max#2, MAX#2, minus#2, plus#2, foldl#3

They will be analysed ascendingly in the following order:
scanr#3 < SCANR#3
max#2 < FOLDL#3
MAX#2 < FOLDL#3
max#2 < foldl#3

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS#2(gen_0':S:M11_20(n868_20), gen_0':S:M11_20(1)) -> gen_c14:c1513_20(n868_20), rt in Omega(1 + n868_20)

Induction Base:
PLUS#2(gen_0':S:M11_20(0), gen_0':S:M11_20(1)) ->_R^Omega(1)
c14

Induction Step:
PLUS#2(gen_0':S:M11_20(+(n868_20, 1)), gen_0':S:M11_20(1)) ->_R^Omega(1)
c15(PLUS#2(gen_0':S:M11_20(n868_20), S(gen_0':S:M11_20(0)))) ->_IH
c15(gen_c14:c1513_20(c869_20))

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

(18)
Obligation:
Innermost TRS:
Rules:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Lemmas:
MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20)) -> gen_c11:c12:c1312_20(n18_20), rt in Omega(1 + n18_20)
PLUS#2(gen_0':S:M11_20(n868_20), gen_0':S:M11_20(1)) -> gen_c14:c1513_20(n868_20), rt in Omega(1 + n868_20)


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
scanr#3, SCANR#3, FOLDL#3, max#2, MAX#2, minus#2, plus#2, foldl#3

They will be analysed ascendingly in the following order:
scanr#3 < SCANR#3
max#2 < FOLDL#3
MAX#2 < FOLDL#3
max#2 < foldl#3

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
scanr#3(gen_Cons:Nil10_20(n1559_20)) -> gen_Cons:Nil10_20(+(1, n1559_20)), rt in Omega(0)

Induction Base:
scanr#3(gen_Cons:Nil10_20(0)) ->_R^Omega(0)
Cons(0', Nil)

Induction Step:
scanr#3(gen_Cons:Nil10_20(+(n1559_20, 1))) ->_R^Omega(0)
cond_scanr_f_z_xs_1(scanr#3(gen_Cons:Nil10_20(n1559_20)), 0') ->_IH
cond_scanr_f_z_xs_1(gen_Cons:Nil10_20(+(1, c1560_20)), 0') ->_R^Omega(0)
Cons(0', Cons(0', gen_Cons:Nil10_20(n1559_20)))

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

(20)
Obligation:
Innermost TRS:
Rules:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Lemmas:
MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20)) -> gen_c11:c12:c1312_20(n18_20), rt in Omega(1 + n18_20)
PLUS#2(gen_0':S:M11_20(n868_20), gen_0':S:M11_20(1)) -> gen_c14:c1513_20(n868_20), rt in Omega(1 + n868_20)
scanr#3(gen_Cons:Nil10_20(n1559_20)) -> gen_Cons:Nil10_20(+(1, n1559_20)), rt in Omega(0)


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
SCANR#3, FOLDL#3, max#2, MAX#2, minus#2, plus#2, foldl#3

They will be analysed ascendingly in the following order:
max#2 < FOLDL#3
MAX#2 < FOLDL#3
max#2 < foldl#3

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SCANR#3(gen_Cons:Nil10_20(n16038_20)) -> gen_c7:c814_20(n16038_20), rt in Omega(1 + n16038_20)

Induction Base:
SCANR#3(gen_Cons:Nil10_20(0)) ->_R^Omega(1)
c7

Induction Step:
SCANR#3(gen_Cons:Nil10_20(+(n16038_20, 1))) ->_R^Omega(1)
c8(COND_SCANR_F_Z_XS_1(scanr#3(gen_Cons:Nil10_20(n16038_20)), 0'), SCANR#3(gen_Cons:Nil10_20(n16038_20))) ->_L^Omega(0)
c8(COND_SCANR_F_Z_XS_1(gen_Cons:Nil10_20(+(1, n16038_20)), 0'), SCANR#3(gen_Cons:Nil10_20(n16038_20))) ->_R^Omega(1)
c8(c, SCANR#3(gen_Cons:Nil10_20(n16038_20))) ->_IH
c8(c, gen_c7:c814_20(c16039_20))

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

(22)
Obligation:
Innermost TRS:
Rules:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Lemmas:
MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20)) -> gen_c11:c12:c1312_20(n18_20), rt in Omega(1 + n18_20)
PLUS#2(gen_0':S:M11_20(n868_20), gen_0':S:M11_20(1)) -> gen_c14:c1513_20(n868_20), rt in Omega(1 + n868_20)
scanr#3(gen_Cons:Nil10_20(n1559_20)) -> gen_Cons:Nil10_20(+(1, n1559_20)), rt in Omega(0)
SCANR#3(gen_Cons:Nil10_20(n16038_20)) -> gen_c7:c814_20(n16038_20), rt in Omega(1 + n16038_20)


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
max#2, FOLDL#3, MAX#2, minus#2, plus#2, foldl#3

They will be analysed ascendingly in the following order:
max#2 < FOLDL#3
MAX#2 < FOLDL#3
max#2 < foldl#3

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
max#2(gen_0':S:M11_20(n20114_20), gen_0':S:M11_20(n20114_20)) -> gen_0':S:M11_20(n20114_20), rt in Omega(0)

Induction Base:
max#2(gen_0':S:M11_20(0), gen_0':S:M11_20(0)) ->_R^Omega(0)
gen_0':S:M11_20(0)

Induction Step:
max#2(gen_0':S:M11_20(+(n20114_20, 1)), gen_0':S:M11_20(+(n20114_20, 1))) ->_R^Omega(0)
S(max#2(gen_0':S:M11_20(n20114_20), gen_0':S:M11_20(n20114_20))) ->_IH
S(gen_0':S:M11_20(c20115_20))

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

(24)
Obligation:
Innermost TRS:
Rules:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Lemmas:
MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20)) -> gen_c11:c12:c1312_20(n18_20), rt in Omega(1 + n18_20)
PLUS#2(gen_0':S:M11_20(n868_20), gen_0':S:M11_20(1)) -> gen_c14:c1513_20(n868_20), rt in Omega(1 + n868_20)
scanr#3(gen_Cons:Nil10_20(n1559_20)) -> gen_Cons:Nil10_20(+(1, n1559_20)), rt in Omega(0)
SCANR#3(gen_Cons:Nil10_20(n16038_20)) -> gen_c7:c814_20(n16038_20), rt in Omega(1 + n16038_20)
max#2(gen_0':S:M11_20(n20114_20), gen_0':S:M11_20(n20114_20)) -> gen_0':S:M11_20(n20114_20), rt in Omega(0)


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
MAX#2, FOLDL#3, minus#2, plus#2, foldl#3

They will be analysed ascendingly in the following order:
MAX#2 < FOLDL#3

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MAX#2(gen_0':S:M11_20(n21555_20), gen_0':S:M11_20(n21555_20)) -> gen_c16:c17:c1816_20(n21555_20), rt in Omega(1 + n21555_20)

Induction Base:
MAX#2(gen_0':S:M11_20(0), gen_0':S:M11_20(0)) ->_R^Omega(1)
c16

Induction Step:
MAX#2(gen_0':S:M11_20(+(n21555_20, 1)), gen_0':S:M11_20(+(n21555_20, 1))) ->_R^Omega(1)
c18(MAX#2(gen_0':S:M11_20(n21555_20), gen_0':S:M11_20(n21555_20))) ->_IH
c18(gen_c16:c17:c1816_20(c21556_20))

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

(26)
Obligation:
Innermost TRS:
Rules:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Lemmas:
MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20)) -> gen_c11:c12:c1312_20(n18_20), rt in Omega(1 + n18_20)
PLUS#2(gen_0':S:M11_20(n868_20), gen_0':S:M11_20(1)) -> gen_c14:c1513_20(n868_20), rt in Omega(1 + n868_20)
scanr#3(gen_Cons:Nil10_20(n1559_20)) -> gen_Cons:Nil10_20(+(1, n1559_20)), rt in Omega(0)
SCANR#3(gen_Cons:Nil10_20(n16038_20)) -> gen_c7:c814_20(n16038_20), rt in Omega(1 + n16038_20)
max#2(gen_0':S:M11_20(n20114_20), gen_0':S:M11_20(n20114_20)) -> gen_0':S:M11_20(n20114_20), rt in Omega(0)
MAX#2(gen_0':S:M11_20(n21555_20), gen_0':S:M11_20(n21555_20)) -> gen_c16:c17:c1816_20(n21555_20), rt in Omega(1 + n21555_20)


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
FOLDL#3, minus#2, plus#2, foldl#3
----------------------------------------

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
FOLDL#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(n22576_20)) -> gen_c9:c1015_20(n22576_20), rt in Omega(1 + n22576_20)

Induction Base:
FOLDL#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(0)) ->_R^Omega(1)
c9

Induction Step:
FOLDL#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(+(n22576_20, 1))) ->_R^Omega(1)
c10(FOLDL#3(max#2(gen_0':S:M11_20(0), 0'), gen_Cons:Nil10_20(n22576_20)), MAX#2(gen_0':S:M11_20(0), 0')) ->_L^Omega(0)
c10(FOLDL#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(n22576_20)), MAX#2(gen_0':S:M11_20(0), 0')) ->_IH
c10(gen_c9:c1015_20(c22577_20), MAX#2(gen_0':S:M11_20(0), 0')) ->_L^Omega(1)
c10(gen_c9:c1015_20(n22576_20), gen_c16:c17:c1816_20(0))

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:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Lemmas:
MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20)) -> gen_c11:c12:c1312_20(n18_20), rt in Omega(1 + n18_20)
PLUS#2(gen_0':S:M11_20(n868_20), gen_0':S:M11_20(1)) -> gen_c14:c1513_20(n868_20), rt in Omega(1 + n868_20)
scanr#3(gen_Cons:Nil10_20(n1559_20)) -> gen_Cons:Nil10_20(+(1, n1559_20)), rt in Omega(0)
SCANR#3(gen_Cons:Nil10_20(n16038_20)) -> gen_c7:c814_20(n16038_20), rt in Omega(1 + n16038_20)
max#2(gen_0':S:M11_20(n20114_20), gen_0':S:M11_20(n20114_20)) -> gen_0':S:M11_20(n20114_20), rt in Omega(0)
MAX#2(gen_0':S:M11_20(n21555_20), gen_0':S:M11_20(n21555_20)) -> gen_c16:c17:c1816_20(n21555_20), rt in Omega(1 + n21555_20)
FOLDL#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(n22576_20)) -> gen_c9:c1015_20(n22576_20), rt in Omega(1 + n22576_20)


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
minus#2, plus#2, foldl#3
----------------------------------------

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
minus#2(gen_0':S:M11_20(n24401_20), gen_0':S:M11_20(n24401_20)) -> gen_0':S:M11_20(0), rt in Omega(0)

Induction Base:
minus#2(gen_0':S:M11_20(0), gen_0':S:M11_20(0)) ->_R^Omega(0)
0'

Induction Step:
minus#2(gen_0':S:M11_20(+(n24401_20, 1)), gen_0':S:M11_20(+(n24401_20, 1))) ->_R^Omega(0)
minus#2(gen_0':S:M11_20(n24401_20), gen_0':S:M11_20(n24401_20)) ->_IH
gen_0':S:M11_20(0)

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:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Lemmas:
MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20)) -> gen_c11:c12:c1312_20(n18_20), rt in Omega(1 + n18_20)
PLUS#2(gen_0':S:M11_20(n868_20), gen_0':S:M11_20(1)) -> gen_c14:c1513_20(n868_20), rt in Omega(1 + n868_20)
scanr#3(gen_Cons:Nil10_20(n1559_20)) -> gen_Cons:Nil10_20(+(1, n1559_20)), rt in Omega(0)
SCANR#3(gen_Cons:Nil10_20(n16038_20)) -> gen_c7:c814_20(n16038_20), rt in Omega(1 + n16038_20)
max#2(gen_0':S:M11_20(n20114_20), gen_0':S:M11_20(n20114_20)) -> gen_0':S:M11_20(n20114_20), rt in Omega(0)
MAX#2(gen_0':S:M11_20(n21555_20), gen_0':S:M11_20(n21555_20)) -> gen_c16:c17:c1816_20(n21555_20), rt in Omega(1 + n21555_20)
FOLDL#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(n22576_20)) -> gen_c9:c1015_20(n22576_20), rt in Omega(1 + n22576_20)
minus#2(gen_0':S:M11_20(n24401_20), gen_0':S:M11_20(n24401_20)) -> gen_0':S:M11_20(0), rt in Omega(0)


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
plus#2, foldl#3
----------------------------------------

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus#2(gen_0':S:M11_20(n25619_20), gen_0':S:M11_20(1)) -> gen_0':S:M11_20(+(1, n25619_20)), rt in Omega(0)

Induction Base:
plus#2(gen_0':S:M11_20(0), gen_0':S:M11_20(1)) ->_R^Omega(0)
S(gen_0':S:M11_20(0))

Induction Step:
plus#2(gen_0':S:M11_20(+(n25619_20, 1)), gen_0':S:M11_20(1)) ->_R^Omega(0)
S(plus#2(gen_0':S:M11_20(n25619_20), S(gen_0':S:M11_20(0)))) ->_IH
S(gen_0':S:M11_20(+(1, c25620_20)))

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:
COND_SCANR_F_Z_XS_1(Cons(0', z0), 0') -> c
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), 0') -> c1
COND_SCANR_F_Z_XS_1(Cons(0', z0), M(z1)) -> c2
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(0')) -> c3
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), M(S(z2))) -> c4(MINUS#2(z0, z2))
COND_SCANR_F_Z_XS_1(Cons(0', z0), S(z1)) -> c5
COND_SCANR_F_Z_XS_1(Cons(S(z0), z1), S(z2)) -> c6(PLUS#2(S(z2), S(z0)))
SCANR#3(Nil) -> c7
SCANR#3(Cons(z0, z1)) -> c8(COND_SCANR_F_Z_XS_1(scanr#3(z1), z0), SCANR#3(z1))
FOLDL#3(z0, Nil) -> c9
FOLDL#3(z0, Cons(z1, z2)) -> c10(FOLDL#3(max#2(z0, z1), z2), MAX#2(z0, z1))
MINUS#2(0', z0) -> c11
MINUS#2(S(z0), 0') -> c12
MINUS#2(S(z0), S(z1)) -> c13(MINUS#2(z0, z1))
PLUS#2(0', S(z0)) -> c14
PLUS#2(S(z0), S(z1)) -> c15(PLUS#2(z0, S(z1)))
MAX#2(0', z0) -> c16
MAX#2(S(z0), 0') -> c17
MAX#2(S(z0), S(z1)) -> c18(MAX#2(z0, z1))
MAIN(z0) -> c19(FOLDL#3(0', scanr#3(z0)), SCANR#3(z0))
cond_scanr_f_z_xs_1(Cons(0', z0), 0') -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), 0') -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), M(z1)) -> Cons(0', Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(0')) -> Cons(S(z0), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), M(S(z2))) -> Cons(minus#2(z0, z2), Cons(S(z0), z1))
cond_scanr_f_z_xs_1(Cons(0', z0), S(z1)) -> Cons(S(z1), Cons(0', z0))
cond_scanr_f_z_xs_1(Cons(S(z0), z1), S(z2)) -> Cons(plus#2(S(z2), S(z0)), Cons(S(z0), z1))
scanr#3(Nil) -> Cons(0', Nil)
scanr#3(Cons(z0, z1)) -> cond_scanr_f_z_xs_1(scanr#3(z1), z0)
foldl#3(z0, Nil) -> z0
foldl#3(z0, Cons(z1, z2)) -> foldl#3(max#2(z0, z1), z2)
minus#2(0', z0) -> 0'
minus#2(S(z0), 0') -> S(z0)
minus#2(S(z0), S(z1)) -> minus#2(z0, z1)
plus#2(0', S(z0)) -> S(z0)
plus#2(S(z0), S(z1)) -> S(plus#2(z0, S(z1)))
max#2(0', z0) -> z0
max#2(S(z0), 0') -> S(z0)
max#2(S(z0), S(z1)) -> S(max#2(z0, z1))
main(z0) -> foldl#3(0', scanr#3(z0))

Types:
COND_SCANR_F_Z_XS_1 :: Cons:Nil -> 0':S:M -> c:c1:c2:c3:c4:c5:c6
Cons :: 0':S:M -> Cons:Nil -> Cons:Nil
0' :: 0':S:M
c :: c:c1:c2:c3:c4:c5:c6
S :: 0':S:M -> 0':S:M
c1 :: c:c1:c2:c3:c4:c5:c6
M :: 0':S:M -> 0':S:M
c2 :: c:c1:c2:c3:c4:c5:c6
c3 :: c:c1:c2:c3:c4:c5:c6
c4 :: c11:c12:c13 -> c:c1:c2:c3:c4:c5:c6
MINUS#2 :: 0':S:M -> 0':S:M -> c11:c12:c13
c5 :: c:c1:c2:c3:c4:c5:c6
c6 :: c14:c15 -> c:c1:c2:c3:c4:c5:c6
PLUS#2 :: 0':S:M -> 0':S:M -> c14:c15
SCANR#3 :: Cons:Nil -> c7:c8
Nil :: Cons:Nil
c7 :: c7:c8
c8 :: c:c1:c2:c3:c4:c5:c6 -> c7:c8 -> c7:c8
scanr#3 :: Cons:Nil -> Cons:Nil
FOLDL#3 :: 0':S:M -> Cons:Nil -> c9:c10
c9 :: c9:c10
c10 :: c9:c10 -> c16:c17:c18 -> c9:c10
max#2 :: 0':S:M -> 0':S:M -> 0':S:M
MAX#2 :: 0':S:M -> 0':S:M -> c16:c17:c18
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
c14 :: c14:c15
c15 :: c14:c15 -> c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
MAIN :: Cons:Nil -> c19
c19 :: c9:c10 -> c7:c8 -> c19
cond_scanr_f_z_xs_1 :: Cons:Nil -> 0':S:M -> Cons:Nil
minus#2 :: 0':S:M -> 0':S:M -> 0':S:M
plus#2 :: 0':S:M -> 0':S:M -> 0':S:M
foldl#3 :: 0':S:M -> Cons:Nil -> 0':S:M
main :: Cons:Nil -> 0':S:M
hole_c:c1:c2:c3:c4:c5:c61_20 :: c:c1:c2:c3:c4:c5:c6
hole_Cons:Nil2_20 :: Cons:Nil
hole_0':S:M3_20 :: 0':S:M
hole_c11:c12:c134_20 :: c11:c12:c13
hole_c14:c155_20 :: c14:c15
hole_c7:c86_20 :: c7:c8
hole_c9:c107_20 :: c9:c10
hole_c16:c17:c188_20 :: c16:c17:c18
hole_c199_20 :: c19
gen_Cons:Nil10_20 :: Nat -> Cons:Nil
gen_0':S:M11_20 :: Nat -> 0':S:M
gen_c11:c12:c1312_20 :: Nat -> c11:c12:c13
gen_c14:c1513_20 :: Nat -> c14:c15
gen_c7:c814_20 :: Nat -> c7:c8
gen_c9:c1015_20 :: Nat -> c9:c10
gen_c16:c17:c1816_20 :: Nat -> c16:c17:c18


Lemmas:
MINUS#2(gen_0':S:M11_20(n18_20), gen_0':S:M11_20(n18_20)) -> gen_c11:c12:c1312_20(n18_20), rt in Omega(1 + n18_20)
PLUS#2(gen_0':S:M11_20(n868_20), gen_0':S:M11_20(1)) -> gen_c14:c1513_20(n868_20), rt in Omega(1 + n868_20)
scanr#3(gen_Cons:Nil10_20(n1559_20)) -> gen_Cons:Nil10_20(+(1, n1559_20)), rt in Omega(0)
SCANR#3(gen_Cons:Nil10_20(n16038_20)) -> gen_c7:c814_20(n16038_20), rt in Omega(1 + n16038_20)
max#2(gen_0':S:M11_20(n20114_20), gen_0':S:M11_20(n20114_20)) -> gen_0':S:M11_20(n20114_20), rt in Omega(0)
MAX#2(gen_0':S:M11_20(n21555_20), gen_0':S:M11_20(n21555_20)) -> gen_c16:c17:c1816_20(n21555_20), rt in Omega(1 + n21555_20)
FOLDL#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(n22576_20)) -> gen_c9:c1015_20(n22576_20), rt in Omega(1 + n22576_20)
minus#2(gen_0':S:M11_20(n24401_20), gen_0':S:M11_20(n24401_20)) -> gen_0':S:M11_20(0), rt in Omega(0)
plus#2(gen_0':S:M11_20(n25619_20), gen_0':S:M11_20(1)) -> gen_0':S:M11_20(+(1, n25619_20)), rt in Omega(0)


Generator Equations:
gen_Cons:Nil10_20(0) <=> Nil
gen_Cons:Nil10_20(+(x, 1)) <=> Cons(0', gen_Cons:Nil10_20(x))
gen_0':S:M11_20(0) <=> 0'
gen_0':S:M11_20(+(x, 1)) <=> S(gen_0':S:M11_20(x))
gen_c11:c12:c1312_20(0) <=> c11
gen_c11:c12:c1312_20(+(x, 1)) <=> c13(gen_c11:c12:c1312_20(x))
gen_c14:c1513_20(0) <=> c14
gen_c14:c1513_20(+(x, 1)) <=> c15(gen_c14:c1513_20(x))
gen_c7:c814_20(0) <=> c7
gen_c7:c814_20(+(x, 1)) <=> c8(c, gen_c7:c814_20(x))
gen_c9:c1015_20(0) <=> c9
gen_c9:c1015_20(+(x, 1)) <=> c10(gen_c9:c1015_20(x), c16)
gen_c16:c17:c1816_20(0) <=> c16
gen_c16:c17:c1816_20(+(x, 1)) <=> c18(gen_c16:c17:c1816_20(x))


The following defined symbols remain to be analysed:
foldl#3
----------------------------------------

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
foldl#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(n26617_20)) -> gen_0':S:M11_20(0), rt in Omega(0)

Induction Base:
foldl#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(0)) ->_R^Omega(0)
gen_0':S:M11_20(0)

Induction Step:
foldl#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(+(n26617_20, 1))) ->_R^Omega(0)
foldl#3(max#2(gen_0':S:M11_20(0), 0'), gen_Cons:Nil10_20(n26617_20)) ->_L^Omega(0)
foldl#3(gen_0':S:M11_20(0), gen_Cons:Nil10_20(n26617_20)) ->_IH
gen_0':S:M11_20(0)

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

(34)
BOUNDS(1, INF)