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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 413 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 2 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 274 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), 49 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 64 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 51 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 605 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 236 ms]
        (26) typed CpxTrs


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

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

   SELECT(z0, z1, Cons(z2, z3)) -> c(MAPCONSAPP(z0, permute(revapp(z1, Cons(z2, z3))), select(z2, Cons(z0, z1), z3)), PERMUTE(revapp(z1, Cons(z2, z3))), REVAPP(z1, Cons(z2, z3)))
   SELECT(z0, z1, Cons(z2, z3)) -> c1(MAPCONSAPP(z0, permute(revapp(z1, Cons(z2, z3))), select(z2, Cons(z0, z1), z3)), SELECT(z2, Cons(z0, z1), z3))
   SELECT(z0, z1, Nil) -> c2(MAPCONSAPP(z0, permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c3(REVAPP(z1, Cons(z0, z2)))
   REVAPP(Nil, z0) -> c4
   PERMUTE(Cons(z0, z1)) -> c5(SELECT(z0, Nil, z1))
   PERMUTE(Nil) -> c6
   MAPCONSAPP(z0, Cons(z1, z2), z3) -> c7(MAPCONSAPP(z0, z2, z3))
   MAPCONSAPP(z0, Nil, z1) -> c8
   GOAL(z0) -> c9(PERMUTE(z0))

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

   select(z0, z1, Cons(z2, z3)) -> mapconsapp(z0, permute(revapp(z1, Cons(z2, z3))), select(z2, Cons(z0, z1), z3))
   select(z0, z1, Nil) -> mapconsapp(z0, permute(revapp(z1, Nil)), Nil)
   revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
   revapp(Nil, z0) -> z0
   permute(Cons(z0, z1)) -> select(z0, Nil, z1)
   permute(Nil) -> Cons(Nil, Nil)
   mapconsapp(z0, Cons(z1, z2), z3) -> Cons(Cons(z0, z1), mapconsapp(z0, z2, z3))
   mapconsapp(z0, Nil, z1) -> z1
   goal(z0) -> permute(z0)

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

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

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


The TRS R consists of the following rules:

   SELECT(z0, z1, Cons(z2, z3)) -> c(MAPCONSAPP(z0, permute(revapp(z1, Cons(z2, z3))), select(z2, Cons(z0, z1), z3)), PERMUTE(revapp(z1, Cons(z2, z3))), REVAPP(z1, Cons(z2, z3)))
   SELECT(z0, z1, Cons(z2, z3)) -> c1(MAPCONSAPP(z0, permute(revapp(z1, Cons(z2, z3))), select(z2, Cons(z0, z1), z3)), SELECT(z2, Cons(z0, z1), z3))
   SELECT(z0, z1, Nil) -> c2(MAPCONSAPP(z0, permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c3(REVAPP(z1, Cons(z0, z2)))
   REVAPP(Nil, z0) -> c4
   PERMUTE(Cons(z0, z1)) -> c5(SELECT(z0, Nil, z1))
   PERMUTE(Nil) -> c6
   MAPCONSAPP(z0, Cons(z1, z2), z3) -> c7(MAPCONSAPP(z0, z2, z3))
   MAPCONSAPP(z0, Nil, z1) -> c8
   GOAL(z0) -> c9(PERMUTE(z0))

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

   select(z0, z1, Cons(z2, z3)) -> mapconsapp(z0, permute(revapp(z1, Cons(z2, z3))), select(z2, Cons(z0, z1), z3))
   select(z0, z1, Nil) -> mapconsapp(z0, permute(revapp(z1, Nil)), Nil)
   revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
   revapp(Nil, z0) -> z0
   permute(Cons(z0, z1)) -> select(z0, Nil, z1)
   permute(Nil) -> Cons(Nil, Nil)
   mapconsapp(z0, Cons(z1, z2), z3) -> Cons(Cons(z0, z1), mapconsapp(z0, z2, z3))
   mapconsapp(z0, Nil, z1) -> z1
   goal(z0) -> permute(z0)

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

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

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

   SELECT(z0, z1, Cons(z2, z3)) -> c(MAPCONSAPP(z0, permute(revapp(z1, Cons(z2, z3))), select(z2, Cons(z0, z1), z3)), PERMUTE(revapp(z1, Cons(z2, z3))), REVAPP(z1, Cons(z2, z3)))
   SELECT(z0, z1, Cons(z2, z3)) -> c1(MAPCONSAPP(z0, permute(revapp(z1, Cons(z2, z3))), select(z2, Cons(z0, z1), z3)), SELECT(z2, Cons(z0, z1), z3))
   SELECT(z0, z1, Nil) -> c2(MAPCONSAPP(z0, permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1, Nil))
   REVAPP(Cons(z0, z1), z2) -> c3(REVAPP(z1, Cons(z0, z2)))
   REVAPP(Nil, z0) -> c4
   PERMUTE(Cons(z0, z1)) -> c5(SELECT(z0, Nil, z1))
   PERMUTE(Nil) -> c6
   MAPCONSAPP(z0, Cons(z1, z2), z3) -> c7(MAPCONSAPP(z0, z2, z3))
   MAPCONSAPP(z0, Nil, z1) -> c8
   GOAL(z0) -> c9(PERMUTE(z0))

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

   select(z0, z1, Cons(z2, z3)) -> mapconsapp(z0, permute(revapp(z1, Cons(z2, z3))), select(z2, Cons(z0, z1), z3))
   select(z0, z1, Nil) -> mapconsapp(z0, permute(revapp(z1, Nil)), Nil)
   revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
   revapp(Nil, z0) -> z0
   permute(Cons(z0, z1)) -> select(z0, Nil, z1)
   permute(Nil) -> Cons(Nil, Nil)
   mapconsapp(z0, Cons(z1, z2), z3) -> Cons(Cons(z0, z1), mapconsapp(z0, z2, z3))
   mapconsapp(z0, Nil, z1) -> z1
   goal(z0) -> permute(z0)

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
SELECT/0
Cons/0
MAPCONSAPP/0
select/0
REVAPP/1
mapconsapp/0

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

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

   SELECT(z1, Cons(z3)) -> c(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), PERMUTE(revapp(z1, Cons(z3))), REVAPP(z1, Cons(z3)))
   SELECT(z1, Cons(z3)) -> c1(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), SELECT(z2, Cons(z1), z3))
   SELECT(z1, Nil) -> c2(MAPCONSAPP(permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1))
   REVAPP(Cons(z1)) -> c3(REVAPP(z1))
   REVAPP(Nil) -> c4
   PERMUTE(Cons(z1)) -> c5(SELECT(Nil, z1))
   PERMUTE(Nil) -> c6
   MAPCONSAPP(Cons(z2), z3) -> c7(MAPCONSAPP(z2, z3))
   MAPCONSAPP(Nil, z1) -> c8
   GOAL(z0) -> c9(PERMUTE(z0))

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

   select(z1, Cons(z3)) -> mapconsapp(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3))
   select(z1, Nil) -> mapconsapp(permute(revapp(z1, Nil)), Nil)
   revapp(Cons(z1), z2) -> revapp(z1, Cons(z2))
   revapp(Nil, z0) -> z0
   permute(Cons(z1)) -> select(Nil, z1)
   permute(Nil) -> Cons(Nil)
   mapconsapp(Cons(z2), z3) -> Cons(mapconsapp(z2, z3))
   mapconsapp(Nil, z1) -> z1
   goal(z0) -> permute(z0)

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

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

(8)
Obligation:
Innermost TRS:
Rules:
SELECT(z1, Cons(z3)) -> c(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), PERMUTE(revapp(z1, Cons(z3))), REVAPP(z1, Cons(z3)))
SELECT(z1, Cons(z3)) -> c1(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), SELECT(z2, Cons(z1), z3))
SELECT(z1, Nil) -> c2(MAPCONSAPP(permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1))
REVAPP(Cons(z1)) -> c3(REVAPP(z1))
REVAPP(Nil) -> c4
PERMUTE(Cons(z1)) -> c5(SELECT(Nil, z1))
PERMUTE(Nil) -> c6
MAPCONSAPP(Cons(z2), z3) -> c7(MAPCONSAPP(z2, z3))
MAPCONSAPP(Nil, z1) -> c8
GOAL(z0) -> c9(PERMUTE(z0))
select(z1, Cons(z3)) -> mapconsapp(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3))
select(z1, Nil) -> mapconsapp(permute(revapp(z1, Nil)), Nil)
revapp(Cons(z1), z2) -> revapp(z1, Cons(z2))
revapp(Nil, z0) -> z0
permute(Cons(z1)) -> select(Nil, z1)
permute(Nil) -> Cons(Nil)
mapconsapp(Cons(z2), z3) -> Cons(mapconsapp(z2, z3))
mapconsapp(Nil, z1) -> z1
goal(z0) -> permute(z0)

