YES
TRS:
 {     implies(x, or(y, z)) -> or(y, implies(x, z)),
         implies(not(x), y) -> or(x, y),
  implies(not(x), or(y, z)) -> implies(y, or(x, z))}
 RUF:
  Strict:
   {implies(x, or(y, z)) -> or(y, implies(x, z))}
  Weak:
   {}
  DP:
   Strict:
    {implies#(x, or(y, z)) -> implies#(x, z)}
   Weak:
   {implies(x, or(y, z)) -> or(y, implies(x, z))}
   EDG:
    {(implies#(x, or(y, z)) -> implies#(x, z), implies#(x, or(y, z)) -> implies#(x, z))}
    SCCS:
     Scc:
      {implies#(x, or(y, z)) -> implies#(x, z)}
     SCC:
      Strict:
       {implies#(x, or(y, z)) -> implies#(x, z)}
      Weak:
      {implies(x, or(y, z)) -> or(y, implies(x, z))}
      SPSC:
       Simple Projection:
        pi(implies#) = 1
       Strict:
        {}
       Qed