YES
Time: 0.026968
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:
  DP:
   {  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)}
  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)}
  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 (2):
    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 (2):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [.](x0, x1) = x0 + x1,
       
       [f](x0) = 0,
       
       [g](x0) = x0 + 1,
       
       [nil] = 1,
       
       [g#](x0) = x0
      Strict:
       g# .(x, .(y, z)) -> g# .(.(x, y), z)
       0 + 1y + 1x + 1z >= 0 + 1y + 1x + 1z
       g# .(x, nil()) -> g# x
       1 + 1x >= 0 + 1x
      Weak:
       
     EDG:
      {(g# .(x, .(y, z)) -> g# .(.(x, y), z), g# .(x, .(y, z)) -> g# .(.(x, y), z))}
      SCCS (1):
       Scc:
        {g# .(x, .(y, z)) -> g# .(.(x, y), z)}
       SCC (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)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [.](x0, x1) = x0 + 1,
          
          [f](x0) = 0,
          
          [g](x0) = x0 + 1,
          
          [nil] = 1,
          
          [g#](x0) = x0
         Strict:
          g# .(x, .(y, z)) -> g# .(.(x, y), z)
          2 + 0y + 0x + 1z >= 1 + 0y + 0x + 1z
         Weak:
          
        Qed
   SCC (2):
    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:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [.](x0, x1) = x0 + x1,
      
      [f](x0) = x0 + 1,
      
      [g](x0) = x0 + 1,
      
      [nil] = 1,
      
      [f#](x0) = x0
     Strict:
      f# .(.(x, y), z) -> f# .(x, .(y, z))
      0 + 1y + 1x + 1z >= 0 + 1y + 1x + 1z
      f# .(nil(), y) -> f# y
      1 + 1y >= 0 + 1y
     Weak:
      
    EDG:
     {(f# .(.(x, y), z) -> f# .(x, .(y, z)), f# .(.(x, y), z) -> f# .(x, .(y, z)))}
     SCCS (1):
      Scc:
       {f# .(.(x, y), z) -> f# .(x, .(y, z))}
      SCC (1):
       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:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [.](x0, x1) = x0 + 1,
         
         [f](x0) = x0 + 1,
         
         [g](x0) = x0 + 1,
         
         [nil] = 1,
         
         [f#](x0) = x0
        Strict:
         f# .(.(x, y), z) -> f# .(x, .(y, z))
         2 + 0y + 1x + 0z >= 1 + 0y + 1x + 0z
        Weak:
         
       Qed