Types:
SELECT :: Cons:Nil -> Cons:Nil -> c:c1:c2
Cons :: Cons:Nil -> Cons:Nil
c :: c7:c8 -> c5:c6 -> REVAPP -> c:c1:c2
MAPCONSAPP :: Cons:Nil -> Cons:Nil -> c7:c8
permute :: Cons:Nil -> Cons:Nil
revapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
select :: Cons:Nil -> Cons:Nil -> Cons:Nil
PERMUTE :: Cons:Nil -> c5:c6
REVAPP :: Cons:Nil -> Cons:Nil -> REVAPP
c1 :: c7:c8 -> SELECT -> c:c1:c2
SELECT :: z2 -> Cons:Nil -> Cons:Nil -> SELECT
z2 :: z2
Nil :: Cons:Nil
c2 :: c7:c8 -> c5:c6 -> c3:c4 -> c:c1:c2
REVAPP :: Cons:Nil -> c3:c4
c3 :: c3:c4 -> c3:c4
c4 :: c3:c4
c5 :: c:c1:c2 -> c5:c6
c6 :: c5:c6
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8
GOAL :: Cons:Nil -> c9
c9 :: c5:c6 -> c9
mapconsapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil
hole_c:c1:c21_10 :: c:c1:c2
hole_Cons:Nil2_10 :: Cons:Nil
hole_c7:c83_10 :: c7:c8
hole_c5:c64_10 :: c5:c6
hole_REVAPP5_10 :: REVAPP
hole_SELECT6_10 :: SELECT
hole_z27_10 :: z2
hole_c3:c48_10 :: c3:c4
hole_c99_10 :: c9
gen_Cons:Nil10_10 :: Nat -> Cons:Nil
gen_c7:c811_10 :: Nat -> c7:c8
gen_c3:c412_10 :: Nat -> c3:c4

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MAPCONSAPP, permute, revapp, select, PERMUTE, REVAPP, mapconsapp

They will be analysed ascendingly in the following order:
MAPCONSAPP < PERMUTE
permute = select
permute < PERMUTE
revapp < select
revapp < PERMUTE
select < PERMUTE
mapconsapp < select
REVAPP < PERMUTE

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

(10)
Obligation:
Innermost TRS:
Rules:
SELECT(z1, Cons(z3)) -> c(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), PERMUTE(revapp(z1, Cons(z3))), REVAPP(z1, Cons(z3)))
SELECT(z1, Cons(z3)) -> c1(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), SELECT(z2, Cons(z1), z3))
SELECT(z1, Nil) -> c2(MAPCONSAPP(permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1))
REVAPP(Cons(z1)) -> c3(REVAPP(z1))
REVAPP(Nil) -> c4
PERMUTE(Cons(z1)) -> c5(SELECT(Nil, z1))
PERMUTE(Nil) -> c6
MAPCONSAPP(Cons(z2), z3) -> c7(MAPCONSAPP(z2, z3))
MAPCONSAPP(Nil, z1) -> c8
GOAL(z0) -> c9(PERMUTE(z0))
select(z1, Cons(z3)) -> mapconsapp(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3))
select(z1, Nil) -> mapconsapp(permute(revapp(z1, Nil)), Nil)
revapp(Cons(z1), z2) -> revapp(z1, Cons(z2))
revapp(Nil, z0) -> z0
permute(Cons(z1)) -> select(Nil, z1)
permute(Nil) -> Cons(Nil)
mapconsapp(Cons(z2), z3) -> Cons(mapconsapp(z2, z3))
mapconsapp(Nil, z1) -> z1
goal(z0) -> permute(z0)

