YES

Problem:
 quot(0(),s(y),s(z)) -> 0()
 quot(s(x),s(y),z) -> quot(x,y,z)
 quot(x,0(),s(z)) -> s(quot(x,s(z),s(z)))

Proof:
 DP Processor:
  DPs:
   quot#(s(x),s(y),z) -> quot#(x,y,z)
   quot#(x,0(),s(z)) -> quot#(x,s(z),s(z))
  TRS:
   quot(0(),s(y),s(z)) -> 0()
   quot(s(x),s(y),z) -> quot(x,y,z)
   quot(x,0(),s(z)) -> s(quot(x,s(z),s(z)))
  EDG Processor:
   DPs:
    quot#(s(x),s(y),z) -> quot#(x,y,z)
    quot#(x,0(),s(z)) -> quot#(x,s(z),s(z))
   TRS:
    quot(0(),s(y),s(z)) -> 0()
    quot(s(x),s(y),z) -> quot(x,y,z)
    quot(x,0(),s(z)) -> s(quot(x,s(z),s(z)))
   graph:
    quot#(s(x),s(y),z) -> quot#(x,y,z) ->
    quot#(s(x),s(y),z) -> quot#(x,y,z)
    quot#(s(x),s(y),z) -> quot#(x,y,z) ->
    quot#(x,0(),s(z)) -> quot#(x,s(z),s(z))
    quot#(x,0(),s(z)) -> quot#(x,s(z),s(z)) -> quot#(s(x),s(y),z) -> quot#(x,y,z)
   Subterm Criterion Processor:
    simple projection:
     pi(quot#) = 0
    problem:
     DPs:
      quot#(x,0(),s(z)) -> quot#(x,s(z),s(z))
     TRS:
      quot(0(),s(y),s(z)) -> 0()
      quot(s(x),s(y),z) -> quot(x,y,z)
      quot(x,0(),s(z)) -> s(quot(x,s(z),s(z)))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [quot#](x0, x1, x2) = x1,
      
      [quot](x0, x1, x2) = 1,
      
      [s](x0) = 0,
      
      [0] = 1
     orientation:
      quot#(x,0(),s(z)) = 1 >= 0 = quot#(x,s(z),s(z))
      
      quot(0(),s(y),s(z)) = 1 >= 1 = 0()
      
      quot(s(x),s(y),z) = 1 >= 1 = quot(x,y,z)
      
      quot(x,0(),s(z)) = 1 >= 0 = s(quot(x,s(z),s(z)))
     problem:
      DPs:
       
      TRS:
       quot(0(),s(y),s(z)) -> 0()
       quot(s(x),s(y),z) -> quot(x,y,z)
       quot(x,0(),s(z)) -> s(quot(x,s(z),s(z)))
     Qed