X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter10.ma;h=8fe459cd2ef9f99f4a8d9183a879be3112ef9401;hb=ceb81586cd493164f9c980c4f97ed0b4dbc6f545;hp=24efb3e983e9f6986be23ed8055d09df08388b51;hpb=1e15bf5aab8c4d4bdefc1bca9084459a0442a847;p=helm.git

diff --git a/weblib/tutorial/chapter10.ma b/weblib/tutorial/chapter10.ma
index 24efb3e98..8fe459cd2 100644
--- a/weblib/tutorial/chapter10.ma
+++ b/weblib/tutorial/chapter10.ma
@@ -1,11 +1,10 @@
 (* 
-h1Equivalence/h1*)
+h1Regular Expressions Equivalence/h1*)
 
 include "tutorial/chapter9.ma".
 
-(* We say that two pres \langle i_1,b_1\rangle$ and
-$\langle i_1,b_1\rangle$ are {\em cofinal} if and only if
-$b_1 = b_2$. *)
+(* We say that two pres 〈i_1,b_1〉 and 〈i_1,b_1〉 are {\em cofinal} if and 
+only if b_1 = b_2. *)
 
 definition cofinal ≝ λS.λp:(a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S)a title="Product" href="cic:/fakeuri.def(1)"×/a(a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S). 
   a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p).
@@ -35,7 +34,7 @@ definition occ ≝ λS.λe1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)
 
 lemma occ_enough: ∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.
 (∀w.(a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S w (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2))→ a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉)
- →∀w.a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉.
+ →∀w.a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e2〉.
 #S #e1 #e2 #H #w
 cases (a href="cic:/matita/tutorial/chapter5/decidable_sublist.def(6)"decidable_sublist/a S w (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2)) [@H] -H #H
  >a href="cic:/matita/tutorial/chapter9/to_pit.def(10)"to_pit/a [2: @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H) #H1 #a #memba @a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"sublist_unique_append_l1/a @H1 //]
@@ -76,9 +75,9 @@ definition is_bisim ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,
 (* Using lemma equiv_sem_occ it is easy to prove the following result: *)
 
 lemma bisim_to_sem: ∀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 ?.∀e1,e2: a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
-  a href="cic:/matita/tutorial/chapter10/is_bisim.def(8)"is_bisim/a S l (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2) → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉 l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1}a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2}.
+  a href="cic:/matita/tutorial/chapter10/is_bisim.def(8)"is_bisim/a S l (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a S e1 e2) → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ?a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉 l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1}a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2}.
 #S #l #e1 #e2 #Hbisim #Hmemb @a href="cic:/matita/tutorial/chapter10/equiv_sem_occ.def(17)"equiv_sem_occ/a 
-#w #Hsub @(a href="cic:/matita/basics/logic/proj1.def(2)"proj1/a … (Hbisim a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e2〉 ?))
+#w #Hsub @(a href="cic:/matita/basics/logic/proj1.def(2)"proj1/a … (Hbisim a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e1,a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e2〉 ?))
 lapply Hsub @(a href="cic:/matita/basics/list/list_elim_left.def(10)"list_elim_left/a … w) [//]
 #a #w1 #Hind #Hsub >a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"moves_left/a >a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"moves_left/a @(a href="cic:/matita/basics/logic/proj2.def(2)"proj2/a …(Hbisim …(Hind ?)))
   [#x #Hx @Hsub @a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"memb_append_l1/a //
@@ -183,7 +182,7 @@ qed. *)
 
 let rec pitem_enum S (i:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on i ≝
   match i with
-  [ z ⇒ (a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/aspan class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/spanspan class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/span S)a title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]
+  [ z ⇒ (a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/a S)a title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]
   | e ⇒ (a href="cic:/matita/tutorial/chapter7/pitem.con(0,2,1)"pe/a S)a title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]
   | s y ⇒ (a href="cic:/matita/tutorial/chapter7/pitem.con(0,3,1)"ps/a S y)a title="cons" href="cic:/fakeuri.def(1)":/a:(a href="cic:/matita/tutorial/chapter7/pitem.con(0,4,1)"pp/a S y)a title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]
   | o i1 i2 ⇒ a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (a href="cic:/matita/tutorial/chapter7/pitem.con(0,6,1)"po/a S) (pitem_enum S i1) (pitem_enum S i2)
@@ -202,7 +201,7 @@ lemma pitem_enum_complete : ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pit
 qed.
 
 definition pre_enum ≝ λS.λi:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S.
