From 2c8ab06343516b70b4900a95366fd011eee9d09d Mon Sep 17 00:00:00 2001 From: matitaweb Date: Thu, 8 Mar 2012 07:43:40 +0000 Subject: [PATCH] commit by user utente2 --- weblib/tutorial/chapter10.ma | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 -- 2.39.2