commit by user andrea

[helm.git] / matita / matita / lib / re / moves.ma

diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma
index f4da274a6beecbf4b9feeda9d6172ebbde65d330..6e4dbb974cc1f24cde622bb13848e38bf945b18d 100644 (file)
--- a/matita/matita/lib/re/moves.ma
+++ b/matita/matita/lib/re/moves.ma
@@ -497,8 +497,11 @@ definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
 example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
 normalize // qed.
 
+definition exp10 ≝ a·a·a·a·a·a·a·a·a·a·a·a·(a^* ).
+definition exp11 ≝ (a·a·a·a·a + a·a·a·a·a·a·a)^*.
 
-
+example ex2 : \fst (equiv ? (exp10+exp11) exp10) = true.
+normalize // qed.