Types:
SELECT :: Cons:Nil -> Cons:Nil -> c:c1:c2
Cons :: Cons:Nil -> Cons:Nil
c :: c7:c8 -> c5:c6 -> REVAPP -> c:c1:c2
MAPCONSAPP :: Cons:Nil -> Cons:Nil -> c7:c8
permute :: Cons:Nil -> Cons:Nil
revapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
select :: Cons:Nil -> Cons:Nil -> Cons:Nil
PERMUTE :: Cons:Nil -> c5:c6
REVAPP :: Cons:Nil -> Cons:Nil -> REVAPP
c1 :: c7:c8 -> SELECT -> c:c1:c2
SELECT :: z2 -> Cons:Nil -> Cons:Nil -> SELECT
z2 :: z2
Nil :: Cons:Nil
c2 :: c7:c8 -> c5:c6 -> c3:c4 -> c:c1:c2
REVAPP :: Cons:Nil -> c3:c4
c3 :: c3:c4 -> c3:c4
c4 :: c3:c4
c5 :: c:c1:c2 -> c5:c6
c6 :: c5:c6
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8
GOAL :: Cons:Nil -> c9
c9 :: c5:c6 -> c9
mapconsapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil
hole_c:c1:c21_10 :: c:c1:c2
hole_Cons:Nil2_10 :: Cons:Nil
hole_c7:c83_10 :: c7:c8
hole_c5:c64_10 :: c5:c6
hole_REVAPP5_10 :: REVAPP
hole_SELECT6_10 :: SELECT
hole_z27_10 :: z2
hole_c3:c48_10 :: c3:c4
hole_c99_10 :: c9
gen_Cons:Nil10_10 :: Nat -> Cons:Nil
gen_c7:c811_10 :: Nat -> c7:c8
gen_c3:c412_10 :: Nat -> c3:c4


Generator Equations:
gen_Cons:Nil10_10(0) <=> Nil
gen_Cons:Nil10_10(+(x, 1)) <=> Cons(gen_Cons:Nil10_10(x))
gen_c7:c811_10(0) <=> c8
gen_c7:c811_10(+(x, 1)) <=> c7(gen_c7:c811_10(x))
gen_c3:c412_10(0) <=> c4
gen_c3:c412_10(+(x, 1)) <=> c3(gen_c3:c412_10(x))


The following defined symbols remain to be analysed:
MAPCONSAPP, permute, revapp, select, PERMUTE, REVAPP, mapconsapp

They will be analysed ascendingly in the following order:
MAPCONSAPP < PERMUTE
permute = select
permute < PERMUTE
revapp < select
revapp < PERMUTE
select < PERMUTE
mapconsapp < select
REVAPP < PERMUTE

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MAPCONSAPP(gen_Cons:Nil10_10(n14_10), gen_Cons:Nil10_10(b)) -> gen_c7:c811_10(n14_10), rt in Omega(1 + n14_10)

Induction Base:
MAPCONSAPP(gen_Cons:Nil10_10(0), gen_Cons:Nil10_10(b)) ->_R^Omega(1)
c8

Induction Step:
MAPCONSAPP(gen_Cons:Nil10_10(+(n14_10, 1)), gen_Cons:Nil10_10(b)) ->_R^Omega(1)
c7(MAPCONSAPP(gen_Cons:Nil10_10(n14_10), gen_Cons:Nil10_10(b))) ->_IH
c7(gen_c7:c811_10(c15_10))

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:
SELECT(z1, Cons(z3)) -> c(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), PERMUTE(revapp(z1, Cons(z3))), REVAPP(z1, Cons(z3)))
SELECT(z1, Cons(z3)) -> c1(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), SELECT(z2, Cons(z1), z3))
SELECT(z1, Nil) -> c2(MAPCONSAPP(permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1))
REVAPP(Cons(z1)) -> c3(REVAPP(z1))
REVAPP(Nil) -> c4
PERMUTE(Cons(z1)) -> c5(SELECT(Nil, z1))
PERMUTE(Nil) -> c6
MAPCONSAPP(Cons(z2), z3) -> c7(MAPCONSAPP(z2, z3))
MAPCONSAPP(Nil, z1) -> c8
GOAL(z0) -> c9(PERMUTE(z0))
select(z1, Cons(z3)) -> mapconsapp(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3))
select(z1, Nil) -> mapconsapp(permute(revapp(z1, Nil)), Nil)
revapp(Cons(z1), z2) -> revapp(z1, Cons(z2))
revapp(Nil, z0) -> z0
permute(Cons(z1)) -> select(Nil, z1)
permute(Nil) -> Cons(Nil)
mapconsapp(Cons(z2), z3) -> Cons(mapconsapp(z2, z3))
mapconsapp(Nil, z1) -> z1
goal(z0) -> permute(z0)

Types:
SELECT :: Cons:Nil -> Cons:Nil -> c:c1:c2
Cons :: Cons:Nil -> Cons:Nil
c :: c7:c8 -> c5:c6 -> REVAPP -> c:c1:c2
MAPCONSAPP :: Cons:Nil -> Cons:Nil -> c7:c8
permute :: Cons:Nil -> Cons:Nil
revapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
select :: Cons:Nil -> Cons:Nil -> Cons:Nil
PERMUTE :: Cons:Nil -> c5:c6
REVAPP :: Cons:Nil -> Cons:Nil -> REVAPP
c1 :: c7:c8 -> SELECT -> c:c1:c2
SELECT :: z2 -> Cons:Nil -> Cons:Nil -> SELECT
z2 :: z2
Nil :: Cons:Nil
c2 :: c7:c8 -> c5:c6 -> c3:c4 -> c:c1:c2
REVAPP :: Cons:Nil -> c3:c4
c3 :: c3:c4 -> c3:c4
c4 :: c3:c4
c5 :: c:c1:c2 -> c5:c6
c6 :: c5:c6
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8
GOAL :: Cons:Nil -> c9
c9 :: c5:c6 -> c9
mapconsapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil
hole_c:c1:c21_10 :: c:c1:c2
hole_Cons:Nil2_10 :: Cons:Nil
hole_c7:c83_10 :: c7:c8
hole_c5:c64_10 :: c5:c6
hole_REVAPP5_10 :: REVAPP
hole_SELECT6_10 :: SELECT
hole_z27_10 :: z2
hole_c3:c48_10 :: c3:c4
hole_c99_10 :: c9
gen_Cons:Nil10_10 :: Nat -> Cons:Nil
gen_c7:c811_10 :: Nat -> c7:c8
gen_c3:c412_10 :: Nat -> c3:c4


Generator Equations:
gen_Cons:Nil10_10(0) <=> Nil
gen_Cons:Nil10_10(+(x, 1)) <=> Cons(gen_Cons:Nil10_10(x))
gen_c7:c811_10(0) <=> c8
gen_c7:c811_10(+(x, 1)) <=> c7(gen_c7:c811_10(x))
gen_c3:c412_10(0) <=> c4
gen_c3:c412_10(+(x, 1)) <=> c3(gen_c3:c412_10(x))


The following defined symbols remain to be analysed:
MAPCONSAPP, permute, revapp, select, PERMUTE, REVAPP, mapconsapp

