X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter6.ma;h=1a8b65aa35885a4ce7bfac32c1c9b9ca652f8a6d;hb=a2ba04cd90e76937720b16e37cb12a39b46181e3;hp=21e6e75aa935862bb4be22dceed0dab8a13ed066;hpb=7956b9a84e0556d2d24fffedbbbabcd9e248d702;p=helm.git

diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma
index 21e6e75aa..1a8b65aa3 100644
--- a/weblib/tutorial/chapter6.ma
+++ b/weblib/tutorial/chapter6.ma
@@ -5,7 +5,7 @@ defined in Chapter 4 to formal languages. A formal language is an arbitrary set
 of words over a given alphabet, that we shall represent as a predicate over words. 
 A word (or string) over an alphabet S is just a list of elements of S. *) 
 
-definition word ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S.
+definition word ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"/span S.
 
 (* For any alphabet there is only one word of length 0, the iempty word/i, which is 
 denoted by ϵ .*) 
@@ -27,7 +27,7 @@ A · B of two languages A and B, the so called Kleene's star A* of A and the
 derivative of a language A w.r.t. a given character a. *)
 
 definition cat : ∀S,l1,l2,w.Prop ≝ 
-  λS.λl1,l2.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/aw1,w2.w1 a title="append" href="cic:/fakeuri.def(1)"@/a w2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a l1 w1 a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 w2.
+  λS.λl1,l2.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/aspan class="error" title="Parse error: [sym_] or [ident] expected after [sym∃] (in [term])"/spanw1,w2.w1 a title="append" href="cic:/fakeuri.def(1)"@/a w2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a l1 w1 a title="logical and" href="cic:/fakeuri.def(1)"∧/aspan class="error" title="Parse error: [term] expected after [sym∧] (in [term])"/span l2 w2.
 
 notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
 interpretation "cat lang" 'middot a b = (cat ? a b).
@@ -40,7 +40,7 @@ match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons
 (* Given a list of words l and a language r, (conjunct l r) is true if and only if
 all words in l are in r, that is for every w in l, r w holds. *)
 
-let rec conjunct (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop) on l: Prop ≝
+let rec conjunct (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: RPAREN expected after [term] (in [arg])"/span (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop) on l: Prop ≝
 match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons w tl ⇒ r w a title="logical and" href="cic:/fakeuri.def(1)"∧/a conjunct ? tl r ]. 
 
 (* Given a language l, the kleene's star of l, denoted by l*, is the set of 
@@ -58,7 +58,7 @@ sets. The operation of concatenation behaves well with respect to this equality.
 lemma cat_ext_l: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. 
   A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="cat lang" href="cic:/fakeuri.def(1)"·/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="cat lang" href="cic:/fakeuri.def(1)"·/a B.
 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
-cases (H w1) /span class="autotactic"6span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ 
+cases (H w1) /span class="autotactic"6span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
 qed.
 
 lemma cat_ext_r: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop.