* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            and(false(),y) -> false()
            and(true(),y) -> y
            eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
            eq(apply(t,s),lambda(x,t)) -> false()
            eq(apply(t,s),var(l)) -> false()
            eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
            eq(cons(t,l),nil()) -> false()
            eq(lambda(x,t),apply(t,s)) -> false()
            eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
            eq(lambda(x,t),var(l)) -> false()
            eq(nil(),cons(t,l)) -> false()
            eq(nil(),nil()) -> true()
            eq(var(l),apply(t,s)) -> false()
            eq(var(l),lambda(x,t)) -> false()
            eq(var(l),var(l')) -> eq(l,l')
            if(false(),var(k),var(l')) -> var(l')
            if(true(),var(k),var(l')) -> var(k)
            ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
            ren(x,y,lambda(z,t)) -> lambda(var(cons(x,cons(y,cons(lambda(z,t),nil()))))
                                          ,ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)))
            ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
        - Signature:
            {and/2,eq/2,if/3,ren/3} / {apply/2,cons/2,false/0,lambda/2,nil/0,true/0,var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and,eq,if,ren} and constructors {apply,cons,false,lambda
            ,nil,true,var}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            and(false(),y) -> false()
            and(true(),y) -> y
            eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
            eq(apply(t,s),lambda(x,t)) -> false()
            eq(apply(t,s),var(l)) -> false()
            eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
            eq(cons(t,l),nil()) -> false()
            eq(lambda(x,t),apply(t,s)) -> false()
            eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
            eq(lambda(x,t),var(l)) -> false()
            eq(nil(),cons(t,l)) -> false()
            eq(nil(),nil()) -> true()
            eq(var(l),apply(t,s)) -> false()
            eq(var(l),lambda(x,t)) -> false()
            eq(var(l),var(l')) -> eq(l,l')
            if(false(),var(k),var(l')) -> var(l')
            if(true(),var(k),var(l')) -> var(k)
            ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
            ren(x,y,lambda(z,t)) -> lambda(var(cons(x,cons(y,cons(lambda(z,t),nil()))))
                                          ,ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)))
            ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
        - Signature:
            {and/2,eq/2,if/3,ren/3} / {apply/2,cons/2,false/0,lambda/2,nil/0,true/0,var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {and,eq,if,ren} and constructors {apply,cons,false,lambda
            ,nil,true,var}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          eq(x,z){x -> apply(x,y),z -> apply(z,u)} =
            eq(apply(x,y),apply(z,u)) ->^+ and(eq(x,z),eq(y,u))
              = C[eq(x,z) = eq(x,z){}]

WORST_CASE(Omega(n^1),?)