WORST_CASE(Omega(n^2),?)
proof of input_fNlWOOhKzx.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), 14 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 262 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), 79 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 29 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 7437 ms]
        (22) BEST
            (23) proven lower bound
                (24) LowerBoundPropagationProof [FINISHED, 0 ms]
                (25) BOUNDS(n^2, INF)
            (26) typed CpxTrs


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

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

   fact(X) -> if(zero(X), s(0), prod(X, fact(p(X))))
   add(0, X) -> X
   add(s(X), Y) -> s(add(X, Y))
   prod(0, X) -> 0
   prod(s(X), Y) -> add(Y, prod(X, Y))
   if(true, X, Y) -> X
   if(false, X, Y) -> Y
   zero(0) -> true
   zero(s(X)) -> false
   p(s(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:
   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
Tuples:
   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
S tuples:
   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
K tuples:none
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   FACT_1, ADD_2, PROD_2, IF_3, ZERO_1, P_1

Compound Symbols:   c_2, c1_4, c2, c3_1, c4, c5_2, c6, c7, c8, c9, c10


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

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

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

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

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

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

(8)
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

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

(9) 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

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

(10)
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

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

(11) 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).
----------------------------------------

(12)
Complex Obligation (BEST)

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

(13)
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

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

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

(15)
BOUNDS(n^1, INF)

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

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


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

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

(17) 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).
----------------------------------------

(18)
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

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

(19) 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).
----------------------------------------

(20)
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

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

(21) 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).
----------------------------------------

(22)
Complex Obligation (BEST)

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

(23)
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

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

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

(25)
BOUNDS(n^2, INF)

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

(26)
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