They will be analysed ascendingly in the following order:
MAPCONSAPP < PERMUTE
permute = select
permute < PERMUTE
revapp < select
revapp < PERMUTE
select < PERMUTE
mapconsapp < select
REVAPP < PERMUTE

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
SELECT(z1, Cons(z3)) -> c(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), PERMUTE(revapp(z1, Cons(z3))), REVAPP(z1, Cons(z3)))
SELECT(z1, Cons(z3)) -> c1(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), SELECT(z2, Cons(z1), z3))
SELECT(z1, Nil) -> c2(MAPCONSAPP(permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1))
REVAPP(Cons(z1)) -> c3(REVAPP(z1))
REVAPP(Nil) -> c4
PERMUTE(Cons(z1)) -> c5(SELECT(Nil, z1))
PERMUTE(Nil) -> c6
MAPCONSAPP(Cons(z2), z3) -> c7(MAPCONSAPP(z2, z3))
MAPCONSAPP(Nil, z1) -> c8
GOAL(z0) -> c9(PERMUTE(z0))
select(z1, Cons(z3)) -> mapconsapp(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3))
select(z1, Nil) -> mapconsapp(permute(revapp(z1, Nil)), Nil)
revapp(Cons(z1), z2) -> revapp(z1, Cons(z2))
revapp(Nil, z0) -> z0
permute(Cons(z1)) -> select(Nil, z1)
permute(Nil) -> Cons(Nil)
mapconsapp(Cons(z2), z3) -> Cons(mapconsapp(z2, z3))
mapconsapp(Nil, z1) -> z1
goal(z0) -> permute(z0)

Types:
SELECT :: Cons:Nil -> Cons:Nil -> c:c1:c2
Cons :: Cons:Nil -> Cons:Nil
c :: c7:c8 -> c5:c6 -> REVAPP -> c:c1:c2
MAPCONSAPP :: Cons:Nil -> Cons:Nil -> c7:c8
permute :: Cons:Nil -> Cons:Nil
revapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
select :: Cons:Nil -> Cons:Nil -> Cons:Nil
PERMUTE :: Cons:Nil -> c5:c6
REVAPP :: Cons:Nil -> Cons:Nil -> REVAPP
c1 :: c7:c8 -> SELECT -> c:c1:c2
SELECT :: z2 -> Cons:Nil -> Cons:Nil -> SELECT
z2 :: z2
Nil :: Cons:Nil
c2 :: c7:c8 -> c5:c6 -> c3:c4 -> c:c1:c2
REVAPP :: Cons:Nil -> c3:c4
c3 :: c3:c4 -> c3:c4
c4 :: c3:c4
c5 :: c:c1:c2 -> c5:c6
c6 :: c5:c6
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8
GOAL :: Cons:Nil -> c9
c9 :: c5:c6 -> c9
mapconsapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil
hole_c:c1:c21_10 :: c:c1:c2
hole_Cons:Nil2_10 :: Cons:Nil
hole_c7:c83_10 :: c7:c8
hole_c5:c64_10 :: c5:c6
hole_REVAPP5_10 :: REVAPP
hole_SELECT6_10 :: SELECT
hole_z27_10 :: z2
hole_c3:c48_10 :: c3:c4
hole_c99_10 :: c9
gen_Cons:Nil10_10 :: Nat -> Cons:Nil
gen_c7:c811_10 :: Nat -> c7:c8
gen_c3:c412_10 :: Nat -> c3:c4


Lemmas:
MAPCONSAPP(gen_Cons:Nil10_10(n14_10), gen_Cons:Nil10_10(b)) -> gen_c7:c811_10(n14_10), rt in Omega(1 + n14_10)


Generator Equations:
gen_Cons:Nil10_10(0) <=> Nil
gen_Cons:Nil10_10(+(x, 1)) <=> Cons(gen_Cons:Nil10_10(x))
gen_c7:c811_10(0) <=> c8
gen_c7:c811_10(+(x, 1)) <=> c7(gen_c7:c811_10(x))
gen_c3:c412_10(0) <=> c4
gen_c3:c412_10(+(x, 1)) <=> c3(gen_c3:c412_10(x))


The following defined symbols remain to be analysed:
revapp, permute, select, PERMUTE, REVAPP, mapconsapp

They will be analysed ascendingly in the following order:
permute = select
permute < PERMUTE
revapp < select
revapp < PERMUTE
select < PERMUTE
mapconsapp < select
REVAPP < PERMUTE

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
revapp(gen_Cons:Nil10_10(n561_10), gen_Cons:Nil10_10(b)) -> gen_Cons:Nil10_10(+(n561_10, b)), rt in Omega(0)

Induction Base:
revapp(gen_Cons:Nil10_10(0), gen_Cons:Nil10_10(b)) ->_R^Omega(0)
gen_Cons:Nil10_10(b)

Induction Step:
revapp(gen_Cons:Nil10_10(+(n561_10, 1)), gen_Cons:Nil10_10(b)) ->_R^Omega(0)
revapp(gen_Cons:Nil10_10(n561_10), Cons(gen_Cons:Nil10_10(b))) ->_IH
gen_Cons:Nil10_10(+(+(b, 1), c562_10))

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

(18)
Obligation:
Innermost TRS:
Rules:
SELECT(z1, Cons(z3)) -> c(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), PERMUTE(revapp(z1, Cons(z3))), REVAPP(z1, Cons(z3)))
SELECT(z1, Cons(z3)) -> c1(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), SELECT(z2, Cons(z1), z3))
SELECT(z1, Nil) -> c2(MAPCONSAPP(permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1))
REVAPP(Cons(z1)) -> c3(REVAPP(z1))
REVAPP(Nil) -> c4
PERMUTE(Cons(z1)) -> c5(SELECT(Nil, z1))
PERMUTE(Nil) -> c6
MAPCONSAPP(Cons(z2), z3) -> c7(MAPCONSAPP(z2, z3))
MAPCONSAPP(Nil, z1) -> c8
GOAL(z0) -> c9(PERMUTE(z0))
select(z1, Cons(z3)) -> mapconsapp(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3))
select(z1, Nil) -> mapconsapp(permute(revapp(z1, Nil)), Nil)
revapp(Cons(z1), z2) -> revapp(z1, Cons(z2))
revapp(Nil, z0) -> z0
permute(Cons(z1)) -> select(Nil, z1)
permute(Nil) -> Cons(Nil)
mapconsapp(Cons(z2), z3) -> Cons(mapconsapp(z2, z3))
mapconsapp(Nil, z1) -> z1
goal(z0) -> permute(z0)

