From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Thu, 8 Mar 2012 07:43:40 +0000 (+0000)
Subject: commit by user utente2
X-Git-Tag: make_still_working~1871
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2c8ab06343516b70b4900a95366fd011eee9d09d;p=helm.git

commit by user utente2
---

diff --git a/weblib/tutorial/chapter10.ma b/weblib/tutorial/chapter10.ma
index 08c78c632..a5595ac50 100644
--- a/weblib/tutorial/chapter10.ma
+++ b/weblib/tutorial/chapter10.ma
@@ -202,7 +202,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.
@@ -260,7 +260,7 @@ lemma bisim_correct: ∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.de
      |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
        [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 //
        ]
@@ -348,7 +348,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,4 +393,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