YES
TRS:
 {        f(nil()) -> nil(),
    f(.(nil(), y)) -> .(nil(), f(y)),
  f(.(.(x, y), z)) -> f(.(x, .(y, z))),
          g(nil()) -> nil(),
    g(.(x, nil())) -> .(g(x), nil()),
  g(.(x, .(y, z))) -> g(.(.(x, y), z))}
 DP:
  Strict:
   {  f#(.(nil(), y)) -> f#(y),
    f#(.(.(x, y), z)) -> f#(.(x, .(y, z))),
      g#(.(x, nil())) -> g#(x),
    g#(.(x, .(y, z))) -> g#(.(.(x, y), z))}
  Weak:
  {        f(nil()) -> nil(),
     f(.(nil(), y)) -> .(nil(), f(y)),
   f(.(.(x, y), z)) -> f(.(x, .(y, z))),
           g(nil()) -> nil(),
     g(.(x, nil())) -> .(g(x), nil()),
   g(.(x, .(y, z))) -> g(.(.(x, y), z))}
  EDG:
   {(g#(.(x, nil())) -> g#(x), g#(.(x, .(y, z))) -> g#(.(.(x, y), z)))
    (g#(.(x, nil())) -> g#(x), g#(.(x, nil())) -> g#(x))
    (g#(.(x, .(y, z))) -> g#(.(.(x, y), z)), g#(.(x, .(y, z))) -> g#(.(.(x, y), z)))
    (g#(.(x, .(y, z))) -> g#(.(.(x, y), z)), g#(.(x, nil())) -> g#(x))
    (f#(.(.(x, y), z)) -> f#(.(x, .(y, z))), f#(.(nil(), y)) -> f#(y))
    (f#(.(.(x, y), z)) -> f#(.(x, .(y, z))), f#(.(.(x, y), z)) -> f#(.(x, .(y, z))))
    (f#(.(nil(), y)) -> f#(y), f#(.(nil(), y)) -> f#(y))
    (f#(.(nil(), y)) -> f#(y), f#(.(.(x, y), z)) -> f#(.(x, .(y, z))))}
   SCCS:
    Scc:
     {  g#(.(x, nil())) -> g#(x),
      g#(.(x, .(y, z))) -> g#(.(.(x, y), z))}
    Scc:
     {  f#(.(nil(), y)) -> f#(y),
      f#(.(.(x, y), z)) -> f#(.(x, .(y, z)))}
    SCC:
     Strict:
      {  g#(.(x, nil())) -> g#(x),
       g#(.(x, .(y, z))) -> g#(.(.(x, y), z))}
     Weak:
     {        f(nil()) -> nil(),
        f(.(nil(), y)) -> .(nil(), f(y)),
      f(.(.(x, y), z)) -> f(.(x, .(y, z))),
              g(nil()) -> nil(),
        g(.(x, nil())) -> .(g(x), nil()),
      g(.(x, .(y, z))) -> g(.(.(x, y), z))}
     POLY:
      Argument Filtering:
       pi(g#) = 0, pi(g) = [], pi(.) = [0,1], pi(f) = [], pi(nil) = []
      Usable Rules:
       {}
      Interpretation:
       [.](x0, x1) = x0 + x1,
       [nil] = 1
      Strict:
       {g#(.(x, .(y, z))) -> g#(.(.(x, y), z))}
      Weak:
       {        f(nil()) -> nil(),
          f(.(nil(), y)) -> .(nil(), f(y)),
        f(.(.(x, y), z)) -> f(.(x, .(y, z))),
                g(nil()) -> nil(),
          g(.(x, nil())) -> .(g(x), nil()),
        g(.(x, .(y, z))) -> g(.(.(x, y), z))}
      EDG:
       {(g#(.(x, .(y, z))) -> g#(.(.(x, y), z)), g#(.(x, .(y, z))) -> g#(.(.(x, y), z)))}
       SCCS:
        Scc:
         {g#(.(x, .(y, z))) -> g#(.(.(x, y), z))}
        SCC:
         Strict:
          {g#(.(x, .(y, z))) -> g#(.(.(x, y), z))}
         Weak:
         {        f(nil()) -> nil(),
            f(.(nil(), y)) -> .(nil(), f(y)),
          f(.(.(x, y), z)) -> f(.(x, .(y, z))),
                  g(nil()) -> nil(),
            g(.(x, nil())) -> .(g(x), nil()),
          g(.(x, .(y, z))) -> g(.(.(x, y), z))}
         POLY:
          Argument Filtering:
           pi(g#) = [0], pi(g) = [], pi(.) = [1], pi(f) = [], pi(nil) = []
          Usable Rules:
           {}
          Interpretation:
           [g#](x0) = x0 + 1,
           [.](x0) = x0 + 1
          Strict:
           {}
          Weak:
           {        f(nil()) -> nil(),
              f(.(nil(), y)) -> .(nil(), f(y)),
            f(.(.(x, y), z)) -> f(.(x, .(y, z))),
                    g(nil()) -> nil(),
              g(.(x, nil())) -> .(g(x), nil()),
            g(.(x, .(y, z))) -> g(.(.(x, y), z))}
          Qed
    SCC:
     Strict:
      {  f#(.(nil(), y)) -> f#(y),
       f#(.(.(x, y), z)) -> f#(.(x, .(y, z)))}
     Weak:
     {        f(nil()) -> nil(),
        f(.(nil(), y)) -> .(nil(), f(y)),
      f(.(.(x, y), z)) -> f(.(x, .(y, z))),
              g(nil()) -> nil(),
        g(.(x, nil())) -> .(g(x), nil()),
      g(.(x, .(y, z))) -> g(.(.(x, y), z))}
     POLY:
      Argument Filtering:
       pi(g) = [], pi(.) = [0,1], pi(f#) = [0], pi(f) = [], pi(nil) = []
      Usable Rules:
       {}
      Interpretation:
       [f#](x0) = x0 + 1,
       [.](x0, x1) = x0 + x1 + 1,
       [nil] = 0
      Strict:
       {f#(.(.(x, y), z)) -> f#(.(x, .(y, z)))}
      Weak:
       {        f(nil()) -> nil(),
          f(.(nil(), y)) -> .(nil(), f(y)),
        f(.(.(x, y), z)) -> f(.(x, .(y, z))),
                g(nil()) -> nil(),
          g(.(x, nil())) -> .(g(x), nil()),
        g(.(x, .(y, z))) -> g(.(.(x, y), z))}
      EDG:
       {(f#(.(.(x, y), z)) -> f#(.(x, .(y, z))), f#(.(.(x, y), z)) -> f#(.(x, .(y, z))))}
       SCCS:
        Scc:
         {f#(.(.(x, y), z)) -> f#(.(x, .(y, z)))}
        SCC:
         Strict:
          {f#(.(.(x, y), z)) -> f#(.(x, .(y, z)))}
         Weak:
         {        f(nil()) -> nil(),
            f(.(nil(), y)) -> .(nil(), f(y)),
          f(.(.(x, y), z)) -> f(.(x, .(y, z))),
                  g(nil()) -> nil(),
            g(.(x, nil())) -> .(g(x), nil()),
          g(.(x, .(y, z))) -> g(.(.(x, y), z))}
         POLY:
          Argument Filtering:
           pi(g) = [], pi(.) = [0], pi(f#) = [0], pi(f) = [], pi(nil) = []
          Usable Rules:
           {}
          Interpretation:
           [f#](x0) = x0 + 1,
           [.](x0) = x0 + 1
          Strict:
           {}
          Weak:
           {        f(nil()) -> nil(),
              f(.(nil(), y)) -> .(nil(), f(y)),
            f(.(.(x, y), z)) -> f(.(x, .(y, z))),
                    g(nil()) -> nil(),
              g(.(x, nil())) -> .(g(x), nil()),
            g(.(x, .(y, z))) -> g(.(.(x, y), z))}
          Qed