* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            apply(op,v1,v2) -> apply[Ite](eqExp(v1,v2),op,v1,v2)
            checkConstrExp(Bsf(op1,b11,b12),Bsf(op2,b21,b22)) -> True()
            checkConstrExp(Bsf(op1,b11,b12),Eq(eq21,eq22)) -> False()
            checkConstrExp(Bsf(op1,b11,b12),Error(e21,e22)) -> False()
            checkConstrExp(Bsf(op1,b11,b12),F()) -> False()
            checkConstrExp(Bsf(op1,b11,b12),Fun(fn2,fe2)) -> False()
            checkConstrExp(Bsf(op1,b11,b12),ITE(i2,t2,e2)) -> False()
            checkConstrExp(Bsf(op1,b11,b12),T()) -> False()
            checkConstrExp(Bsf(op1,b11,b12),Var(v2)) -> False()
            checkConstrExp(Eq(eq11,eq12),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(Eq(eq11,eq12),Eq(eq21,eq22)) -> True()
            checkConstrExp(Eq(eq11,eq12),Error(e21,e22)) -> False()
            checkConstrExp(Eq(eq11,eq12),F()) -> False()
            checkConstrExp(Eq(eq11,eq12),Fun(fn2,fe2)) -> False()
            checkConstrExp(Eq(eq11,eq12),ITE(i2,t2,e2)) -> False()
            checkConstrExp(Eq(eq11,eq12),T()) -> False()
            checkConstrExp(Eq(eq11,eq12),Var(v2)) -> False()
            checkConstrExp(Error(e11,e12),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(Error(e11,e12),Eq(eq21,eq22)) -> False()
            checkConstrExp(Error(e11,e12),Error(e21,e22)) -> True()
            checkConstrExp(Error(e11,e12),F()) -> False()
            checkConstrExp(Error(e11,e12),Fun(fn2,fe2)) -> False()
            checkConstrExp(Error(e11,e12),ITE(i2,t2,e2)) -> False()
            checkConstrExp(Error(e11,e12),T()) -> False()
            checkConstrExp(Error(e11,e12),Var(v2)) -> False()
            checkConstrExp(F(),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(F(),Eq(eq21,eq22)) -> False()
            checkConstrExp(F(),Error(e21,e22)) -> False()
            checkConstrExp(F(),F()) -> True()
            checkConstrExp(F(),Fun(fn2,fe2)) -> False()
            checkConstrExp(F(),ITE(i2,t2,e2)) -> False()
            checkConstrExp(F(),T()) -> False()
            checkConstrExp(F(),Var(v2)) -> False()
            checkConstrExp(Fun(fn1,fe1),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(Fun(fn1,fe1),Eq(eq21,eq22)) -> False()
            checkConstrExp(Fun(fn1,fe1),Error(e21,e22)) -> False()
            checkConstrExp(Fun(fn1,fe1),F()) -> False()
            checkConstrExp(Fun(fn1,fe1),Fun(fn2,fe2)) -> True()
            checkConstrExp(Fun(fn1,fe1),ITE(i2,t2,e2)) -> False()
            checkConstrExp(Fun(fn1,fe1),T()) -> False()
            checkConstrExp(Fun(fn1,fe1),Var(v2)) -> False()
            checkConstrExp(ITE(i1,t1,e1),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(ITE(i1,t1,e1),Eq(eq21,eq22)) -> False()
            checkConstrExp(ITE(i1,t1,e1),Error(e21,e22)) -> False()
            checkConstrExp(ITE(i1,t1,e1),F()) -> False()
            checkConstrExp(ITE(i1,t1,e1),Fun(fn2,fe2)) -> False()
            checkConstrExp(ITE(i1,t1,e1),ITE(i2,t2,e2)) -> True()
            checkConstrExp(ITE(i1,t1,e1),T()) -> False()
            checkConstrExp(ITE(i1,t1,e1),Var(v2)) -> False()
            checkConstrExp(T(),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(T(),Eq(eq21,eq22)) -> False()
            checkConstrExp(T(),Error(e21,e22)) -> False()
            checkConstrExp(T(),F()) -> False()
            checkConstrExp(T(),Fun(fn2,fe2)) -> False()
            checkConstrExp(T(),ITE(i2,t2,e2)) -> False()
            checkConstrExp(T(),T()) -> True()
            checkConstrExp(T(),Var(v2)) -> False()
            checkConstrExp(Var(v1),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(Var(v1),Eq(eq21,eq22)) -> False()
            checkConstrExp(Var(v1),Error(e21,e22)) -> False()
            checkConstrExp(Var(v1),F()) -> False()
            checkConstrExp(Var(v1),Fun(fn2,fe2)) -> False()
            checkConstrExp(Var(v1),ITE(i2,t2,e2)) -> False()
            checkConstrExp(Var(v1),T()) -> False()
            checkConstrExp(Var(v1),Var(v2)) -> True()
            eeval(Bsf(op,t1,t2),ns,vs,p) -> eeval[Let](Bsf(op,t1,t2),ns,vs,p,eeval(t1,ns,vs,p))
            eeval(Eq(f,s),ns,vs,p) -> eeval[True][Ite](eqExp(eeval(f,ns,vs,p),eeval(s,ns,vs,p)),Eq(f,s),ns,vs,p)
            eeval(Error(e11,e12),ns,vs,p) -> eeval[False][Ite](False(),Error(e11,e12),ns,vs,p)
            eeval(F(),ns,vs,p) -> F()
            eeval(Fun(n,e),ns,vs,p) -> eeval[False][Let](Fun(n,e),ns,vs,p,lookbody(n,p))
            eeval(ITE(i,t,e),ns,vs,p) -> eeval[Ite](checkConstrExp(eeval(i,ns,vs,p),T()),ITE(i,t,e),ns,vs,p)
            eeval(T(),ns,vs,p) -> T()
            eeval(Var(int),ns,vs,p) -> lookvar(int,ns,vs)
            eqExp(Bsf(o1,b11,b12),Bsf(o2,b21,b22)) -> and(True(),and(eqExp(b11,b21),eqExp(b12,b22)))
            eqExp(Bsf(op1,b11,b12),Eq(eq21,eq22)) -> False()
            eqExp(Bsf(op1,b11,b12),Error(e21,e22)) -> False()
            eqExp(Bsf(op1,b11,b12),F()) -> False()
            eqExp(Bsf(op1,b11,b12),Fun(fn2,fe2)) -> False()
            eqExp(Bsf(op1,b11,b12),ITE(i2,t2,e2)) -> False()
            eqExp(Bsf(op1,b11,b12),T()) -> False()
            eqExp(Bsf(op1,b11,b12),Var(v2)) -> False()
            eqExp(Eq(eq11,eq12),Bsf(op2,b21,b22)) -> False()
            eqExp(Eq(eq11,eq12),Eq(eq21,eq22)) -> and(eqExp(eq11,eq21),eqExp(eq12,eq22))
            eqExp(Eq(eq11,eq12),Error(e21,e22)) -> False()
            eqExp(Eq(eq11,eq12),F()) -> False()
            eqExp(Eq(eq11,eq12),Fun(fn2,fe2)) -> False()
            eqExp(Eq(eq11,eq12),ITE(i2,t2,e2)) -> False()
            eqExp(Eq(eq11,eq12),T()) -> False()
            eqExp(Eq(eq11,eq12),Var(v2)) -> False()
            eqExp(Error(e11,e12),Bsf(op2,b21,b22)) -> False()
            eqExp(Error(e11,e12),Eq(eq21,eq22)) -> False()
            eqExp(Error(e11,e12),Error(e21,e22)) -> and(eqExp(e11,e21),eqExp(e12,e22))
            eqExp(Error(e11,e12),F()) -> False()
            eqExp(Error(e11,e12),Fun(fn2,fe2)) -> False()
            eqExp(Error(e11,e12),ITE(i2,t2,e2)) -> False()
            eqExp(Error(e11,e12),T()) -> False()
            eqExp(Error(e11,e12),Var(v2)) -> False()
            eqExp(F(),Bsf(op2,b21,b22)) -> False()
            eqExp(F(),Eq(eq21,eq22)) -> False()
            eqExp(F(),Error(e21,e22)) -> False()
            eqExp(F(),F()) -> True()
            eqExp(F(),Fun(fn2,fe2)) -> False()
            eqExp(F(),ITE(i2,t2,e2)) -> False()
            eqExp(F(),T()) -> False()
            eqExp(F(),Var(v2)) -> False()
            eqExp(Fun(fn1,fe1),Bsf(op2,b21,b22)) -> False()
            eqExp(Fun(fn1,fe1),Eq(eq21,eq22)) -> False()
            eqExp(Fun(fn1,fe1),Error(e21,e22)) -> False()
            eqExp(Fun(fn1,fe1),F()) -> False()
            eqExp(Fun(fn1,fe1),Fun(fn2,fe2)) -> and(!EQ(fn1,fn2),eqExp(fe1,fe2))
            eqExp(Fun(fn1,fe1),ITE(i2,t2,e2)) -> False()
            eqExp(Fun(fn1,fe1),T()) -> False()
            eqExp(Fun(fn1,fe1),Var(v2)) -> False()
            eqExp(ITE(i1,t1,e1),Bsf(op2,b21,b22)) -> False()
            eqExp(ITE(i1,t1,e1),Eq(eq21,eq22)) -> False()
            eqExp(ITE(i1,t1,e1),Error(e21,e22)) -> False()
            eqExp(ITE(i1,t1,e1),F()) -> False()
            eqExp(ITE(i1,t1,e1),Fun(fn2,fe2)) -> False()
            eqExp(ITE(i1,t1,e1),ITE(i2,t2,e2)) -> and(eqExp(i1,i2),and(eqExp(t1,t2),eqExp(e1,e2)))
            eqExp(ITE(i1,t1,e1),T()) -> False()
            eqExp(ITE(i1,t1,e1),Var(v2)) -> False()
            eqExp(T(),Bsf(op2,b21,b22)) -> False()
            eqExp(T(),Eq(eq21,eq22)) -> False()
            eqExp(T(),Error(e21,e22)) -> False()
            eqExp(T(),F()) -> False()
            eqExp(T(),Fun(fn2,fe2)) -> False()
            eqExp(T(),ITE(i2,t2,e2)) -> False()
            eqExp(T(),T()) -> True()
            eqExp(T(),Var(v2)) -> False()
            eqExp(Var(v1),Bsf(op2,b21,b22)) -> False()
            eqExp(Var(v1),Eq(eq21,eq22)) -> False()
            eqExp(Var(v1),Error(e21,e22)) -> False()
            eqExp(Var(v1),F()) -> False()
            eqExp(Var(v1),Fun(fn2,fe2)) -> False()
            eqExp(Var(v1),ITE(i2,t2,e2)) -> False()
            eqExp(Var(v1),T()) -> False()
            eqExp(Var(v1),Var(v2)) -> !EQ(v1,v2)
            eqOps(o1,o2) -> True()
            getBsfFirstTerm(Bsf(op,t1,t2)) -> t1
            getBsfOp(Bsf(op,t1,t2)) -> op
            getBsfSecondTerm(Bsf(op,t1,t2)) -> t2
            getConst(Cst(int)) -> int
            getEqFirst(Eq(f,s)) -> f
            getEqSecond(Eq(f,s)) -> s
            getFuncExp(Fun(n,e)) -> e
            getFuncName(Fun(n,e)) -> n
            getIfFalse(ITE(i,t,e)) -> e
            getIfGuard(ITE(i,t,e)) -> i
            getIfTrue(ITE(i,t,e)) -> t
            getVar(Var(int)) -> int
            lookbody(f,Cons(Fun(n,e),xs)) -> lookbody[Ite](!EQ(f,n),f,Cons(Fun(n,e),xs))
            lookname(f,Cons(Fun(n,e),xs)) -> lookname[Ite](!EQ(f,n),f,Cons(Fun(n,e),xs))
            lookvar(x',Cons(x,xs),vs) -> lookvar[Ite](!EQ(x',x),x',Cons(x,xs),vs)
            run(Cons(Fun(f0,e),xs),input) -> run[Let][Let](Cons(Fun(f0,e),xs),input,f0,lookbody(f0,Cons(Fun(f0,e),xs)))
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            apply[Ite](False(),op,v1,v2) -> F()
            apply[Ite](True(),op,v1,v2) -> T()
            eeval[False][Ite](False(),Fun(n,e),ns,vs,p) -> eeval[False][Let](Fun(n,e),ns,vs,p,lookbody(n,p))
            eeval[False][Ite](True(),Eq(f,s),ns,vs,p) -> eeval[True][Ite](eqExp(eeval(f,ns,vs,p),eeval(s,ns,vs,p))
                                                                         ,Eq(f,s)
                                                                         ,ns
                                                                         ,vs
                                                                         ,p)
            eeval[False][Let](Fun(n,e),ns,vs,p,ef) -> eeval[False][Let][Let](Fun(n,e),ns,vs,p,ef,lookname(n,p))
            eeval[False][Let][Let](Fun(n,e),ns,vs,p,ef,nf) -> eeval[Let][Let][Let](Fun(n,e)
                                                                                  ,ns
                                                                                  ,vs
                                                                                  ,p
                                                                                  ,ef
                                                                                  ,nf
                                                                                  ,eeval(e,ns,vs,p))
            eeval[Ite](False(),ITE(i,t,e),ns,vs,p) -> eeval(e,ns,vs,p)
            eeval[Ite](True(),ITE(i,t,e),ns,vs,p) -> eeval(t,ns,vs,p)
            eeval[Let](Bsf(op,t1,t2),ns,vs,p,v1) -> eeval[Let][Let](Bsf(op,t1,t2),ns,vs,p,v1,eeval(t2,ns,vs,p))
            eeval[Let][Let](Bsf(op,t1,t2),ns,vs,p,v1,v2) -> apply(op,v1,v2)
            eeval[Let][Let][Let](e,ns,vs,p,ef,nf,v) -> eeval(ef,Cons(nf,Nil()),Cons(v,Nil()),p)
            eeval[True][Ite](False(),e,ns,vs,p) -> F()
            eeval[True][Ite](True(),e,ns,vs,p) -> T()
            lookbody[Ite](False(),f,Cons(x,xs)) -> lookbody(f,xs)
            lookbody[Ite](True(),f,Cons(Fun(n,e),xs)) -> e
            lookname[Ite](False(),f,Cons(x,xs)) -> lookname(f,xs)
            lookname[Ite](True(),f,Cons(Fun(n,e),xs)) -> n
            lookvar[Ite](False(),x',Cons(x'',xs'),Cons(x,xs)) -> lookvar(x',xs',xs)
            lookvar[Ite](True(),x',ns,Cons(x,xs)) -> x
            run[Let](p,input,f0,ef,nf) -> eeval(ef,Cons(nf,Nil()),Cons(input,Nil()),p)
            run[Let][Let](p,input,f0,ef) -> run[Let](p,input,f0,ef,lookname(f0,p))
        - Signature:
            {!EQ/2,and/2,apply/3,apply[Ite]/4,checkConstrExp/2,eeval/4,eeval[False][Ite]/5,eeval[False][Let]/5
            ,eeval[False][Let][Let]/6,eeval[Ite]/5,eeval[Let]/5,eeval[Let][Let]/6,eeval[Let][Let][Let]/7
            ,eeval[True][Ite]/5,eqExp/2,eqOps/2,getBsfFirstTerm/1,getBsfOp/1,getBsfSecondTerm/1,getConst/1,getEqFirst/1
            ,getEqSecond/1,getFuncExp/1,getFuncName/1,getIfFalse/1,getIfGuard/1,getIfTrue/1,getVar/1,lookbody/2
            ,lookbody[Ite]/3,lookname/2,lookname[Ite]/3,lookvar/3,lookvar[Ite]/4,run/2,run[Let]/5
            ,run[Let][Let]/4} / {0/0,Bsf/3,Cons/2,Cst/1,Eq/2,Error/2,F/0,False/0,Fun/2,ITE/3,Nil/0,S/1,T/0,True/0,Var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,and,apply,apply[Ite],checkConstrExp,eeval
            ,eeval[False][Ite],eeval[False][Let],eeval[False][Let][Let],eeval[Ite],eeval[Let],eeval[Let][Let]
            ,eeval[Let][Let][Let],eeval[True][Ite],eqExp,eqOps,getBsfFirstTerm,getBsfOp,getBsfSecondTerm,getConst
            ,getEqFirst,getEqSecond,getFuncExp,getFuncName,getIfFalse,getIfGuard,getIfTrue,getVar,lookbody,lookbody[Ite]
            ,lookname,lookname[Ite],lookvar,lookvar[Ite],run,run[Let],run[Let][Let]} and constructors {0,Bsf,Cons,Cst,Eq
            ,Error,F,False,Fun,ITE,Nil,S,T,True,Var}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            apply(op,v1,v2) -> apply[Ite](eqExp(v1,v2),op,v1,v2)
            checkConstrExp(Bsf(op1,b11,b12),Bsf(op2,b21,b22)) -> True()
            checkConstrExp(Bsf(op1,b11,b12),Eq(eq21,eq22)) -> False()
            checkConstrExp(Bsf(op1,b11,b12),Error(e21,e22)) -> False()
            checkConstrExp(Bsf(op1,b11,b12),F()) -> False()
            checkConstrExp(Bsf(op1,b11,b12),Fun(fn2,fe2)) -> False()
            checkConstrExp(Bsf(op1,b11,b12),ITE(i2,t2,e2)) -> False()
            checkConstrExp(Bsf(op1,b11,b12),T()) -> False()
            checkConstrExp(Bsf(op1,b11,b12),Var(v2)) -> False()
            checkConstrExp(Eq(eq11,eq12),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(Eq(eq11,eq12),Eq(eq21,eq22)) -> True()
            checkConstrExp(Eq(eq11,eq12),Error(e21,e22)) -> False()
            checkConstrExp(Eq(eq11,eq12),F()) -> False()
            checkConstrExp(Eq(eq11,eq12),Fun(fn2,fe2)) -> False()
            checkConstrExp(Eq(eq11,eq12),ITE(i2,t2,e2)) -> False()
            checkConstrExp(Eq(eq11,eq12),T()) -> False()
            checkConstrExp(Eq(eq11,eq12),Var(v2)) -> False()
            checkConstrExp(Error(e11,e12),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(Error(e11,e12),Eq(eq21,eq22)) -> False()
            checkConstrExp(Error(e11,e12),Error(e21,e22)) -> True()
            checkConstrExp(Error(e11,e12),F()) -> False()
            checkConstrExp(Error(e11,e12),Fun(fn2,fe2)) -> False()
            checkConstrExp(Error(e11,e12),ITE(i2,t2,e2)) -> False()
            checkConstrExp(Error(e11,e12),T()) -> False()
            checkConstrExp(Error(e11,e12),Var(v2)) -> False()
            checkConstrExp(F(),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(F(),Eq(eq21,eq22)) -> False()
            checkConstrExp(F(),Error(e21,e22)) -> False()
            checkConstrExp(F(),F()) -> True()
            checkConstrExp(F(),Fun(fn2,fe2)) -> False()
            checkConstrExp(F(),ITE(i2,t2,e2)) -> False()
            checkConstrExp(F(),T()) -> False()
            checkConstrExp(F(),Var(v2)) -> False()
            checkConstrExp(Fun(fn1,fe1),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(Fun(fn1,fe1),Eq(eq21,eq22)) -> False()
            checkConstrExp(Fun(fn1,fe1),Error(e21,e22)) -> False()
            checkConstrExp(Fun(fn1,fe1),F()) -> False()
            checkConstrExp(Fun(fn1,fe1),Fun(fn2,fe2)) -> True()
            checkConstrExp(Fun(fn1,fe1),ITE(i2,t2,e2)) -> False()
            checkConstrExp(Fun(fn1,fe1),T()) -> False()
            checkConstrExp(Fun(fn1,fe1),Var(v2)) -> False()
            checkConstrExp(ITE(i1,t1,e1),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(ITE(i1,t1,e1),Eq(eq21,eq22)) -> False()
            checkConstrExp(ITE(i1,t1,e1),Error(e21,e22)) -> False()
            checkConstrExp(ITE(i1,t1,e1),F()) -> False()
            checkConstrExp(ITE(i1,t1,e1),Fun(fn2,fe2)) -> False()
            checkConstrExp(ITE(i1,t1,e1),ITE(i2,t2,e2)) -> True()
            checkConstrExp(ITE(i1,t1,e1),T()) -> False()
            checkConstrExp(ITE(i1,t1,e1),Var(v2)) -> False()
            checkConstrExp(T(),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(T(),Eq(eq21,eq22)) -> False()
            checkConstrExp(T(),Error(e21,e22)) -> False()
            checkConstrExp(T(),F()) -> False()
            checkConstrExp(T(),Fun(fn2,fe2)) -> False()
            checkConstrExp(T(),ITE(i2,t2,e2)) -> False()
            checkConstrExp(T(),T()) -> True()
            checkConstrExp(T(),Var(v2)) -> False()
            checkConstrExp(Var(v1),Bsf(op2,b21,b22)) -> False()
            checkConstrExp(Var(v1),Eq(eq21,eq22)) -> False()
            checkConstrExp(Var(v1),Error(e21,e22)) -> False()
            checkConstrExp(Var(v1),F()) -> False()
            checkConstrExp(Var(v1),Fun(fn2,fe2)) -> False()
            checkConstrExp(Var(v1),ITE(i2,t2,e2)) -> False()
            checkConstrExp(Var(v1),T()) -> False()
            checkConstrExp(Var(v1),Var(v2)) -> True()
            eeval(Bsf(op,t1,t2),ns,vs,p) -> eeval[Let](Bsf(op,t1,t2),ns,vs,p,eeval(t1,ns,vs,p))
            eeval(Eq(f,s),ns,vs,p) -> eeval[True][Ite](eqExp(eeval(f,ns,vs,p),eeval(s,ns,vs,p)),Eq(f,s),ns,vs,p)
            eeval(Error(e11,e12),ns,vs,p) -> eeval[False][Ite](False(),Error(e11,e12),ns,vs,p)
            eeval(F(),ns,vs,p) -> F()
            eeval(Fun(n,e),ns,vs,p) -> eeval[False][Let](Fun(n,e),ns,vs,p,lookbody(n,p))
            eeval(ITE(i,t,e),ns,vs,p) -> eeval[Ite](checkConstrExp(eeval(i,ns,vs,p),T()),ITE(i,t,e),ns,vs,p)
            eeval(T(),ns,vs,p) -> T()
            eeval(Var(int),ns,vs,p) -> lookvar(int,ns,vs)
            eqExp(Bsf(o1,b11,b12),Bsf(o2,b21,b22)) -> and(True(),and(eqExp(b11,b21),eqExp(b12,b22)))
            eqExp(Bsf(op1,b11,b12),Eq(eq21,eq22)) -> False()
            eqExp(Bsf(op1,b11,b12),Error(e21,e22)) -> False()
            eqExp(Bsf(op1,b11,b12),F()) -> False()
            eqExp(Bsf(op1,b11,b12),Fun(fn2,fe2)) -> False()
            eqExp(Bsf(op1,b11,b12),ITE(i2,t2,e2)) -> False()
            eqExp(Bsf(op1,b11,b12),T()) -> False()
            eqExp(Bsf(op1,b11,b12),Var(v2)) -> False()
            eqExp(Eq(eq11,eq12),Bsf(op2,b21,b22)) -> False()
            eqExp(Eq(eq11,eq12),Eq(eq21,eq22)) -> and(eqExp(eq11,eq21),eqExp(eq12,eq22))
            eqExp(Eq(eq11,eq12),Error(e21,e22)) -> False()
            eqExp(Eq(eq11,eq12),F()) -> False()
            eqExp(Eq(eq11,eq12),Fun(fn2,fe2)) -> False()
            eqExp(Eq(eq11,eq12),ITE(i2,t2,e2)) -> False()
            eqExp(Eq(eq11,eq12),T()) -> False()
            eqExp(Eq(eq11,eq12),Var(v2)) -> False()
            eqExp(Error(e11,e12),Bsf(op2,b21,b22)) -> False()
            eqExp(Error(e11,e12),Eq(eq21,eq22)) -> False()
            eqExp(Error(e11,e12),Error(e21,e22)) -> and(eqExp(e11,e21),eqExp(e12,e22))
            eqExp(Error(e11,e12),F()) -> False()
            eqExp(Error(e11,e12),Fun(fn2,fe2)) -> False()
            eqExp(Error(e11,e12),ITE(i2,t2,e2)) -> False()
            eqExp(Error(e11,e12),T()) -> False()
            eqExp(Error(e11,e12),Var(v2)) -> False()
            eqExp(F(),Bsf(op2,b21,b22)) -> False()
            eqExp(F(),Eq(eq21,eq22)) -> False()
            eqExp(F(),Error(e21,e22)) -> False()
            eqExp(F(),F()) -> True()
            eqExp(F(),Fun(fn2,fe2)) -> False()
            eqExp(F(),ITE(i2,t2,e2)) -> False()
            eqExp(F(),T()) -> False()
            eqExp(F(),Var(v2)) -> False()
            eqExp(Fun(fn1,fe1),Bsf(op2,b21,b22)) -> False()
            eqExp(Fun(fn1,fe1),Eq(eq21,eq22)) -> False()
            eqExp(Fun(fn1,fe1),Error(e21,e22)) -> False()
            eqExp(Fun(fn1,fe1),F()) -> False()
            eqExp(Fun(fn1,fe1),Fun(fn2,fe2)) -> and(!EQ(fn1,fn2),eqExp(fe1,fe2))
            eqExp(Fun(fn1,fe1),ITE(i2,t2,e2)) -> False()
            eqExp(Fun(fn1,fe1),T()) -> False()
            eqExp(Fun(fn1,fe1),Var(v2)) -> False()
            eqExp(ITE(i1,t1,e1),Bsf(op2,b21,b22)) -> False()
            eqExp(ITE(i1,t1,e1),Eq(eq21,eq22)) -> False()
            eqExp(ITE(i1,t1,e1),Error(e21,e22)) -> False()
            eqExp(ITE(i1,t1,e1),F()) -> False()
            eqExp(ITE(i1,t1,e1),Fun(fn2,fe2)) -> False()
            eqExp(ITE(i1,t1,e1),ITE(i2,t2,e2)) -> and(eqExp(i1,i2),and(eqExp(t1,t2),eqExp(e1,e2)))
            eqExp(ITE(i1,t1,e1),T()) -> False()
            eqExp(ITE(i1,t1,e1),Var(v2)) -> False()
            eqExp(T(),Bsf(op2,b21,b22)) -> False()
            eqExp(T(),Eq(eq21,eq22)) -> False()
            eqExp(T(),Error(e21,e22)) -> False()
            eqExp(T(),F()) -> False()
            eqExp(T(),Fun(fn2,fe2)) -> False()
            eqExp(T(),ITE(i2,t2,e2)) -> False()
            eqExp(T(),T()) -> True()
            eqExp(T(),Var(v2)) -> False()
            eqExp(Var(v1),Bsf(op2,b21,b22)) -> False()
            eqExp(Var(v1),Eq(eq21,eq22)) -> False()
            eqExp(Var(v1),Error(e21,e22)) -> False()
            eqExp(Var(v1),F()) -> False()
            eqExp(Var(v1),Fun(fn2,fe2)) -> False()
            eqExp(Var(v1),ITE(i2,t2,e2)) -> False()
            eqExp(Var(v1),T()) -> False()
            eqExp(Var(v1),Var(v2)) -> !EQ(v1,v2)
            eqOps(o1,o2) -> True()
            getBsfFirstTerm(Bsf(op,t1,t2)) -> t1
            getBsfOp(Bsf(op,t1,t2)) -> op
            getBsfSecondTerm(Bsf(op,t1,t2)) -> t2
            getConst(Cst(int)) -> int
            getEqFirst(Eq(f,s)) -> f
            getEqSecond(Eq(f,s)) -> s
            getFuncExp(Fun(n,e)) -> e
            getFuncName(Fun(n,e)) -> n
            getIfFalse(ITE(i,t,e)) -> e
            getIfGuard(ITE(i,t,e)) -> i
            getIfTrue(ITE(i,t,e)) -> t
            getVar(Var(int)) -> int
            lookbody(f,Cons(Fun(n,e),xs)) -> lookbody[Ite](!EQ(f,n),f,Cons(Fun(n,e),xs))
            lookname(f,Cons(Fun(n,e),xs)) -> lookname[Ite](!EQ(f,n),f,Cons(Fun(n,e),xs))
            lookvar(x',Cons(x,xs),vs) -> lookvar[Ite](!EQ(x',x),x',Cons(x,xs),vs)
            run(Cons(Fun(f0,e),xs),input) -> run[Let][Let](Cons(Fun(f0,e),xs),input,f0,lookbody(f0,Cons(Fun(f0,e),xs)))
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            apply[Ite](False(),op,v1,v2) -> F()
            apply[Ite](True(),op,v1,v2) -> T()
            eeval[False][Ite](False(),Fun(n,e),ns,vs,p) -> eeval[False][Let](Fun(n,e),ns,vs,p,lookbody(n,p))
            eeval[False][Ite](True(),Eq(f,s),ns,vs,p) -> eeval[True][Ite](eqExp(eeval(f,ns,vs,p),eeval(s,ns,vs,p))
                                                                         ,Eq(f,s)
                                                                         ,ns
                                                                         ,vs
                                                                         ,p)
            eeval[False][Let](Fun(n,e),ns,vs,p,ef) -> eeval[False][Let][Let](Fun(n,e),ns,vs,p,ef,lookname(n,p))
            eeval[False][Let][Let](Fun(n,e),ns,vs,p,ef,nf) -> eeval[Let][Let][Let](Fun(n,e)
                                                                                  ,ns
                                                                                  ,vs
                                                                                  ,p
                                                                                  ,ef
                                                                                  ,nf
                                                                                  ,eeval(e,ns,vs,p))
            eeval[Ite](False(),ITE(i,t,e),ns,vs,p) -> eeval(e,ns,vs,p)
            eeval[Ite](True(),ITE(i,t,e),ns,vs,p) -> eeval(t,ns,vs,p)
            eeval[Let](Bsf(op,t1,t2),ns,vs,p,v1) -> eeval[Let][Let](Bsf(op,t1,t2),ns,vs,p,v1,eeval(t2,ns,vs,p))
            eeval[Let][Let](Bsf(op,t1,t2),ns,vs,p,v1,v2) -> apply(op,v1,v2)
            eeval[Let][Let][Let](e,ns,vs,p,ef,nf,v) -> eeval(ef,Cons(nf,Nil()),Cons(v,Nil()),p)
            eeval[True][Ite](False(),e,ns,vs,p) -> F()
            eeval[True][Ite](True(),e,ns,vs,p) -> T()
            lookbody[Ite](False(),f,Cons(x,xs)) -> lookbody(f,xs)
            lookbody[Ite](True(),f,Cons(Fun(n,e),xs)) -> e
            lookname[Ite](False(),f,Cons(x,xs)) -> lookname(f,xs)
            lookname[Ite](True(),f,Cons(Fun(n,e),xs)) -> n
            lookvar[Ite](False(),x',Cons(x'',xs'),Cons(x,xs)) -> lookvar(x',xs',xs)
            lookvar[Ite](True(),x',ns,Cons(x,xs)) -> x
            run[Let](p,input,f0,ef,nf) -> eeval(ef,Cons(nf,Nil()),Cons(input,Nil()),p)
            run[Let][Let](p,input,f0,ef) -> run[Let](p,input,f0,ef,lookname(f0,p))
        - Signature:
            {!EQ/2,and/2,apply/3,apply[Ite]/4,checkConstrExp/2,eeval/4,eeval[False][Ite]/5,eeval[False][Let]/5
            ,eeval[False][Let][Let]/6,eeval[Ite]/5,eeval[Let]/5,eeval[Let][Let]/6,eeval[Let][Let][Let]/7
            ,eeval[True][Ite]/5,eqExp/2,eqOps/2,getBsfFirstTerm/1,getBsfOp/1,getBsfSecondTerm/1,getConst/1,getEqFirst/1
            ,getEqSecond/1,getFuncExp/1,getFuncName/1,getIfFalse/1,getIfGuard/1,getIfTrue/1,getVar/1,lookbody/2
            ,lookbody[Ite]/3,lookname/2,lookname[Ite]/3,lookvar/3,lookvar[Ite]/4,run/2,run[Let]/5
            ,run[Let][Let]/4} / {0/0,Bsf/3,Cons/2,Cst/1,Eq/2,Error/2,F/0,False/0,Fun/2,ITE/3,Nil/0,S/1,T/0,True/0,Var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,and,apply,apply[Ite],checkConstrExp,eeval
            ,eeval[False][Ite],eeval[False][Let],eeval[False][Let][Let],eeval[Ite],eeval[Let],eeval[Let][Let]
            ,eeval[Let][Let][Let],eeval[True][Ite],eqExp,eqOps,getBsfFirstTerm,getBsfOp,getBsfSecondTerm,getConst
            ,getEqFirst,getEqSecond,getFuncExp,getFuncName,getIfFalse,getIfGuard,getIfTrue,getVar,lookbody,lookbody[Ite]
            ,lookname,lookname[Ite],lookvar,lookvar[Ite],run,run[Let],run[Let][Let]} and constructors {0,Bsf,Cons,Cst,Eq
            ,Error,F,False,Fun,ITE,Nil,S,T,True,Var}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          eeval(y,u,v,w){y -> Bsf(x,y,z)} =
            eeval(Bsf(x,y,z),u,v,w) ->^+ eeval[Let](Bsf(x,y,z),u,v,w,eeval(y,u,v,w))
              = C[eeval(y,u,v,w) = eeval(y,u,v,w){}]

WORST_CASE(Omega(n^1),?)