Types:
SELECT :: Cons:Nil -> Cons:Nil -> c:c1:c2
Cons :: Cons:Nil -> Cons:Nil
c :: c7:c8 -> c5:c6 -> REVAPP -> c:c1:c2
MAPCONSAPP :: Cons:Nil -> Cons:Nil -> c7:c8
permute :: Cons:Nil -> Cons:Nil
revapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
select :: Cons:Nil -> Cons:Nil -> Cons:Nil
PERMUTE :: Cons:Nil -> c5:c6
REVAPP :: Cons:Nil -> Cons:Nil -> REVAPP
c1 :: c7:c8 -> SELECT -> c:c1:c2
SELECT :: z2 -> Cons:Nil -> Cons:Nil -> SELECT
z2 :: z2
Nil :: Cons:Nil
c2 :: c7:c8 -> c5:c6 -> c3:c4 -> c:c1:c2
REVAPP :: Cons:Nil -> c3:c4
c3 :: c3:c4 -> c3:c4
c4 :: c3:c4
c5 :: c:c1:c2 -> c5:c6
c6 :: c5:c6
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8
GOAL :: Cons:Nil -> c9
c9 :: c5:c6 -> c9
mapconsapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil
hole_c:c1:c21_10 :: c:c1:c2
hole_Cons:Nil2_10 :: Cons:Nil
hole_c7:c83_10 :: c7:c8
hole_c5:c64_10 :: c5:c6
hole_REVAPP5_10 :: REVAPP
hole_SELECT6_10 :: SELECT
hole_z27_10 :: z2
hole_c3:c48_10 :: c3:c4
hole_c99_10 :: c9
gen_Cons:Nil10_10 :: Nat -> Cons:Nil
gen_c7:c811_10 :: Nat -> c7:c8
gen_c3:c412_10 :: Nat -> c3:c4


Lemmas:
MAPCONSAPP(gen_Cons:Nil10_10(n14_10), gen_Cons:Nil10_10(b)) -> gen_c7:c811_10(n14_10), rt in Omega(1 + n14_10)
revapp(gen_Cons:Nil10_10(n561_10), gen_Cons:Nil10_10(b)) -> gen_Cons:Nil10_10(+(n561_10, b)), rt in Omega(0)


Generator Equations:
gen_Cons:Nil10_10(0) <=> Nil
gen_Cons:Nil10_10(+(x, 1)) <=> Cons(gen_Cons:Nil10_10(x))
gen_c7:c811_10(0) <=> c8
gen_c7:c811_10(+(x, 1)) <=> c7(gen_c7:c811_10(x))
gen_c3:c412_10(0) <=> c4
gen_c3:c412_10(+(x, 1)) <=> c3(gen_c3:c412_10(x))


The following defined symbols remain to be analysed:
REVAPP, permute, select, PERMUTE, mapconsapp

They will be analysed ascendingly in the following order:
permute = select
permute < PERMUTE
select < PERMUTE
mapconsapp < select
REVAPP < PERMUTE

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REVAPP(gen_Cons:Nil10_10(n1535_10)) -> gen_c3:c412_10(n1535_10), rt in Omega(1 + n1535_10)

Induction Base:
REVAPP(gen_Cons:Nil10_10(0)) ->_R^Omega(1)
c4

Induction Step:
REVAPP(gen_Cons:Nil10_10(+(n1535_10, 1))) ->_R^Omega(1)
c3(REVAPP(gen_Cons:Nil10_10(n1535_10))) ->_IH
c3(gen_c3:c412_10(c1536_10))

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

(20)
Obligation:
Innermost TRS:
Rules:
SELECT(z1, Cons(z3)) -> c(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), PERMUTE(revapp(z1, Cons(z3))), REVAPP(z1, Cons(z3)))
SELECT(z1, Cons(z3)) -> c1(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), SELECT(z2, Cons(z1), z3))
SELECT(z1, Nil) -> c2(MAPCONSAPP(permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1))
REVAPP(Cons(z1)) -> c3(REVAPP(z1))
REVAPP(Nil) -> c4
PERMUTE(Cons(z1)) -> c5(SELECT(Nil, z1))
PERMUTE(Nil) -> c6
MAPCONSAPP(Cons(z2), z3) -> c7(MAPCONSAPP(z2, z3))
MAPCONSAPP(Nil, z1) -> c8
GOAL(z0) -> c9(PERMUTE(z0))
select(z1, Cons(z3)) -> mapconsapp(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3))
select(z1, Nil) -> mapconsapp(permute(revapp(z1, Nil)), Nil)
revapp(Cons(z1), z2) -> revapp(z1, Cons(z2))
revapp(Nil, z0) -> z0
permute(Cons(z1)) -> select(Nil, z1)
permute(Nil) -> Cons(Nil)
mapconsapp(Cons(z2), z3) -> Cons(mapconsapp(z2, z3))
mapconsapp(Nil, z1) -> z1
goal(z0) -> permute(z0)

Types:
SELECT :: Cons:Nil -> Cons:Nil -> c:c1:c2
Cons :: Cons:Nil -> Cons:Nil
c :: c7:c8 -> c5:c6 -> REVAPP -> c:c1:c2
MAPCONSAPP :: Cons:Nil -> Cons:Nil -> c7:c8
permute :: Cons:Nil -> Cons:Nil
revapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
select :: Cons:Nil -> Cons:Nil -> Cons:Nil
PERMUTE :: Cons:Nil -> c5:c6
REVAPP :: Cons:Nil -> Cons:Nil -> REVAPP
c1 :: c7:c8 -> SELECT -> c:c1:c2
SELECT :: z2 -> Cons:Nil -> Cons:Nil -> SELECT
z2 :: z2
Nil :: Cons:Nil
c2 :: c7:c8 -> c5:c6 -> c3:c4 -> c:c1:c2
REVAPP :: Cons:Nil -> c3:c4
c3 :: c3:c4 -> c3:c4
c4 :: c3:c4
c5 :: c:c1:c2 -> c5:c6
c6 :: c5:c6
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8
GOAL :: Cons:Nil -> c9
c9 :: c5:c6 -> c9
mapconsapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil
hole_c:c1:c21_10 :: c:c1:c2
hole_Cons:Nil2_10 :: Cons:Nil
hole_c7:c83_10 :: c7:c8
hole_c5:c64_10 :: c5:c6
hole_REVAPP5_10 :: REVAPP
hole_SELECT6_10 :: SELECT
hole_z27_10 :: z2
hole_c3:c48_10 :: c3:c4
hole_c99_10 :: c9
gen_Cons:Nil10_10 :: Nat -> Cons:Nil
gen_c7:c811_10 :: Nat -> c7:c8
gen_c3:c412_10 :: Nat -> c3:c4


