YES
Time: 0.022263
TRS:
 {     f(true(), x, y, z) -> del .(y, z),
      f(false(), x, y, z) -> .(x, del .(y, z)),
  =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())),
        =(.(x, y), nil()) -> false(),
        =(nil(), .(y, z)) -> false(),
          =(nil(), nil()) -> true(),
        del .(x, .(y, z)) -> f(=(x, y), x, y, z)}
 DP:
  DP:
   {     f#(true(), x, y, z) -> del# .(y, z),
        f#(false(), x, y, z) -> del# .(y, z),
    =#(.(x, y), .(u(), v())) -> =#(x, u()),
    =#(.(x, y), .(u(), v())) -> =#(y, v()),
          del# .(x, .(y, z)) -> f#(=(x, y), x, y, z),
          del# .(x, .(y, z)) -> =#(x, y)}
  TRS:
  {     f(true(), x, y, z) -> del .(y, z),
       f(false(), x, y, z) -> .(x, del .(y, z)),
   =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())),
         =(.(x, y), nil()) -> false(),
         =(nil(), .(y, z)) -> false(),
           =(nil(), nil()) -> true(),
         del .(x, .(y, z)) -> f(=(x, y), x, y, z)}
  EDG:
   {(del# .(x, .(y, z)) -> =#(x, y), =#(.(x, y), .(u(), v())) -> =#(y, v()))
    (del# .(x, .(y, z)) -> =#(x, y), =#(.(x, y), .(u(), v())) -> =#(x, u()))
    (f#(false(), x, y, z) -> del# .(y, z), del# .(x, .(y, z)) -> =#(x, y))
    (f#(false(), x, y, z) -> del# .(y, z), del# .(x, .(y, z)) -> f#(=(x, y), x, y, z))
    (f#(true(), x, y, z) -> del# .(y, z), del# .(x, .(y, z)) -> f#(=(x, y), x, y, z))
    (f#(true(), x, y, z) -> del# .(y, z), del# .(x, .(y, z)) -> =#(x, y))
    (del# .(x, .(y, z)) -> f#(=(x, y), x, y, z), f#(true(), x, y, z) -> del# .(y, z))
    (del# .(x, .(y, z)) -> f#(=(x, y), x, y, z), f#(false(), x, y, z) -> del# .(y, z))}
   SCCS (1):
    Scc:
     { f#(true(), x, y, z) -> del# .(y, z),
      f#(false(), x, y, z) -> del# .(y, z),
        del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)}
    SCC (3):
     Strict:
      { f#(true(), x, y, z) -> del# .(y, z),
       f#(false(), x, y, z) -> del# .(y, z),
         del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)}
     Weak:
     {     f(true(), x, y, z) -> del .(y, z),
          f(false(), x, y, z) -> .(x, del .(y, z)),
      =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())),
            =(.(x, y), nil()) -> false(),
            =(nil(), .(y, z)) -> false(),
              =(nil(), nil()) -> true(),
            del .(x, .(y, z)) -> f(=(x, y), x, y, z)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [f](x0, x1, x2, x3) = 0,
       
       [=](x0, x1) = x0,
       
       [.](x0, x1) = x0 + x1,
       
       [and](x0, x1) = x0 + x1,
       
       [del](x0) = 0,
       
       [true] = 1,
       
       [false] = 0,
       
       [nil] = 1,
       
       [u] = 1,
       
       [v] = 1,
       
       [f#](x0, x1, x2, x3) = x0 + x1 + x2,
       
       [del#](x0) = x0
      Strict:
       del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)
       0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
       f#(false(), x, y, z) -> del# .(y, z)
       0 + 0x + 1y + 1z >= 0 + 1y + 1z
       f#(true(), x, y, z) -> del# .(y, z)
       1 + 0x + 1y + 1z >= 0 + 1y + 1z
      Weak:
       
     EDG:
      {(f#(false(), x, y, z) -> del# .(y, z), del# .(x, .(y, z)) -> f#(=(x, y), x, y, z))
       (del# .(x, .(y, z)) -> f#(=(x, y), x, y, z), f#(false(), x, y, z) -> del# .(y, z))}
      SCCS (1):
       Scc:
        {f#(false(), x, y, z) -> del# .(y, z),
           del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)}
       SCC (2):
        Strict:
         {f#(false(), x, y, z) -> del# .(y, z),
            del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)}
        Weak:
        {     f(true(), x, y, z) -> del .(y, z),
             f(false(), x, y, z) -> .(x, del .(y, z)),
         =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())),
               =(.(x, y), nil()) -> false(),
               =(nil(), .(y, z)) -> false(),
                 =(nil(), nil()) -> true(),
               del .(x, .(y, z)) -> f(=(x, y), x, y, z)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [f](x0, x1, x2, x3) = 0,
          
          [=](x0, x1) = 0,
          
          [.](x0, x1) = x0 + 1,
          
          [and](x0, x1) = 0,
          
          [del](x0) = x0 + 1,
          
          [true] = 0,
          
          [false] = 0,
          
          [nil] = 0,
          
          [u] = 0,
          
          [v] = 1,
          
          [f#](x0, x1, x2, x3) = x0 + 1,
          
          [del#](x0) = x0
         Strict:
          del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)
          2 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z
          f#(false(), x, y, z) -> del# .(y, z)
          1 + 0x + 0y + 1z >= 1 + 0y + 1z
         Weak:
          
        EDG:
         {}
         SCCS (0):
          
          Qed