MAYBE

Problem:
 fapp(lam(X),Y) -> subst(X,Y)
 subst(v(),Y) -> Y
 subst(lam(X),Y) -> lam(X)
 subst(fapp(X,Z),Y) -> fapp(subst(X,Y),subst(Z,Y))

Proof:
 DP Processor:
  DPs:
   fapp#(lam(X),Y) -> subst#(X,Y)
   subst#(fapp(X,Z),Y) -> subst#(Z,Y)
   subst#(fapp(X,Z),Y) -> subst#(X,Y)
   subst#(fapp(X,Z),Y) -> fapp#(subst(X,Y),subst(Z,Y))
  TRS:
   fapp(lam(X),Y) -> subst(X,Y)
   subst(v(),Y) -> Y
   subst(lam(X),Y) -> lam(X)
   subst(fapp(X,Z),Y) -> fapp(subst(X,Y),subst(Z,Y))
  Open