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


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^11, 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), 1 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 303 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 50 ms]
(14) BEST
    (15) proven lower bound
        (16) LowerBoundPropagationProof [FINISHED, 0 ms]
        (17) BOUNDS(n^1, INF)
    (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 1804 ms]
        (20) BEST
            (21) proven lower bound
                (22) LowerBoundPropagationProof [FINISHED, 0 ms]
                (23) BOUNDS(n^2, INF)
            (24) typed CpxTrs
                (25) RewriteLemmaProof [LOWER BOUND(ID), 19 ms]
                (26) typed CpxTrs
                (27) RewriteLemmaProof [LOWER BOUND(ID), 74 ms]
                (28) typed CpxTrs
                (29) RewriteLemmaProof [LOWER BOUND(ID), 1147 ms]
                (30) typed CpxTrs
                (31) RewriteLemmaProof [LOWER BOUND(ID), 2363 ms]
                (32) BEST
                    (33) proven lower bound
                        (34) LowerBoundPropagationProof [FINISHED, 0 ms]
                        (35) BOUNDS(n^11, INF)
                    (36) typed CpxTrs
                        (37) RewriteLemmaProof [LOWER BOUND(ID), 1288 ms]
                        (38) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   plus(0, x) -> x
   plus(s(x), y) -> s(plus(p(s(x)), y))
   times(0, y) -> 0
   times(s(x), y) -> plus(y, times(p(s(x)), y))
   p(s(0)) -> 0
   p(s(s(x))) -> s(p(s(x)))
   fac(0, x) -> x
   fac(s(x), y) -> fac(p(s(x)), times(s(x), y))
   factorial(x) -> fac(x, s(0))

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:
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
   times(0, z0) -> 0
   times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   fac(0, z0) -> z0
   fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
   factorial(z0) -> fac(z0, s(0))
