MAYBE
* Step 1: Failure MAYBE
  + 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:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE