* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            appe1(App(e1,e2)) -> e1
            appe2(App(e1,e2)) -> e2
            eqTerm(App(t11,t12),App(t21,t22)) -> and(eqTerm(t11,t21),eqTerm(t12,t22))
            eqTerm(App(t11,t12),Lam(i2,l2)) -> False()
            eqTerm(App(t11,t12),V(v2)) -> False()
            eqTerm(Lam(i1,l1),App(t21,t22)) -> False()
            eqTerm(Lam(i1,l1),Lam(i2,l2)) -> and(!EQ(i1,i2),eqTerm(l1,l2))
            eqTerm(Lam(i1,l1),V(v2)) -> False()
            eqTerm(V(v1),App(t21,t22)) -> False()
            eqTerm(V(v1),Lam(i2,l2)) -> False()
            eqTerm(V(v1),V(v2)) -> !EQ(v1,v2)
            islam(App(t1,t2)) -> False()
            islam(Lam(int,term)) -> True()
            islam(V(int)) -> False()
            isvar(App(t1,t2)) -> False()
            isvar(Lam(int,term)) -> False()
            isvar(V(int)) -> True()
            lambdaint(e) -> red(e)
            lambody(Lam(var,exp)) -> exp
            lamvar(Lam(var,exp)) -> V(var)
            mkapp(e1,e2) -> App(e1,e2)
            mklam(V(name),e) -> Lam(name,e)
            red(App(e1,e2)) -> red[Let](App(e1,e2),red(e1))
            red(Lam(int,term)) -> Lam(int,term)
            red(V(int)) -> V(int)
            subst(x,a,App(e1,e2)) -> mkapp(subst(x,a,e1),subst(x,a,e2))
            subst(x,a,Lam(var,exp)) -> subst[True][Ite](eqTerm(x,V(var)),x,a,Lam(var,exp))
            subst(x,a,V(int)) -> subst[Ite](eqTerm(x,V(int)),x,a,V(int))
        - 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()
            red[Let](App(e1,e2),f) -> red[Let][Let](App(e1,e2),f,red(e2))
            red[Let][Let](e,App(t1,t2),e2) -> App(App(t1,t2),e2)
            red[Let][Let](e,Lam(var,exp),a) -> red(subst(V(var),a,exp))
            red[Let][Let](e,V(int),e2) -> App(V(int),e2)
            subst[Ite](False(),x,a,e) -> e
            subst[Ite](True(),x,a,e) -> a
            subst[True][Ite](False(),x,a,Lam(var,exp)) -> mklam(V(var),subst(x,a,exp))
            subst[True][Ite](True(),x,a,e) -> e
        - Signature:
            {!EQ/2,and/2,appe1/1,appe2/1,eqTerm/2,islam/1,isvar/1,lambdaint/1,lambody/1,lamvar/1,mkapp/2,mklam/2,red/1
            ,red[Let]/2,red[Let][Let]/3,subst/3,subst[Ite]/4,subst[True][Ite]/4} / {0/0,App/2,False/0,Lam/2,S/1,True/0
            ,V/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,and,appe1,appe2,eqTerm,islam,isvar,lambdaint,lambody
            ,lamvar,mkapp,mklam,red,red[Let],red[Let][Let],subst,subst[Ite],subst[True][Ite]} and constructors {0,App
            ,False,Lam,S,True,V}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            appe1(App(e1,e2)) -> e1
            appe2(App(e1,e2)) -> e2
            eqTerm(App(t11,t12),App(t21,t22)) -> and(eqTerm(t11,t21),eqTerm(t12,t22))
            eqTerm(App(t11,t12),Lam(i2,l2)) -> False()
            eqTerm(App(t11,t12),V(v2)) -> False()
            eqTerm(Lam(i1,l1),App(t21,t22)) -> False()
            eqTerm(Lam(i1,l1),Lam(i2,l2)) -> and(!EQ(i1,i2),eqTerm(l1,l2))
            eqTerm(Lam(i1,l1),V(v2)) -> False()
            eqTerm(V(v1),App(t21,t22)) -> False()
            eqTerm(V(v1),Lam(i2,l2)) -> False()
            eqTerm(V(v1),V(v2)) -> !EQ(v1,v2)
            islam(App(t1,t2)) -> False()
            islam(Lam(int,term)) -> True()
            islam(V(int)) -> False()
            isvar(App(t1,t2)) -> False()
            isvar(Lam(int,term)) -> False()
            isvar(V(int)) -> True()
            lambdaint(e) -> red(e)
            lambody(Lam(var,exp)) -> exp
            lamvar(Lam(var,exp)) -> V(var)
            mkapp(e1,e2) -> App(e1,e2)
            mklam(V(name),e) -> Lam(name,e)
            red(App(e1,e2)) -> red[Let](App(e1,e2),red(e1))
            red(Lam(int,term)) -> Lam(int,term)
            red(V(int)) -> V(int)
            subst(x,a,App(e1,e2)) -> mkapp(subst(x,a,e1),subst(x,a,e2))
            subst(x,a,Lam(var,exp)) -> subst[True][Ite](eqTerm(x,V(var)),x,a,Lam(var,exp))
            subst(x,a,V(int)) -> subst[Ite](eqTerm(x,V(int)),x,a,V(int))
        - 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()
            red[Let](App(e1,e2),f) -> red[Let][Let](App(e1,e2),f,red(e2))
            red[Let][Let](e,App(t1,t2),e2) -> App(App(t1,t2),e2)
            red[Let][Let](e,Lam(var,exp),a) -> red(subst(V(var),a,exp))
            red[Let][Let](e,V(int),e2) -> App(V(int),e2)
            subst[Ite](False(),x,a,e) -> e
            subst[Ite](True(),x,a,e) -> a
            subst[True][Ite](False(),x,a,Lam(var,exp)) -> mklam(V(var),subst(x,a,exp))
            subst[True][Ite](True(),x,a,e) -> e
        - Signature:
            {!EQ/2,and/2,appe1/1,appe2/1,eqTerm/2,islam/1,isvar/1,lambdaint/1,lambody/1,lamvar/1,mkapp/2,mklam/2,red/1
            ,red[Let]/2,red[Let][Let]/3,subst/3,subst[Ite]/4,subst[True][Ite]/4} / {0/0,App/2,False/0,Lam/2,S/1,True/0
            ,V/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,and,appe1,appe2,eqTerm,islam,isvar,lambdaint,lambody
            ,lamvar,mkapp,mklam,red,red[Let],red[Let][Let],subst,subst[Ite],subst[True][Ite]} and constructors {0,App
            ,False,Lam,S,True,V}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          eqTerm(x,z){x -> App(x,y),z -> App(z,u)} =
            eqTerm(App(x,y),App(z,u)) ->^+ and(eqTerm(x,z),eqTerm(y,u))
              = C[eqTerm(x,z) = eqTerm(x,z){}]

WORST_CASE(Omega(n^1),?)