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


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, 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), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 378 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), 57 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 43 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 88 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 1827 ms]
        (24) typed CpxTrs


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

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


The TRS R consists of the following rules:

   lt(0, s(x)) -> true
   lt(x, 0) -> false
   lt(s(x), s(y)) -> lt(x, y)
   fibo(0) -> fib(0)
   fibo(s(0)) -> fib(s(0))
   fibo(s(s(x))) -> sum(fibo(s(x)), fibo(x))
   fib(0) -> s(0)
   fib(s(0)) -> s(0)
   fib(s(s(x))) -> if(true, 0, s(s(x)), 0, 0)
   if(true, c, s(s(x)), a, b) -> if(lt(s(c), s(s(x))), s(c), s(s(x)), b, c)
   if(false, c, s(s(x)), a, b) -> sum(fibo(a), fibo(b))
   sum(x, 0) -> x
   sum(x, s(y)) -> s(sum(x, y))

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:
   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   fibo(0) -> fib(0)
   fibo(s(0)) -> fib(s(0))
   fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
   fib(0) -> s(0)
   fib(s(0)) -> s(0)
   fib(s(s(z0))) -> if(true, 0, s(s(z0)), 0, 0)
   if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
   if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
   sum(z0, 0) -> z0
   sum(z0, s(z1)) -> s(sum(z0, z1))
