tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            FIB(0()) -> c7()
            FIB(s(0())) -> c8()
            FIB(s(s(z0))) -> c9(IF(true(),0(),s(s(z0)),0(),0()))
            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))
            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))
            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))))
            LT(z0,0()) -> c1()
            LT(0(),s(z0)) -> c()
            LT(s(z0),s(z1)) -> c2(LT(z0,z1))
            SUM(z0,0()) -> c13()
            SUM(z0,s(z1)) -> c14(SUM(z0,z1))
        - Weak TRS:
            fib(0()) -> s(0())
            fib(s(0())) -> s(0())
            fib(s(s(z0))) -> if(true(),0(),s(s(z0)),0(),0())
            fibo(0()) -> fib(0())
            fibo(s(0())) -> fib(s(0()))
            fibo(s(s(z0))) -> sum(fibo(s(z0)),fibo(z0))
            if(false(),z0,s(s(z1)),z2,z3) -> sum(fibo(z2),fibo(z3))
            if(true(),z0,s(s(z1)),z2,z3) -> if(lt(s(z0),s(s(z1))),s(z0),s(s(z1)),z3,z0)
            lt(z0,0()) -> false()
            lt(0(),s(z0)) -> true()
            lt(s(z0),s(z1)) -> lt(z0,z1)
            sum(z0,0()) -> z0
            sum(z0,s(z1)) -> s(sum(z0,z1))
        - Signature:
            {FIB/1,FIBO/1,IF/5,LT/2,SUM/2,fib/1,fibo/1,if/5,lt/2,sum/2} / {0/0,c/0,c1/0,c10/2,c11/2,c12/2,c13/0,c14/1
            ,c2/1,c3/1,c4/1,c5/2,c6/2,c7/0,c8/0,c9/1,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {FIB,FIBO,IF,LT,SUM,fib,fibo,if,lt
            ,sum} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            FIB(0()) -> c7()
            FIB(s(0())) -> c8()
            FIB(s(s(z0))) -> c9(IF(true(),0(),s(s(z0)),0(),0()))
            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))
            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))
            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))))
            LT(z0,0()) -> c1()
            LT(0(),s(z0)) -> c()
            LT(s(z0),s(z1)) -> c2(LT(z0,z1))
            SUM(z0,0()) -> c13()
            SUM(z0,s(z1)) -> c14(SUM(z0,z1))
        - Weak TRS:
            fib(0()) -> s(0())
            fib(s(0())) -> s(0())
            fib(s(s(z0))) -> if(true(),0(),s(s(z0)),0(),0())
            fibo(0()) -> fib(0())
            fibo(s(0())) -> fib(s(0()))
            fibo(s(s(z0))) -> sum(fibo(s(z0)),fibo(z0))
            if(false(),z0,s(s(z1)),z2,z3) -> sum(fibo(z2),fibo(z3))
            if(true(),z0,s(s(z1)),z2,z3) -> if(lt(s(z0),s(s(z1))),s(z0),s(s(z1)),z3,z0)
            lt(z0,0()) -> false()
            lt(0(),s(z0)) -> true()
            lt(s(z0),s(z1)) -> lt(z0,z1)
            sum(z0,0()) -> z0
            sum(z0,s(z1)) -> s(sum(z0,z1))
        - Signature:
            {FIB/1,FIBO/1,IF/5,LT/2,SUM/2,fib/1,fibo/1,if/5,lt/2,sum/2} / {0/0,c/0,c1/0,c10/2,c11/2,c12/2,c13/0,c14/1
            ,c2/1,c3/1,c4/1,c5/2,c6/2,c7/0,c8/0,c9/1,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {FIB,FIBO,IF,LT,SUM,fib,fibo,if,lt
            ,sum} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            FIB(0()) -> c7()
            FIB(s(0())) -> c8()
            FIB(s(s(z0))) -> c9(IF(true(),0(),s(s(z0)),0(),0()))
            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))
            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))
            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))))
            LT(z0,0()) -> c1()
            LT(0(),s(z0)) -> c()
            LT(s(z0),s(z1)) -> c2(LT(z0,z1))
            SUM(z0,0()) -> c13()
            SUM(z0,s(z1)) -> c14(SUM(z0,z1))
        - Weak TRS:
            fib(0()) -> s(0())
            fib(s(0())) -> s(0())
            fib(s(s(z0))) -> if(true(),0(),s(s(z0)),0(),0())
            fibo(0()) -> fib(0())
            fibo(s(0())) -> fib(s(0()))
            fibo(s(s(z0))) -> sum(fibo(s(z0)),fibo(z0))
            if(false(),z0,s(s(z1)),z2,z3) -> sum(fibo(z2),fibo(z3))
            if(true(),z0,s(s(z1)),z2,z3) -> if(lt(s(z0),s(s(z1))),s(z0),s(s(z1)),z3,z0)
            lt(z0,0()) -> false()
            lt(0(),s(z0)) -> true()
            lt(s(z0),s(z1)) -> lt(z0,z1)
            sum(z0,0()) -> z0
            sum(z0,s(z1)) -> s(sum(z0,z1))
        - Signature:
            {FIB/1,FIBO/1,IF/5,LT/2,SUM/2,fib/1,fibo/1,if/5,lt/2,sum/2} / {0/0,c/0,c1/0,c10/2,c11/2,c12/2,c13/0,c14/1
            ,c2/1,c3/1,c4/1,c5/2,c6/2,c7/0,c8/0,c9/1,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {FIB,FIBO,IF,LT,SUM,fib,fibo,if,lt
            ,sum} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          FIBO(s(x)){x -> s(x)} =
            FIBO(s(s(x))) ->^+ c5(SUM(fibo(s(x)),fibo(x)),FIBO(s(x)))
              = C[FIBO(s(x)) = FIBO(s(x)){}]

WORST_CASE(Omega(n^1),?)