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


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 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), 3 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 701 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), 31 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 95 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 925 ms]
        (22) BEST
            (23) proven lower bound
                (24) LowerBoundPropagationProof [FINISHED, 0 ms]
                (25) BOUNDS(n^2, INF)
            (26) typed CpxTrs
                (27) RewriteLemmaProof [LOWER BOUND(ID), 65.5 s]
                (28) typed CpxTrs
                (29) RewriteLemmaProof [LOWER BOUND(ID), 64.9 s]
                (30) typed CpxTrs
                (31) RewriteLemmaProof [LOWER BOUND(ID), 64.9 s]
                (32) typed CpxTrs
                (33) RewriteLemmaProof [LOWER BOUND(ID), 2582 ms]
                (34) typed CpxTrs
                (35) RewriteLemmaProof [LOWER BOUND(ID), 2607 ms]
                (36) typed CpxTrs
                (37) RewriteLemmaProof [LOWER BOUND(ID), 2594 ms]
                (38) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   from(X) -> cons(X, from(s(X)))
   2ndspos(0, Z) -> rnil
   2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z))
   2ndsneg(0, Z) -> rnil
   2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z))
   pi(X) -> 2ndspos(X, from(0))
   plus(0, Y) -> Y
   plus(s(X), Y) -> s(plus(X, Y))
   times(0, Y) -> 0
   times(s(X), Y) -> plus(Y, times(X, Y))
   square(X) -> times(X, X)

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:
   from(z0) -> cons(z0, from(s(z0)))
   2ndspos(0, z0) -> rnil
   2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
   2ndsneg(0, z0) -> rnil
   2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
   pi(z0) -> 2ndspos(z0, from(0))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(0, z0) -> 0
   times(s(z0), z1) -> plus(z1, times(z0, z1))
   square(z0) -> times(z0, z0)
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   2NDSPOS(0, z0) -> c1
   2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
   2NDSNEG(0, z0) -> c3
   2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
   PI(z0) -> c5(2NDSPOS(z0, from(0)), FROM(0))
   PLUS(0, z0) -> c6
   PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
   TIMES(0, z0) -> c8
   TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   SQUARE(z0) -> c10(TIMES(z0, z0))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
   2NDSPOS(0, z0) -> c1
   2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
   2NDSNEG(0, z0) -> c3
   2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
   PI(z0) -> c5(2NDSPOS(z0, from(0)), FROM(0))
   PLUS(0, z0) -> c6
   PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
   TIMES(0, z0) -> c8
   TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   SQUARE(z0) -> c10(TIMES(z0, z0))
K tuples:none
Defined Rule Symbols:   from_1, 2ndspos_2, 2ndsneg_2, pi_1, plus_2, times_2, square_1

Defined Pair Symbols:   FROM_1, 2NDSPOS_2, 2NDSNEG_2, PI_1, PLUS_2, TIMES_2, SQUARE_1

Compound Symbols:   c_1, c1, c2_1, c3, c4_1, c5_2, c6, c7_1, c8, c9_2, c10_1


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

(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^2, INF).


The TRS R consists of the following rules:

   FROM(z0) -> c(FROM(s(z0)))
   2NDSPOS(0, z0) -> c1
   2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
   2NDSNEG(0, z0) -> c3
   2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
   PI(z0) -> c5(2NDSPOS(z0, from(0)), FROM(0))
   PLUS(0, z0) -> c6
   PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
   TIMES(0, z0) -> c8
   TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   SQUARE(z0) -> c10(TIMES(z0, z0))

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

   from(z0) -> cons(z0, from(s(z0)))
   2ndspos(0, z0) -> rnil
   2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
   2ndsneg(0, z0) -> rnil
   2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
   pi(z0) -> 2ndspos(z0, from(0))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(0, z0) -> 0
   times(s(z0), z1) -> plus(z1, times(z0, z1))
   square(z0) -> times(z0, 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^2, INF).


