YES
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:
  Strict:
   {     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)}
  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)}
  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:
    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:
     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:
      Argument Filtering:
       pi(v) = [], pi(u) = [], pi(and) = [], pi(nil) = [], pi(false) = [], pi(true) = [], pi(.) = [1], pi(del#) = 0, pi(del) = [], pi(=) = [], pi(f#) = [3], pi(f) = []
      Usable Rules:
       {}
      Interpretation:
       [f#](x0) = x0 + 1,
       [.](x0) = x0 + 1
      Strict:
       { f#(true(), x, y, z) -> del#(.(y, z)),
        f#(false(), x, y, z) -> del#(.(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)}
      EDG:
       {}
       SCCS:
        
        Qed