X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=weblib%2Ftutorial%2Fchapter10.ma;h=15961e5367ff674cf433e224f7f882eaa4b721fd;hb=4b8544042a6f3c5f5d303d4120c69abbc34ce15b;hp=95e3a55c121f51e6d4e870933c552901846fd0a8;hpb=913bed2d206d20e9aa1b34fa52a97c9a6a73d896;p=helm.git diff --git a/weblib/tutorial/chapter10.ma b/weblib/tutorial/chapter10.ma index 95e3a55c1..15961e536 100644 --- a/weblib/tutorial/chapter10.ma +++ b/weblib/tutorial/chapter10.ma @@ -3,19 +3,18 @@ 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). +img class="anchor" src="icons/tick.png" id="cofinal"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). (* As a corollary of decidable_sem, we have that two expressions e1 and e2 are equivalent iff for any word w the states reachable through w are cofinal. *) -theorem equiv_sem: âS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.â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)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2} a title="iff" href="cic:/fakeuri.def(1)"â/a â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ã. +img class="anchor" src="icons/tick.png" id="equiv_sem"theorem equiv_sem: âS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.â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{e1a title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2a title="in_prl" href="cic:/fakeuri.def(1)"}/a a title="iff" href="cic:/fakeuri.def(1)"â/a â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 e2a title="Pair construction" href="cic:/fakeuri.def(1)"ã/a. #S #e1 #e2 % [#same_sem #w cut (âb1,b2. a href="cic:/matita/basics/logic/iff.def(1)"iff/a (b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) (b2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) â (b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b2)) @@ -30,12 +29,12 @@ length of w; moreover, so far, we made no assumption over the cardinality of S. Instead of requiring S to be finite, we may restrict the analysis to characters occurring in the given pres. *) -definition occ â λS.λe1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. - a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1|)) (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|)). +img class="anchor" src="icons/tick.png" id="occ"definition occ â λS.λe1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1a title="forget" href="cic:/fakeuri.def(1)"|/a)) (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2a title="forget" href="cic:/fakeuri.def(1)"|/a)). -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ã. +img class="anchor" src="icons/tick.png" id="occ_enough"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 e2a title="Pair construction" href="cic:/fakeuri.def(1)"ã/a) + ââ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 e2a title="Pair construction" href="cic:/fakeuri.def(1)"ã/a. #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 //] @@ -46,9 +45,9 @@ qed. (* The following is a stronger version of equiv_sem, relative to characters occurring the given regular expressions. *) -lemma equiv_sem_occ: â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ã) -â 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}. +img class="anchor" src="icons/tick.png" id="equiv_sem_occ"lemma equiv_sem_occ: â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 e2a title="Pair construction" href="cic:/fakeuri.def(1)"ã/a) +â a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1a title="in_prl" href="cic:/fakeuri.def(1)"}/aa title="extensional equality" href="cic:/fakeuri.def(1)"=/a1a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2a title="in_prl" href="cic:/fakeuri.def(1)"}/a. #S #e1 #e2 #H @(a href="cic:/matita/basics/logic/proj2.def(2)"proj2/a ⦠(a href="cic:/matita/tutorial/chapter10/equiv_sem.def(16)"equiv_sem/a â¦)) @a href="cic:/matita/tutorial/chapter10/occ_enough.def(11)"occ_enough/a #w @H qed. @@ -59,10 +58,10 @@ We say that a list of pairs of pres is a bisimulation if it is closed w.r.t. moves, and all its members are cofinal. *) -definition sons â λ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 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 href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (λa.a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p)),a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p))ã) l. +img class="anchor" src="icons/tick.png" id="sons"definition sons â λ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 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 href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (λa.a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p)),a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p))a title="Pair construction" href="cic:/fakeuri.def(1)"ã/a) l. -lemma memb_sons: âS,l.âp,q:(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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? p (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a ? l q) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a â +img class="anchor" src="icons/tick.png" id="memb_sons"lemma memb_sons: âS,l.âp,q:(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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? p (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a ? l q) 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)"â/aa.(a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a q)) 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/move.fix(0,2,6)"move/a ? a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a q)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p). #S #l elim l [#p #q normalize in ⢠(%â?); #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/] @@ -70,15 +69,15 @@ lemma memb_sons: âS,l.âp,q:(a href="cic:/matita/tutorial/chapter7/pre.def(1 [#H @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ⦠a) >(\P H) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ |#H @Hind @H] qed. -definition is_bisim â λ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 ?.λalpha:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S. +img class="anchor" src="icons/tick.png" id="is_bisim"definition is_bisim â λ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 ?.λalpha:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a 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 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 href="cic:/matita/tutorial/chapter10/cofinal.def(2)"cofinal/a ? p a title="logical and" href="cic:/fakeuri.def(1)"â§/a (a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a ? (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a ? alpha p) l). (* 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}. +img class="anchor" src="icons/tick.png" id="bisim_to_sem"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,e2a title="Pair construction" href="cic:/fakeuri.def(1)"ã/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="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1a title="in_prl" href="cic:/fakeuri.def(1)"}/aa title="extensional equality" href="cic:/fakeuri.def(1)"=/a1a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2a title="in_prl" href="cic:/fakeuri.def(1)"}/a. #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 e2a title="Pair construction" href="cic:/fakeuri.def(1)"ã/a ?)) 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 // @@ -112,17 +111,17 @@ so we have just to check cofinality for any node we add to visited. Here is the extremely simple algorithm: *) -let rec bisim S l n (frontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?) on n â +img class="anchor" src="icons/tick.png" id="bisim"let rec bisim S l n (frontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?) on n â match n with - [ O â a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visitedã (* assert false *) + [ O â a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visiteda title="Pair construction" href="cic:/fakeuri.def(1)"ã/a (* assert false *) | S m â match frontier with - [ nil â a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visitedã + [ nil â a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visiteda title="Pair construction" href="cic:/fakeuri.def(1)"ã/a | cons hd tl â if a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a hd)) (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a hd)) then - bisim S l m (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? (λx.a href="cic:/matita/basics/bool/notb.def(1)"notb/a (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? x (hda title="cons" href="cic:/fakeuri.def(1)":/a:visited))) - (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a S l hd)) tl) (hda title="cons" href="cic:/fakeuri.def(1)":/a:visited) - else a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visitedã + bisim S l m (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? (λx.a href="cic:/matita/basics/bool/notb.def(1)"notb/a (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? x (hda title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/avisited))) + (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a S l hd)) tl) (hda title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/avisited) + else a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visiteda title="Pair construction" href="cic:/fakeuri.def(1)"ã/a ] ]. @@ -134,43 +133,43 @@ if and only if all visited nodes are cofinal. The following results explicitly state the behaviour of bisim is the general case and in some relevant instances *) -lemma unfold_bisim: âS,l,n.âfrontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. +img class="anchor" src="icons/tick.png" id="unfold_bisim"lemma unfold_bisim: âS,l,n.âfrontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l n frontier visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a match n with - [ O â a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visitedã (* assert false *) + [ O â a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visiteda title="Pair construction" href="cic:/fakeuri.def(1)"ã/a (* assert false *) | S m â match frontier with - [ nil â a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visitedã + [ nil â a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visiteda title="Pair construction" href="cic:/fakeuri.def(1)"ã/a | cons hd tl â if a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a hd)) (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a hd)) then - a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l m (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? (λx.a href="cic:/matita/basics/bool/notb.def(1)"notb/a(a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? x (hda title="cons" href="cic:/fakeuri.def(1)":/a:visited))) - (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a S l hd)) tl) (hda title="cons" href="cic:/fakeuri.def(1)":/a:visited) - else a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visitedã + a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l m (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? (λx.a href="cic:/matita/basics/bool/notb.def(1)"notb/a(a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? x (hda title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/avisited))) + (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a S l hd)) tl) (hda title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/avisited) + else a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visiteda title="Pair construction" href="cic:/fakeuri.def(1)"ã/a ] ]. #S #l #n cases n // qed. -lemma bisim_never: âS,l.âfrontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. - a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a frontier visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visitedã. +img class="anchor" src="icons/tick.png" id="bisim_never"lemma bisim_never: âS,l.âfrontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. + a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a frontier visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visiteda title="Pair construction" href="cic:/fakeuri.def(1)"ã/a. #frontier #visited >a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"unfold_bisim/a // qed. -lemma bisim_end: âSig,l,m.âvisited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. - a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="nil" href="cic:/fakeuri.def(1)"[/a] visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visitedã. +img class="anchor" src="icons/tick.png" id="bisim_end"lemma bisim_end: âSig,l,m.âvisited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. + a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a,visiteda title="Pair construction" href="cic:/fakeuri.def(1)"ã/a. #n #visisted >a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"unfold_bisim/a // qed. -lemma bisim_step_true: âSig,l,m.âp.âfrontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. +img class="anchor" src="icons/tick.png" id="bisim_step_true"lemma bisim_step_true: âSig,l,m.âp.âfrontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a (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="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p)) 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/chapter10/bisim.fix(0,2,8)"bisim/a Sig l (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) (pa title="cons" href="cic:/fakeuri.def(1)":/a:frontier) visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a - a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l m (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? (λx.a href="cic:/matita/basics/bool/notb.def(1)"notb/a(a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? x (pa title="cons" href="cic:/fakeuri.def(1)":/a:visited))) - (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a Sig l p)) frontier) (pa title="cons" href="cic:/fakeuri.def(1)":/a:visited). + a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) (pa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/afrontier) visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a + a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l m (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a ? (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? (λx.a href="cic:/matita/basics/bool/notb.def(1)"notb/a(a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a ? x (pa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/avisited))) + (a href="cic:/matita/tutorial/chapter10/sons.def(7)"sons/a Sig l p)) frontier) (pa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/avisited). #Sig #l #m #p #frontier #visited #test >a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"unfold_bisim/a whd in ⢠(??%?); >test // qed. -lemma bisim_step_false: âSig,l,m.âp.âfrontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. +img class="anchor" src="icons/tick.png" id="bisim_step_false"lemma bisim_step_false: âSig,l,m.âp.âfrontier,visited: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a ?. a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a (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="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/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 â - a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) (pa title="cons" href="cic:/fakeuri.def(1)":/a:frontier) visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visitedã. + a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a Sig l (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) (pa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/afrontier) visited a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"ã/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,visiteda title="Pair construction" href="cic:/fakeuri.def(1)"ã/a. #Sig #l #m #p #frontier #visited #test >a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"unfold_bisim/a whd in ⢠(??%?); >test // qed. @@ -181,18 +180,18 @@ enumerate all possible pres: *) #b cases b normalize // qed. *) -let rec pitem_enum S (i:a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on i â +img class="anchor" src="icons/tick.png" id="pitem_enum"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] - | 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] + [ 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)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa 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)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa 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)":/aa 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)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa 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) | c i1 i2 â a href="cic:/matita/basics/list/compose.def(2)"compose/a ??? (a href="cic:/matita/tutorial/chapter7/pitem.con(0,5,1)"pc/a S) (pitem_enum S i1) (pitem_enum S i2) | k i â a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (a href="cic:/matita/tutorial/chapter7/pitem.con(0,7,1)"pk/a S) (pitem_enum S i) ]. -lemma pitem_enum_complete : âS.âi:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. - a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a (a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"DeqItem/a S) i (a href="cic:/matita/tutorial/chapter10/pitem_enum.fix(0,1,3)"pitem_enum/a S (a title="forget" href="cic:/fakeuri.def(1)"|/ai|)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. +img class="anchor" src="icons/tick.png" id="pitem_enum_complete"lemma pitem_enum_complete : âS.âi:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a (a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"DeqItem/a S) i (a href="cic:/matita/tutorial/chapter10/pitem_enum.fix(0,1,3)"pitem_enum/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/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. #S #i elim i [1,2:// |3,4:#c normalize >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ⦠c)) // @@ -201,47 +200,47 @@ 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 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]). +img class="anchor" src="icons/tick.png" id="pre_enum"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,ba title="Pair construction" href="cic:/fakeuri.def(1)"ã/a) (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)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa 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. -#S * #i #b @(a href="cic:/matita/tutorial/chapter5/memb_compose.def(6)"memb_compose/a (a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"DeqItem/a S) a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"DeqBool/a ? (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"ã/ai,bã)) +img class="anchor" src="icons/tick.png" id="pre_enum_complete"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 ea title="forget" href="cic:/fakeuri.def(1)"|/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. +#S * #i #b @(a href="cic:/matita/tutorial/chapter5/memb_compose.def(6)"memb_compose/a (a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"DeqItem/a S) a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"DeqBool/a ? (λi,b.a title="Pair construction" href="cic:/fakeuri.def(1)"ã/ai,ba title="Pair construction" href="cic:/fakeuri.def(1)"ã/a)) // 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). +img class="anchor" src="icons/tick.png" id="space_enum"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,e2a title="Pair construction" href="cic:/fakeuri.def(1)"ã/a) (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. -#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ã)) +img class="anchor" src="icons/tick.png" id="space_enum_complete"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,e2a title="Pair construction" href="cic:/fakeuri.def(1)"ã/a (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 e1a title="forget" href="cic:/fakeuri.def(1)"|/a) (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2a title="forget" href="cic:/fakeuri.def(1)"|/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. +#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,ba title="Pair construction" href="cic:/fakeuri.def(1)"ã/a)) // 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 ?. +img class="anchor" src="icons/tick.png" id="all_reachable"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). -definition disjoint â λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λl1,l2. +img class="anchor" src="icons/tick.png" id="disjoint"definition disjoint â λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λl1,l2. âp:S. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S p l1 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 S p l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. (* 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} â +img class="anchor" src="icons/tick.png" id="bisim_correct"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{e1a title="in_prl" href="cic:/fakeuri.def(1)"}/aa title="extensional equality" href="cic:/fakeuri.def(1)"=/a1a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2a title="in_prl" href="cic:/fakeuri.def(1)"}/a â â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)). - a title="norm" href="cic:/fakeuri.def(1)"|/aa 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="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a title="norm" href="cic:/fakeuri.def(1)"|/avisited|â + a title="norm" href="cic:/fakeuri.def(1)"|/aa 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 e1a title="forget" href="cic:/fakeuri.def(1)"|/a) (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2a title="forget" href="cic:/fakeuri.def(1)"|/a)a title="norm" href="cic:/fakeuri.def(1)"|/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a title="norm" href="cic:/fakeuri.def(1)"|/avisiteda title="norm" href="cic:/fakeuri.def(1)"|/aâ a href="cic:/matita/tutorial/chapter10/all_reachable.def(8)"all_reachable/a S e1 e2 visited â a href="cic:/matita/tutorial/chapter10/all_reachable.def(8)"all_reachable/a S e1 e2 frontier â a href="cic:/matita/tutorial/chapter10/disjoint.def(5)"disjoint/a ? frontier visited â a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"bisim/a S l n frontier visited) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #Sig #e1 #e2 #same #l #n elim n [#frontier #visited #abs * #unique #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ⦠abs) - @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a @a href="cic:/matita/tutorial/chapter5/sublist_length.def(9)"sublist_length/a // * #e11 #e21 #membp - cut ((a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e11| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1|) a title="logical and" href="cic:/fakeuri.def(1)"â§/a (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e21| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|)) + @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a @a href="cic:/matita/tutorial/chapter5/sublist_length.def(6)"sublist_length/a // * #e11 #e21 #membp + cut ((|a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e11a title="forget" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e1a title="forget" href="cic:/fakeuri.def(1)"|/a) a title="logical and" href="cic:/fakeuri.def(1)"â§/a (|a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e21a title="forget" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2a title="forget" href="cic:/fakeuri.def(1)"|/a)) [|* #H1 #H2