YES

Problem:
 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))

Proof:
 DP Processor:
  DPs:
   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 Processor:
   DPs:
    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))
   graph:
    g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) -> g#(.(x,nil())) -> g#(x)
    g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) -> g#(.(x,.(y,z))) -> g#(.(.(x,y),z))
    g#(.(x,nil())) -> g#(x) -> g#(.(x,nil())) -> g#(x)
    g#(.(x,nil())) -> g#(x) -> g#(.(x,.(y,z))) -> g#(.(.(x,y),z))
    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)))
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 8/16
    DPs:
     f#(.(.(x,y),z)) -> f#(.(x,.(y,z)))
     f#(.(nil(),y)) -> f#(y)
    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))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [f#](x0) = x0 + 1,
      
      [g](x0) = x0,
      
      [.](x0, x1) = x0 + x1,
      
      [f](x0) = x0,
      
      [nil] = 1
     orientation:
      f#(.(.(x,y),z)) = x + y + z + 1 >= x + y + z + 1 = f#(.(x,.(y,z)))
      
      f#(.(nil(),y)) = y + 2 >= y + 1 = f#(y)
      
      f(nil()) = 1 >= 1 = nil()
      
      f(.(nil(),y)) = y + 1 >= y + 1 = .(nil(),f(y))
      
      f(.(.(x,y),z)) = x + y + z >= x + y + z = f(.(x,.(y,z)))
      
      g(nil()) = 1 >= 1 = nil()
      
      g(.(x,nil())) = x + 1 >= x + 1 = .(g(x),nil())
      
      g(.(x,.(y,z))) = x + y + z >= x + y + z = g(.(.(x,y),z))
     problem:
      DPs:
       f#(.(.(x,y),z)) -> f#(.(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))
     Bounds Processor:
      bound: 0
      enrichment: match
      automaton:
       final states: {11,9,8,6,5,1}
       transitions:
        g0(12) -> 11*
        g0(2) -> 10*
        g0(3) -> 16*
        f60() -> 2*
        f{#,0}(4) -> 1*
        .0(10,5) -> 9*
        .0(5,7) -> 6*
        .0(2,3) -> 4*
        .0(3,2) -> 12*
        .0(5,14) -> 8*
        .0(16,5) -> 11*
        .0(12,2) -> 12*
        .0(2,2) -> 3*
        .0(2,4) -> 4*
        nil0() -> 5*
        f0(2) -> 7*
        f0(4) -> 8*
        f0(3) -> 14*
        5 -> 10,7
        6 -> 8,14,7
        8 -> 14,7
        9 -> 11,16,10
        11 -> 16,10
      problem:
       DPs:
        
       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))
      Qed
    
    DPs:
     g#(.(x,.(y,z))) -> g#(.(.(x,y),z))
     g#(.(x,nil())) -> g#(x)
    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))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [g#](x0) = x0,
      
      [g](x0) = x0 + 1,
      
      [.](x0, x1) = x0 + x1 + 1,
      
      [f](x0) = x0,
      
      [nil] = 1
     orientation:
      g#(.(x,.(y,z))) = x + y + z + 2 >= x + y + z + 2 = g#(.(.(x,y),z))
      
      g#(.(x,nil())) = x + 2 >= x = g#(x)
      
      f(nil()) = 1 >= 1 = nil()
      
      f(.(nil(),y)) = y + 2 >= y + 2 = .(nil(),f(y))
      
      f(.(.(x,y),z)) = x + y + z + 2 >= x + y + z + 2 = f(.(x,.(y,z)))
      
      g(nil()) = 2 >= 1 = nil()
      
      g(.(x,nil())) = x + 3 >= x + 3 = .(g(x),nil())
      
      g(.(x,.(y,z))) = x + y + z + 3 >= x + y + z + 3 = g(.(.(x,y),z))
     problem:
      DPs:
       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))
     Bounds Processor:
      bound: 0
      enrichment: match
      automaton:
       final states: {12,10,8,6,5,1}
       transitions:
        g0(2) -> 11*
        g0(4) -> 12*
        g0(3) -> 15*
        f130() -> 2*
        g{#,0}(4) -> 1*
        .0(4,2) -> 4*
        .0(15,5) -> 12*
        .0(5,7) -> 6*
        .0(2,3) -> 9*
        .0(2,9) -> 9*
        .0(3,2) -> 4*
        .0(5,14) -> 8*
        .0(11,5) -> 10*
        .0(2,2) -> 3*
        nil0() -> 5*
        f0(2) -> 7*
        f0(9) -> 8*
        f0(3) -> 14*
        5 -> 11,7
        6 -> 8,14,7
        8 -> 14,7
        10 -> 12,15,11
        12 -> 15,11
      problem:
       DPs:
        
       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))
      Qed