commit by user andrea

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index 05f5e0152112367275cf463493b17382a3d8c616..a5dfd1c981f218b3a91d6da067d5ffcc638145d4 100644 (file)
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -25,6 +25,25 @@ lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S.
   move S x i^* = (move ? x i)^⊛.
 // qed.
 
+(*
+Example. Let us consider the item                      
+  
+                               (•a + ϵ)((•b)*•a + •b)b
+
+and the two moves w.r.t. the characters a and b. 
+For a, we have two possible positions (all other points gets erased); the innermost 
+point stops in front of the final b, while the other one broadcast inside (b^*a + b)b, 
+so
+ 
+      move((•a + ϵ)((•b)*•a + •b)b,a) = 〈(a + ϵ)((•b)^*•a + •b)•b, false〉
+
+For b, we have two positions too. The innermost point stops in front of the final b too, 
+while the other point reaches the end of b* and must go back through b*a:  
+    
+      move((•a + ϵ)((•b)*•a + •b)b ,b) = 〈(a +  ϵ)((•b)*•a + b)•b, false〉
+
+*)
+
 definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (\fst e).
 
 lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b.