Lemmas:
MAPCONSAPP(gen_Cons:Nil10_10(n14_10), gen_Cons:Nil10_10(b)) -> gen_c7:c811_10(n14_10), rt in Omega(1 + n14_10)
revapp(gen_Cons:Nil10_10(n561_10), gen_Cons:Nil10_10(b)) -> gen_Cons:Nil10_10(+(n561_10, b)), rt in Omega(0)
REVAPP(gen_Cons:Nil10_10(n1535_10)) -> gen_c3:c412_10(n1535_10), rt in Omega(1 + n1535_10)


Generator Equations:
gen_Cons:Nil10_10(0) <=> Nil
gen_Cons:Nil10_10(+(x, 1)) <=> Cons(gen_Cons:Nil10_10(x))
gen_c7:c811_10(0) <=> c8
gen_c7:c811_10(+(x, 1)) <=> c7(gen_c7:c811_10(x))
gen_c3:c412_10(0) <=> c4
gen_c3:c412_10(+(x, 1)) <=> c3(gen_c3:c412_10(x))


The following defined symbols remain to be analysed:
mapconsapp, permute, select, PERMUTE

They will be analysed ascendingly in the following order:
permute = select
permute < PERMUTE
select < PERMUTE
mapconsapp < select

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
mapconsapp(gen_Cons:Nil10_10(n1869_10), gen_Cons:Nil10_10(b)) -> gen_Cons:Nil10_10(+(n1869_10, b)), rt in Omega(0)

Induction Base:
mapconsapp(gen_Cons:Nil10_10(0), gen_Cons:Nil10_10(b)) ->_R^Omega(0)
gen_Cons:Nil10_10(b)

Induction Step:
mapconsapp(gen_Cons:Nil10_10(+(n1869_10, 1)), gen_Cons:Nil10_10(b)) ->_R^Omega(0)
Cons(mapconsapp(gen_Cons:Nil10_10(n1869_10), gen_Cons:Nil10_10(b))) ->_IH
Cons(gen_Cons:Nil10_10(+(b, c1870_10)))

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

(22)
Obligation:
Innermost TRS:
Rules:
SELECT(z1, Cons(z3)) -> c(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), PERMUTE(revapp(z1, Cons(z3))), REVAPP(z1, Cons(z3)))
SELECT(z1, Cons(z3)) -> c1(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), SELECT(z2, Cons(z1), z3))
SELECT(z1, Nil) -> c2(MAPCONSAPP(permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1))
REVAPP(Cons(z1)) -> c3(REVAPP(z1))
REVAPP(Nil) -> c4
PERMUTE(Cons(z1)) -> c5(SELECT(Nil, z1))
PERMUTE(Nil) -> c6
MAPCONSAPP(Cons(z2), z3) -> c7(MAPCONSAPP(z2, z3))
MAPCONSAPP(Nil, z1) -> c8
GOAL(z0) -> c9(PERMUTE(z0))
select(z1, Cons(z3)) -> mapconsapp(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3))
select(z1, Nil) -> mapconsapp(permute(revapp(z1, Nil)), Nil)
revapp(Cons(z1), z2) -> revapp(z1, Cons(z2))
revapp(Nil, z0) -> z0
permute(Cons(z1)) -> select(Nil, z1)
permute(Nil) -> Cons(Nil)
mapconsapp(Cons(z2), z3) -> Cons(mapconsapp(z2, z3))
mapconsapp(Nil, z1) -> z1
goal(z0) -> permute(z0)

Types:
SELECT :: Cons:Nil -> Cons:Nil -> c:c1:c2
Cons :: Cons:Nil -> Cons:Nil
c :: c7:c8 -> c5:c6 -> REVAPP -> c:c1:c2
MAPCONSAPP :: Cons:Nil -> Cons:Nil -> c7:c8
permute :: Cons:Nil -> Cons:Nil
revapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
select :: Cons:Nil -> Cons:Nil -> Cons:Nil
PERMUTE :: Cons:Nil -> c5:c6
REVAPP :: Cons:Nil -> Cons:Nil -> REVAPP
c1 :: c7:c8 -> SELECT -> c:c1:c2
SELECT :: z2 -> Cons:Nil -> Cons:Nil -> SELECT
z2 :: z2
Nil :: Cons:Nil
c2 :: c7:c8 -> c5:c6 -> c3:c4 -> c:c1:c2
REVAPP :: Cons:Nil -> c3:c4
c3 :: c3:c4 -> c3:c4
c4 :: c3:c4
c5 :: c:c1:c2 -> c5:c6
c6 :: c5:c6
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8
GOAL :: Cons:Nil -> c9
c9 :: c5:c6 -> c9
mapconsapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil
hole_c:c1:c21_10 :: c:c1:c2
hole_Cons:Nil2_10 :: Cons:Nil
hole_c7:c83_10 :: c7:c8
hole_c5:c64_10 :: c5:c6
hole_REVAPP5_10 :: REVAPP
hole_SELECT6_10 :: SELECT
hole_z27_10 :: z2
hole_c3:c48_10 :: c3:c4
hole_c99_10 :: c9
gen_Cons:Nil10_10 :: Nat -> Cons:Nil
gen_c7:c811_10 :: Nat -> c7:c8
gen_c3:c412_10 :: Nat -> c3:c4


Lemmas:
MAPCONSAPP(gen_Cons:Nil10_10(n14_10), gen_Cons:Nil10_10(b)) -> gen_c7:c811_10(n14_10), rt in Omega(1 + n14_10)
revapp(gen_Cons:Nil10_10(n561_10), gen_Cons:Nil10_10(b)) -> gen_Cons:Nil10_10(+(n561_10, b)), rt in Omega(0)
REVAPP(gen_Cons:Nil10_10(n1535_10)) -> gen_c3:c412_10(n1535_10), rt in Omega(1 + n1535_10)
mapconsapp(gen_Cons:Nil10_10(n1869_10), gen_Cons:Nil10_10(b)) -> gen_Cons:Nil10_10(+(n1869_10, b)), rt in Omega(0)


Generator Equations:
gen_Cons:Nil10_10(0) <=> Nil
gen_Cons:Nil10_10(+(x, 1)) <=> Cons(gen_Cons:Nil10_10(x))
gen_c7:c811_10(0) <=> c8
gen_c7:c811_10(+(x, 1)) <=> c7(gen_c7:c811_10(x))
gen_c3:c412_10(0) <=> c4
gen_c3:c412_10(+(x, 1)) <=> c3(gen_c3:c412_10(x))


The following defined symbols remain to be analysed:
select, permute, PERMUTE

