From 83db53a5a8d43bcbb06a088666b4c8b38d0aad6a Mon Sep 17 00:00:00 2001
From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Mar 2012 12:09:27 +0000
Subject: [PATCH] commit by user andrea

---
 weblib/tutorial/chapter9.ma | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index 05f5e0152..a5dfd1c98 100644
--- 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. 
-- 
2.39.2