Tuples:
   PLUS(0, z0) -> c
   PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
   TIMES(0, z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
   P(s(0)) -> c4
   P(s(s(z0))) -> c5(P(s(z0)))
   FAC(0, z0) -> c6
   FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
   FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
   FACTORIAL(z0) -> c9(FAC(z0, s(0)))
S tuples:
   PLUS(0, z0) -> c
   PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
   TIMES(0, z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
   P(s(0)) -> c4
   P(s(s(z0))) -> c5(P(s(z0)))
   FAC(0, z0) -> c6
   FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
   FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
   FACTORIAL(z0) -> c9(FAC(z0, s(0)))
K tuples:none
Defined Rule Symbols:   plus_2, times_2, p_1, fac_2, factorial_1

Defined Pair Symbols:   PLUS_2, TIMES_2, P_1, FAC_2, FACTORIAL_1

Compound Symbols:   c, c1_2, c2, c3_3, c4, c5_1, c6, c7_2, c8_2, c9_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^11, INF).


The TRS R consists of the following rules:

   PLUS(0, z0) -> c
   PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
   TIMES(0, z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
   P(s(0)) -> c4
   P(s(s(z0))) -> c5(P(s(z0)))
   FAC(0, z0) -> c6
   FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
   FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
   FACTORIAL(z0) -> c9(FAC(z0, s(0)))

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

   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
   times(0, z0) -> 0
   times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   fac(0, z0) -> z0
   fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
   factorial(z0) -> fac(z0, s(0))

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


The TRS R consists of the following rules:

   PLUS(0', z0) -> c
   PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
   TIMES(0', z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
   P(s(0')) -> c4
   P(s(s(z0))) -> c5(P(s(z0)))
   FAC(0', z0) -> c6
   FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
   FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
   FACTORIAL(z0) -> c9(FAC(z0, s(0')))

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

   plus(0', z0) -> z0
   plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
   times(0', z0) -> 0'
   times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
   p(s(0')) -> 0'
   p(s(s(z0))) -> s(p(s(z0)))
   fac(0', z0) -> z0
   fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
   factorial(z0) -> fac(z0, s(0'))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
PLUS, p, P, TIMES, times, FAC, plus, fac

They will be analysed ascendingly in the following order:
p < PLUS
P < PLUS
PLUS < TIMES
p < TIMES
p < times
p < FAC
p < plus
p < fac
P < TIMES
P < FAC
times < TIMES
TIMES < FAC
times < FAC
plus < times
times < fac

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

(10)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
p, PLUS, P, TIMES, times, FAC, plus, fac

They will be analysed ascendingly in the following order:
p < PLUS
P < PLUS
PLUS < TIMES
p < TIMES
p < times
p < FAC
p < plus
p < fac
P < TIMES
P < FAC
times < TIMES
TIMES < FAC
times < FAC
plus < times
times < fac

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)

Induction Base:
p(gen_0':s8_10(+(1, 0))) ->_R^Omega(0)
0'

Induction Step:
p(gen_0':s8_10(+(1, +(n13_10, 1)))) ->_R^Omega(0)
s(p(s(gen_0':s8_10(n13_10)))) ->_IH
s(gen_0':s8_10(c14_10))

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

(12)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Lemmas:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
P, PLUS, TIMES, times, FAC, plus, fac

They will be analysed ascendingly in the following order:
P < PLUS
PLUS < TIMES
P < TIMES
P < FAC
times < TIMES
TIMES < FAC
times < FAC
plus < times
times < fac

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
P(gen_0':s8_10(+(1, n338_10))) -> gen_c4:c59_10(n338_10), rt in Omega(1 + n338_10)

Induction Base:
P(gen_0':s8_10(+(1, 0))) ->_R^Omega(1)
c4

Induction Step:
P(gen_0':s8_10(+(1, +(n338_10, 1)))) ->_R^Omega(1)
c5(P(s(gen_0':s8_10(n338_10)))) ->_IH
c5(gen_c4:c59_10(c339_10))

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

(14)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Lemmas:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
P, PLUS, TIMES, times, FAC, plus, fac

They will be analysed ascendingly in the following order:
P < PLUS
PLUS < TIMES
P < TIMES
P < FAC
times < TIMES
TIMES < FAC
times < FAC
plus < times
times < fac

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Lemmas:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)
P(gen_0':s8_10(+(1, n338_10))) -> gen_c4:c59_10(n338_10), rt in Omega(1 + n338_10)


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
PLUS, TIMES, times, FAC, plus, fac

They will be analysed ascendingly in the following order:
PLUS < TIMES
times < TIMES
TIMES < FAC
times < FAC
plus < times
times < fac

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_0':s8_10(n694_10), gen_0':s8_10(b)) -> *12_10, rt in Omega(n694_10 + n694_10^2)

Induction Base:
PLUS(gen_0':s8_10(0), gen_0':s8_10(b))

Induction Step:
PLUS(gen_0':s8_10(+(n694_10, 1)), gen_0':s8_10(b)) ->_R^Omega(1)
c1(PLUS(p(s(gen_0':s8_10(n694_10))), gen_0':s8_10(b)), P(s(gen_0':s8_10(n694_10)))) ->_L^Omega(0)
c1(PLUS(gen_0':s8_10(n694_10), gen_0':s8_10(b)), P(s(gen_0':s8_10(n694_10)))) ->_IH
c1(*12_10, P(s(gen_0':s8_10(n694_10)))) ->_L^Omega(1 + n694_10)
c1(*12_10, gen_c4:c59_10(n694_10))

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

(20)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Lemmas:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)
P(gen_0':s8_10(+(1, n338_10))) -> gen_c4:c59_10(n338_10), rt in Omega(1 + n338_10)


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
PLUS, TIMES, times, FAC, plus, fac

They will be analysed ascendingly in the following order:
PLUS < TIMES
times < TIMES
TIMES < FAC
times < FAC
plus < times
times < fac

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

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

(23)
BOUNDS(n^2, INF)

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

(24)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Lemmas:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)
P(gen_0':s8_10(+(1, n338_10))) -> gen_c4:c59_10(n338_10), rt in Omega(1 + n338_10)
PLUS(gen_0':s8_10(n694_10), gen_0':s8_10(b)) -> *12_10, rt in Omega(n694_10 + n694_10^2)


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
plus, TIMES, times, FAC, fac

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < FAC
times < FAC
plus < times
times < fac

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus(gen_0':s8_10(n10506_10), gen_0':s8_10(b)) -> gen_0':s8_10(+(n10506_10, b)), rt in Omega(0)

Induction Base:
plus(gen_0':s8_10(0), gen_0':s8_10(b)) ->_R^Omega(0)
gen_0':s8_10(b)

Induction Step:
plus(gen_0':s8_10(+(n10506_10, 1)), gen_0':s8_10(b)) ->_R^Omega(0)
s(plus(p(s(gen_0':s8_10(n10506_10))), gen_0':s8_10(b))) ->_L^Omega(0)
s(plus(gen_0':s8_10(n10506_10), gen_0':s8_10(b))) ->_IH
s(gen_0':s8_10(+(b, c10507_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:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Lemmas:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)
P(gen_0':s8_10(+(1, n338_10))) -> gen_c4:c59_10(n338_10), rt in Omega(1 + n338_10)
PLUS(gen_0':s8_10(n694_10), gen_0':s8_10(b)) -> *12_10, rt in Omega(n694_10 + n694_10^2)
plus(gen_0':s8_10(n10506_10), gen_0':s8_10(b)) -> gen_0':s8_10(+(n10506_10, b)), rt in Omega(0)


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
times, TIMES, FAC, fac

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < FAC
times < FAC
times < fac

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
times(gen_0':s8_10(n11603_10), gen_0':s8_10(b)) -> gen_0':s8_10(*(n11603_10, b)), rt in Omega(0)

Induction Base:
times(gen_0':s8_10(0), gen_0':s8_10(b)) ->_R^Omega(0)
0'

Induction Step:
times(gen_0':s8_10(+(n11603_10, 1)), gen_0':s8_10(b)) ->_R^Omega(0)
plus(gen_0':s8_10(b), times(p(s(gen_0':s8_10(n11603_10))), gen_0':s8_10(b))) ->_L^Omega(0)
plus(gen_0':s8_10(b), times(gen_0':s8_10(n11603_10), gen_0':s8_10(b))) ->_IH
plus(gen_0':s8_10(b), gen_0':s8_10(*(c11604_10, b))) ->_L^Omega(0)
gen_0':s8_10(+(b, *(n11603_10, b)))

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:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Lemmas:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)
P(gen_0':s8_10(+(1, n338_10))) -> gen_c4:c59_10(n338_10), rt in Omega(1 + n338_10)
PLUS(gen_0':s8_10(n694_10), gen_0':s8_10(b)) -> *12_10, rt in Omega(n694_10 + n694_10^2)
plus(gen_0':s8_10(n10506_10), gen_0':s8_10(b)) -> gen_0':s8_10(+(n10506_10, b)), rt in Omega(0)
times(gen_0':s8_10(n11603_10), gen_0':s8_10(b)) -> gen_0':s8_10(*(n11603_10, b)), rt in Omega(0)


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
TIMES, FAC, fac

They will be analysed ascendingly in the following order:
TIMES < FAC

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
TIMES(gen_0':s8_10(n13447_10), gen_0':s8_10(0)) -> *12_10, rt in Omega(n13447_10 + n13447_10^2)

Induction Base:
TIMES(gen_0':s8_10(0), gen_0':s8_10(0))

Induction Step:
TIMES(gen_0':s8_10(+(n13447_10, 1)), gen_0':s8_10(0)) ->_R^Omega(1)
c3(PLUS(gen_0':s8_10(0), times(p(s(gen_0':s8_10(n13447_10))), gen_0':s8_10(0))), TIMES(p(s(gen_0':s8_10(n13447_10))), gen_0':s8_10(0)), P(s(gen_0':s8_10(n13447_10)))) ->_L^Omega(0)
c3(PLUS(gen_0':s8_10(0), times(gen_0':s8_10(n13447_10), gen_0':s8_10(0))), TIMES(p(s(gen_0':s8_10(n13447_10))), gen_0':s8_10(0)), P(s(gen_0':s8_10(n13447_10)))) ->_L^Omega(0)
c3(PLUS(gen_0':s8_10(0), gen_0':s8_10(*(n13447_10, 0))), TIMES(p(s(gen_0':s8_10(n13447_10))), gen_0':s8_10(0)), P(s(gen_0':s8_10(n13447_10)))) ->_R^Omega(1)
c3(c, TIMES(p(s(gen_0':s8_10(n13447_10))), gen_0':s8_10(0)), P(s(gen_0':s8_10(n13447_10)))) ->_L^Omega(0)
c3(c, TIMES(gen_0':s8_10(n13447_10), gen_0':s8_10(0)), P(s(gen_0':s8_10(n13447_10)))) ->_IH
c3(c, *12_10, P(s(gen_0':s8_10(n13447_10)))) ->_L^Omega(1 + n13447_10)
c3(c, *12_10, gen_c4:c59_10(n13447_10))

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

(30)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Lemmas:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)
P(gen_0':s8_10(+(1, n338_10))) -> gen_c4:c59_10(n338_10), rt in Omega(1 + n338_10)
PLUS(gen_0':s8_10(n694_10), gen_0':s8_10(b)) -> *12_10, rt in Omega(n694_10 + n694_10^2)
plus(gen_0':s8_10(n10506_10), gen_0':s8_10(b)) -> gen_0':s8_10(+(n10506_10, b)), rt in Omega(0)
times(gen_0':s8_10(n11603_10), gen_0':s8_10(b)) -> gen_0':s8_10(*(n11603_10, b)), rt in Omega(0)
TIMES(gen_0':s8_10(n13447_10), gen_0':s8_10(0)) -> *12_10, rt in Omega(n13447_10 + n13447_10^2)


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
FAC, fac
----------------------------------------

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
FAC(gen_0':s8_10(n34218_10), gen_0':s8_10(b)) -> *12_10, rt in Omega(b*n34218_10^3 + b*n34218_10^4 + b*n34218_10^5 + b^2*n34218_10^5 + b^2*n34218_10^6 + b^2*n34218_10^7 + b^2*n34218_10^8 + b^2*n34218_10^9 + n34218_10 + n34218_10^2)

Induction Base:
FAC(gen_0':s8_10(0), gen_0':s8_10(b))

Induction Step:
FAC(gen_0':s8_10(+(n34218_10, 1)), gen_0':s8_10(b)) ->_R^Omega(1)
c8(FAC(p(s(gen_0':s8_10(n34218_10))), times(s(gen_0':s8_10(n34218_10)), gen_0':s8_10(b))), TIMES(s(gen_0':s8_10(n34218_10)), gen_0':s8_10(b))) ->_L^Omega(0)
c8(FAC(gen_0':s8_10(n34218_10), times(s(gen_0':s8_10(n34218_10)), gen_0':s8_10(b))), TIMES(s(gen_0':s8_10(n34218_10)), gen_0':s8_10(b))) ->_R^Omega(0)
c8(FAC(gen_0':s8_10(n34218_10), plus(gen_0':s8_10(b), times(p(s(gen_0':s8_10(n34218_10))), gen_0':s8_10(b)))), TIMES(s(gen_0':s8_10(n34218_10)), gen_0':s8_10(b))) ->_L^Omega(0)
c8(FAC(gen_0':s8_10(n34218_10), plus(gen_0':s8_10(b), times(gen_0':s8_10(n34218_10), gen_0':s8_10(b)))), TIMES(s(gen_0':s8_10(n34218_10)), gen_0':s8_10(b))) ->_L^Omega(0)
c8(FAC(gen_0':s8_10(n34218_10), plus(gen_0':s8_10(b), gen_0':s8_10(*(n34218_10, b)))), TIMES(s(gen_0':s8_10(n34218_10)), gen_0':s8_10(b))) ->_L^Omega(0)
c8(FAC(gen_0':s8_10(n34218_10), gen_0':s8_10(+(b, *(n34218_10, b)))), TIMES(s(gen_0':s8_10(n34218_10)), gen_0':s8_10(*(n34218_10, b)))) ->_IH
c8(*12_10, TIMES(s(gen_0':s8_10(n34218_10)), gen_0':s8_10(*(n34218_10, +(b, *(n34218_10, b)))))) ->_R^Omega(1)
c8(*12_10, c3(PLUS(gen_0':s8_10(+(*(n34218_10, b), *(*(n34218_10, n34218_10), b))), times(p(s(gen_0':s8_10(n34218_10))), gen_0':s8_10(+(*(n34218_10, b), *(*(n34218_10, n34218_10), b))))), TIMES(p(s(gen_0':s8_10(n34218_10))), gen_0':s8_10(+(*(n34218_10, b), *(*(n34218_10, n34218_10), b)))), P(s(gen_0':s8_10(n34218_10))))) ->_L^Omega(0)
c8(*12_10, c3(PLUS(gen_0':s8_10(+(*(n34218_10, b), *(*(n34218_10, n34218_10), b))), times(gen_0':s8_10(n34218_10), gen_0':s8_10(+(*(n34218_10, b), *(*(n34218_10, n34218_10), b))))), TIMES(p(s(gen_0':s8_10(n34218_10))), gen_0':s8_10(+(*(n34218_10, b), *(*(n34218_10, n34218_10), b)))), P(s(gen_0':s8_10(n34218_10))))) ->_L^Omega(0)
c8(*12_10, c3(PLUS(gen_0':s8_10(+(*(n34218_10, +(*(n34218_10, b), *(*(n34218_10, n34218_10), b))), *(*(n34218_10, n34218_10), +(*(n34218_10, b), *(*(n34218_10, n34218_10), b))))), gen_0':s8_10(*(n34218_10, +(*(n34218_10, b), *(*(n34218_10, n34218_10), b))))), TIMES(p(s(gen_0':s8_10(n34218_10))), gen_0':s8_10(+(*(n34218_10, +(*(n34218_10, b), *(*(n34218_10, n34218_10), b))), *(*(n34218_10, n34218_10), +(*(n34218_10, b), *(*(n34218_10, n34218_10), b)))))), P(s(gen_0':s8_10(n34218_10))))) ->_L^Omega(b*n34218_10^2 + 2*b*n34218_10^3 + b*n34218_10^4 + b^2*n34218_10^4 + 4*b^2*n34218_10^5 + 6*b^2*n34218_10^6 + 4*b^2*n34218_10^7 + b^2*n34218_10^8)
c8(*12_10, c3(*12_10, TIMES(p(s(gen_0':s8_10(n34218_10))), gen_0':s8_10(+(+(*(*(n34218_10, n34218_10), +(*(*(n34218_10, n34218_10), b), *(*(*(n34218_10, n34218_10), n34218_10), b))), *(2, *(*(*(n34218_10, n34218_10), n34218_10), +(*(*(n34218_10, n34218_10), b), *(*(*(n34218_10, n34218_10), n34218_10), b))))), *(*(*(*(n34218_10, n34218_10), n34218_10), n34218_10), +(*(*(n34218_10, n34218_10), b), *(*(*(n34218_10, n34218_10), n34218_10), b)))))), P(s(gen_0':s8_10(n34218_10))))) ->_L^Omega(0)
c8(*12_10, c3(*12_10, TIMES(gen_0':s8_10(n34218_10), gen_0':s8_10(+(+(+(*(*(*(*(n34218_10, n34218_10), n34218_10), n34218_10), b), *(3, *(*(*(*(*(n34218_10, n34218_10), n34218_10), n34218_10), n34218_10), b))), *(3, *(*(*(*(*(*(n34218_10, n34218_10), n34218_10), n34218_10), n34218_10), n34218_10), b))), *(*(*(*(*(*(*(n34218_10, n34218_10), n34218_10), n34218_10), n34218_10), n34218_10), n34218_10), b)))), P(s(gen_0':s8_10(n34218_10))))) ->_L^Omega(1 + n34218_10)
c8(*12_10, c3(*12_10, TIMES(gen_0':s8_10(n34218_10), gen_0':s8_10(+(+(+(*(*(*(*(n34218_10, n34218_10), n34218_10), n34218_10), b), *(3, *(*(*(*(*(n34218_10, n34218_10), n34218_10), n34218_10), n34218_10), b))), *(3, *(*(*(*(*(*(n34218_10, n34218_10), n34218_10), n34218_10), n34218_10), n34218_10), b))), *(*(*(*(*(*(*(n34218_10, n34218_10), n34218_10), n34218_10), n34218_10), n34218_10), n34218_10), b)))), gen_c4:c59_10(n34218_10)))

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

(32)
Complex Obligation (BEST)

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

(33)
Obligation:
Proved the lower bound n^11 for the following obligation:

Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Lemmas:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)
P(gen_0':s8_10(+(1, n338_10))) -> gen_c4:c59_10(n338_10), rt in Omega(1 + n338_10)
PLUS(gen_0':s8_10(n694_10), gen_0':s8_10(b)) -> *12_10, rt in Omega(n694_10 + n694_10^2)
plus(gen_0':s8_10(n10506_10), gen_0':s8_10(b)) -> gen_0':s8_10(+(n10506_10, b)), rt in Omega(0)
times(gen_0':s8_10(n11603_10), gen_0':s8_10(b)) -> gen_0':s8_10(*(n11603_10, b)), rt in Omega(0)
TIMES(gen_0':s8_10(n13447_10), gen_0':s8_10(0)) -> *12_10, rt in Omega(n13447_10 + n13447_10^2)


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
FAC, fac
----------------------------------------

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

(35)
BOUNDS(n^11, INF)

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

(36)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
P(s(0')) -> c4
P(s(s(z0))) -> c5(P(s(z0)))
FAC(0', z0) -> c6
FAC(s(z0), z1) -> c7(FAC(p(s(z0)), times(s(z0), z1)), P(s(z0)))
FAC(s(z0), z1) -> c8(FAC(p(s(z0)), times(s(z0), z1)), TIMES(s(z0), z1))
FACTORIAL(z0) -> c9(FAC(z0, s(0')))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
fac(0', z0) -> z0
fac(s(z0), z1) -> fac(p(s(z0)), times(s(z0), z1))
factorial(z0) -> fac(z0, s(0'))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c4:c5 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c4:c5
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c4:c5 -> c2:c3
times :: 0':s -> 0':s -> 0':s
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
FAC :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8
c8 :: c6:c7:c8 -> c2:c3 -> c6:c7:c8
FACTORIAL :: 0':s -> c9
c9 :: c6:c7:c8 -> c9
plus :: 0':s -> 0':s -> 0':s
fac :: 0':s -> 0':s -> 0':s
factorial :: 0':s -> 0':s
hole_c:c11_10 :: c:c1
hole_0':s2_10 :: 0':s
hole_c4:c53_10 :: c4:c5
hole_c2:c34_10 :: c2:c3
hole_c6:c7:c85_10 :: c6:c7:c8
hole_c96_10 :: c9
gen_c:c17_10 :: Nat -> c:c1
gen_0':s8_10 :: Nat -> 0':s
gen_c4:c59_10 :: Nat -> c4:c5
gen_c2:c310_10 :: Nat -> c2:c3
gen_c6:c7:c811_10 :: Nat -> c6:c7:c8


Lemmas:
p(gen_0':s8_10(+(1, n13_10))) -> gen_0':s8_10(n13_10), rt in Omega(0)
P(gen_0':s8_10(+(1, n338_10))) -> gen_c4:c59_10(n338_10), rt in Omega(1 + n338_10)
PLUS(gen_0':s8_10(n694_10), gen_0':s8_10(b)) -> *12_10, rt in Omega(n694_10 + n694_10^2)
plus(gen_0':s8_10(n10506_10), gen_0':s8_10(b)) -> gen_0':s8_10(+(n10506_10, b)), rt in Omega(0)
times(gen_0':s8_10(n11603_10), gen_0':s8_10(b)) -> gen_0':s8_10(*(n11603_10, b)), rt in Omega(0)
TIMES(gen_0':s8_10(n13447_10), gen_0':s8_10(0)) -> *12_10, rt in Omega(n13447_10 + n13447_10^2)
FAC(gen_0':s8_10(n34218_10), gen_0':s8_10(b)) -> *12_10, rt in Omega(b*n34218_10^3 + b*n34218_10^4 + b*n34218_10^5 + b^2*n34218_10^5 + b^2*n34218_10^6 + b^2*n34218_10^7 + b^2*n34218_10^8 + b^2*n34218_10^9 + n34218_10 + n34218_10^2)


Generator Equations:
gen_c:c17_10(0) <=> c
gen_c:c17_10(+(x, 1)) <=> c1(gen_c:c17_10(x), c4)
gen_0':s8_10(0) <=> 0'
gen_0':s8_10(+(x, 1)) <=> s(gen_0':s8_10(x))
gen_c4:c59_10(0) <=> c4
gen_c4:c59_10(+(x, 1)) <=> c5(gen_c4:c59_10(x))
gen_c2:c310_10(0) <=> c2
gen_c2:c310_10(+(x, 1)) <=> c3(c, gen_c2:c310_10(x), c4)
gen_c6:c7:c811_10(0) <=> c6
gen_c6:c7:c811_10(+(x, 1)) <=> c7(gen_c6:c7:c811_10(x), c4)


The following defined symbols remain to be analysed:
fac
----------------------------------------

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
fac(gen_0':s8_10(n60534_10), gen_0':s8_10(b)) -> *12_10, rt in Omega(0)

Induction Base:
fac(gen_0':s8_10(0), gen_0':s8_10(b))

Induction Step:
fac(gen_0':s8_10(+(n60534_10, 1)), gen_0':s8_10(b)) ->_R^Omega(0)
fac(p(s(gen_0':s8_10(n60534_10))), times(s(gen_0':s8_10(n60534_10)), gen_0':s8_10(b))) ->_L^Omega(0)
fac(gen_0':s8_10(n60534_10), times(s(gen_0':s8_10(n60534_10)), gen_0':s8_10(b))) ->_L^Omega(0)
fac(gen_0':s8_10(n60534_10), gen_0':s8_10(*(+(n60534_10, 1), b))) ->_IH
*12_10

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

(38)
BOUNDS(1, INF)