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: 1
      enrichment: match-dp
      automaton:
       final states: {6}
       transitions:
        f{#,0}(8) -> 6*
        .0(3,1) -> 1*
        .0(3,3) -> 1*
        .0(4,2) -> 4,1
        .0(4,4) -> 1*
        .0(5,5) -> 7*
        .0(5,7) -> 8*
        .0(1,2) -> 1*
        .0(1,4) -> 1*
        .0(2,1) -> 1*
        .0(2,3) -> 1*
        .0(3,2) -> 1*
        .0(3,4) -> 1*
        .0(4,1) -> 1*
        .0(4,3) -> 1*
        .0(1,1) -> 1*
        .0(1,3) -> 1*
        .0(2,2) -> 2,1
        .0(2,4) -> 1*
        f0(2) -> 2*
        f0(4) -> 2*
        f0(1) -> 2*
        f0(3) -> 2*
        nil0() -> 4,2,3
        g0(2) -> 4*
        g0(4) -> 4*
        g0(1) -> 4*
        g0(3) -> 4*
        f{#,1}(12) -> 6*
        .1(2,12) -> 12*
        .1(2,14) -> 12*
        .1(3,7) -> 11*
        .1(3,11) -> 12*
        .1(4,12) -> 12*
        .1(4,14) -> 12*
        .1(1,12) -> 12*
        .1(1,14) -> 12*
        .1(2,7) -> 14*
        .1(2,11) -> 12*
        .1(3,12) -> 12*
        .1(3,14) -> 12*
        .1(4,7) -> 14*
        .1(4,11) -> 12*
        .1(1,7) -> 11*
        .1(1,11) -> 12*
        1 -> 5*
        2 -> 5*
        3 -> 5*
        4 -> 5*
      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: 1
      enrichment: match-dp
      automaton:
       final states: {6}
       transitions:
        .0(3,1) -> 1*
        .0(3,3) -> 1*
        .0(4,2) -> 4,1
        .0(4,4) -> 1*
        .0(5,5) -> 7*
        .0(1,2) -> 1*
        .0(1,4) -> 1*
        .0(2,1) -> 1*
        .0(2,3) -> 1*
        .0(7,5) -> 8*
        .0(3,2) -> 1*
        .0(3,4) -> 1*
        .0(4,1) -> 1*
        .0(4,3) -> 1*
        .0(1,1) -> 1*
        .0(1,3) -> 1*
        .0(2,2) -> 2,1
        .0(2,4) -> 1*
        f0(2) -> 2*
        f0(4) -> 2*
        f0(1) -> 2*
        f0(3) -> 2*
        nil0() -> 4,2,3
        g0(2) -> 4*
        g0(4) -> 4*
        g0(1) -> 4*
        g0(3) -> 4*
        .1(14,2) -> 12*
        .1(14,4) -> 12*
        .1(11,2) -> 12*
        .1(11,4) -> 12*
        .1(12,1) -> 12*
        .1(7,1) -> 14*
        .1(12,3) -> 12*
        .1(7,3) -> 11*
        .1(14,1) -> 12*
        .1(14,3) -> 12*
        .1(11,1) -> 12*
        .1(11,3) -> 12*
        .1(12,2) -> 12*
        .1(7,2) -> 11*
        .1(12,4) -> 12*
        .1(7,4) -> 14*
        g{#,0}(8) -> 6*
        g{#,1}(12) -> 6*
        1 -> 5*
        2 -> 5*
        3 -> 5*
        4 -> 5*
      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