YES
Time: 0.006644
TRS:
 {       purge nil() -> nil(),
       purge .(x, y) -> .(x, purge remove(x, y)),
    remove(x, nil()) -> nil(),
  remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(x, z)))}
 DP:
  DP:
   {     purge# .(x, y) -> purge# remove(x, y),
         purge# .(x, y) -> remove#(x, y),
    remove#(x, .(y, z)) -> remove#(x, z)}
  TRS:
  {       purge nil() -> nil(),
        purge .(x, y) -> .(x, purge remove(x, y)),
     remove(x, nil()) -> nil(),
   remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(x, z)))}
  EDG:
   {(remove#(x, .(y, z)) -> remove#(x, z), remove#(x, .(y, z)) -> remove#(x, z))
    (purge# .(x, y) -> remove#(x, y), remove#(x, .(y, z)) -> remove#(x, z))
    (purge# .(x, y) -> purge# remove(x, y), purge# .(x, y) -> purge# remove(x, y))
    (purge# .(x, y) -> purge# remove(x, y), purge# .(x, y) -> remove#(x, y))}
   SCCS (2):
    Scc:
     {remove#(x, .(y, z)) -> remove#(x, z)}
    Scc:
     {purge# .(x, y) -> purge# remove(x, y)}
    SCC (1):
     Strict:
      {remove#(x, .(y, z)) -> remove#(x, z)}
     Weak:
     {       purge nil() -> nil(),
           purge .(x, y) -> .(x, purge remove(x, y)),
        remove(x, nil()) -> nil(),
      remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(x, z)))}
     SPSC:
      Simple Projection:
       pi(remove#) = 1
      Strict:
       {}
      Qed
    SCC (1):
     Strict:
      {purge# .(x, y) -> purge# remove(x, y)}
     Weak:
     {       purge nil() -> nil(),
           purge .(x, y) -> .(x, purge remove(x, y)),
        remove(x, nil()) -> nil(),
      remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(x, z)))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2) = 0,
       
       [.](x0, x1) = 1,
       
       [remove](x0, x1) = 0,
       
       [=](x0, x1) = 0,
       
       [purge](x0) = x0 + 1,
       
       [nil] = 0,
       
       [purge#](x0) = x0 + 1
      Strict:
       purge# .(x, y) -> purge# remove(x, y)
       2 + 0x + 0y >= 1 + 0x + 0y
      Weak:
       
     Qed