They will be analysed ascendingly in the following order:
permute = select
permute < PERMUTE
select < PERMUTE

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
select(gen_Cons:Nil10_10(1), gen_Cons:Nil10_10(n2859_10)) -> *13_10, rt in Omega(0)

Induction Base:
select(gen_Cons:Nil10_10(1), gen_Cons:Nil10_10(0))

Induction Step:
select(gen_Cons:Nil10_10(1), gen_Cons:Nil10_10(+(n2859_10, 1))) ->_R^Omega(0)
mapconsapp(permute(revapp(gen_Cons:Nil10_10(1), Cons(gen_Cons:Nil10_10(n2859_10)))), select(Cons(gen_Cons:Nil10_10(1)), gen_Cons:Nil10_10(n2859_10))) ->_L^Omega(0)
mapconsapp(permute(gen_Cons:Nil10_10(+(1, +(n2859_10, 1)))), select(Cons(gen_Cons:Nil10_10(1)), gen_Cons:Nil10_10(n2859_10))) ->_R^Omega(0)
mapconsapp(select(Nil, gen_Cons:Nil10_10(+(1, n2859_10))), select(Cons(gen_Cons:Nil10_10(1)), gen_Cons:Nil10_10(n2859_10))) ->_R^Omega(0)
mapconsapp(mapconsapp(permute(revapp(Nil, Cons(gen_Cons:Nil10_10(n2859_10)))), select(Cons(Nil), gen_Cons:Nil10_10(n2859_10))), select(Cons(gen_Cons:Nil10_10(1)), gen_Cons:Nil10_10(n2859_10))) ->_L^Omega(0)
mapconsapp(mapconsapp(permute(gen_Cons:Nil10_10(+(0, +(n2859_10, 1)))), select(Cons(Nil), gen_Cons:Nil10_10(n2859_10))), select(Cons(gen_Cons:Nil10_10(1)), gen_Cons:Nil10_10(n2859_10))) ->_R^Omega(0)
mapconsapp(mapconsapp(select(Nil, gen_Cons:Nil10_10(n2859_10)), select(Cons(Nil), gen_Cons:Nil10_10(n2859_10))), select(Cons(gen_Cons:Nil10_10(1)), gen_Cons:Nil10_10(n2859_10))) ->_IH
mapconsapp(mapconsapp(select(Nil, gen_Cons:Nil10_10(n2859_10)), *13_10), select(Cons(gen_Cons:Nil10_10(1)), gen_Cons:Nil10_10(n2859_10)))

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:
SELECT(z1, Cons(z3)) -> c(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), PERMUTE(revapp(z1, Cons(z3))), REVAPP(z1, Cons(z3)))
SELECT(z1, Cons(z3)) -> c1(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), SELECT(z2, Cons(z1), z3))
SELECT(z1, Nil) -> c2(MAPCONSAPP(permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1))
REVAPP(Cons(z1)) -> c3(REVAPP(z1))
REVAPP(Nil) -> c4
PERMUTE(Cons(z1)) -> c5(SELECT(Nil, z1))
PERMUTE(Nil) -> c6
MAPCONSAPP(Cons(z2), z3) -> c7(MAPCONSAPP(z2, z3))
MAPCONSAPP(Nil, z1) -> c8
GOAL(z0) -> c9(PERMUTE(z0))
select(z1, Cons(z3)) -> mapconsapp(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3))
select(z1, Nil) -> mapconsapp(permute(revapp(z1, Nil)), Nil)
revapp(Cons(z1), z2) -> revapp(z1, Cons(z2))
revapp(Nil, z0) -> z0
permute(Cons(z1)) -> select(Nil, z1)
permute(Nil) -> Cons(Nil)
mapconsapp(Cons(z2), z3) -> Cons(mapconsapp(z2, z3))
mapconsapp(Nil, z1) -> z1
goal(z0) -> permute(z0)

Types:
SELECT :: Cons:Nil -> Cons:Nil -> c:c1:c2
Cons :: Cons:Nil -> Cons:Nil
c :: c7:c8 -> c5:c6 -> REVAPP -> c:c1:c2
MAPCONSAPP :: Cons:Nil -> Cons:Nil -> c7:c8
permute :: Cons:Nil -> Cons:Nil
revapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
select :: Cons:Nil -> Cons:Nil -> Cons:Nil
PERMUTE :: Cons:Nil -> c5:c6
REVAPP :: Cons:Nil -> Cons:Nil -> REVAPP
c1 :: c7:c8 -> SELECT -> c:c1:c2
SELECT :: z2 -> Cons:Nil -> Cons:Nil -> SELECT
z2 :: z2
Nil :: Cons:Nil
c2 :: c7:c8 -> c5:c6 -> c3:c4 -> c:c1:c2
REVAPP :: Cons:Nil -> c3:c4
c3 :: c3:c4 -> c3:c4
c4 :: c3:c4
c5 :: c:c1:c2 -> c5:c6
c6 :: c5:c6
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8
GOAL :: Cons:Nil -> c9
c9 :: c5:c6 -> c9
mapconsapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil
hole_c:c1:c21_10 :: c:c1:c2
hole_Cons:Nil2_10 :: Cons:Nil
hole_c7:c83_10 :: c7:c8
hole_c5:c64_10 :: c5:c6
hole_REVAPP5_10 :: REVAPP
hole_SELECT6_10 :: SELECT
hole_z27_10 :: z2
hole_c3:c48_10 :: c3:c4
hole_c99_10 :: c9
gen_Cons:Nil10_10 :: Nat -> Cons:Nil
gen_c7:c811_10 :: Nat -> c7:c8
gen_c3:c412_10 :: Nat -> c3:c4


Lemmas:
MAPCONSAPP(gen_Cons:Nil10_10(n14_10), gen_Cons:Nil10_10(b)) -> gen_c7:c811_10(n14_10), rt in Omega(1 + n14_10)
revapp(gen_Cons:Nil10_10(n561_10), gen_Cons:Nil10_10(b)) -> gen_Cons:Nil10_10(+(n561_10, b)), rt in Omega(0)
REVAPP(gen_Cons:Nil10_10(n1535_10)) -> gen_c3:c412_10(n1535_10), rt in Omega(1 + n1535_10)
mapconsapp(gen_Cons:Nil10_10(n1869_10), gen_Cons:Nil10_10(b)) -> gen_Cons:Nil10_10(+(n1869_10, b)), rt in Omega(0)
select(gen_Cons:Nil10_10(1), gen_Cons:Nil10_10(n2859_10)) -> *13_10, rt in Omega(0)