-  a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,b〉) (a href="cic:/matita/tutorial/chapter10/pitem_enum.fix(0,1,3)"pitem_enum/a S i) a title="cons" href="cic:/fakeuri.def(1)"[/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a;a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a].
+  a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,b〉) ( a href="cic:/matita/tutorial/chapter10/pitem_enum.fix(0,1,3)"pitem_enum/a S i) (a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="cons" href="cic:/fakeuri.def(1)":/a:a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]).
   
 lemma pre_enum_complete : ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.
   a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? e (a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"pre_enum/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e|)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
@@ -210,15 +209,15 @@ lemma pre_enum_complete : ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.d
 // cases b normalize //
 qed.
  
-definition space_enum ≝ λS.λi1,i2:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S.
-  a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (λe1,e2.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉) (a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"pre_enum/a S i1) (a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"pre_enum/a S i2).
+definition space_enum ≝ λS.λi1,i2: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S.
+  a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (λe1,e2.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉) ( a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"pre_enum/a S i1) (a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"pre_enum/a S i2).
 
 lemma space_enum_complete : ∀S.∀e1,e2: a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.
-  a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉 (a href="cic:/matita/tutorial/chapter10/space_enum.def(5)"space_enum/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1|) (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+  a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉 ( a href="cic:/matita/tutorial/chapter10/space_enum.def(5)"space_enum/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1|) (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 #S #e1 #e2 @(a href="cic:/matita/tutorial/chapter5/memb_compose.def(6)"memb_compose/a … (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,b〉))
 // qed.
 
-definition all_reachable ≝ λS.λe1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?.
+definition all_reachable ≝ λS.λe1,e2: a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?.
 a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"uniqueb/a ? l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a 
   ∀p. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? p l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
     a title="exists" href="cic:/fakeuri.def(1)"∃/aw.(a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p) a title="logical and" href="cic:/fakeuri.def(1)"∧/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p). 
@@ -228,8 +227,8 @@ definition disjoint ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,
         
 (* We are ready to prove that bisim is correct; we use the invariant 
 that at each call of bisim the two lists visited and frontier only contain 
-nodes reachable from \langle e_1,e_2\rangle, hence it is absurd to suppose 
-to meet a pair which is not cofinal. *)
+nodes reachable from 〈e_1,e_2〉, hence it is absurd to suppose to meet a pair 
+which is not cofinal. *)
 
 lemma bisim_correct: ∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1}a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2} → 
  ∀l,n.∀frontier,visited:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ((a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S)a title="Product" href="cic:/fakeuri.def(1)"×/a(a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S)).
@@ -258,14 +257,14 @@ lemma bisim_correct: ∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.de
         |#p1 #H (cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … H)) [#eqp >(\P eqp) // |@r_visited]
         ]
      |whd % [@a href="cic:/matita/tutorial/chapter5/unique_append_unique.def(6)"unique_append_unique/a @(a href="cic:/matita/basics/bool/andb_true_r.def(4)"andb_true_r/a … u_frontier)]
-      @a href="cic:/matita/tutorial/chapter5/unique_append_elim.dec"unique_append_elim/a #q #H
+      @a href="cic:/matita/tutorial/chapter5/unique_append_elim.def(7)"unique_append_elim/a #q #H
        [cases (a href="cic:/matita/tutorial/chapter10/memb_sons.def(8)"memb_sons/a … (a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"memb_filter_memb/a … H)) -H
-        #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (w1a title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa]))
+        #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (w1a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a])))
         >a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"moves_left/a >a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"moves_left/a >mw1 >mw2 >m1 >m2 % // 
        |@r_frontier @a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"memb_cons/a //
        ]
-     |@a href="cic:/matita/tutorial/chapter5/unique_append_elim.dec"unique_append_elim/a #q #H
-       [@a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a @(a href="cic:/matita/tutorial/chapter5/filter_true.def(5)"filter_true/a … H)
+     |@a href="cic:/matita/tutorial/chapter5/unique_append_elim.def(7)"unique_append_elim/a #q #H
+       [@a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a @(a href="cic:/matita/tutorial/chapter5/memb_filter_true.def(5)"memb_filter_true/a … H)
        |cut ((qa title="eqb" href="cic:/fakeuri.def(1)"=/a=p) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) 
          [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"memb_cons/a //]
         cases (a href="cic:/matita/basics/bool/andb_true.def(5)"andb_true/a … u_frontier) #notp #_ @(\bf ?) 
@@ -274,7 +273,7 @@ lemma bisim_correct: ∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.de
      ]
    ]  
 qed.  
-   
+
 (* For completeness, we use the invariant that all the nodes in visited are cofinal, 
 and the sons of visited are either in visited or in the frontier; since
 at the end frontier is empty, visited is hence a bisimulation. *)
@@ -348,7 +347,7 @@ definition equiv ≝ λSig.λre1,re2:a href="cic:/matita/tutorial/chapter7/re.i
   let e2 ≝ a title="eclose" href="cic:/fakeuri.def(1)"•/a(a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a ? re2) in
   let n ≝ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/list/length.fix(0,1,1)"length/a ? (a href="cic:/matita/tutorial/chapter10/space_enum.def(5)"space_enum/a Sig (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1|) (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|))) in
   let sig ≝ (a href="cic:/matita/tutorial/chapter10/occ.def(7)"occ/a Sig e1 e2) in
-  (a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a ? sig n a title="cons" href="cic:/fakeuri.def(1)"[/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉] a title="nil" href="cic:/fakeuri.def(1)"[/a]).
+  (a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a ? sig n (a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ae1,e2〉a title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="nil" href="cic:/fakeuri.def(1)"[/a]).
 
 theorem euqiv_sem : ∀Sig.∀e1,e2:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a Sig.
    a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter10/equiv.def(9)"equiv/a ? e1 e2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{e1} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{e2}.
@@ -393,6 +392,4 @@ definition exp8 ≝ a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa ti
 definition exp9 ≝ (a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/a a title="re or" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/aa title="re cat" href="cic:/fakeuri.def(1)"·/aa href="cic:/matita/tutorial/chapter10/a.def(9)"a/a)a title="re star" href="cic:/fakeuri.def(1)"^/a*.
 
 example ex1 : a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter10/equiv.def(9)"equiv/a ? (a href="cic:/matita/tutorial/chapter10/exp8.def(10)"exp8/aa title="re or" href="cic:/fakeuri.def(1)"+/aa href="cic:/matita/tutorial/chapter10/exp9.def(10)"exp9/a) a href="cic:/matita/tutorial/chapter10/exp9.def(10)"exp9/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
-normalize // qed.
-
-
+normalize // qed.
\ No newline at end of file