The TRS R consists of the following rules:

   FROM(z0) -> c(FROM(s(z0)))
   2NDSPOS(0', z0) -> c1
   2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
   2NDSNEG(0', z0) -> c3
   2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
   PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
   PLUS(0', z0) -> c6
   PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
   TIMES(0', z0) -> c8
   TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   SQUARE(z0) -> c10(TIMES(z0, z0))

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

   from(z0) -> cons(z0, from(s(z0)))
   2ndspos(0', z0) -> rnil
   2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
   2ndsneg(0', z0) -> rnil
   2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
   pi(z0) -> 2ndspos(z0, from(0'))
   plus(0', z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(0', z0) -> 0'
   times(s(z0), z1) -> plus(z1, times(z0, z1))
   square(z0) -> times(z0, z0)

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

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

(8)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
FROM, 2NDSPOS, 2NDSNEG, from, PLUS, TIMES, times, 2ndspos, 2ndsneg, plus

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG
PLUS < TIMES
times < TIMES
plus < times
2ndspos = 2ndsneg

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

(10)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
FROM, 2NDSPOS, 2NDSNEG, from, PLUS, TIMES, times, 2ndspos, 2ndsneg, plus

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG
PLUS < TIMES
times < TIMES
plus < times
2ndspos = 2ndsneg

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)

Induction Base:
PLUS(gen_s:0'13_11(0), gen_s:0'13_11(b)) ->_R^Omega(1)
c6

Induction Step:
PLUS(gen_s:0'13_11(+(n329_11, 1)), gen_s:0'13_11(b)) ->_R^Omega(1)
c7(PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b))) ->_IH
c7(gen_c6:c715_11(c330_11))

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:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
PLUS, 2NDSPOS, 2NDSNEG, TIMES, times, 2ndspos, 2ndsneg, plus

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG
PLUS < TIMES
times < TIMES
plus < times
2ndspos = 2ndsneg

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Lemmas:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
plus, 2NDSPOS, 2NDSNEG, TIMES, times, 2ndspos, 2ndsneg

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG
times < TIMES
plus < times
2ndspos = 2ndsneg

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(+(n1016_11, b)), rt in Omega(0)

Induction Base:
plus(gen_s:0'13_11(0), gen_s:0'13_11(b)) ->_R^Omega(0)
gen_s:0'13_11(b)

Induction Step:
plus(gen_s:0'13_11(+(n1016_11, 1)), gen_s:0'13_11(b)) ->_R^Omega(0)
s(plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b))) ->_IH
s(gen_s:0'13_11(+(b, c1017_11)))

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:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Lemmas:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)
plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(+(n1016_11, b)), rt in Omega(0)


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
times, 2NDSPOS, 2NDSNEG, TIMES, 2ndspos, 2ndsneg

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG
times < TIMES
2ndspos = 2ndsneg

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
times(gen_s:0'13_11(n2407_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(*(n2407_11, b)), rt in Omega(0)

Induction Base:
times(gen_s:0'13_11(0), gen_s:0'13_11(b)) ->_R^Omega(0)
0'

Induction Step:
times(gen_s:0'13_11(+(n2407_11, 1)), gen_s:0'13_11(b)) ->_R^Omega(0)
plus(gen_s:0'13_11(b), times(gen_s:0'13_11(n2407_11), gen_s:0'13_11(b))) ->_IH
plus(gen_s:0'13_11(b), gen_s:0'13_11(*(c2408_11, b))) ->_L^Omega(0)
gen_s:0'13_11(+(b, *(n2407_11, b)))

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:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Lemmas:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)
plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(+(n1016_11, b)), rt in Omega(0)
times(gen_s:0'13_11(n2407_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(*(n2407_11, b)), rt in Omega(0)


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
TIMES, 2NDSPOS, 2NDSNEG, 2ndspos, 2ndsneg

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG
2ndspos = 2ndsneg

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
TIMES(gen_s:0'13_11(n4169_11), gen_s:0'13_11(b)) -> *18_11, rt in Omega(b*n4169_11 + n4169_11)

Induction Base:
TIMES(gen_s:0'13_11(0), gen_s:0'13_11(b))

Induction Step:
TIMES(gen_s:0'13_11(+(n4169_11, 1)), gen_s:0'13_11(b)) ->_R^Omega(1)
c9(PLUS(gen_s:0'13_11(b), times(gen_s:0'13_11(n4169_11), gen_s:0'13_11(b))), TIMES(gen_s:0'13_11(n4169_11), gen_s:0'13_11(b))) ->_L^Omega(0)
c9(PLUS(gen_s:0'13_11(b), gen_s:0'13_11(*(n4169_11, b))), TIMES(gen_s:0'13_11(n4169_11), gen_s:0'13_11(b))) ->_L^Omega(1 + b)
c9(gen_c6:c715_11(b), TIMES(gen_s:0'13_11(n4169_11), gen_s:0'13_11(*(n4169_11, b)))) ->_IH
c9(gen_c6:c715_11(*(n4169_11, b)), *18_11)

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

(22)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Lemmas:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)
plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(+(n1016_11, b)), rt in Omega(0)
times(gen_s:0'13_11(n2407_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(*(n2407_11, b)), rt in Omega(0)


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
TIMES, 2NDSPOS, 2NDSNEG, 2ndspos, 2ndsneg

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG
2ndspos = 2ndsneg

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

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

(25)
BOUNDS(n^2, INF)

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

(26)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Lemmas:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)
plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(+(n1016_11, b)), rt in Omega(0)
times(gen_s:0'13_11(n2407_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(*(n2407_11, b)), rt in Omega(0)
TIMES(gen_s:0'13_11(n4169_11), gen_s:0'13_11(b)) -> *18_11, rt in Omega(b*n4169_11 + n4169_11)


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
2ndsneg, 2NDSPOS, 2NDSNEG, 2ndspos

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG
2ndspos = 2ndsneg

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
2ndsneg(gen_s:0'13_11(*(2, n42788_11)), gen_cons14_11(*(4, n42788_11))) -> *18_11, rt in Omega(0)

Induction Base:
2ndsneg(gen_s:0'13_11(*(2, 0)), gen_cons14_11(*(4, 0)))

Induction Step:
2ndsneg(gen_s:0'13_11(*(2, +(n42788_11, 1))), gen_cons14_11(*(4, +(n42788_11, 1)))) ->_R^Omega(0)
rcons(negrecip(0'), 2ndspos(gen_s:0'13_11(+(1, *(2, n42788_11))), gen_cons14_11(+(2, *(4, n42788_11))))) ->_R^Omega(0)
rcons(negrecip(0'), rcons(posrecip(0'), 2ndsneg(gen_s:0'13_11(*(2, n42788_11)), gen_cons14_11(*(4, n42788_11))))) ->_IH
rcons(negrecip(0'), rcons(posrecip(0'), *18_11))

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

(28)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Lemmas:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)
plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(+(n1016_11, b)), rt in Omega(0)
times(gen_s:0'13_11(n2407_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(*(n2407_11, b)), rt in Omega(0)
TIMES(gen_s:0'13_11(n4169_11), gen_s:0'13_11(b)) -> *18_11, rt in Omega(b*n4169_11 + n4169_11)
2ndsneg(gen_s:0'13_11(*(2, n42788_11)), gen_cons14_11(*(4, n42788_11))) -> *18_11, rt in Omega(0)


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
2ndspos, 2NDSPOS, 2NDSNEG

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG
2ndspos = 2ndsneg

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
2ndspos(gen_s:0'13_11(*(2, n1027549_11)), gen_cons14_11(*(4, n1027549_11))) -> *18_11, rt in Omega(0)

Induction Base:
2ndspos(gen_s:0'13_11(*(2, 0)), gen_cons14_11(*(4, 0)))

Induction Step:
2ndspos(gen_s:0'13_11(*(2, +(n1027549_11, 1))), gen_cons14_11(*(4, +(n1027549_11, 1)))) ->_R^Omega(0)
rcons(posrecip(0'), 2ndsneg(gen_s:0'13_11(+(1, *(2, n1027549_11))), gen_cons14_11(+(2, *(4, n1027549_11))))) ->_R^Omega(0)
rcons(posrecip(0'), rcons(negrecip(0'), 2ndspos(gen_s:0'13_11(*(2, n1027549_11)), gen_cons14_11(*(4, n1027549_11))))) ->_IH
rcons(posrecip(0'), rcons(negrecip(0'), *18_11))

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:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Lemmas:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)
plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(+(n1016_11, b)), rt in Omega(0)
times(gen_s:0'13_11(n2407_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(*(n2407_11, b)), rt in Omega(0)
TIMES(gen_s:0'13_11(n4169_11), gen_s:0'13_11(b)) -> *18_11, rt in Omega(b*n4169_11 + n4169_11)
2ndsneg(gen_s:0'13_11(*(2, n42788_11)), gen_cons14_11(*(4, n42788_11))) -> *18_11, rt in Omega(0)
2ndspos(gen_s:0'13_11(*(2, n1027549_11)), gen_cons14_11(*(4, n1027549_11))) -> *18_11, rt in Omega(0)


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
2ndsneg, 2NDSPOS, 2NDSNEG

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG
2ndspos = 2ndsneg

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
2ndsneg(gen_s:0'13_11(*(2, n2020627_11)), gen_cons14_11(*(4, n2020627_11))) -> *18_11, rt in Omega(0)

Induction Base:
2ndsneg(gen_s:0'13_11(*(2, 0)), gen_cons14_11(*(4, 0)))

Induction Step:
2ndsneg(gen_s:0'13_11(*(2, +(n2020627_11, 1))), gen_cons14_11(*(4, +(n2020627_11, 1)))) ->_R^Omega(0)
rcons(negrecip(0'), 2ndspos(gen_s:0'13_11(+(1, *(2, n2020627_11))), gen_cons14_11(+(2, *(4, n2020627_11))))) ->_R^Omega(0)
rcons(negrecip(0'), rcons(posrecip(0'), 2ndsneg(gen_s:0'13_11(*(2, n2020627_11)), gen_cons14_11(*(4, n2020627_11))))) ->_IH
rcons(negrecip(0'), rcons(posrecip(0'), *18_11))

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:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Lemmas:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)
plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(+(n1016_11, b)), rt in Omega(0)
times(gen_s:0'13_11(n2407_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(*(n2407_11, b)), rt in Omega(0)
TIMES(gen_s:0'13_11(n4169_11), gen_s:0'13_11(b)) -> *18_11, rt in Omega(b*n4169_11 + n4169_11)
2ndsneg(gen_s:0'13_11(*(2, n2020627_11)), gen_cons14_11(*(4, n2020627_11))) -> *18_11, rt in Omega(0)
2ndspos(gen_s:0'13_11(*(2, n1027549_11)), gen_cons14_11(*(4, n1027549_11))) -> *18_11, rt in Omega(0)


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
2NDSNEG, 2NDSPOS

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
2NDSNEG(gen_s:0'13_11(*(2, n3017360_11)), gen_cons14_11(*(4, n3017360_11))) -> *18_11, rt in Omega(n3017360_11)

Induction Base:
2NDSNEG(gen_s:0'13_11(*(2, 0)), gen_cons14_11(*(4, 0)))

Induction Step:
2NDSNEG(gen_s:0'13_11(*(2, +(n3017360_11, 1))), gen_cons14_11(*(4, +(n3017360_11, 1)))) ->_R^Omega(1)
c4(2NDSPOS(gen_s:0'13_11(+(1, *(2, n3017360_11))), gen_cons14_11(+(2, *(4, n3017360_11))))) ->_R^Omega(1)
c4(c2(2NDSNEG(gen_s:0'13_11(*(2, n3017360_11)), gen_cons14_11(*(4, n3017360_11))))) ->_IH
c4(c2(*18_11))

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

(34)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Lemmas:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)
plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(+(n1016_11, b)), rt in Omega(0)
times(gen_s:0'13_11(n2407_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(*(n2407_11, b)), rt in Omega(0)
TIMES(gen_s:0'13_11(n4169_11), gen_s:0'13_11(b)) -> *18_11, rt in Omega(b*n4169_11 + n4169_11)
2ndsneg(gen_s:0'13_11(*(2, n2020627_11)), gen_cons14_11(*(4, n2020627_11))) -> *18_11, rt in Omega(0)
2ndspos(gen_s:0'13_11(*(2, n1027549_11)), gen_cons14_11(*(4, n1027549_11))) -> *18_11, rt in Omega(0)
2NDSNEG(gen_s:0'13_11(*(2, n3017360_11)), gen_cons14_11(*(4, n3017360_11))) -> *18_11, rt in Omega(n3017360_11)


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
2NDSPOS

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
2NDSPOS(gen_s:0'13_11(*(2, n3023881_11)), gen_cons14_11(*(4, n3023881_11))) -> *18_11, rt in Omega(n3023881_11)

Induction Base:
2NDSPOS(gen_s:0'13_11(*(2, 0)), gen_cons14_11(*(4, 0)))

Induction Step:
2NDSPOS(gen_s:0'13_11(*(2, +(n3023881_11, 1))), gen_cons14_11(*(4, +(n3023881_11, 1)))) ->_R^Omega(1)
c2(2NDSNEG(gen_s:0'13_11(+(1, *(2, n3023881_11))), gen_cons14_11(+(2, *(4, n3023881_11))))) ->_R^Omega(1)
c2(c4(2NDSPOS(gen_s:0'13_11(*(2, n3023881_11)), gen_cons14_11(*(4, n3023881_11))))) ->_IH
c2(c4(*18_11))

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

(36)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
2NDSPOS(0', z0) -> c1
2NDSPOS(s(z0), cons(z1, cons(z2, z3))) -> c2(2NDSNEG(z0, z3))
2NDSNEG(0', z0) -> c3
2NDSNEG(s(z0), cons(z1, cons(z2, z3))) -> c4(2NDSPOS(z0, z3))
PI(z0) -> c5(2NDSPOS(z0, from(0')), FROM(0'))
PLUS(0', z0) -> c6
PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
TIMES(0', z0) -> c8
TIMES(s(z0), z1) -> c9(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
SQUARE(z0) -> c10(TIMES(z0, z0))
from(z0) -> cons(z0, from(s(z0)))
2ndspos(0', z0) -> rnil
2ndspos(s(z0), cons(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3))
2ndsneg(0', z0) -> rnil
2ndsneg(s(z0), cons(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3))
pi(z0) -> 2ndspos(z0, from(0'))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
square(z0) -> times(z0, z0)

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
2NDSPOS :: s:0' -> cons -> c1:c2
0' :: s:0'
c1 :: c1:c2
cons :: s:0' -> cons -> cons
c2 :: c3:c4 -> c1:c2
2NDSNEG :: s:0' -> cons -> c3:c4
c3 :: c3:c4
c4 :: c1:c2 -> c3:c4
PI :: s:0' -> c5
c5 :: c1:c2 -> c -> c5
from :: s:0' -> cons
PLUS :: s:0' -> s:0' -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TIMES :: s:0' -> s:0' -> c8:c9
c8 :: c8:c9
c9 :: c6:c7 -> c8:c9 -> c8:c9
times :: s:0' -> s:0' -> s:0'
SQUARE :: s:0' -> c10
c10 :: c8:c9 -> c10
2ndspos :: s:0' -> cons -> rnil:rcons
rnil :: rnil:rcons
rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons
posrecip :: s:0' -> posrecip:negrecip
2ndsneg :: s:0' -> cons -> rnil:rcons
negrecip :: s:0' -> posrecip:negrecip
pi :: s:0' -> rnil:rcons
plus :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons4_11 :: cons
hole_c3:c45_11 :: c3:c4
hole_c56_11 :: c5
hole_c6:c77_11 :: c6:c7
hole_c8:c98_11 :: c8:c9
hole_c109_11 :: c10
hole_rnil:rcons10_11 :: rnil:rcons
hole_posrecip:negrecip11_11 :: posrecip:negrecip
gen_c12_11 :: Nat -> c
gen_s:0'13_11 :: Nat -> s:0'
gen_cons14_11 :: Nat -> cons
gen_c6:c715_11 :: Nat -> c6:c7
gen_c8:c916_11 :: Nat -> c8:c9
gen_rnil:rcons17_11 :: Nat -> rnil:rcons


Lemmas:
PLUS(gen_s:0'13_11(n329_11), gen_s:0'13_11(b)) -> gen_c6:c715_11(n329_11), rt in Omega(1 + n329_11)
plus(gen_s:0'13_11(n1016_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(+(n1016_11, b)), rt in Omega(0)
times(gen_s:0'13_11(n2407_11), gen_s:0'13_11(b)) -> gen_s:0'13_11(*(n2407_11, b)), rt in Omega(0)
TIMES(gen_s:0'13_11(n4169_11), gen_s:0'13_11(b)) -> *18_11, rt in Omega(b*n4169_11 + n4169_11)
2ndsneg(gen_s:0'13_11(*(2, n2020627_11)), gen_cons14_11(*(4, n2020627_11))) -> *18_11, rt in Omega(0)
2ndspos(gen_s:0'13_11(*(2, n1027549_11)), gen_cons14_11(*(4, n1027549_11))) -> *18_11, rt in Omega(0)
2NDSNEG(gen_s:0'13_11(*(2, n3017360_11)), gen_cons14_11(*(4, n3017360_11))) -> *18_11, rt in Omega(n3017360_11)
2NDSPOS(gen_s:0'13_11(*(2, n3023881_11)), gen_cons14_11(*(4, n3023881_11))) -> *18_11, rt in Omega(n3023881_11)


Generator Equations:
gen_c12_11(0) <=> hole_c1_11
gen_c12_11(+(x, 1)) <=> c(gen_c12_11(x))
gen_s:0'13_11(0) <=> 0'
gen_s:0'13_11(+(x, 1)) <=> s(gen_s:0'13_11(x))
gen_cons14_11(0) <=> hole_cons4_11
gen_cons14_11(+(x, 1)) <=> cons(0', gen_cons14_11(x))
gen_c6:c715_11(0) <=> c6
gen_c6:c715_11(+(x, 1)) <=> c7(gen_c6:c715_11(x))
gen_c8:c916_11(0) <=> c8
gen_c8:c916_11(+(x, 1)) <=> c9(c6, gen_c8:c916_11(x))
gen_rnil:rcons17_11(0) <=> rnil
gen_rnil:rcons17_11(+(x, 1)) <=> rcons(posrecip(0'), gen_rnil:rcons17_11(x))


The following defined symbols remain to be analysed:
2NDSNEG

They will be analysed ascendingly in the following order:
2NDSPOS = 2NDSNEG

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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
2NDSNEG(gen_s:0'13_11(*(2, n3031780_11)), gen_cons14_11(*(4, n3031780_11))) -> *18_11, rt in Omega(n3031780_11)

Induction Base:
2NDSNEG(gen_s:0'13_11(*(2, 0)), gen_cons14_11(*(4, 0)))

Induction Step:
2NDSNEG(gen_s:0'13_11(*(2, +(n3031780_11, 1))), gen_cons14_11(*(4, +(n3031780_11, 1)))) ->_R^Omega(1)
c4(2NDSPOS(gen_s:0'13_11(+(1, *(2, n3031780_11))), gen_cons14_11(+(2, *(4, n3031780_11))))) ->_R^Omega(1)
c4(c2(2NDSNEG(gen_s:0'13_11(*(2, n3031780_11)), gen_cons14_11(*(4, n3031780_11))))) ->_IH
c4(c2(*18_11))

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

(38)
BOUNDS(1, INF)