From: matitaweb Date: Thu, 8 Mar 2012 10:02:01 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1868 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=913bed2d206d20e9aa1b34fa52a97c9a6a73d896;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter10.ma b/weblib/tutorial/chapter10.ma index a5595ac50..95e3a55c1 100644 --- a/weblib/tutorial/chapter10.ma +++ b/weblib/tutorial/chapter10.ma @@ -258,14 +258,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)"@/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 … Hspan class="error" title="error location"/span) |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 ?)