YES

Problem:
 a(h(),h(),h(),x) -> s(x)
 a(l,x,s(y),h()) -> a(l,x,y,s(h()))
 a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
 a(l,s(x),h(),z) -> a(l,x,z,z)
 a(s(l),h(),h(),z) -> a(l,z,h(),z)
 +(x,h()) -> x
 +(h(),x) -> x
 +(s(x),s(y)) -> s(s(+(x,y)))
 +(+(x,y),z) -> +(x,+(y,z))
 s(h()) -> 1()
 app(nil(),k) -> k
 app(l,nil()) -> l
 app(cons(x,l),k) -> cons(x,app(l,k))
 sum(cons(x,nil())) -> cons(x,nil())
 sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))

Proof:
 DP Processor:
  DPs:
   a#(h(),h(),h(),x) -> s#(x)
   a#(l,x,s(y),h()) -> s#(h())
   a#(l,x,s(y),h()) -> a#(l,x,y,s(h()))
   a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
   a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z))
   a#(l,s(x),h(),z) -> a#(l,x,z,z)
   a#(s(l),h(),h(),z) -> a#(l,z,h(),z)
   +#(s(x),s(y)) -> +#(x,y)
   +#(s(x),s(y)) -> s#(+(x,y))
   +#(s(x),s(y)) -> s#(s(+(x,y)))
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
   app#(cons(x,l),k) -> app#(l,k)
   sum#(cons(x,cons(y,l))) -> a#(x,y,h(),h())
   sum#(cons(x,cons(y,l))) -> sum#(cons(a(x,y,h(),h()),l))
  TRS:
   a(h(),h(),h(),x) -> s(x)
   a(l,x,s(y),h()) -> a(l,x,y,s(h()))
   a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
   a(l,s(x),h(),z) -> a(l,x,z,z)
   a(s(l),h(),h(),z) -> a(l,z,h(),z)
   +(x,h()) -> x
   +(h(),x) -> x
   +(s(x),s(y)) -> s(s(+(x,y)))
   +(+(x,y),z) -> +(x,+(y,z))
   s(h()) -> 1()
   app(nil(),k) -> k
   app(l,nil()) -> l
   app(cons(x,l),k) -> cons(x,app(l,k))
   sum(cons(x,nil())) -> cons(x,nil())
   sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
  EDG Processor:
   DPs:
    a#(h(),h(),h(),x) -> s#(x)
    a#(l,x,s(y),h()) -> s#(h())
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h()))
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z))
    a#(l,s(x),h(),z) -> a#(l,x,z,z)
    a#(s(l),h(),h(),z) -> a#(l,z,h(),z)
    +#(s(x),s(y)) -> +#(x,y)
    +#(s(x),s(y)) -> s#(+(x,y))
    +#(s(x),s(y)) -> s#(s(+(x,y)))
    +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z))
    app#(cons(x,l),k) -> app#(l,k)
    sum#(cons(x,cons(y,l))) -> a#(x,y,h(),h())
    sum#(cons(x,cons(y,l))) -> sum#(cons(a(x,y,h(),h()),l))
   TRS:
    a(h(),h(),h(),x) -> s(x)
    a(l,x,s(y),h()) -> a(l,x,y,s(h()))
    a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
    a(l,s(x),h(),z) -> a(l,x,z,z)
    a(s(l),h(),h(),z) -> a(l,z,h(),z)
    +(x,h()) -> x
    +(h(),x) -> x
    +(s(x),s(y)) -> s(s(+(x,y)))
    +(+(x,y),z) -> +(x,+(y,z))
    s(h()) -> 1()
    app(nil(),k) -> k
    app(l,nil()) -> l
    app(cons(x,l),k) -> cons(x,app(l,k))
    sum(cons(x,nil())) -> cons(x,nil())
    sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
   graph:
    sum#(cons(x,cons(y,l))) -> sum#(cons(a(x,y,h(),h()),l)) ->
    sum#(cons(x,cons(y,l))) -> a#(x,y,h(),h())
    sum#(cons(x,cons(y,l))) -> sum#(cons(a(x,y,h(),h()),l)) ->
    sum#(cons(x,cons(y,l))) -> sum#(cons(a(x,y,h(),h()),l))
    sum#(cons(x,cons(y,l))) -> a#(x,y,h(),h()) ->
    a#(h(),h(),h(),x) -> s#(x)
    sum#(cons(x,cons(y,l))) -> a#(x,y,h(),h()) ->
    a#(l,s(x),h(),z) -> a#(l,x,z,z)
    sum#(cons(x,cons(y,l))) -> a#(x,y,h(),h()) ->
    a#(s(l),h(),h(),z) -> a#(l,z,h(),z)
    app#(cons(x,l),k) -> app#(l,k) -> app#(cons(x,l),k) -> app#(l,k)
    +#(+(x,y),z) -> +#(y,z) -> +#(s(x),s(y)) -> +#(x,y)
    +#(+(x,y),z) -> +#(y,z) -> +#(s(x),s(y)) -> s#(+(x,y))
    +#(+(x,y),z) -> +#(y,z) -> +#(s(x),s(y)) -> s#(s(+(x,y)))
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(s(x),s(y)) -> +#(x,y)
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(s(x),s(y)) -> s#(+(x,y))
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(s(x),s(y)) -> s#(s(+(x,y)))
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(s(x),s(y)) -> +#(x,y) -> +#(s(x),s(y)) -> +#(x,y)
    +#(s(x),s(y)) -> +#(x,y) -> +#(s(x),s(y)) -> s#(+(x,y))
    +#(s(x),s(y)) -> +#(x,y) -> +#(s(x),s(y)) -> s#(s(+(x,y)))
    +#(s(x),s(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(y,z)
    +#(s(x),s(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(x,+(y,z))
    a#(s(l),h(),h(),z) -> a#(l,z,h(),z) ->
    a#(h(),h(),h(),x) -> s#(x)
    a#(s(l),h(),h(),z) -> a#(l,z,h(),z) ->
    a#(l,s(x),h(),z) -> a#(l,x,z,z)
    a#(s(l),h(),h(),z) -> a#(l,z,h(),z) ->
    a#(s(l),h(),h(),z) -> a#(l,z,h(),z)
    a#(l,s(x),h(),z) -> a#(l,x,z,z) -> a#(h(),h(),h(),x) -> s#(x)
    a#(l,s(x),h(),z) -> a#(l,x,z,z) -> a#(l,x,s(y),h()) -> s#(h())
    a#(l,s(x),h(),z) -> a#(l,x,z,z) ->
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h()))
    a#(l,s(x),h(),z) -> a#(l,x,z,z) ->
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
    a#(l,s(x),h(),z) -> a#(l,x,z,z) ->
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z))
    a#(l,s(x),h(),z) -> a#(l,x,z,z) ->
    a#(l,s(x),h(),z) -> a#(l,x,z,z)
    a#(l,s(x),h(),z) -> a#(l,x,z,z) ->
    a#(s(l),h(),h(),z) -> a#(l,z,h(),z)
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z) ->
    a#(h(),h(),h(),x) -> s#(x)
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z) ->
    a#(l,x,s(y),h()) -> s#(h())
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z) ->
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h()))
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z) ->
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z) ->
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z))
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z) ->
    a#(l,s(x),h(),z) -> a#(l,x,z,z)
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z) ->
    a#(s(l),h(),h(),z) -> a#(l,z,h(),z)
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z)) ->
    a#(h(),h(),h(),x) -> s#(x)
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z)) ->
    a#(l,x,s(y),h()) -> s#(h())
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z)) ->
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h()))
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z)) ->
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z)) ->
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z))
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z)) ->
    a#(l,s(x),h(),z) -> a#(l,x,z,z)
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z)) ->
    a#(s(l),h(),h(),z) -> a#(l,z,h(),z)
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h())) ->
    a#(h(),h(),h(),x) -> s#(x)
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h())) ->
    a#(l,x,s(y),h()) -> s#(h())
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h())) ->
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h()))
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h())) ->
    a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h())) ->
    a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z))
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h())) ->
    a#(l,s(x),h(),z) -> a#(l,x,z,z)
    a#(l,x,s(y),h()) -> a#(l,x,y,s(h())) -> a#(s(l),h(),h(),z) -> a#(l,z,h(),z)
   SCC Processor:
    #sccs: 4
    #rules: 10
    #arcs: 52/225
    DPs:
     +#(+(x,y),z) -> +#(y,z)
     +#(+(x,y),z) -> +#(x,+(y,z))
     +#(s(x),s(y)) -> +#(x,y)
    TRS:
     a(h(),h(),h(),x) -> s(x)
     a(l,x,s(y),h()) -> a(l,x,y,s(h()))
     a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
     a(l,s(x),h(),z) -> a(l,x,z,z)
     a(s(l),h(),h(),z) -> a(l,z,h(),z)
     +(x,h()) -> x
     +(h(),x) -> x
     +(s(x),s(y)) -> s(s(+(x,y)))
     +(+(x,y),z) -> +(x,+(y,z))
     s(h()) -> 1()
     app(nil(),k) -> k
     app(l,nil()) -> l
     app(cons(x,l),k) -> cons(x,app(l,k))
     sum(cons(x,nil())) -> cons(x,nil())
     sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
    Subterm Criterion Processor:
     simple projection:
      pi(+#) = 0
     problem:
      DPs:
       
      TRS:
       a(h(),h(),h(),x) -> s(x)
       a(l,x,s(y),h()) -> a(l,x,y,s(h()))
       a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
       a(l,s(x),h(),z) -> a(l,x,z,z)
       a(s(l),h(),h(),z) -> a(l,z,h(),z)
       +(x,h()) -> x
       +(h(),x) -> x
       +(s(x),s(y)) -> s(s(+(x,y)))
       +(+(x,y),z) -> +(x,+(y,z))
       s(h()) -> 1()
       app(nil(),k) -> k
       app(l,nil()) -> l
       app(cons(x,l),k) -> cons(x,app(l,k))
       sum(cons(x,nil())) -> cons(x,nil())
       sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
     Qed
    
    DPs:
     app#(cons(x,l),k) -> app#(l,k)
    TRS:
     a(h(),h(),h(),x) -> s(x)
     a(l,x,s(y),h()) -> a(l,x,y,s(h()))
     a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
     a(l,s(x),h(),z) -> a(l,x,z,z)
     a(s(l),h(),h(),z) -> a(l,z,h(),z)
     +(x,h()) -> x
     +(h(),x) -> x
     +(s(x),s(y)) -> s(s(+(x,y)))
     +(+(x,y),z) -> +(x,+(y,z))
     s(h()) -> 1()
     app(nil(),k) -> k
     app(l,nil()) -> l
     app(cons(x,l),k) -> cons(x,app(l,k))
     sum(cons(x,nil())) -> cons(x,nil())
     sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      TRS:
       a(h(),h(),h(),x) -> s(x)
       a(l,x,s(y),h()) -> a(l,x,y,s(h()))
       a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
       a(l,s(x),h(),z) -> a(l,x,z,z)
       a(s(l),h(),h(),z) -> a(l,z,h(),z)
       +(x,h()) -> x
       +(h(),x) -> x
       +(s(x),s(y)) -> s(s(+(x,y)))
       +(+(x,y),z) -> +(x,+(y,z))
       s(h()) -> 1()
       app(nil(),k) -> k
       app(l,nil()) -> l
       app(cons(x,l),k) -> cons(x,app(l,k))
       sum(cons(x,nil())) -> cons(x,nil())
       sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
     Qed
    
    DPs:
     sum#(cons(x,cons(y,l))) -> sum#(cons(a(x,y,h(),h()),l))
    TRS:
     a(h(),h(),h(),x) -> s(x)
     a(l,x,s(y),h()) -> a(l,x,y,s(h()))
     a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
     a(l,s(x),h(),z) -> a(l,x,z,z)
     a(s(l),h(),h(),z) -> a(l,z,h(),z)
     +(x,h()) -> x
     +(h(),x) -> x
     +(s(x),s(y)) -> s(s(+(x,y)))
     +(+(x,y),z) -> +(x,+(y,z))
     s(h()) -> 1()
     app(nil(),k) -> k
     app(l,nil()) -> l
     app(cons(x,l),k) -> cons(x,app(l,k))
     sum(cons(x,nil())) -> cons(x,nil())
     sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [sum#](x0) = x0,
      
      [sum](x0) = 1,
      
      [cons](x0, x1) = x1 + 1,
      
      [app](x0, x1) = x0 + x1,
      
      [nil] = 0,
      
      [1] = 0,
      
      [+](x0, x1) = x0 + x1,
      
      [s](x0) = 0,
      
      [a](x0, x1, x2, x3) = 1,
      
      [h] = 0
     orientation:
      sum#(cons(x,cons(y,l))) = l + 2 >= l + 1 = sum#(cons(a(x,y,h(),h()),l))
      
      a(h(),h(),h(),x) = 1 >= 0 = s(x)
      
      a(l,x,s(y),h()) = 1 >= 1 = a(l,x,y,s(h()))
      
      a(l,x,s(y),s(z)) = 1 >= 1 = a(l,x,y,a(l,x,s(y),z))
      
      a(l,s(x),h(),z) = 1 >= 1 = a(l,x,z,z)
      
      a(s(l),h(),h(),z) = 1 >= 1 = a(l,z,h(),z)
      
      +(x,h()) = x >= x = x
      
      +(h(),x) = x >= x = x
      
      +(s(x),s(y)) = 0 >= 0 = s(s(+(x,y)))
      
      +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
      
      s(h()) = 0 >= 0 = 1()
      
      app(nil(),k) = k >= k = k
      
      app(l,nil()) = l >= l = l
      
      app(cons(x,l),k) = k + l + 1 >= k + l + 1 = cons(x,app(l,k))
      
      sum(cons(x,nil())) = 1 >= 1 = cons(x,nil())
      
      sum(cons(x,cons(y,l))) = 1 >= 1 = sum(cons(a(x,y,h(),h()),l))
     problem:
      DPs:
       
      TRS:
       a(h(),h(),h(),x) -> s(x)
       a(l,x,s(y),h()) -> a(l,x,y,s(h()))
       a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
       a(l,s(x),h(),z) -> a(l,x,z,z)
       a(s(l),h(),h(),z) -> a(l,z,h(),z)
       +(x,h()) -> x
       +(h(),x) -> x
       +(s(x),s(y)) -> s(s(+(x,y)))
       +(+(x,y),z) -> +(x,+(y,z))
       s(h()) -> 1()
       app(nil(),k) -> k
       app(l,nil()) -> l
       app(cons(x,l),k) -> cons(x,app(l,k))
       sum(cons(x,nil())) -> cons(x,nil())
       sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
     Qed
    
    DPs:
     a#(s(l),h(),h(),z) -> a#(l,z,h(),z)
     a#(l,s(x),h(),z) -> a#(l,x,z,z)
     a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z))
     a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
     a#(l,x,s(y),h()) -> a#(l,x,y,s(h()))
    TRS:
     a(h(),h(),h(),x) -> s(x)
     a(l,x,s(y),h()) -> a(l,x,y,s(h()))
     a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
     a(l,s(x),h(),z) -> a(l,x,z,z)
     a(s(l),h(),h(),z) -> a(l,z,h(),z)
     +(x,h()) -> x
     +(h(),x) -> x
     +(s(x),s(y)) -> s(s(+(x,y)))
     +(+(x,y),z) -> +(x,+(y,z))
     s(h()) -> 1()
     app(nil(),k) -> k
     app(l,nil()) -> l
     app(cons(x,l),k) -> cons(x,app(l,k))
     sum(cons(x,nil())) -> cons(x,nil())
     sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
    Subterm Criterion Processor:
     simple projection:
      pi(a#) = 0
     problem:
      DPs:
       a#(l,s(x),h(),z) -> a#(l,x,z,z)
       a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z))
       a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
       a#(l,x,s(y),h()) -> a#(l,x,y,s(h()))
      TRS:
       a(h(),h(),h(),x) -> s(x)
       a(l,x,s(y),h()) -> a(l,x,y,s(h()))
       a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
       a(l,s(x),h(),z) -> a(l,x,z,z)
       a(s(l),h(),h(),z) -> a(l,z,h(),z)
       +(x,h()) -> x
       +(h(),x) -> x
       +(s(x),s(y)) -> s(s(+(x,y)))
       +(+(x,y),z) -> +(x,+(y,z))
       s(h()) -> 1()
       app(nil(),k) -> k
       app(l,nil()) -> l
       app(cons(x,l),k) -> cons(x,app(l,k))
       sum(cons(x,nil())) -> cons(x,nil())
       sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
     Subterm Criterion Processor:
      simple projection:
       pi(a#) = 1
      problem:
       DPs:
        a#(l,x,s(y),s(z)) -> a#(l,x,y,a(l,x,s(y),z))
        a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
        a#(l,x,s(y),h()) -> a#(l,x,y,s(h()))
       TRS:
        a(h(),h(),h(),x) -> s(x)
        a(l,x,s(y),h()) -> a(l,x,y,s(h()))
        a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
        a(l,s(x),h(),z) -> a(l,x,z,z)
        a(s(l),h(),h(),z) -> a(l,z,h(),z)
        +(x,h()) -> x
        +(h(),x) -> x
        +(s(x),s(y)) -> s(s(+(x,y)))
        +(+(x,y),z) -> +(x,+(y,z))
        s(h()) -> 1()
        app(nil(),k) -> k
        app(l,nil()) -> l
        app(cons(x,l),k) -> cons(x,app(l,k))
        sum(cons(x,nil())) -> cons(x,nil())
        sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
      Subterm Criterion Processor:
       simple projection:
        pi(a#) = 2
       problem:
        DPs:
         a#(l,x,s(y),s(z)) -> a#(l,x,s(y),z)
        TRS:
         a(h(),h(),h(),x) -> s(x)
         a(l,x,s(y),h()) -> a(l,x,y,s(h()))
         a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
         a(l,s(x),h(),z) -> a(l,x,z,z)
         a(s(l),h(),h(),z) -> a(l,z,h(),z)
         +(x,h()) -> x
         +(h(),x) -> x
         +(s(x),s(y)) -> s(s(+(x,y)))
         +(+(x,y),z) -> +(x,+(y,z))
         s(h()) -> 1()
         app(nil(),k) -> k
         app(l,nil()) -> l
         app(cons(x,l),k) -> cons(x,app(l,k))
         sum(cons(x,nil())) -> cons(x,nil())
         sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
       Subterm Criterion Processor:
        simple projection:
         pi(a#) = 3
        problem:
         DPs:
          
         TRS:
          a(h(),h(),h(),x) -> s(x)
          a(l,x,s(y),h()) -> a(l,x,y,s(h()))
          a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
          a(l,s(x),h(),z) -> a(l,x,z,z)
          a(s(l),h(),h(),z) -> a(l,z,h(),z)
          +(x,h()) -> x
          +(h(),x) -> x
          +(s(x),s(y)) -> s(s(+(x,y)))
          +(+(x,y),z) -> +(x,+(y,z))
          s(h()) -> 1()
          app(nil(),k) -> k
          app(l,nil()) -> l
          app(cons(x,l),k) -> cons(x,app(l,k))
          sum(cons(x,nil())) -> cons(x,nil())
          sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h(),h()),l))
        Qed