YES
Time: 0.001472
TRS:
 {  f(x, y, s z) -> s f(0(), 1(), z),
  f(0(), 1(), x) -> f(s x, x, x)}
 DP:
  DP:
   {  f#(x, y, s z) -> f#(0(), 1(), z),
    f#(0(), 1(), x) -> f#(s x, x, x)}
  TRS:
  {  f(x, y, s z) -> s f(0(), 1(), z),
   f(0(), 1(), x) -> f(s x, x, x)}
  EDG:
   {(f#(0(), 1(), x) -> f#(s x, x, x), f#(x, y, s z) -> f#(0(), 1(), z))
    (f#(x, y, s z) -> f#(0(), 1(), z), f#(x, y, s z) -> f#(0(), 1(), z))
    (f#(x, y, s z) -> f#(0(), 1(), z), f#(0(), 1(), x) -> f#(s x, x, x))}
   SCCS (1):
    Scc:
     {  f#(x, y, s z) -> f#(0(), 1(), z),
      f#(0(), 1(), x) -> f#(s x, x, x)}
    SCC (2):
     Strict:
      {  f#(x, y, s z) -> f#(0(), 1(), z),
       f#(0(), 1(), x) -> f#(s x, x, x)}
     Weak:
     {  f(x, y, s z) -> s f(0(), 1(), z),
      f(0(), 1(), x) -> f(s x, x, x)}
     SPSC:
      Simple Projection:
       pi(f#) = 2
      Strict:
       {f#(0(), 1(), x) -> f#(s x, x, x)}
      EDG:
       {}
       SCCS (0):
        
        Qed