diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 5f562ed2f..c36647259 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1326,14 +1326,15 @@ verified, there is no need to worry about the $\G\F g$ term.
 Here are the basic rewriting rules for binary operators (excluding $\OR$ and
 $\AND$ which are considered in Spot as $n$-ary operators):
 \begin{align*}
-  \1 \U f &\equiv \F f             & f \W \0 &\equiv \G f \\
-  f \M \1 &\equiv \F f             & \0 \R f &\equiv \G f \\
-  (\X f)\U (\X g) &\equiv \X(f\U g) & (\X f)\W(\X g) &\equiv \X(f\W g) \\
-  (\X f)\M (\X g) &\equiv \X(f\M g) & (\X f)\R(\X g) &\equiv \X(f\R g) \\
-  f \U(\G f) &\equiv \G f          & f \W(\G f) &\equiv \G f \\
-  f \M(\F f) &\equiv \F f          & f \R(\F f) &\equiv \F f \\
-  f \U (g \OR \G(f)) &\equiv f\W g & f \W (g \OR \G(f)) &\equiv f\W g\\
-  f \M (g \AND \F(f)) &\equiv f\M g & f \R (g \AND \F(f)) &\equiv f\M g
+  \1 \U f             & \equiv \F f      & f \W \0             & \equiv \G f      \\
+  f \M \1             & \equiv \F f      & \0 \R f             & \equiv \G f      \\
+  (\X f)\U (\X g)     & \equiv \X(f\U g) & (\X f)\W(\X g)      & \equiv \X(f\W g) \\
+  (\X f)\M (\X g)     & \equiv \X(f\M g) & (\X f)\R(\X g)      & \equiv \X(f\R g) \\
+  f \U(\G f)          & \equiv \G f      & f \W(\G f)          & \equiv \G f      \\
+  f \M(\F f)          & \equiv \F f      & f \R(\F f)          & \equiv \F f      \\
+  f \U (g \OR \G(f))  & \equiv f\W g     & f \W (g \OR \G(f))  & \equiv f\W g     \\
+  f \M (g \AND \F(f)) & \equiv f\M g     & f \R (g \AND \F(f)) & \equiv f\M g     \\
+  f \U (g \AND f)     & \equiv g\M f     & f \W (g \AND f)     & \equiv g\R f
 \end{align*}
 
 Here are the basic rewriting rules for $n$-ary operators ($\AND$ and
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 66eb7578a..33fb36967 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -1,5 +1,5 @@
-// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
-// l'Epita (LRDE).
+// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -1509,10 +1509,15 @@ namespace spot
 
 		    // a U (b | c | G(a)) = a W (b | c)
 		    // a W (b | c | G(a)) = a W (b | c)
+		    // a U (a & b & c) = (b & c) M a
+		    // a W (a & b & c) = (b & c) R a
 		    if (b->kind() == formula::MultOp)
 		      {
 			multop* fm2 = static_cast<multop*>(b);
-			if (fm2->op() == multop::Or)
+			multop::type bt = fm2->op();
+			// a U (b | c | G(a)) = a W (b | c)
+			// a W (b | c | G(a)) = a W (b | c)
+			if (bt == multop::Or)
 			  {
 			    int s = fm2->size();
 			    for (int i = 0; i < s; ++i)
@@ -1538,6 +1543,30 @@ namespace spot
 				  }
 			      }
 			  }
+			// a U (b & a & c) == (b & c) M a
+			// a W (b & a & c) == (b & c) R a
+			if (bt == multop::And)
+			  {
+			    int s = fm2->size();
+			    for (int i = 0; i < s; ++i)
+			      {
+				if (fm2->nth(i) != a)
+				  continue;
+				multop::vec* v = new multop::vec;
+				v->reserve(s - 1);
+				int j;
+				for (j = 0; j < i; ++j)
+				  v->push_back(fm2->nth(j)->clone());
+				// skip j=i
+				for (++j; j < s; ++j)
+				  v->push_back(fm2->nth(j)->clone());
+				b->destroy();
+				result_ = recurse_destroy(binop::instance
+				  (op == binop::U ? binop::M : binop::R,
+				   multop::instance(multop::And, v), a));
+				return;
+			      }
+			  }
 		      }
 		  }
 		else if (op == binop::M || op == binop::R)