YES
Time: 0.023593
TRS:
 {     rev nil() -> nil(),
     rev .(x, y) -> ++(rev y, .(x, nil())),
    ++(nil(), y) -> y,
  ++(.(x, y), z) -> .(x, ++(y, z)),
     car .(x, y) -> x,
     cdr .(x, y) -> y,
      null nil() -> true(),
    null .(x, y) -> false()}
 DP:
  DP:
   {   rev# .(x, y) -> rev# y,
       rev# .(x, y) -> ++#(rev y, .(x, nil())),
    ++#(.(x, y), z) -> ++#(y, z)}
  TRS:
  {     rev nil() -> nil(),
      rev .(x, y) -> ++(rev y, .(x, nil())),
     ++(nil(), y) -> y,
   ++(.(x, y), z) -> .(x, ++(y, z)),
      car .(x, y) -> x,
      cdr .(x, y) -> y,
       null nil() -> true(),
     null .(x, y) -> false()}
  UR:
   {     rev nil() -> nil(),
       rev .(x, y) -> ++(rev y, .(x, nil())),
      ++(nil(), y) -> y,
    ++(.(x, y), z) -> .(x, ++(y, z))}
   EDG:
    {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))
     (rev# .(x, y) -> ++#(rev y, .(x, nil())), ++#(.(x, y), z) -> ++#(y, z))
     (rev# .(x, y) -> rev# y, rev# .(x, y) -> rev# y)
     (rev# .(x, y) -> rev# y, rev# .(x, y) -> ++#(rev y, .(x, nil())))}
    STATUS:
     arrows: 0.555556
     SCCS (2):
      Scc:
       {rev# .(x, y) -> rev# y}
      Scc:
       {++#(.(x, y), z) -> ++#(y, z)}
      
      SCC (1):
       Strict:
        {rev# .(x, y) -> rev# y}
       Weak:
       {     rev nil() -> nil(),
           rev .(x, y) -> ++(rev y, .(x, nil())),
          ++(nil(), y) -> y,
        ++(.(x, y), z) -> .(x, ++(y, z)),
           car .(x, y) -> x,
           cdr .(x, y) -> y,
            null nil() -> true(),
          null .(x, y) -> false()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [++](x0, x1) = 0,
         
         [.](x0, x1) = x0 + 1,
         
         [rev](x0) = 0,
         
         [car](x0) = x0,
         
         [cdr](x0) = 0,
         
         [null](x0) = x0 + 1,
         
         [nil] = 1,
         
         [true] = 0,
         
         [false] = 0,
         
         [rev#](x0) = x0
        Strict:
         rev# .(x, y) -> rev# y
         1 + 1y + 0x >= 0 + 1y
        Weak:
         null .(x, y) -> false()
         2 + 1y + 0x >= 0
         null nil() -> true()
         2 >= 0
         cdr .(x, y) -> y
         0 + 0y + 0x >= 1y
         car .(x, y) -> x
         1 + 1y + 0x >= 1x
         ++(.(x, y), z) -> .(x, ++(y, z))
         0 + 0y + 0x + 0z >= 1 + 0y + 0x + 0z
         ++(nil(), y) -> y
         0 + 0y >= 1y
         rev .(x, y) -> ++(rev y, .(x, nil()))
         0 + 0y + 0x >= 0 + 0y + 0x
         rev nil() -> nil()
         0 >= 1
       Qed
     
     SCC (1):
      Strict:
       {++#(.(x, y), z) -> ++#(y, z)}
      Weak:
      {     rev nil() -> nil(),
          rev .(x, y) -> ++(rev y, .(x, nil())),
         ++(nil(), y) -> y,
       ++(.(x, y), z) -> .(x, ++(y, z)),
          car .(x, y) -> x,
          cdr .(x, y) -> y,
           null nil() -> true(),
         null .(x, y) -> false()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [++](x0, x1) = 0,
        
        [.](x0, x1) = x0 + 1,
        
        [rev](x0) = 0,
        
        [car](x0) = x0,
        
        [cdr](x0) = 0,
        
        [null](x0) = x0 + 1,
        
        [nil] = 1,
        
        [true] = 0,
        
        [false] = 0,
        
        [++#](x0, x1) = x0
       Strict:
        ++#(.(x, y), z) -> ++#(y, z)
        1 + 1y + 0x + 0z >= 0 + 1y + 0z
       Weak:
        null .(x, y) -> false()
        2 + 1y + 0x >= 0
        null nil() -> true()
        2 >= 0
        cdr .(x, y) -> y
        0 + 0y + 0x >= 1y
        car .(x, y) -> x
        1 + 1y + 0x >= 1x
        ++(.(x, y), z) -> .(x, ++(y, z))
        0 + 0y + 0x + 0z >= 1 + 0y + 0x + 0z
        ++(nil(), y) -> y
        0 + 0y >= 1y
        rev .(x, y) -> ++(rev y, .(x, nil()))
        0 + 0y + 0x >= 0 + 0y + 0x
        rev nil() -> nil()
        0 >= 1
      Qed