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


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

(0) CpxRelTRS
(1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CpxRelTRS
(3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) typed CpxTrs
(5) OrderProof [LOWER BOUND(ID), 0 ms]
(6) typed CpxTrs
(7) RewriteLemmaProof [LOWER BOUND(ID), 282 ms]
(8) BEST
    (9) proven lower bound
        (10) LowerBoundPropagationProof [FINISHED, 0 ms]
        (11) BOUNDS(n^1, INF)
    (12) typed CpxTrs
        (13) RewriteLemmaProof [LOWER BOUND(ID), 26 ms]
        (14) typed CpxTrs
        (15) RewriteLemmaProof [LOWER BOUND(ID), 101 ms]
        (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 8250 ms]
        (18) BEST
            (19) proven lower bound
                (20) LowerBoundPropagationProof [FINISHED, 0 ms]
                (21) BOUNDS(n^2, INF)
            (22) typed CpxTrs


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

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

   FACT(z0) -> c(IF(zero(z0), s(0), prod(z0, fact(p(z0)))), ZERO(z0))
   FACT(z0) -> c1(IF(zero(z0), s(0), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
   ADD(0, z0) -> c2
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(0, z0) -> c4
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   ZERO(0) -> c8
   ZERO(s(z0)) -> c9
   P(s(z0)) -> c10

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

   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0

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

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

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

   FACT(z0) -> c(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), ZERO(z0))
   FACT(z0) -> c1(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
   ADD(0', z0) -> c2
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(0', z0) -> c4
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   ZERO(0') -> c8
   ZERO(s(z0)) -> c9
   P(s(z0)) -> c10

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

   fact(z0) -> if(zero(z0), s(0'), prod(z0, fact(p(z0))))
   add(0', z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0', z0) -> 0'
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0') -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0

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

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

(4)
Obligation:
Innermost TRS:
Rules:
FACT(z0) -> c(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), ZERO(z0))
FACT(z0) -> c1(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
ADD(0', z0) -> c2
ADD(s(z0), z1) -> c3(ADD(z0, z1))
PROD(0', z0) -> c4
PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ZERO(0') -> c8
ZERO(s(z0)) -> c9
P(s(z0)) -> c10
fact(z0) -> if(zero(z0), s(0'), prod(z0, fact(p(z0))))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
prod(0', z0) -> 0'
prod(s(z0), z1) -> add(z1, prod(z0, z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
zero(0') -> true
zero(s(z0)) -> false
p(s(z0)) -> z0

Types:
FACT :: 0':s -> c:c1
c :: c6:c7 -> c8:c9 -> c:c1
IF :: true:false -> 0':s -> 0':s -> c6:c7
zero :: 0':s -> true:false
s :: 0':s -> 0':s
0' :: 0':s
prod :: 0':s -> 0':s -> 0':s
fact :: 0':s -> 0':s
p :: 0':s -> 0':s
ZERO :: 0':s -> c8:c9
c1 :: c6:c7 -> c4:c5 -> c:c1 -> c10 -> c:c1
PROD :: 0':s -> 0':s -> c4:c5
P :: 0':s -> c10
ADD :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c6:c7
c8 :: c8:c9
c9 :: c8:c9
c10 :: c10
if :: true:false -> 0':s -> 0':s -> 0':s
add :: 0':s -> 0':s -> 0':s
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c6:c73_11 :: c6:c7
hole_c8:c94_11 :: c8:c9
hole_true:false5_11 :: true:false
hole_c4:c56_11 :: c4:c5
hole_c107_11 :: c10
hole_c2:c38_11 :: c2:c3
gen_c:c19_11 :: Nat -> c:c1
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c511_11 :: Nat -> c4:c5
gen_c2:c312_11 :: Nat -> c2:c3

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

(5) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
FACT, prod, fact, PROD, ADD, add

They will be analysed ascendingly in the following order:
prod < FACT
fact < FACT
PROD < FACT
prod < fact
prod < PROD
add < prod
ADD < PROD

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

(6)
Obligation:
Innermost TRS:
Rules:
FACT(z0) -> c(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), ZERO(z0))
FACT(z0) -> c1(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
ADD(0', z0) -> c2
ADD(s(z0), z1) -> c3(ADD(z0, z1))
PROD(0', z0) -> c4
PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ZERO(0') -> c8
ZERO(s(z0)) -> c9
P(s(z0)) -> c10
fact(z0) -> if(zero(z0), s(0'), prod(z0, fact(p(z0))))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
prod(0', z0) -> 0'
prod(s(z0), z1) -> add(z1, prod(z0, z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
zero(0') -> true
zero(s(z0)) -> false
p(s(z0)) -> z0

Types:
FACT :: 0':s -> c:c1
c :: c6:c7 -> c8:c9 -> c:c1
IF :: true:false -> 0':s -> 0':s -> c6:c7
zero :: 0':s -> true:false
s :: 0':s -> 0':s
0' :: 0':s
prod :: 0':s -> 0':s -> 0':s
fact :: 0':s -> 0':s
p :: 0':s -> 0':s
ZERO :: 0':s -> c8:c9
c1 :: c6:c7 -> c4:c5 -> c:c1 -> c10 -> c:c1
PROD :: 0':s -> 0':s -> c4:c5
P :: 0':s -> c10
ADD :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c6:c7
c8 :: c8:c9
c9 :: c8:c9
c10 :: c10
if :: true:false -> 0':s -> 0':s -> 0':s
add :: 0':s -> 0':s -> 0':s
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c6:c73_11 :: c6:c7
hole_c8:c94_11 :: c8:c9
hole_true:false5_11 :: true:false
hole_c4:c56_11 :: c4:c5
hole_c107_11 :: c10
hole_c2:c38_11 :: c2:c3
gen_c:c19_11 :: Nat -> c:c1
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c511_11 :: Nat -> c4:c5
gen_c2:c312_11 :: Nat -> c2:c3


Generator Equations:
gen_c:c19_11(0) <=> c(c6, c8)
gen_c:c19_11(+(x, 1)) <=> c1(c6, c4, gen_c:c19_11(x), c10)
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c511_11(0) <=> c4
gen_c4:c511_11(+(x, 1)) <=> c5(c2, gen_c4:c511_11(x))
gen_c2:c312_11(0) <=> c2
gen_c2:c312_11(+(x, 1)) <=> c3(gen_c2:c312_11(x))


The following defined symbols remain to be analysed:
ADD, FACT, prod, fact, PROD, add

They will be analysed ascendingly in the following order:
prod < FACT
fact < FACT
PROD < FACT
prod < fact
prod < PROD
add < prod
ADD < PROD

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

(7) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ADD(gen_0':s10_11(n14_11), gen_0':s10_11(b)) -> gen_c2:c312_11(n14_11), rt in Omega(1 + n14_11)

Induction Base:
ADD(gen_0':s10_11(0), gen_0':s10_11(b)) ->_R^Omega(1)
c2

Induction Step:
ADD(gen_0':s10_11(+(n14_11, 1)), gen_0':s10_11(b)) ->_R^Omega(1)
c3(ADD(gen_0':s10_11(n14_11), gen_0':s10_11(b))) ->_IH
c3(gen_c2:c312_11(c15_11))

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

(8)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
FACT(z0) -> c(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), ZERO(z0))
FACT(z0) -> c1(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
ADD(0', z0) -> c2
ADD(s(z0), z1) -> c3(ADD(z0, z1))
PROD(0', z0) -> c4
PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ZERO(0') -> c8
ZERO(s(z0)) -> c9
P(s(z0)) -> c10
fact(z0) -> if(zero(z0), s(0'), prod(z0, fact(p(z0))))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
prod(0', z0) -> 0'
prod(s(z0), z1) -> add(z1, prod(z0, z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
zero(0') -> true
zero(s(z0)) -> false
p(s(z0)) -> z0

Types:
FACT :: 0':s -> c:c1
c :: c6:c7 -> c8:c9 -> c:c1
IF :: true:false -> 0':s -> 0':s -> c6:c7
zero :: 0':s -> true:false
s :: 0':s -> 0':s
0' :: 0':s
prod :: 0':s -> 0':s -> 0':s
fact :: 0':s -> 0':s
p :: 0':s -> 0':s
ZERO :: 0':s -> c8:c9
c1 :: c6:c7 -> c4:c5 -> c:c1 -> c10 -> c:c1
PROD :: 0':s -> 0':s -> c4:c5
P :: 0':s -> c10
ADD :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c6:c7
c8 :: c8:c9
c9 :: c8:c9
c10 :: c10
if :: true:false -> 0':s -> 0':s -> 0':s
add :: 0':s -> 0':s -> 0':s
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c6:c73_11 :: c6:c7
hole_c8:c94_11 :: c8:c9
hole_true:false5_11 :: true:false
hole_c4:c56_11 :: c4:c5
hole_c107_11 :: c10
hole_c2:c38_11 :: c2:c3
gen_c:c19_11 :: Nat -> c:c1
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c511_11 :: Nat -> c4:c5
gen_c2:c312_11 :: Nat -> c2:c3


Generator Equations:
gen_c:c19_11(0) <=> c(c6, c8)
gen_c:c19_11(+(x, 1)) <=> c1(c6, c4, gen_c:c19_11(x), c10)
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c511_11(0) <=> c4
gen_c4:c511_11(+(x, 1)) <=> c5(c2, gen_c4:c511_11(x))
gen_c2:c312_11(0) <=> c2
gen_c2:c312_11(+(x, 1)) <=> c3(gen_c2:c312_11(x))


The following defined symbols remain to be analysed:
ADD, FACT, prod, fact, PROD, add

They will be analysed ascendingly in the following order:
prod < FACT
fact < FACT
PROD < FACT
prod < fact
prod < PROD
add < prod
ADD < PROD

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

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

(11)
BOUNDS(n^1, INF)

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

(12)
Obligation:
Innermost TRS:
Rules:
FACT(z0) -> c(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), ZERO(z0))
FACT(z0) -> c1(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
ADD(0', z0) -> c2
ADD(s(z0), z1) -> c3(ADD(z0, z1))
PROD(0', z0) -> c4
PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ZERO(0') -> c8
ZERO(s(z0)) -> c9
P(s(z0)) -> c10
fact(z0) -> if(zero(z0), s(0'), prod(z0, fact(p(z0))))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
prod(0', z0) -> 0'
prod(s(z0), z1) -> add(z1, prod(z0, z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
zero(0') -> true
zero(s(z0)) -> false
p(s(z0)) -> z0

Types:
FACT :: 0':s -> c:c1
c :: c6:c7 -> c8:c9 -> c:c1
IF :: true:false -> 0':s -> 0':s -> c6:c7
zero :: 0':s -> true:false
s :: 0':s -> 0':s
0' :: 0':s
prod :: 0':s -> 0':s -> 0':s
fact :: 0':s -> 0':s
p :: 0':s -> 0':s
ZERO :: 0':s -> c8:c9
c1 :: c6:c7 -> c4:c5 -> c:c1 -> c10 -> c:c1
PROD :: 0':s -> 0':s -> c4:c5
P :: 0':s -> c10
ADD :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c6:c7
c8 :: c8:c9
c9 :: c8:c9
c10 :: c10
if :: true:false -> 0':s -> 0':s -> 0':s
add :: 0':s -> 0':s -> 0':s
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c6:c73_11 :: c6:c7
hole_c8:c94_11 :: c8:c9
hole_true:false5_11 :: true:false
hole_c4:c56_11 :: c4:c5
hole_c107_11 :: c10
hole_c2:c38_11 :: c2:c3
gen_c:c19_11 :: Nat -> c:c1
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c511_11 :: Nat -> c4:c5
gen_c2:c312_11 :: Nat -> c2:c3


Lemmas:
ADD(gen_0':s10_11(n14_11), gen_0':s10_11(b)) -> gen_c2:c312_11(n14_11), rt in Omega(1 + n14_11)


Generator Equations:
gen_c:c19_11(0) <=> c(c6, c8)
gen_c:c19_11(+(x, 1)) <=> c1(c6, c4, gen_c:c19_11(x), c10)
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c511_11(0) <=> c4
gen_c4:c511_11(+(x, 1)) <=> c5(c2, gen_c4:c511_11(x))
gen_c2:c312_11(0) <=> c2
gen_c2:c312_11(+(x, 1)) <=> c3(gen_c2:c312_11(x))


The following defined symbols remain to be analysed:
add, FACT, prod, fact, PROD

They will be analysed ascendingly in the following order:
prod < FACT
fact < FACT
PROD < FACT
prod < fact
prod < PROD
add < prod

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
add(gen_0':s10_11(n674_11), gen_0':s10_11(b)) -> gen_0':s10_11(+(n674_11, b)), rt in Omega(0)

Induction Base:
add(gen_0':s10_11(0), gen_0':s10_11(b)) ->_R^Omega(0)
gen_0':s10_11(b)

Induction Step:
add(gen_0':s10_11(+(n674_11, 1)), gen_0':s10_11(b)) ->_R^Omega(0)
s(add(gen_0':s10_11(n674_11), gen_0':s10_11(b))) ->_IH
s(gen_0':s10_11(+(b, c675_11)))

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

(14)
Obligation:
Innermost TRS:
Rules:
FACT(z0) -> c(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), ZERO(z0))
FACT(z0) -> c1(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
ADD(0', z0) -> c2
ADD(s(z0), z1) -> c3(ADD(z0, z1))
PROD(0', z0) -> c4
PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ZERO(0') -> c8
ZERO(s(z0)) -> c9
P(s(z0)) -> c10
fact(z0) -> if(zero(z0), s(0'), prod(z0, fact(p(z0))))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
prod(0', z0) -> 0'
prod(s(z0), z1) -> add(z1, prod(z0, z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
zero(0') -> true
zero(s(z0)) -> false
p(s(z0)) -> z0

Types:
FACT :: 0':s -> c:c1
c :: c6:c7 -> c8:c9 -> c:c1
IF :: true:false -> 0':s -> 0':s -> c6:c7
zero :: 0':s -> true:false
s :: 0':s -> 0':s
0' :: 0':s
prod :: 0':s -> 0':s -> 0':s
fact :: 0':s -> 0':s
p :: 0':s -> 0':s
ZERO :: 0':s -> c8:c9
c1 :: c6:c7 -> c4:c5 -> c:c1 -> c10 -> c:c1
PROD :: 0':s -> 0':s -> c4:c5
P :: 0':s -> c10
ADD :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c6:c7
c8 :: c8:c9
c9 :: c8:c9
c10 :: c10
if :: true:false -> 0':s -> 0':s -> 0':s
add :: 0':s -> 0':s -> 0':s
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c6:c73_11 :: c6:c7
hole_c8:c94_11 :: c8:c9
hole_true:false5_11 :: true:false
hole_c4:c56_11 :: c4:c5
hole_c107_11 :: c10
hole_c2:c38_11 :: c2:c3
gen_c:c19_11 :: Nat -> c:c1
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c511_11 :: Nat -> c4:c5
gen_c2:c312_11 :: Nat -> c2:c3


Lemmas:
ADD(gen_0':s10_11(n14_11), gen_0':s10_11(b)) -> gen_c2:c312_11(n14_11), rt in Omega(1 + n14_11)
add(gen_0':s10_11(n674_11), gen_0':s10_11(b)) -> gen_0':s10_11(+(n674_11, b)), rt in Omega(0)


Generator Equations:
gen_c:c19_11(0) <=> c(c6, c8)
gen_c:c19_11(+(x, 1)) <=> c1(c6, c4, gen_c:c19_11(x), c10)
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c511_11(0) <=> c4
gen_c4:c511_11(+(x, 1)) <=> c5(c2, gen_c4:c511_11(x))
gen_c2:c312_11(0) <=> c2
gen_c2:c312_11(+(x, 1)) <=> c3(gen_c2:c312_11(x))


The following defined symbols remain to be analysed:
prod, FACT, fact, PROD

They will be analysed ascendingly in the following order:
prod < FACT
fact < FACT
PROD < FACT
prod < fact
prod < PROD

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
prod(gen_0':s10_11(n1867_11), gen_0':s10_11(b)) -> gen_0':s10_11(*(n1867_11, b)), rt in Omega(0)

Induction Base:
prod(gen_0':s10_11(0), gen_0':s10_11(b)) ->_R^Omega(0)
0'

Induction Step:
prod(gen_0':s10_11(+(n1867_11, 1)), gen_0':s10_11(b)) ->_R^Omega(0)
add(gen_0':s10_11(b), prod(gen_0':s10_11(n1867_11), gen_0':s10_11(b))) ->_IH
add(gen_0':s10_11(b), gen_0':s10_11(*(c1868_11, b))) ->_L^Omega(0)
gen_0':s10_11(+(b, *(n1867_11, b)))

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

(16)
Obligation:
Innermost TRS:
Rules:
FACT(z0) -> c(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), ZERO(z0))
FACT(z0) -> c1(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
ADD(0', z0) -> c2
ADD(s(z0), z1) -> c3(ADD(z0, z1))
PROD(0', z0) -> c4
PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ZERO(0') -> c8
ZERO(s(z0)) -> c9
P(s(z0)) -> c10
fact(z0) -> if(zero(z0), s(0'), prod(z0, fact(p(z0))))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
prod(0', z0) -> 0'
prod(s(z0), z1) -> add(z1, prod(z0, z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
zero(0') -> true
zero(s(z0)) -> false
p(s(z0)) -> z0

Types:
FACT :: 0':s -> c:c1
c :: c6:c7 -> c8:c9 -> c:c1
IF :: true:false -> 0':s -> 0':s -> c6:c7
zero :: 0':s -> true:false
s :: 0':s -> 0':s
0' :: 0':s
prod :: 0':s -> 0':s -> 0':s
fact :: 0':s -> 0':s
p :: 0':s -> 0':s
ZERO :: 0':s -> c8:c9
c1 :: c6:c7 -> c4:c5 -> c:c1 -> c10 -> c:c1
PROD :: 0':s -> 0':s -> c4:c5
P :: 0':s -> c10
ADD :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c6:c7
c8 :: c8:c9
c9 :: c8:c9
c10 :: c10
if :: true:false -> 0':s -> 0':s -> 0':s
add :: 0':s -> 0':s -> 0':s
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c6:c73_11 :: c6:c7
hole_c8:c94_11 :: c8:c9
hole_true:false5_11 :: true:false
hole_c4:c56_11 :: c4:c5
hole_c107_11 :: c10
hole_c2:c38_11 :: c2:c3
gen_c:c19_11 :: Nat -> c:c1
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c511_11 :: Nat -> c4:c5
gen_c2:c312_11 :: Nat -> c2:c3


Lemmas:
ADD(gen_0':s10_11(n14_11), gen_0':s10_11(b)) -> gen_c2:c312_11(n14_11), rt in Omega(1 + n14_11)
add(gen_0':s10_11(n674_11), gen_0':s10_11(b)) -> gen_0':s10_11(+(n674_11, b)), rt in Omega(0)
prod(gen_0':s10_11(n1867_11), gen_0':s10_11(b)) -> gen_0':s10_11(*(n1867_11, b)), rt in Omega(0)


Generator Equations:
gen_c:c19_11(0) <=> c(c6, c8)
gen_c:c19_11(+(x, 1)) <=> c1(c6, c4, gen_c:c19_11(x), c10)
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c511_11(0) <=> c4
gen_c4:c511_11(+(x, 1)) <=> c5(c2, gen_c4:c511_11(x))
gen_c2:c312_11(0) <=> c2
gen_c2:c312_11(+(x, 1)) <=> c3(gen_c2:c312_11(x))


The following defined symbols remain to be analysed:
fact, FACT, PROD

They will be analysed ascendingly in the following order:
fact < FACT
PROD < FACT

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PROD(gen_0':s10_11(n189426_11), gen_0':s10_11(b)) -> *13_11, rt in Omega(b*n189426_11 + n189426_11)

Induction Base:
PROD(gen_0':s10_11(0), gen_0':s10_11(b))

Induction Step:
PROD(gen_0':s10_11(+(n189426_11, 1)), gen_0':s10_11(b)) ->_R^Omega(1)
c5(ADD(gen_0':s10_11(b), prod(gen_0':s10_11(n189426_11), gen_0':s10_11(b))), PROD(gen_0':s10_11(n189426_11), gen_0':s10_11(b))) ->_L^Omega(0)
c5(ADD(gen_0':s10_11(b), gen_0':s10_11(*(n189426_11, b))), PROD(gen_0':s10_11(n189426_11), gen_0':s10_11(b))) ->_L^Omega(1 + b)
c5(gen_c2:c312_11(b), PROD(gen_0':s10_11(n189426_11), gen_0':s10_11(*(n189426_11, b)))) ->_IH
c5(gen_c2:c312_11(*(n189426_11, b)), *13_11)

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

(18)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
FACT(z0) -> c(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), ZERO(z0))
FACT(z0) -> c1(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
ADD(0', z0) -> c2
ADD(s(z0), z1) -> c3(ADD(z0, z1))
PROD(0', z0) -> c4
PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ZERO(0') -> c8
ZERO(s(z0)) -> c9
P(s(z0)) -> c10
fact(z0) -> if(zero(z0), s(0'), prod(z0, fact(p(z0))))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
prod(0', z0) -> 0'
prod(s(z0), z1) -> add(z1, prod(z0, z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
zero(0') -> true
zero(s(z0)) -> false
p(s(z0)) -> z0

Types:
FACT :: 0':s -> c:c1
c :: c6:c7 -> c8:c9 -> c:c1
IF :: true:false -> 0':s -> 0':s -> c6:c7
zero :: 0':s -> true:false
s :: 0':s -> 0':s
0' :: 0':s
prod :: 0':s -> 0':s -> 0':s
fact :: 0':s -> 0':s
p :: 0':s -> 0':s
ZERO :: 0':s -> c8:c9
c1 :: c6:c7 -> c4:c5 -> c:c1 -> c10 -> c:c1
PROD :: 0':s -> 0':s -> c4:c5
P :: 0':s -> c10
ADD :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c6:c7
c8 :: c8:c9
c9 :: c8:c9
c10 :: c10
if :: true:false -> 0':s -> 0':s -> 0':s
add :: 0':s -> 0':s -> 0':s
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c6:c73_11 :: c6:c7
hole_c8:c94_11 :: c8:c9
hole_true:false5_11 :: true:false
hole_c4:c56_11 :: c4:c5
hole_c107_11 :: c10
hole_c2:c38_11 :: c2:c3
gen_c:c19_11 :: Nat -> c:c1
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c511_11 :: Nat -> c4:c5
gen_c2:c312_11 :: Nat -> c2:c3


Lemmas:
ADD(gen_0':s10_11(n14_11), gen_0':s10_11(b)) -> gen_c2:c312_11(n14_11), rt in Omega(1 + n14_11)
add(gen_0':s10_11(n674_11), gen_0':s10_11(b)) -> gen_0':s10_11(+(n674_11, b)), rt in Omega(0)
prod(gen_0':s10_11(n1867_11), gen_0':s10_11(b)) -> gen_0':s10_11(*(n1867_11, b)), rt in Omega(0)


Generator Equations:
gen_c:c19_11(0) <=> c(c6, c8)
gen_c:c19_11(+(x, 1)) <=> c1(c6, c4, gen_c:c19_11(x), c10)
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c511_11(0) <=> c4
gen_c4:c511_11(+(x, 1)) <=> c5(c2, gen_c4:c511_11(x))
gen_c2:c312_11(0) <=> c2
gen_c2:c312_11(+(x, 1)) <=> c3(gen_c2:c312_11(x))


The following defined symbols remain to be analysed:
PROD, FACT

They will be analysed ascendingly in the following order:
PROD < FACT

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

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

(21)
BOUNDS(n^2, INF)

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

(22)
Obligation:
Innermost TRS:
Rules:
FACT(z0) -> c(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), ZERO(z0))
FACT(z0) -> c1(IF(zero(z0), s(0'), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
ADD(0', z0) -> c2
ADD(s(z0), z1) -> c3(ADD(z0, z1))
PROD(0', z0) -> c4
PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ZERO(0') -> c8
ZERO(s(z0)) -> c9
P(s(z0)) -> c10
fact(z0) -> if(zero(z0), s(0'), prod(z0, fact(p(z0))))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
prod(0', z0) -> 0'
prod(s(z0), z1) -> add(z1, prod(z0, z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
zero(0') -> true
zero(s(z0)) -> false
p(s(z0)) -> z0

Types:
FACT :: 0':s -> c:c1
c :: c6:c7 -> c8:c9 -> c:c1
IF :: true:false -> 0':s -> 0':s -> c6:c7
zero :: 0':s -> true:false
s :: 0':s -> 0':s
0' :: 0':s
prod :: 0':s -> 0':s -> 0':s
fact :: 0':s -> 0':s
p :: 0':s -> 0':s
ZERO :: 0':s -> c8:c9
c1 :: c6:c7 -> c4:c5 -> c:c1 -> c10 -> c:c1
PROD :: 0':s -> 0':s -> c4:c5
P :: 0':s -> c10
ADD :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c6:c7
c8 :: c8:c9
c9 :: c8:c9
c10 :: c10
if :: true:false -> 0':s -> 0':s -> 0':s
add :: 0':s -> 0':s -> 0':s
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c6:c73_11 :: c6:c7
hole_c8:c94_11 :: c8:c9
hole_true:false5_11 :: true:false
hole_c4:c56_11 :: c4:c5
hole_c107_11 :: c10
hole_c2:c38_11 :: c2:c3
gen_c:c19_11 :: Nat -> c:c1
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c511_11 :: Nat -> c4:c5
gen_c2:c312_11 :: Nat -> c2:c3


Lemmas:
ADD(gen_0':s10_11(n14_11), gen_0':s10_11(b)) -> gen_c2:c312_11(n14_11), rt in Omega(1 + n14_11)
add(gen_0':s10_11(n674_11), gen_0':s10_11(b)) -> gen_0':s10_11(+(n674_11, b)), rt in Omega(0)
prod(gen_0':s10_11(n1867_11), gen_0':s10_11(b)) -> gen_0':s10_11(*(n1867_11, b)), rt in Omega(0)
PROD(gen_0':s10_11(n189426_11), gen_0':s10_11(b)) -> *13_11, rt in Omega(b*n189426_11 + n189426_11)


Generator Equations:
gen_c:c19_11(0) <=> c(c6, c8)
gen_c:c19_11(+(x, 1)) <=> c1(c6, c4, gen_c:c19_11(x), c10)
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c511_11(0) <=> c4
gen_c4:c511_11(+(x, 1)) <=> c5(c2, gen_c4:c511_11(x))
gen_c2:c312_11(0) <=> c2
gen_c2:c312_11(+(x, 1)) <=> c3(gen_c2:c312_11(x))


The following defined symbols remain to be analysed:
FACT