diff --git a/ChangeLog b/ChangeLog
index b0744d86f..cedc70695 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,19 @@
+2010-04-15  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	More simplifications rules for M.
+
+	* src/ltlvisit/reduce.cc (reduce_visitor): Add the following
+	implication rewriting rules:
+	a M (b M c) = a M c if a implies b.
+	a M (b R c) = a M c if a implies b.
+	a R (b R c) = a R c if a implies b.
+	a R (b M c) = b M c if b implies a.
+	a M (b M c) = b M c if b implies a.
+	The latter rule was fixed from an incorrectly copied&pasted
+	rule for a M (b R c) = b R c if b implies a (this is wrong).
+	Also remove the wrong rule for a W (b U c) = b U c if a implies b.
+	* src/ltltest/reduccmp.test: Add more tests.
+
 2010-04-15  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Speed up syntactic_implication() for constants.
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 62a5374e2..bf2bc072d 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -143,6 +143,16 @@ for x in ../reduccmp ../reductaustr; do
      ;;
   esac
 
+  # Syntactic implication
+  run 0 $x '(a & b) R (a R c)' '(a & b)R c'
+  run 0 $x 'a R ((a & b) R c)' '(a & b)R c'
+  run 0 $x 'a R ((a & b) M c)' '(a & b)M c'
+  run 0 $x 'a M ((a & b) M c)' '(a & b)M c'
+  run 0 $x '(a & b) M (a R c)' '(a & b)M c'
+  run 0 $x '(a & b) M (a M c)' '(a & b)M c'
+  run 0 $x 'a M ((a&b) R c)' 'a M ((a&b) R c)' #not reduced.
+  run 0 $x '(a&b) W (a U c)' '(a&b) W (a U c)' #not reduced.
+
   # Eventuality and universality class reduction
   run 0 $x 'FFa' 'Fa'
   run 0 $x 'FGFa' 'GFa'
diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc
index 12bb69afa..af7ca3505 100644
--- a/src/ltlvisit/reduce.cc
+++ b/src/ltlvisit/reduce.cc
@@ -201,9 +201,10 @@ namespace spot
 		      return;
 		    }
 		  /* b < a => a R (b R c) = b R c */
+		  /* b < a => a R (b M c) = b M c */
 		  {
 		    binop* bo = dynamic_cast<binop*>(f2);
-		    if (bo && bo->op() == binop::R
+		    if (bo && (bo->op() == binop::R || bo->op() == binop::M)
 			&& syntactic_implication(bo->first(), f1))
 		      {
 			result_ = f2;
@@ -211,6 +212,18 @@ namespace spot
 			return;
 		      }
 		  }
+		  /* a < b => a R (b R c) = a R c */
+		  {
+		    binop* bo = dynamic_cast<binop*>(f2);
+		    if (bo && bo->op() == binop::R
+			&& syntactic_implication(f1, bo->first()))
+		      {
+			result_ = binop::instance(binop::R, f1,
+						  bo->second()->clone());
+			f2->destroy();
+			return;
+		      }
+		  }
 		  break;
 
 		case binop::W:
@@ -229,11 +242,10 @@ namespace spot
 		      f2->destroy();
 		      return;
 		    }
-		  /* a < b => a W (b U c) = (b U c) */
 		  /* a < b => a W (b W c) = (b W c) */
 		  {
 		    binop* bo = dynamic_cast<binop*>(f2);
-		    if (bo && (bo->op() == binop::U || bo->op() == binop::W)
+		    if (bo && bo->op() == binop::W
 			&& syntactic_implication(f1, bo->first()))
 		      {
 			result_ = f2;
@@ -259,10 +271,10 @@ namespace spot
 		      f2->destroy();
 		      return;
 		    }
-		  /* b < a => a R (b R c) = b R c */
+		  /* b < a => a M (b M c) = b M c */
 		  {
 		    binop* bo = dynamic_cast<binop*>(f2);
-		    if (bo && bo->op() == binop::R
+		    if (bo && bo->op() == binop::M
 			&& syntactic_implication(bo->first(), f1))
 		      {
 			result_ = f2;
@@ -270,6 +282,19 @@ namespace spot
 			return;
 		      }
 		  }
+		  /* a < b => a M (b M c) = a M c */
+		  /* a < b => a M (b R c) = a M c */
+		  {
+		    binop* bo = dynamic_cast<binop*>(f2);
+		    if (bo && (bo->op() == binop::M || bo->op() == binop::R)
+			&& syntactic_implication(f1, bo->first()))
+		      {
+			result_ = binop::instance(binop::M, f1,
+						  bo->second()->clone());
+			f2->destroy();
+			return;
+		      }
+		  }
 		  break;
 		}
 	    }