Tuples:
   LT(0, s(z0)) -> c
   LT(z0, 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   FIBO(0) -> c3(FIB(0))
   FIBO(s(0)) -> c4(FIB(s(0)))
   FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
   FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
   FIB(0) -> c7
   FIB(s(0)) -> c8
   FIB(s(s(z0))) -> c9(IF(true, 0, s(s(z0)), 0, 0))
   IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
   IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
   IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
   SUM(z0, 0) -> c13
   SUM(z0, s(z1)) -> c14(SUM(z0, z1))
S tuples:
   LT(0, s(z0)) -> c
   LT(z0, 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   FIBO(0) -> c3(FIB(0))
   FIBO(s(0)) -> c4(FIB(s(0)))
   FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
   FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
   FIB(0) -> c7
   FIB(s(0)) -> c8
   FIB(s(s(z0))) -> c9(IF(true, 0, s(s(z0)), 0, 0))
   IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
   IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
   IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
   SUM(z0, 0) -> c13
   SUM(z0, s(z1)) -> c14(SUM(z0, z1))
K tuples:none
Defined Rule Symbols:   lt_2, fibo_1, fib_1, if_5, sum_2

Defined Pair Symbols:   LT_2, FIBO_1, FIB_1, IF_5, SUM_2

Compound Symbols:   c, c1, c2_1, c3_1, c4_1, c5_2, c6_2, c7, c8, c9_1, c10_2, c11_2, c12_2, c13, c14_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^1, INF).


The TRS R consists of the following rules:

   LT(0, s(z0)) -> c
   LT(z0, 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   FIBO(0) -> c3(FIB(0))
   FIBO(s(0)) -> c4(FIB(s(0)))
   FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
   FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
   FIB(0) -> c7
   FIB(s(0)) -> c8
   FIB(s(s(z0))) -> c9(IF(true, 0, s(s(z0)), 0, 0))
   IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
   IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
   IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
   SUM(z0, 0) -> c13
   SUM(z0, s(z1)) -> c14(SUM(z0, z1))

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

   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   fibo(0) -> fib(0)
   fibo(s(0)) -> fib(s(0))
   fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
   fib(0) -> s(0)
   fib(s(0)) -> s(0)
   fib(s(s(z0))) -> if(true, 0, s(s(z0)), 0, 0)
   if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
   if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
   sum(z0, 0) -> z0
   sum(z0, s(z1)) -> s(sum(z0, z1))

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


The TRS R consists of the following rules:

   LT(0', s(z0)) -> c
   LT(z0, 0') -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   FIBO(0') -> c3(FIB(0'))
   FIBO(s(0')) -> c4(FIB(s(0')))
   FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
   FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
   FIB(0') -> c7
   FIB(s(0')) -> c8
   FIB(s(s(z0))) -> c9(IF(true, 0', s(s(z0)), 0', 0'))
   IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
   IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
   IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
   SUM(z0, 0') -> c13
   SUM(z0, s(z1)) -> c14(SUM(z0, z1))

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

   lt(0', s(z0)) -> true
   lt(z0, 0') -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   fibo(0') -> fib(0')
   fibo(s(0')) -> fib(s(0'))
   fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
   fib(0') -> s(0')
   fib(s(0')) -> s(0')
   fib(s(s(z0))) -> if(true, 0', s(s(z0)), 0', 0')
   if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
   if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
   sum(z0, 0') -> z0
   sum(z0, s(z1)) -> s(sum(z0, z1))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
FIBO(0') -> c3(FIB(0'))
FIBO(s(0')) -> c4(FIB(s(0')))
FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
FIB(0') -> c7
FIB(s(0')) -> c8
FIB(s(s(z0))) -> c9(IF(true, 0', s(s(z0)), 0', 0'))
IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
SUM(z0, 0') -> c13
SUM(z0, s(z1)) -> c14(SUM(z0, z1))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
fibo(0') -> fib(0')
fibo(s(0')) -> fib(s(0'))
fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
fib(0') -> s(0')
fib(s(0')) -> s(0')
fib(s(s(z0))) -> if(true, 0', s(s(z0)), 0', 0')
if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
sum(z0, 0') -> z0
sum(z0, s(z1)) -> s(sum(z0, z1))

Types:
LT :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
s :: 0':s -> 0':s
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
FIBO :: 0':s -> c3:c4:c5:c6
c3 :: c7:c8:c9 -> c3:c4:c5:c6
FIB :: 0':s -> c7:c8:c9
c4 :: c7:c8:c9 -> c3:c4:c5:c6
c5 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
SUM :: 0':s -> 0':s -> c13:c14
fibo :: 0':s -> 0':s
c6 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c10:c11:c12 -> c7:c8:c9
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c10:c11:c12
true :: true:false
c10 :: c10:c11:c12 -> c:c1:c2 -> c10:c11:c12
lt :: 0':s -> 0':s -> true:false
false :: true:false
c11 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c13 :: c13:c14
c14 :: c13:c14 -> c13:c14
fib :: 0':s -> 0':s
sum :: 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_15 :: c:c1:c2
hole_0':s2_15 :: 0':s
hole_c3:c4:c5:c63_15 :: c3:c4:c5:c6
hole_c7:c8:c94_15 :: c7:c8:c9
hole_c13:c145_15 :: c13:c14
hole_c10:c11:c126_15 :: c10:c11:c12
hole_true:false7_15 :: true:false
gen_c:c1:c28_15 :: Nat -> c:c1:c2
gen_0':s9_15 :: Nat -> 0':s
gen_c3:c4:c5:c610_15 :: Nat -> c3:c4:c5:c6
gen_c13:c1411_15 :: Nat -> c13:c14
gen_c10:c11:c1212_15 :: Nat -> c10:c11:c12

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LT, FIBO, FIB, SUM, fibo, IF, lt, fib, sum, if

They will be analysed ascendingly in the following order:
LT < IF
FIBO = FIB
SUM < FIBO
fibo < FIBO
FIBO = IF
FIB = IF
SUM < IF
fibo < IF
fibo = fib
sum < fibo
fibo = if
lt < IF
lt < if
fib = if
sum < if

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

(10)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
FIBO(0') -> c3(FIB(0'))
FIBO(s(0')) -> c4(FIB(s(0')))
FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
FIB(0') -> c7
FIB(s(0')) -> c8
FIB(s(s(z0))) -> c9(IF(true, 0', s(s(z0)), 0', 0'))
IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
SUM(z0, 0') -> c13
SUM(z0, s(z1)) -> c14(SUM(z0, z1))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
fibo(0') -> fib(0')
fibo(s(0')) -> fib(s(0'))
fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
fib(0') -> s(0')
fib(s(0')) -> s(0')
fib(s(s(z0))) -> if(true, 0', s(s(z0)), 0', 0')
if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
sum(z0, 0') -> z0
sum(z0, s(z1)) -> s(sum(z0, z1))

Types:
LT :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
s :: 0':s -> 0':s
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
FIBO :: 0':s -> c3:c4:c5:c6
c3 :: c7:c8:c9 -> c3:c4:c5:c6
FIB :: 0':s -> c7:c8:c9
c4 :: c7:c8:c9 -> c3:c4:c5:c6
c5 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
SUM :: 0':s -> 0':s -> c13:c14
fibo :: 0':s -> 0':s
c6 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c10:c11:c12 -> c7:c8:c9
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c10:c11:c12
true :: true:false
c10 :: c10:c11:c12 -> c:c1:c2 -> c10:c11:c12
lt :: 0':s -> 0':s -> true:false
false :: true:false
c11 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c13 :: c13:c14
c14 :: c13:c14 -> c13:c14
fib :: 0':s -> 0':s
sum :: 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_15 :: c:c1:c2
hole_0':s2_15 :: 0':s
hole_c3:c4:c5:c63_15 :: c3:c4:c5:c6
hole_c7:c8:c94_15 :: c7:c8:c9
hole_c13:c145_15 :: c13:c14
hole_c10:c11:c126_15 :: c10:c11:c12
hole_true:false7_15 :: true:false
gen_c:c1:c28_15 :: Nat -> c:c1:c2
gen_0':s9_15 :: Nat -> 0':s
gen_c3:c4:c5:c610_15 :: Nat -> c3:c4:c5:c6
gen_c13:c1411_15 :: Nat -> c13:c14
gen_c10:c11:c1212_15 :: Nat -> c10:c11:c12


Generator Equations:
gen_c:c1:c28_15(0) <=> c
gen_c:c1:c28_15(+(x, 1)) <=> c2(gen_c:c1:c28_15(x))
gen_0':s9_15(0) <=> 0'
gen_0':s9_15(+(x, 1)) <=> s(gen_0':s9_15(x))
gen_c3:c4:c5:c610_15(0) <=> c3(c7)
gen_c3:c4:c5:c610_15(+(x, 1)) <=> c5(c13, gen_c3:c4:c5:c610_15(x))
gen_c13:c1411_15(0) <=> c13
gen_c13:c1411_15(+(x, 1)) <=> c14(gen_c13:c1411_15(x))
gen_c10:c11:c1212_15(0) <=> c11(c13, c3(c7))
gen_c10:c11:c1212_15(+(x, 1)) <=> c10(gen_c10:c11:c1212_15(x), c)


The following defined symbols remain to be analysed:
LT, FIBO, FIB, SUM, fibo, IF, lt, fib, sum, if

They will be analysed ascendingly in the following order:
LT < IF
FIBO = FIB
SUM < FIBO
fibo < FIBO
FIBO = IF
FIB = IF
SUM < IF
fibo < IF
fibo = fib
sum < fibo
fibo = if
lt < IF
lt < if
fib = if
sum < if

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LT(gen_0':s9_15(n14_15), gen_0':s9_15(+(1, n14_15))) -> gen_c:c1:c28_15(n14_15), rt in Omega(1 + n14_15)

Induction Base:
LT(gen_0':s9_15(0), gen_0':s9_15(+(1, 0))) ->_R^Omega(1)
c

Induction Step:
LT(gen_0':s9_15(+(n14_15, 1)), gen_0':s9_15(+(1, +(n14_15, 1)))) ->_R^Omega(1)
c2(LT(gen_0':s9_15(n14_15), gen_0':s9_15(+(1, n14_15)))) ->_IH
c2(gen_c:c1:c28_15(c15_15))

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:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
FIBO(0') -> c3(FIB(0'))
FIBO(s(0')) -> c4(FIB(s(0')))
FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
FIB(0') -> c7
FIB(s(0')) -> c8
FIB(s(s(z0))) -> c9(IF(true, 0', s(s(z0)), 0', 0'))
IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
SUM(z0, 0') -> c13
SUM(z0, s(z1)) -> c14(SUM(z0, z1))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
fibo(0') -> fib(0')
fibo(s(0')) -> fib(s(0'))
fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
fib(0') -> s(0')
fib(s(0')) -> s(0')
fib(s(s(z0))) -> if(true, 0', s(s(z0)), 0', 0')
if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
sum(z0, 0') -> z0
sum(z0, s(z1)) -> s(sum(z0, z1))

Types:
LT :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
s :: 0':s -> 0':s
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
FIBO :: 0':s -> c3:c4:c5:c6
c3 :: c7:c8:c9 -> c3:c4:c5:c6
FIB :: 0':s -> c7:c8:c9
c4 :: c7:c8:c9 -> c3:c4:c5:c6
c5 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
SUM :: 0':s -> 0':s -> c13:c14
fibo :: 0':s -> 0':s
c6 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c10:c11:c12 -> c7:c8:c9
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c10:c11:c12
true :: true:false
c10 :: c10:c11:c12 -> c:c1:c2 -> c10:c11:c12
lt :: 0':s -> 0':s -> true:false
false :: true:false
c11 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c13 :: c13:c14
c14 :: c13:c14 -> c13:c14
fib :: 0':s -> 0':s
sum :: 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_15 :: c:c1:c2
hole_0':s2_15 :: 0':s
hole_c3:c4:c5:c63_15 :: c3:c4:c5:c6
hole_c7:c8:c94_15 :: c7:c8:c9
hole_c13:c145_15 :: c13:c14
hole_c10:c11:c126_15 :: c10:c11:c12
hole_true:false7_15 :: true:false
gen_c:c1:c28_15 :: Nat -> c:c1:c2
gen_0':s9_15 :: Nat -> 0':s
gen_c3:c4:c5:c610_15 :: Nat -> c3:c4:c5:c6
gen_c13:c1411_15 :: Nat -> c13:c14
gen_c10:c11:c1212_15 :: Nat -> c10:c11:c12


Generator Equations:
gen_c:c1:c28_15(0) <=> c
gen_c:c1:c28_15(+(x, 1)) <=> c2(gen_c:c1:c28_15(x))
gen_0':s9_15(0) <=> 0'
gen_0':s9_15(+(x, 1)) <=> s(gen_0':s9_15(x))
gen_c3:c4:c5:c610_15(0) <=> c3(c7)
gen_c3:c4:c5:c610_15(+(x, 1)) <=> c5(c13, gen_c3:c4:c5:c610_15(x))
gen_c13:c1411_15(0) <=> c13
gen_c13:c1411_15(+(x, 1)) <=> c14(gen_c13:c1411_15(x))
gen_c10:c11:c1212_15(0) <=> c11(c13, c3(c7))
gen_c10:c11:c1212_15(+(x, 1)) <=> c10(gen_c10:c11:c1212_15(x), c)


The following defined symbols remain to be analysed:
LT, FIBO, FIB, SUM, fibo, IF, lt, fib, sum, if

They will be analysed ascendingly in the following order:
LT < IF
FIBO = FIB
SUM < FIBO
fibo < FIBO
FIBO = IF
FIB = IF
SUM < IF
fibo < IF
fibo = fib
sum < fibo
fibo = if
lt < IF
lt < if
fib = if
sum < if

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
FIBO(0') -> c3(FIB(0'))
FIBO(s(0')) -> c4(FIB(s(0')))
FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
FIB(0') -> c7
FIB(s(0')) -> c8
FIB(s(s(z0))) -> c9(IF(true, 0', s(s(z0)), 0', 0'))
IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
SUM(z0, 0') -> c13
SUM(z0, s(z1)) -> c14(SUM(z0, z1))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
fibo(0') -> fib(0')
fibo(s(0')) -> fib(s(0'))
fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
fib(0') -> s(0')
fib(s(0')) -> s(0')
fib(s(s(z0))) -> if(true, 0', s(s(z0)), 0', 0')
if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
sum(z0, 0') -> z0
sum(z0, s(z1)) -> s(sum(z0, z1))

Types:
LT :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
s :: 0':s -> 0':s
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
FIBO :: 0':s -> c3:c4:c5:c6
c3 :: c7:c8:c9 -> c3:c4:c5:c6
FIB :: 0':s -> c7:c8:c9
c4 :: c7:c8:c9 -> c3:c4:c5:c6
c5 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
SUM :: 0':s -> 0':s -> c13:c14
fibo :: 0':s -> 0':s
c6 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c10:c11:c12 -> c7:c8:c9
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c10:c11:c12
true :: true:false
c10 :: c10:c11:c12 -> c:c1:c2 -> c10:c11:c12
lt :: 0':s -> 0':s -> true:false
false :: true:false
c11 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c13 :: c13:c14
c14 :: c13:c14 -> c13:c14
fib :: 0':s -> 0':s
sum :: 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_15 :: c:c1:c2
hole_0':s2_15 :: 0':s
hole_c3:c4:c5:c63_15 :: c3:c4:c5:c6
hole_c7:c8:c94_15 :: c7:c8:c9
hole_c13:c145_15 :: c13:c14
hole_c10:c11:c126_15 :: c10:c11:c12
hole_true:false7_15 :: true:false
gen_c:c1:c28_15 :: Nat -> c:c1:c2
gen_0':s9_15 :: Nat -> 0':s
gen_c3:c4:c5:c610_15 :: Nat -> c3:c4:c5:c6
gen_c13:c1411_15 :: Nat -> c13:c14
gen_c10:c11:c1212_15 :: Nat -> c10:c11:c12


Lemmas:
LT(gen_0':s9_15(n14_15), gen_0':s9_15(+(1, n14_15))) -> gen_c:c1:c28_15(n14_15), rt in Omega(1 + n14_15)


Generator Equations:
gen_c:c1:c28_15(0) <=> c
gen_c:c1:c28_15(+(x, 1)) <=> c2(gen_c:c1:c28_15(x))
gen_0':s9_15(0) <=> 0'
gen_0':s9_15(+(x, 1)) <=> s(gen_0':s9_15(x))
gen_c3:c4:c5:c610_15(0) <=> c3(c7)
gen_c3:c4:c5:c610_15(+(x, 1)) <=> c5(c13, gen_c3:c4:c5:c610_15(x))
gen_c13:c1411_15(0) <=> c13
gen_c13:c1411_15(+(x, 1)) <=> c14(gen_c13:c1411_15(x))
gen_c10:c11:c1212_15(0) <=> c11(c13, c3(c7))
gen_c10:c11:c1212_15(+(x, 1)) <=> c10(gen_c10:c11:c1212_15(x), c)


The following defined symbols remain to be analysed:
SUM, FIBO, FIB, fibo, IF, lt, fib, sum, if

They will be analysed ascendingly in the following order:
FIBO = FIB
SUM < FIBO
fibo < FIBO
FIBO = IF
FIB = IF
SUM < IF
fibo < IF
fibo = fib
sum < fibo
fibo = if
lt < IF
lt < if
fib = if
sum < if

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SUM(gen_0':s9_15(a), gen_0':s9_15(n679_15)) -> gen_c13:c1411_15(n679_15), rt in Omega(1 + n679_15)

Induction Base:
SUM(gen_0':s9_15(a), gen_0':s9_15(0)) ->_R^Omega(1)
c13

Induction Step:
SUM(gen_0':s9_15(a), gen_0':s9_15(+(n679_15, 1))) ->_R^Omega(1)
c14(SUM(gen_0':s9_15(a), gen_0':s9_15(n679_15))) ->_IH
c14(gen_c13:c1411_15(c680_15))

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

(18)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
FIBO(0') -> c3(FIB(0'))
FIBO(s(0')) -> c4(FIB(s(0')))
FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
FIB(0') -> c7
FIB(s(0')) -> c8
FIB(s(s(z0))) -> c9(IF(true, 0', s(s(z0)), 0', 0'))
IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
SUM(z0, 0') -> c13
SUM(z0, s(z1)) -> c14(SUM(z0, z1))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
fibo(0') -> fib(0')
fibo(s(0')) -> fib(s(0'))
fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
fib(0') -> s(0')
fib(s(0')) -> s(0')
fib(s(s(z0))) -> if(true, 0', s(s(z0)), 0', 0')
if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
sum(z0, 0') -> z0
sum(z0, s(z1)) -> s(sum(z0, z1))

Types:
LT :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
s :: 0':s -> 0':s
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
FIBO :: 0':s -> c3:c4:c5:c6
c3 :: c7:c8:c9 -> c3:c4:c5:c6
FIB :: 0':s -> c7:c8:c9
c4 :: c7:c8:c9 -> c3:c4:c5:c6
c5 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
SUM :: 0':s -> 0':s -> c13:c14
fibo :: 0':s -> 0':s
c6 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c10:c11:c12 -> c7:c8:c9
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c10:c11:c12
true :: true:false
c10 :: c10:c11:c12 -> c:c1:c2 -> c10:c11:c12
lt :: 0':s -> 0':s -> true:false
false :: true:false
c11 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c13 :: c13:c14
c14 :: c13:c14 -> c13:c14
fib :: 0':s -> 0':s
sum :: 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_15 :: c:c1:c2
hole_0':s2_15 :: 0':s
hole_c3:c4:c5:c63_15 :: c3:c4:c5:c6
hole_c7:c8:c94_15 :: c7:c8:c9
hole_c13:c145_15 :: c13:c14
hole_c10:c11:c126_15 :: c10:c11:c12
hole_true:false7_15 :: true:false
gen_c:c1:c28_15 :: Nat -> c:c1:c2
gen_0':s9_15 :: Nat -> 0':s
gen_c3:c4:c5:c610_15 :: Nat -> c3:c4:c5:c6
gen_c13:c1411_15 :: Nat -> c13:c14
gen_c10:c11:c1212_15 :: Nat -> c10:c11:c12


Lemmas:
LT(gen_0':s9_15(n14_15), gen_0':s9_15(+(1, n14_15))) -> gen_c:c1:c28_15(n14_15), rt in Omega(1 + n14_15)
SUM(gen_0':s9_15(a), gen_0':s9_15(n679_15)) -> gen_c13:c1411_15(n679_15), rt in Omega(1 + n679_15)


Generator Equations:
gen_c:c1:c28_15(0) <=> c
gen_c:c1:c28_15(+(x, 1)) <=> c2(gen_c:c1:c28_15(x))
gen_0':s9_15(0) <=> 0'
gen_0':s9_15(+(x, 1)) <=> s(gen_0':s9_15(x))
gen_c3:c4:c5:c610_15(0) <=> c3(c7)
gen_c3:c4:c5:c610_15(+(x, 1)) <=> c5(c13, gen_c3:c4:c5:c610_15(x))
gen_c13:c1411_15(0) <=> c13
gen_c13:c1411_15(+(x, 1)) <=> c14(gen_c13:c1411_15(x))
gen_c10:c11:c1212_15(0) <=> c11(c13, c3(c7))
gen_c10:c11:c1212_15(+(x, 1)) <=> c10(gen_c10:c11:c1212_15(x), c)


The following defined symbols remain to be analysed:
lt, FIBO, FIB, fibo, IF, fib, sum, if

They will be analysed ascendingly in the following order:
FIBO = FIB
fibo < FIBO
FIBO = IF
FIB = IF
fibo < IF
fibo = fib
sum < fibo
fibo = if
lt < IF
lt < if
fib = if
sum < if

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
lt(gen_0':s9_15(n1471_15), gen_0':s9_15(+(1, n1471_15))) -> true, rt in Omega(0)

Induction Base:
lt(gen_0':s9_15(0), gen_0':s9_15(+(1, 0))) ->_R^Omega(0)
true

Induction Step:
lt(gen_0':s9_15(+(n1471_15, 1)), gen_0':s9_15(+(1, +(n1471_15, 1)))) ->_R^Omega(0)
lt(gen_0':s9_15(n1471_15), gen_0':s9_15(+(1, n1471_15))) ->_IH
true

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:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
FIBO(0') -> c3(FIB(0'))
FIBO(s(0')) -> c4(FIB(s(0')))
FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
FIB(0') -> c7
FIB(s(0')) -> c8
FIB(s(s(z0))) -> c9(IF(true, 0', s(s(z0)), 0', 0'))
IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
SUM(z0, 0') -> c13
SUM(z0, s(z1)) -> c14(SUM(z0, z1))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
fibo(0') -> fib(0')
fibo(s(0')) -> fib(s(0'))
fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
fib(0') -> s(0')
fib(s(0')) -> s(0')
fib(s(s(z0))) -> if(true, 0', s(s(z0)), 0', 0')
if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
sum(z0, 0') -> z0
sum(z0, s(z1)) -> s(sum(z0, z1))

Types:
LT :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
s :: 0':s -> 0':s
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
FIBO :: 0':s -> c3:c4:c5:c6
c3 :: c7:c8:c9 -> c3:c4:c5:c6
FIB :: 0':s -> c7:c8:c9
c4 :: c7:c8:c9 -> c3:c4:c5:c6
c5 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
SUM :: 0':s -> 0':s -> c13:c14
fibo :: 0':s -> 0':s
c6 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c10:c11:c12 -> c7:c8:c9
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c10:c11:c12
true :: true:false
c10 :: c10:c11:c12 -> c:c1:c2 -> c10:c11:c12
lt :: 0':s -> 0':s -> true:false
false :: true:false
c11 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c13 :: c13:c14
c14 :: c13:c14 -> c13:c14
fib :: 0':s -> 0':s
sum :: 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_15 :: c:c1:c2
hole_0':s2_15 :: 0':s
hole_c3:c4:c5:c63_15 :: c3:c4:c5:c6
hole_c7:c8:c94_15 :: c7:c8:c9
hole_c13:c145_15 :: c13:c14
hole_c10:c11:c126_15 :: c10:c11:c12
hole_true:false7_15 :: true:false
gen_c:c1:c28_15 :: Nat -> c:c1:c2
gen_0':s9_15 :: Nat -> 0':s
gen_c3:c4:c5:c610_15 :: Nat -> c3:c4:c5:c6
gen_c13:c1411_15 :: Nat -> c13:c14
gen_c10:c11:c1212_15 :: Nat -> c10:c11:c12


Lemmas:
LT(gen_0':s9_15(n14_15), gen_0':s9_15(+(1, n14_15))) -> gen_c:c1:c28_15(n14_15), rt in Omega(1 + n14_15)
SUM(gen_0':s9_15(a), gen_0':s9_15(n679_15)) -> gen_c13:c1411_15(n679_15), rt in Omega(1 + n679_15)
lt(gen_0':s9_15(n1471_15), gen_0':s9_15(+(1, n1471_15))) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c28_15(0) <=> c
gen_c:c1:c28_15(+(x, 1)) <=> c2(gen_c:c1:c28_15(x))
gen_0':s9_15(0) <=> 0'
gen_0':s9_15(+(x, 1)) <=> s(gen_0':s9_15(x))
gen_c3:c4:c5:c610_15(0) <=> c3(c7)
gen_c3:c4:c5:c610_15(+(x, 1)) <=> c5(c13, gen_c3:c4:c5:c610_15(x))
gen_c13:c1411_15(0) <=> c13
gen_c13:c1411_15(+(x, 1)) <=> c14(gen_c13:c1411_15(x))
gen_c10:c11:c1212_15(0) <=> c11(c13, c3(c7))
gen_c10:c11:c1212_15(+(x, 1)) <=> c10(gen_c10:c11:c1212_15(x), c)


The following defined symbols remain to be analysed:
sum, FIBO, FIB, fibo, IF, fib, if

They will be analysed ascendingly in the following order:
FIBO = FIB
fibo < FIBO
FIBO = IF
FIB = IF
fibo < IF
fibo = fib
sum < fibo
fibo = if
fib = if
sum < if

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sum(gen_0':s9_15(a), gen_0':s9_15(n1907_15)) -> gen_0':s9_15(+(n1907_15, a)), rt in Omega(0)

Induction Base:
sum(gen_0':s9_15(a), gen_0':s9_15(0)) ->_R^Omega(0)
gen_0':s9_15(a)

Induction Step:
sum(gen_0':s9_15(a), gen_0':s9_15(+(n1907_15, 1))) ->_R^Omega(0)
s(sum(gen_0':s9_15(a), gen_0':s9_15(n1907_15))) ->_IH
s(gen_0':s9_15(+(a, c1908_15)))

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

(22)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
FIBO(0') -> c3(FIB(0'))
FIBO(s(0')) -> c4(FIB(s(0')))
FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
FIB(0') -> c7
FIB(s(0')) -> c8
FIB(s(s(z0))) -> c9(IF(true, 0', s(s(z0)), 0', 0'))
IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
SUM(z0, 0') -> c13
SUM(z0, s(z1)) -> c14(SUM(z0, z1))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
fibo(0') -> fib(0')
fibo(s(0')) -> fib(s(0'))
fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
fib(0') -> s(0')
fib(s(0')) -> s(0')
fib(s(s(z0))) -> if(true, 0', s(s(z0)), 0', 0')
if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
sum(z0, 0') -> z0
sum(z0, s(z1)) -> s(sum(z0, z1))

Types:
LT :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
s :: 0':s -> 0':s
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
FIBO :: 0':s -> c3:c4:c5:c6
c3 :: c7:c8:c9 -> c3:c4:c5:c6
FIB :: 0':s -> c7:c8:c9
c4 :: c7:c8:c9 -> c3:c4:c5:c6
c5 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
SUM :: 0':s -> 0':s -> c13:c14
fibo :: 0':s -> 0':s
c6 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c10:c11:c12 -> c7:c8:c9
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c10:c11:c12
true :: true:false
c10 :: c10:c11:c12 -> c:c1:c2 -> c10:c11:c12
lt :: 0':s -> 0':s -> true:false
false :: true:false
c11 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c13 :: c13:c14
c14 :: c13:c14 -> c13:c14
fib :: 0':s -> 0':s
sum :: 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_15 :: c:c1:c2
hole_0':s2_15 :: 0':s
hole_c3:c4:c5:c63_15 :: c3:c4:c5:c6
hole_c7:c8:c94_15 :: c7:c8:c9
hole_c13:c145_15 :: c13:c14
hole_c10:c11:c126_15 :: c10:c11:c12
hole_true:false7_15 :: true:false
gen_c:c1:c28_15 :: Nat -> c:c1:c2
gen_0':s9_15 :: Nat -> 0':s
gen_c3:c4:c5:c610_15 :: Nat -> c3:c4:c5:c6
gen_c13:c1411_15 :: Nat -> c13:c14
gen_c10:c11:c1212_15 :: Nat -> c10:c11:c12


Lemmas:
LT(gen_0':s9_15(n14_15), gen_0':s9_15(+(1, n14_15))) -> gen_c:c1:c28_15(n14_15), rt in Omega(1 + n14_15)
SUM(gen_0':s9_15(a), gen_0':s9_15(n679_15)) -> gen_c13:c1411_15(n679_15), rt in Omega(1 + n679_15)
lt(gen_0':s9_15(n1471_15), gen_0':s9_15(+(1, n1471_15))) -> true, rt in Omega(0)
sum(gen_0':s9_15(a), gen_0':s9_15(n1907_15)) -> gen_0':s9_15(+(n1907_15, a)), rt in Omega(0)


Generator Equations:
gen_c:c1:c28_15(0) <=> c
gen_c:c1:c28_15(+(x, 1)) <=> c2(gen_c:c1:c28_15(x))
gen_0':s9_15(0) <=> 0'
gen_0':s9_15(+(x, 1)) <=> s(gen_0':s9_15(x))
gen_c3:c4:c5:c610_15(0) <=> c3(c7)
gen_c3:c4:c5:c610_15(+(x, 1)) <=> c5(c13, gen_c3:c4:c5:c610_15(x))
gen_c13:c1411_15(0) <=> c13
gen_c13:c1411_15(+(x, 1)) <=> c14(gen_c13:c1411_15(x))
gen_c10:c11:c1212_15(0) <=> c11(c13, c3(c7))
gen_c10:c11:c1212_15(+(x, 1)) <=> c10(gen_c10:c11:c1212_15(x), c)


The following defined symbols remain to be analysed:
fib, FIBO, FIB, fibo, IF, if

They will be analysed ascendingly in the following order:
FIBO = FIB
fibo < FIBO
FIBO = IF
FIB = IF
fibo < IF
fibo = fib
fibo = if
fib = if

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
fibo(gen_0':s9_15(+(2, n5445_15))) -> *13_15, rt in Omega(0)

Induction Base:
fibo(gen_0':s9_15(+(2, 0)))

Induction Step:
fibo(gen_0':s9_15(+(2, +(n5445_15, 1)))) ->_R^Omega(0)
sum(fibo(s(gen_0':s9_15(+(1, n5445_15)))), fibo(gen_0':s9_15(+(1, n5445_15)))) ->_IH
sum(*13_15, fibo(gen_0':s9_15(+(1, n5445_15))))

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

(24)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
FIBO(0') -> c3(FIB(0'))
FIBO(s(0')) -> c4(FIB(s(0')))
FIBO(s(s(z0))) -> c5(SUM(fibo(s(z0)), fibo(z0)), FIBO(s(z0)))
FIBO(s(s(z0))) -> c6(SUM(fibo(s(z0)), fibo(z0)), FIBO(z0))
FIB(0') -> c7
FIB(s(0')) -> c8
FIB(s(s(z0))) -> c9(IF(true, 0', s(s(z0)), 0', 0'))
IF(true, z0, s(s(z1)), z2, z3) -> c10(IF(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0), LT(s(z0), s(s(z1))))
IF(false, z0, s(s(z1)), z2, z3) -> c11(SUM(fibo(z2), fibo(z3)), FIBO(z2))
IF(false, z0, s(s(z1)), z2, z3) -> c12(SUM(fibo(z2), fibo(z3)), FIBO(z3))
SUM(z0, 0') -> c13
SUM(z0, s(z1)) -> c14(SUM(z0, z1))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
fibo(0') -> fib(0')
fibo(s(0')) -> fib(s(0'))
fibo(s(s(z0))) -> sum(fibo(s(z0)), fibo(z0))
fib(0') -> s(0')
fib(s(0')) -> s(0')
fib(s(s(z0))) -> if(true, 0', s(s(z0)), 0', 0')
if(true, z0, s(s(z1)), z2, z3) -> if(lt(s(z0), s(s(z1))), s(z0), s(s(z1)), z3, z0)
if(false, z0, s(s(z1)), z2, z3) -> sum(fibo(z2), fibo(z3))
sum(z0, 0') -> z0
sum(z0, s(z1)) -> s(sum(z0, z1))

Types:
LT :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
s :: 0':s -> 0':s
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
FIBO :: 0':s -> c3:c4:c5:c6
c3 :: c7:c8:c9 -> c3:c4:c5:c6
FIB :: 0':s -> c7:c8:c9
c4 :: c7:c8:c9 -> c3:c4:c5:c6
c5 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
SUM :: 0':s -> 0':s -> c13:c14
fibo :: 0':s -> 0':s
c6 :: c13:c14 -> c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c10:c11:c12 -> c7:c8:c9
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c10:c11:c12
true :: true:false
c10 :: c10:c11:c12 -> c:c1:c2 -> c10:c11:c12
lt :: 0':s -> 0':s -> true:false
false :: true:false
c11 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c12 :: c13:c14 -> c3:c4:c5:c6 -> c10:c11:c12
c13 :: c13:c14
c14 :: c13:c14 -> c13:c14
fib :: 0':s -> 0':s
sum :: 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_15 :: c:c1:c2
hole_0':s2_15 :: 0':s
hole_c3:c4:c5:c63_15 :: c3:c4:c5:c6
hole_c7:c8:c94_15 :: c7:c8:c9
hole_c13:c145_15 :: c13:c14
hole_c10:c11:c126_15 :: c10:c11:c12
hole_true:false7_15 :: true:false
gen_c:c1:c28_15 :: Nat -> c:c1:c2
gen_0':s9_15 :: Nat -> 0':s
gen_c3:c4:c5:c610_15 :: Nat -> c3:c4:c5:c6
gen_c13:c1411_15 :: Nat -> c13:c14
gen_c10:c11:c1212_15 :: Nat -> c10:c11:c12


Lemmas:
LT(gen_0':s9_15(n14_15), gen_0':s9_15(+(1, n14_15))) -> gen_c:c1:c28_15(n14_15), rt in Omega(1 + n14_15)
SUM(gen_0':s9_15(a), gen_0':s9_15(n679_15)) -> gen_c13:c1411_15(n679_15), rt in Omega(1 + n679_15)
lt(gen_0':s9_15(n1471_15), gen_0':s9_15(+(1, n1471_15))) -> true, rt in Omega(0)
sum(gen_0':s9_15(a), gen_0':s9_15(n1907_15)) -> gen_0':s9_15(+(n1907_15, a)), rt in Omega(0)
fibo(gen_0':s9_15(+(2, n5445_15))) -> *13_15, rt in Omega(0)


Generator Equations:
gen_c:c1:c28_15(0) <=> c
gen_c:c1:c28_15(+(x, 1)) <=> c2(gen_c:c1:c28_15(x))
gen_0':s9_15(0) <=> 0'
gen_0':s9_15(+(x, 1)) <=> s(gen_0':s9_15(x))
gen_c3:c4:c5:c610_15(0) <=> c3(c7)
gen_c3:c4:c5:c610_15(+(x, 1)) <=> c5(c13, gen_c3:c4:c5:c610_15(x))
gen_c13:c1411_15(0) <=> c13
gen_c13:c1411_15(+(x, 1)) <=> c14(gen_c13:c1411_15(x))
gen_c10:c11:c1212_15(0) <=> c11(c13, c3(c7))
gen_c10:c11:c1212_15(+(x, 1)) <=> c10(gen_c10:c11:c1212_15(x), c)


The following defined symbols remain to be analysed:
fib, FIBO, FIB, IF, if

They will be analysed ascendingly in the following order:
FIBO = FIB
fibo < FIBO
FIBO = IF
FIB = IF
fibo < IF
fibo = fib
fibo = if
fib = if