commit by user andrea

[helm.git] / weblib / tutorial / chapter9.ma

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index c7585df80f775b72be82981149eee8493761515e..a5dfd1c981f218b3a91d6da067d5ffcc638145d4 100644 (file)
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -1,5 +1,7 @@
-include "re.ma".
-include "basics/listb.ma".
+(* 
+\ 5h1\ 6Moves\ 5/h1\ 6*)
+
+include "chapter8.ma".
 
 let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
  match E with
@@ -23,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. 
@@ -157,5 +178,4 @@ lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
     |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/ 
     ]
   ]
-qed.
-
+qed.
\ No newline at end of file