Generator Equations:
gen_Cons:Nil10_10(0) <=> Nil
gen_Cons:Nil10_10(+(x, 1)) <=> Cons(gen_Cons:Nil10_10(x))
gen_c7:c811_10(0) <=> c8
gen_c7:c811_10(+(x, 1)) <=> c7(gen_c7:c811_10(x))
gen_c3:c412_10(0) <=> c4
gen_c3:c412_10(+(x, 1)) <=> c3(gen_c3:c412_10(x))


The following defined symbols remain to be analysed:
permute, PERMUTE

They will be analysed ascendingly in the following order:
permute = select
permute < PERMUTE
select < PERMUTE

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
permute(gen_Cons:Nil10_10(+(1, n8640_10))) -> *13_10, rt in Omega(0)

Induction Base:
permute(gen_Cons:Nil10_10(+(1, 0)))

Induction Step:
permute(gen_Cons:Nil10_10(+(1, +(n8640_10, 1)))) ->_R^Omega(0)
select(Nil, gen_Cons:Nil10_10(+(1, n8640_10))) ->_R^Omega(0)
mapconsapp(permute(revapp(Nil, Cons(gen_Cons:Nil10_10(n8640_10)))), select(Cons(Nil), gen_Cons:Nil10_10(n8640_10))) ->_L^Omega(0)
mapconsapp(permute(gen_Cons:Nil10_10(+(0, +(n8640_10, 1)))), select(Cons(Nil), gen_Cons:Nil10_10(n8640_10))) ->_IH
mapconsapp(*13_10, select(Cons(Nil), gen_Cons:Nil10_10(n8640_10))) ->_L^Omega(0)
mapconsapp(*13_10, *13_10)

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

(26)
Obligation:
Innermost TRS:
Rules:
SELECT(z1, Cons(z3)) -> c(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), PERMUTE(revapp(z1, Cons(z3))), REVAPP(z1, Cons(z3)))
SELECT(z1, Cons(z3)) -> c1(MAPCONSAPP(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3)), SELECT(z2, Cons(z1), z3))
SELECT(z1, Nil) -> c2(MAPCONSAPP(permute(revapp(z1, Nil)), Nil), PERMUTE(revapp(z1, Nil)), REVAPP(z1))
REVAPP(Cons(z1)) -> c3(REVAPP(z1))
REVAPP(Nil) -> c4
PERMUTE(Cons(z1)) -> c5(SELECT(Nil, z1))
PERMUTE(Nil) -> c6
MAPCONSAPP(Cons(z2), z3) -> c7(MAPCONSAPP(z2, z3))
MAPCONSAPP(Nil, z1) -> c8
GOAL(z0) -> c9(PERMUTE(z0))
select(z1, Cons(z3)) -> mapconsapp(permute(revapp(z1, Cons(z3))), select(Cons(z1), z3))
select(z1, Nil) -> mapconsapp(permute(revapp(z1, Nil)), Nil)
revapp(Cons(z1), z2) -> revapp(z1, Cons(z2))
revapp(Nil, z0) -> z0
permute(Cons(z1)) -> select(Nil, z1)
permute(Nil) -> Cons(Nil)
mapconsapp(Cons(z2), z3) -> Cons(mapconsapp(z2, z3))
mapconsapp(Nil, z1) -> z1
goal(z0) -> permute(z0)

Types:
SELECT :: Cons:Nil -> Cons:Nil -> c:c1:c2
Cons :: Cons:Nil -> Cons:Nil
c :: c7:c8 -> c5:c6 -> REVAPP -> c:c1:c2
MAPCONSAPP :: Cons:Nil -> Cons:Nil -> c7:c8
permute :: Cons:Nil -> Cons:Nil
revapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
select :: Cons:Nil -> Cons:Nil -> Cons:Nil
PERMUTE :: Cons:Nil -> c5:c6
REVAPP :: Cons:Nil -> Cons:Nil -> REVAPP
c1 :: c7:c8 -> SELECT -> c:c1:c2
SELECT :: z2 -> Cons:Nil -> Cons:Nil -> SELECT
z2 :: z2
Nil :: Cons:Nil
c2 :: c7:c8 -> c5:c6 -> c3:c4 -> c:c1:c2
REVAPP :: Cons:Nil -> c3:c4
c3 :: c3:c4 -> c3:c4
c4 :: c3:c4
c5 :: c:c1:c2 -> c5:c6
c6 :: c5:c6
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8
GOAL :: Cons:Nil -> c9
c9 :: c5:c6 -> c9
mapconsapp :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil
hole_c:c1:c21_10 :: c:c1:c2
hole_Cons:Nil2_10 :: Cons:Nil
hole_c7:c83_10 :: c7:c8
hole_c5:c64_10 :: c5:c6
hole_REVAPP5_10 :: REVAPP
hole_SELECT6_10 :: SELECT
hole_z27_10 :: z2
hole_c3:c48_10 :: c3:c4
hole_c99_10 :: c9
gen_Cons:Nil10_10 :: Nat -> Cons:Nil
gen_c7:c811_10 :: Nat -> c7:c8
gen_c3:c412_10 :: Nat -> c3:c4


Lemmas:
MAPCONSAPP(gen_Cons:Nil10_10(n14_10), gen_Cons:Nil10_10(b)) -> gen_c7:c811_10(n14_10), rt in Omega(1 + n14_10)
revapp(gen_Cons:Nil10_10(n561_10), gen_Cons:Nil10_10(b)) -> gen_Cons:Nil10_10(+(n561_10, b)), rt in Omega(0)
REVAPP(gen_Cons:Nil10_10(n1535_10)) -> gen_c3:c412_10(n1535_10), rt in Omega(1 + n1535_10)
mapconsapp(gen_Cons:Nil10_10(n1869_10), gen_Cons:Nil10_10(b)) -> gen_Cons:Nil10_10(+(n1869_10, b)), rt in Omega(0)
select(gen_Cons:Nil10_10(1), gen_Cons:Nil10_10(n2859_10)) -> *13_10, rt in Omega(0)
permute(gen_Cons:Nil10_10(+(1, n8640_10))) -> *13_10, rt in Omega(0)


Generator Equations:
gen_Cons:Nil10_10(0) <=> Nil
gen_Cons:Nil10_10(+(x, 1)) <=> Cons(gen_Cons:Nil10_10(x))
gen_c7:c811_10(0) <=> c8
gen_c7:c811_10(+(x, 1)) <=> c7(gen_c7:c811_10(x))
gen_c3:c412_10(0) <=> c4
gen_c3:c412_10(+(x, 1)) <=> c3(gen_c3:c412_10(x))


The following defined symbols remain to be analysed:
select, PERMUTE

They will be analysed ascendingly in the following order:
permute = select
permute < PERMUTE
select < PERMUTE