]> matita.cs.unibo.it Git - helm.git/blob - weblib/tutorial/chapter10.ma
update in basic_2 (bugfix)
[helm.git] / weblib / tutorial / chapter10.ma
1 (* 
2 \ 5h1\ 6Regular Expressions Equivalence\ 5/h1\ 6*)
3
4 include "tutorial/chapter9.ma".
5
6 (* We say that two pres 〈i_1,b_1〉 and 〈i_1,b_1〉 are {\em cofinal} if and 
7 only if b_1 = b_2. *)
8
9 \ 5img class="anchor" src="icons/tick.png" id="cofinal"\ 6definition cofinal ≝ λS.λp:(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S)\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S). 
10   \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p).
11
12 (* As a corollary of decidable_sem, we have that two expressions
13 e1 and e2 are equivalent iff for any word w the states reachable 
14 through w are cofinal. *)
15
16 \ 5img class="anchor" src="icons/tick.png" id="equiv_sem"\ 6theorem equiv_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
17   \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 ∀w.\ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"\ 6cofinal\ 5/a\ 6 ? \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e1,\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6.
18 #S #e1 #e2 % 
19 [#same_sem #w 
20   cut (∀b1,b2. \ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 (b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) (b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → (b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b2)) 
21     [* * // * #H1 #H2 [@\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @H1 //| @H2 //]]
22   #Hcut @Hcut @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter9/decidable_sem.def(15)"\ 6decidable_sem\ 5/a\ 6
23   @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 [|@same_sem] @\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter9/decidable_sem.def(15)"\ 6decidable_sem\ 5/a\ 6
24 |#H #w1 @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter9/decidable_sem.def(15)"\ 6decidable_sem\ 5/a\ 6] <H @\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter9/decidable_sem.def(15)"\ 6decidable_sem\ 5/a\ 6]
25 qed.
26
27 (* This does not directly imply decidability: we have no bound over the
28 length of w; moreover, so far, we made no assumption over the cardinality 
29 of S. Instead of requiring S to be finite, we may restrict the analysis
30 to characters occurring in the given pres. *)
31
32 \ 5img class="anchor" src="icons/tick.png" id="occ"\ 6definition occ ≝ λS.λe1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
33   \ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"\ 6occur\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e1\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) (\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"\ 6occur\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)).
34
35 \ 5img class="anchor" src="icons/tick.png" id="occ_enough"\ 6lemma occ_enough: ∀S.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
36 (∀w.(\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"\ 6occ\ 5/a\ 6 S e1 e2))→ \ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"\ 6cofinal\ 5/a\ 6 ? \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e1,\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6)
37  →∀w.\ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"\ 6cofinal\ 5/a\ 6 ? \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e1,\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6.
38 #S #e1 #e2 #H #w
39 cases (\ 5a href="cic:/matita/tutorial/chapter5/decidable_sublist.def(6)"\ 6decidable_sublist\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"\ 6occ\ 5/a\ 6 S e1 e2)) [@H] -H #H
40  >\ 5a href="cic:/matita/tutorial/chapter9/to_pit.def(10)"\ 6to_pit\ 5/a\ 6 [2: @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 #a #memba @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"\ 6sublist_unique_append_l1\ 5/a\ 6 @H1 //]
41  >\ 5a href="cic:/matita/tutorial/chapter9/to_pit.def(10)"\ 6to_pit\ 5/a\ 6 [2: @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 #a #memba  @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"\ 6sublist_unique_append_l2\ 5/a\ 6 @H1 //]
42  //
43 qed.
44
45 (* The following is a stronger version of equiv_sem, relative to characters
46 occurring the given regular expressions. *)
47
48 \ 5img class="anchor" src="icons/tick.png" id="equiv_sem_occ"\ 6lemma equiv_sem_occ: ∀S.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
49 (∀w.(\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"\ 6occ\ 5/a\ 6 S e1 e2))→ \ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"\ 6cofinal\ 5/a\ 6 ? \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e1,\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6)
50 → \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6\ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
51 #S #e1 #e2 #H @(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter10/equiv_sem.def(16)"\ 6equiv_sem\ 5/a\ 6 …)) @\ 5a href="cic:/matita/tutorial/chapter10/occ_enough.def(11)"\ 6occ_enough\ 5/a\ 6 #w @H 
52 qed.
53
54 (* 
55 \ 5h2\ 6Bisimulations\ 5/h2\ 6
56
57 We say that a list of pairs of pres is a bisimulation if it is closed
58 w.r.t. moves, and all its members are cofinal.
59 *)
60
61 \ 5img class="anchor" src="icons/tick.png" id="sons"\ 6definition sons ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λl:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S.λp:(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S)\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S). 
62  \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? (λa.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p)),\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p))\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6) l.
63
64 \ 5img class="anchor" src="icons/tick.png" id="memb_sons"\ 6lemma memb_sons: ∀S,l.∀p,q:(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S)\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S). \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? p (\ 5a href="cic:/matita/tutorial/chapter10/sons.def(7)"\ 6sons\ 5/a\ 6 ? l q) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
65   \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6a.(\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 q)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6
66       \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 q)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p).
67 #S #l elim l [#p #q normalize in ⊢ (%→?); #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] 
68 #a #tl #Hind #p #q #H cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … H) -H
69   [#H @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … a) >(\P H) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ |#H @Hind @H]
70 qed.
71
72 \ 5img class="anchor" src="icons/tick.png" id="is_bisim"\ 6definition is_bisim ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λl:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ?.λalpha:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S.
73   ∀p:(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S)\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S). \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? p l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"\ 6cofinal\ 5/a\ 6 ? p \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter10/sons.def(7)"\ 6sons\ 5/a\ 6 ? alpha p) l).
74
75 (* Using lemma equiv_sem_occ it is easy to prove the following result: *)
76
77 \ 5img class="anchor" src="icons/tick.png" id="bisim_to_sem"\ 6lemma bisim_to_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ?.∀e1,e2: \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
78   \ 5a href="cic:/matita/tutorial/chapter10/is_bisim.def(8)"\ 6is_bisim\ 5/a\ 6 S l (\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"\ 6occ\ 5/a\ 6 S e1 e2) → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6e1,e2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6\ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
79 #S #l #e1 #e2 #Hbisim #Hmemb @\ 5a href="cic:/matita/tutorial/chapter10/equiv_sem_occ.def(17)"\ 6equiv_sem_occ\ 5/a\ 6 
80 #w #Hsub @(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hbisim \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e1,\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 ?))
81 lapply Hsub @(\ 5a href="cic:/matita/basics/list/list_elim_left.def(10)"\ 6list_elim_left\ 5/a\ 6 … w) [//]
82 #a #w1 #Hind #Hsub >\ 5a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"\ 6moves_left\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"\ 6moves_left\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 …(Hbisim …(Hind ?)))
83   [#x #Hx @Hsub @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"\ 6memb_append_l1\ 5/a\ 6 //
84   |cut (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"\ 6occ\ 5/a\ 6 S e1 e2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) [@Hsub @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6memb_append_l2\ 5/a\ 6 //] #occa 
85    @(\ 5a href="cic:/matita/tutorial/chapter5/memb_map.def(5)"\ 6memb_map\ 5/a\ 6 … occa)
86   ]
87 qed.
88
89 (* This is already an interesting result: checking if l is a bisimulation 
90 is decidable, hence we could generate l with some untrusted piece of code 
91 and then run a (boolean version of) is_bisim to check that it is actually 
92 a bisimulation. 
93 However, in order to prove that equivalence of regular expressions
94 is decidable we must prove that we can always effectively build such a list 
95 (or find a counterexample).
96 The idea is that the list we are interested in is just the set of 
97 all pair of pres reachable from the initial pair via some
98 sequence of moves. 
99
100 The algorithm for computing reachable nodes in graph is a very 
101 traditional one. We split nodes in two disjoint lists: a list of 
102 visited nodes and a frontier, composed by all nodes connected
103 to a node in visited but not visited already. At each step we select a node 
104 a from the frontier, compute its sons, add a to the set of 
105 visited nodes and the (not already visited) sons to the frontier. 
106
107 Instead of fist computing reachable nodes and then performing the 
108 bisimilarity test we can directly integrate it in the algorithm:
109 the set of visited nodes is closed by construction w.r.t. reachability,
110 so we have just to check cofinality for any node we add to visited.
111
112 Here is the extremely simple algorithm: *)
113
114 \ 5img class="anchor" src="icons/tick.png" id="bisim"\ 6let rec bisim S l n (frontier,visited: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ?) on n ≝
115   match n with 
116   [ O ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,visited\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (* assert false *)
117   | S m ⇒ 
118     match frontier with
119     [ nil ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6,visited\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6
120     | cons hd tl ⇒
121       if \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 hd)) (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 hd)) then
122         bisim S l m (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 ? (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 ? (λx.\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? x (hd\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6visited))) 
123         (\ 5a href="cic:/matita/tutorial/chapter10/sons.def(7)"\ 6sons\ 5/a\ 6 S l hd)) tl) (hd\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6visited)
124       else \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,visited\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6
125     ]
126   ].
127
128 (* The integer n is an upper bound to the number of recursive call, 
129 equal to the dimension of the graph. It returns a pair composed
130 by a boolean and a the set of visited nodes; the boolean is true
131 if and only if all visited nodes are cofinal. 
132
133 The following results explicitly state the behaviour of bisim is the general
134 case and in some relevant instances *)
135
136 \ 5img class="anchor" src="icons/tick.png" id="unfold_bisim"\ 6lemma unfold_bisim: ∀S,l,n.∀frontier,visited: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ?.
137   \ 5a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"\ 6bisim\ 5/a\ 6 S l n frontier visited \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
138   match n with 
139   [ O ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,visited\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (* assert false *)
140   | S m ⇒ 
141     match frontier with
142     [ nil ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6,visited\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6
143     | cons hd tl ⇒
144       if \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 hd)) (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 hd)) then
145         \ 5a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"\ 6bisim\ 5/a\ 6 S l m (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 ? (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 ? (λx.\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? x (hd\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6visited))) 
146           (\ 5a href="cic:/matita/tutorial/chapter10/sons.def(7)"\ 6sons\ 5/a\ 6 S l hd)) tl) (hd\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6visited)
147       else \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,visited\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6
148     ]
149   ].
150 #S #l #n cases n // qed.
151
152 \ 5img class="anchor" src="icons/tick.png" id="bisim_never"\ 6lemma bisim_never: ∀S,l.∀frontier,visited: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ?.
153   \ 5a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"\ 6bisim\ 5/a\ 6 S l \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 frontier visited \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,visited\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6.
154 #frontier #visited >\ 5a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"\ 6unfold_bisim\ 5/a\ 6 // 
155 qed.
156
157 \ 5img class="anchor" src="icons/tick.png" id="bisim_end"\ 6lemma bisim_end: ∀Sig,l,m.∀visited: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ?.
158   \ 5a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"\ 6bisim\ 5/a\ 6 Sig l (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 visited \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6,visited\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6.
159 #n #visisted >\ 5a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"\ 6unfold_bisim\ 5/a\ 6 // 
160 qed.
161
162 \ 5img class="anchor" src="icons/tick.png" id="bisim_step_true"\ 6lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ?.
163 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p)) (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
164   \ 5a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"\ 6bisim\ 5/a\ 6 Sig l (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) (p\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6frontier) visited \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
165   \ 5a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"\ 6bisim\ 5/a\ 6 Sig l m (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 ? (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 ? (λx.\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? x (p\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6visited))) 
166     (\ 5a href="cic:/matita/tutorial/chapter10/sons.def(7)"\ 6sons\ 5/a\ 6 Sig l p)) frontier) (p\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6visited).
167 #Sig #l #m #p #frontier #visited #test >\ 5a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"\ 6unfold_bisim\ 5/a\ 6 whd in ⊢ (??%?);  >test // 
168 qed.
169
170 \ 5img class="anchor" src="icons/tick.png" id="bisim_step_false"\ 6lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ?.
171 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p)) (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 →
172   \ 5a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"\ 6bisim\ 5/a\ 6 Sig l (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) (p\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6frontier) visited \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,visited\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6.
173 #Sig #l #m #p #frontier #visited #test >\ 5a href="cic:/matita/tutorial/chapter10/unfold_bisim.def(9)"\ 6unfold_bisim\ 5/a\ 6 whd in ⊢ (??%?); >test // 
174 qed.
175
176 (* In order to prove termination of bisim we must be able to effectively 
177 enumerate all possible pres: *)
178  
179 (* lemma notb_eq_true_l: ∀b. notb b = true → b = false.
180 #b cases b normalize //
181 qed. *)
182
183 \ 5img class="anchor" src="icons/tick.png" id="pitem_enum"\ 6let rec pitem_enum S (i:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on i ≝
184   match i with
185   [ z ⇒ (\ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"\ 6pz\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"\ 6\ 5/span\ 6\ 5span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"\ 6\ 5/span\ 6 S)\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
186   | e ⇒ (\ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,2,1)"\ 6pe\ 5/a\ 6 S)\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
187   | s y ⇒ (\ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,3,1)"\ 6ps\ 5/a\ 6 S y)\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,4,1)"\ 6pp\ 5/a\ 6 S y)\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
188   | o i1 i2 ⇒ \ 5a href="cic:/matita/basics/list/compose.def(2)"\ 6compose\ 5/a\ 6 ??? (\ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,6,1)"\ 6po\ 5/a\ 6 S) (pitem_enum S i1) (pitem_enum S i2)
189   | c i1 i2 ⇒ \ 5a href="cic:/matita/basics/list/compose.def(2)"\ 6compose\ 5/a\ 6 ??? (\ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,5,1)"\ 6pc\ 5/a\ 6 S) (pitem_enum S i1) (pitem_enum S i2)
190   | k i ⇒ \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? (\ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,7,1)"\ 6pk\ 5/a\ 6 S) (pitem_enum S i)
191   ].
192   
193 \ 5img class="anchor" src="icons/tick.png" id="pitem_enum_complete"\ 6lemma pitem_enum_complete : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
194   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"\ 6DeqItem\ 5/a\ 6 S) i (\ 5a href="cic:/matita/tutorial/chapter10/pitem_enum.fix(0,1,3)"\ 6pitem_enum\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
195 #S #i elim i 
196   [1,2://
197   |3,4:#c normalize >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … c)) //
198   |5,6:#i1 #i2 #Hind1 #Hind2 @(\ 5a href="cic:/matita/tutorial/chapter5/memb_compose.def(6)"\ 6memb_compose\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"\ 6DeqItem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"\ 6DeqItem\ 5/a\ 6 S)) //
199   |#i #Hind @(\ 5a href="cic:/matita/tutorial/chapter5/memb_map.def(5)"\ 6memb_map\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"\ 6DeqItem\ 5/a\ 6 S)) //
200   ]
201 qed.
202
203 \ 5img class="anchor" src="icons/tick.png" id="pre_enum"\ 6definition pre_enum ≝ λS.λi:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S.
204   \ 5a href="cic:/matita/basics/list/compose.def(2)"\ 6compose\ 5/a\ 6 ??? (λi,b.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6i,b\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6) (\ 5a href="cic:/matita/tutorial/chapter10/pitem_enum.fix(0,1,3)"\ 6pitem_enum\ 5/a\ 6 S i) (\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6).
205   
206 \ 5img class="anchor" src="icons/tick.png" id="pre_enum_complete"\ 6lemma pre_enum_complete : ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
207   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? e (\ 5a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"\ 6pre_enum\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
208 #S * #i #b @(\ 5a href="cic:/matita/tutorial/chapter5/memb_compose.def(6)"\ 6memb_compose\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/DeqItem.def(6)"\ 6DeqItem\ 5/a\ 6 S) \ 5a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"\ 6DeqBool\ 5/a\ 6 ? (λi,b.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6i,b\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6))
209 // cases b normalize //
210 qed.
211  
212 \ 5img class="anchor" src="icons/tick.png" id="space_enum"\ 6definition space_enum ≝ λS.λi1,i2:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S.
213   \ 5a href="cic:/matita/basics/list/compose.def(2)"\ 6compose\ 5/a\ 6 ??? (λe1,e2.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6e1,e2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6) (\ 5a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"\ 6pre_enum\ 5/a\ 6 S i1) (\ 5a href="cic:/matita/tutorial/chapter10/pre_enum.def(4)"\ 6pre_enum\ 5/a\ 6 S i2).
214
215 \ 5img class="anchor" src="icons/tick.png" id="space_enum_complete"\ 6lemma space_enum_complete : ∀S.∀e1,e2: \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
216   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6e1,e2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter10/space_enum.def(5)"\ 6space_enum\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e1\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6) (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
217 #S #e1 #e2 @(\ 5a href="cic:/matita/tutorial/chapter5/memb_compose.def(6)"\ 6memb_compose\ 5/a\ 6 … (λi,b.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6i,b\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6))
218 // qed.
219
220 \ 5img class="anchor" src="icons/tick.png" id="all_reachable"\ 6definition all_reachable ≝ λS.λe1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ?.
221 \ 5a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"\ 6uniqueb\ 5/a\ 6 ? l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 
222   ∀p. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? p l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
223     \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6w.(\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p). 
224
225 \ 5img class="anchor" src="icons/tick.png" id="disjoint"\ 6definition disjoint ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λl1,l2.
226   ∀p:S. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S p l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →  \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S p l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
227         
228 (* We are ready to prove that bisim is correct; we use the invariant 
229 that at each call of bisim the two lists visited and frontier only contain 
230 nodes reachable from 〈e_1,e_2〉, hence it is absurd to suppose to meet a pair 
231 which is not cofinal. *)
232
233 \ 5img class="anchor" src="icons/tick.png" id="bisim_correct"\ 6lemma bisim_correct: ∀S.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6\ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 → 
234  ∀l,n.∀frontier,visited:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ((\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S)\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S)).
235  \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/space_enum.def(5)"\ 6space_enum\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e1\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6) (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6visited\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6
236  \ 5a href="cic:/matita/tutorial/chapter10/all_reachable.def(8)"\ 6all_reachable\ 5/a\ 6 S e1 e2 visited →  
237  \ 5a href="cic:/matita/tutorial/chapter10/all_reachable.def(8)"\ 6all_reachable\ 5/a\ 6 S e1 e2 frontier →
238  \ 5a href="cic:/matita/tutorial/chapter10/disjoint.def(5)"\ 6disjoint\ 5/a\ 6 ? frontier visited →
239  \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"\ 6bisim\ 5/a\ 6 S l n frontier visited) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
240 #Sig #e1 #e2 #same #l #n elim n 
241   [#frontier #visited #abs * #unique #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … abs)
242    @\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_length.def(6)"\ 6sublist_length\ 5/a\ 6 // * #e11 #e21 #membp 
243    cut ((|\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e11\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e1\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (|\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e21\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))
244    [|* #H1 #H2 <H1 <H2 @\ 5a href="cic:/matita/tutorial/chapter10/space_enum_complete.def(9)"\ 6space_enum_complete\ 5/a\ 6]
245    cases (H … membp) #w * #we1 #we2 <we1 <we2 % >\ 5a href="cic:/matita/tutorial/chapter9/same_kernel_moves.def(9)"\ 6same_kernel_moves\ 5/a\ 6 //    
246   |#m #HI * [#visited #vinv #finv >\ 5a href="cic:/matita/tutorial/chapter10/bisim_end.def(10)"\ 6bisim_end\ 5/a\ 6 //]
247    #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier 
248    #disjoint
249    cut (\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6w.(\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p)) 
250     [@(r_frontier … (\ 5a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"\ 6memb_hd\ 5/a\ 6 … ))] #rp
251    cut (\ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p)) (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6)
252     [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?) 
253      @(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter10/equiv_sem.def(16)"\ 6equiv_sem\ 5/a\ 6 … )) @same] #ptest 
254    >(\ 5a href="cic:/matita/tutorial/chapter10/bisim_step_true.def(10)"\ 6bisim_step_true\ 5/a\ 6 … ptest) @HI -HI 
255      [<\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"\ 6plus_n_Sm\ 5/a\ 6 //
256      |% [whd in ⊢ (??%?); >(disjoint … (\ 5a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"\ 6memb_hd\ 5/a\ 6 …)) whd in ⊢ (??%?); //
257         |#p1 #H (cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … H)) [#eqp >(\P eqp) // |@r_visited]
258         ]
259      |whd % [@\ 5a href="cic:/matita/tutorial/chapter5/unique_append_unique.def(6)"\ 6unique_append_unique\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/bool/andb_true_r.def(4)"\ 6andb_true_r\ 5/a\ 6 … u_frontier)]
260       @\ 5a href="cic:/matita/tutorial/chapter5/unique_append_elim.def(7)"\ 6unique_append_elim\ 5/a\ 6 #q #H
261        [cases (\ 5a href="cic:/matita/tutorial/chapter10/memb_sons.def(8)"\ 6memb_sons\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"\ 6memb_filter_memb\ 5/a\ 6 … H)) -H
262         #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (w1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6)))
263         >\ 5a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"\ 6moves_left\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"\ 6moves_left\ 5/a\ 6 >mw1 >mw2 >m1 >m2 % // 
264        |@r_frontier @\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6memb_cons\ 5/a\ 6 //
265        ]
266      |@\ 5a href="cic:/matita/tutorial/chapter5/unique_append_elim.def(7)"\ 6unique_append_elim\ 5/a\ 6 #q #H
267        [@\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 @(\ 5a href="cic:/matita/tutorial/chapter5/memb_filter_true.def(5)"\ 6memb_filter_true\ 5/a\ 6 … H)
268        |cut ((q=\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6p) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
269          [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6memb_cons\ 5/a\ 6 //]
270         cases (\ 5a href="cic:/matita/basics/bool/andb_true.def(5)"\ 6andb_true\ 5/a\ 6 … u_frontier) #notp #_ @(\bf ?) 
271         @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … \ 5a href="cic:/matita/basics/bool/not_eq_true_false.def(3)"\ 6not_eq_true_false\ 5/a\ 6) #eqqp <notp <eqqp >H //
272        ]
273      ]
274    ]  
275 qed.  
276
277 (* For completeness, we use the invariant that all the nodes in visited are cofinal, 
278 and the sons of visited are either in visited or in the frontier; since
279 at the end frontier is empty, visited is hence a bisimulation. *)
280
281 \ 5img class="anchor" src="icons/tick.png" id="all_true"\ 6definition all_true ≝ λS.λl.∀p:(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S) \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S). \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? p l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
282   (\ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p)) (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6).
283
284 \ 5img class="anchor" src="icons/tick.png" id="sub_sons"\ 6definition sub_sons ≝ λS,l,l1,l2.∀x:(\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S) \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S). 
285 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? x l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter10/sons.def(7)"\ 6sons\ 5/a\ 6 ? l x) l2. 
286
287 \ 5img class="anchor" src="icons/tick.png" id="bisim_complete"\ 6lemma bisim_complete: 
288  ∀S,l,n.∀frontier,visited,visited_res:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 ?.
289  \ 5a href="cic:/matita/tutorial/chapter10/all_true.def(8)"\ 6all_true\ 5/a\ 6 S visited →
290  \ 5a href="cic:/matita/tutorial/chapter10/sub_sons.def(8)"\ 6sub_sons\ 5/a\ 6 S l visited (frontier\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6visited) →
291  \ 5a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"\ 6bisim\ 5/a\ 6 S l n frontier visited \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 〈\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6,visited_res\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 →
292  \ 5a href="cic:/matita/tutorial/chapter10/is_bisim.def(8)"\ 6is_bisim\ 5/a\ 6 S visited_res l \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 ? (frontier\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6visited) visited_res. 
293 #S #l #n elim n
294   [#fron #vis #vis_res #_ #_ >\ 5a href="cic:/matita/tutorial/chapter10/bisim_never.def(10)"\ 6bisim_never\ 5/a\ 6 #H destruct
295   |#m #Hind * 
296     [(* case empty frontier *)
297      -Hind #vis #vis_res #allv #H normalize in  ⊢ (%→?);
298      #H1 destruct % #p 
299       [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
300     |#hd cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 hd)) (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 hd))))
301       [|(* case head of the frontier is non ok (absurd) *)
302        #H #tl #vis #vis_res #allv >(\ 5a href="cic:/matita/tutorial/chapter10/bisim_step_false.def(10)"\ 6bisim_step_false\ 5/a\ 6 … H) #_ #H1 destruct]
303      (* frontier = hd:: tl and hd is ok *)
304      #H #tl #visited #visited_res #allv >(\ 5a href="cic:/matita/tutorial/chapter10/bisim_step_true.def(10)"\ 6bisim_step_true\ 5/a\ 6 … H)
305      (* new_visited = hd::visited are all ok *)
306      cut (\ 5a href="cic:/matita/tutorial/chapter10/all_true.def(8)"\ 6all_true\ 5/a\ 6 S (hd:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6visited)) 
307       [#p #H1 cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … H1) [#eqp >(\P eqp) @H |@allv]]
308      (* we now exploit the induction hypothesis *)
309      #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
310       [#H1 #H2 % // #p #membp @H2 -H2 cases (\ 5a href="cic:/matita/tutorial/chapter5/memb_append.def(5)"\ 6memb_append\ 5/a\ 6 … membp) -membp #membp
311         [cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … membp) -membp #membp
312           [@\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6memb_append_l2\ 5/a\ 6 >(\P membp) @\ 5a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"\ 6memb_hd\ 5/a\ 6
313           |@\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"\ 6memb_append_l1\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"\ 6sublist_unique_append_l2\ 5/a\ 6 // 
314           ]
315         |@\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6memb_append_l2\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6memb_cons\ 5/a\ 6 //
316         ] 
317       |(* the only thing left to prove is the sub_sons invariant *)  
318      #x #membx cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … membx)
319       [(* case x = hd *) 
320        #eqhdx <(\P eqhdx) #xa #membxa
321        (* xa is a son of x; we must distinguish the case xa 
322         was already visited form the case xa is new *)
323        cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 ? xa (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6visited)))
324         [(* xa visited - trivial *) #membxa @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6memb_append_l2\ 5/a\ 6 //
325         |(* xa new *) #membxa @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"\ 6memb_append_l1\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"\ 6sublist_unique_append_l1\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter5/memb_filter_l.def(5)"\ 6memb_filter_l\ 5/a\ 6
326           [>membxa //|//]
327         ]
328       |(* case x in visited *)
329        #H1 #xa #membxa cases (\ 5a href="cic:/matita/tutorial/chapter5/memb_append.def(5)"\ 6memb_append\ 5/a\ 6 … (subH x … H1 … membxa))  
330         [#H2 (cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … H2)) 
331           [#H3 @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6memb_append_l2\ 5/a\ 6 <(\P H3) @\ 5a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"\ 6memb_hd\ 5/a\ 6
332           |#H3 @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"\ 6memb_append_l1\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"\ 6sublist_unique_append_l2\ 5/a\ 6 @H3
333           ]
334         |#H2 @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6memb_append_l2\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6memb_cons\ 5/a\ 6 @H2
335         ]
336       ]
337     ]
338   ]
339 qed.
340
341 (* We can now give the definition of the equivalence algorithm, and
342 prove that two expressions are equivalente if and only if they define
343 the same language. *)
344
345 \ 5img class="anchor" src="icons/tick.png" id="equiv"\ 6definition equiv ≝ λSig.λre1,re2:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 Sig. 
346   let e1 ≝ \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 ? re1) in
347   let e2 ≝ \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 ? re2) in
348   let n ≝ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter10/space_enum.def(5)"\ 6space_enum\ 5/a\ 6 Sig (|\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e1\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6) (|\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))) in
349   let sig ≝ (\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"\ 6occ\ 5/a\ 6 Sig e1 e2) in
350   (\ 5a href="cic:/matita/tutorial/chapter10/bisim.fix(0,2,8)"\ 6bisim\ 5/a\ 6 ? sig n (〈e1,e2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6).
351
352 \ 5img class="anchor" src="icons/tick.png" id="euqiv_sem"\ 6theorem euqiv_sem : ∀Sig.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 Sig.
353    \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter10/equiv.def(9)"\ 6equiv\ 5/a\ 6 ? e1 e2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \sem{e1\ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 =1 \sem{e2\ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
354 #Sig #re1 #re2 %
355   [#H @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter8/re_embedding.def(13)"\ 6re_embedding\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter8/re_embedding.def(13)"\ 6re_embedding\ 5/a\ 6]
356    cut (\ 5a href="cic:/matita/tutorial/chapter10/equiv.def(9)"\ 6equiv\ 5/a\ 6 ? re1 re2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 〈\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter10/equiv.def(9)"\ 6equiv\ 5/a\ 6 ? re1 re2)\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6)
357      [<H //] #Hcut
358    cases (\ 5a href="cic:/matita/tutorial/chapter10/bisim_complete.def(11)"\ 6bisim_complete\ 5/a\ 6 … Hcut) 
359      [2,3: #p whd in ⊢ ((??%?)→?); #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] 
360    #Hbisim #Hsub @(\ 5a href="cic:/matita/tutorial/chapter10/bisim_to_sem.def(18)"\ 6bisim_to_sem\ 5/a\ 6 … Hbisim) 
361    @Hsub @\ 5a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"\ 6memb_hd\ 5/a\ 6
362   |#H @(\ 5a href="cic:/matita/tutorial/chapter10/bisim_correct.def(17)"\ 6bisim_correct\ 5/a\ 6 ? (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 ? re1)) (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 ? re2))) 
363     [@\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/re_embedding.def(13)"\ 6re_embedding\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@H] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter8/re_embedding.def(13)"\ 6re_embedding\ 5/a\ 6
364     |// 
365     |% // #p whd in ⊢ ((??%?)→?); #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/  
366     |% // #p #H >(\ 5a href="cic:/matita/tutorial/chapter5/memb_single.def(5)"\ 6memb_single\ 5/a\ 6 … H) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
367     |#p #_ normalize //
368     ]
369   ]
370 qed.
371
372 \ 5img class="anchor" src="icons/tick.png" id="eqbnat"\ 6definition eqbnat ≝ λn,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 n m.
373
374 \ 5img class="anchor" src="icons/tick.png" id="eqbnat_true"\ 6lemma eqbnat_true : ∀n,m. \ 5a href="cic:/matita/tutorial/chapter10/eqbnat.def(2)"\ 6eqbnat\ 5/a\ 6 n m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m.
375 #n #m % [@\ 5a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"\ 6eqb_true_to_eq\ 5/a\ 6 | @\ 5a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"\ 6eq_to_eqb_true\ 5/a\ 6]
376 qed.
377
378 \ 5img class="anchor" src="icons/tick.png" id="DeqNat"\ 6definition DeqNat ≝ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/eqbnat_true.def(7)"\ 6eqbnat_true\ 5/a\ 6.
379
380 \ 5img class="anchor" src="icons/tick.png" id="a"\ 6definition a ≝ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"\ 6s\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"\ 6DeqNat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
381 \ 5img class="anchor" src="icons/tick.png" id="b"\ 6definition b ≝ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"\ 6s\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"\ 6DeqNat\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6).
382 \ 5img class="anchor" src="icons/tick.png" id="c"\ 6definition c ≝ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,3,1)"\ 6s\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/DeqNat.def(8)"\ 6DeqNat\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6)).
383
384 \ 5img class="anchor" src="icons/tick.png" id="exp1"\ 6definition exp1 ≝ ((\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/b.def(9)"\ 6b\ 5/a\ 6)^\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6).
385 \ 5img class="anchor" src="icons/tick.png" id="exp2"\ 6definition exp2 ≝ \ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter10/b.def(9)"\ 6b\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6)^\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6.
386 \ 5img class="anchor" src="icons/tick.png" id="exp4"\ 6definition exp4 ≝ (\ 5a href="cic:/matita/tutorial/chapter10/b.def(9)"\ 6b\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6)^\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6.
387
388 \ 5img class="anchor" src="icons/tick.png" id="exp6"\ 6definition exp6 ≝ \ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6 \ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6 \ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/b.def(9)"\ 6b\ 5/a\ 6^\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="re or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/b.def(9)"\ 6b\ 5/a\ 6^\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 ).
389 \ 5img class="anchor" src="icons/tick.png" id="exp7"\ 6definition exp7 ≝ \ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6 \ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6^\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/b.def(9)"\ 6b\ 5/a\ 6^\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6.
390
391 \ 5img class="anchor" src="icons/tick.png" id="exp8"\ 6definition exp8 ≝ \ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6^\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 ).
392 \ 5img class="anchor" src="icons/tick.png" id="exp9"\ 6definition exp9 ≝ (\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6 \ 5a title="re or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6\ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/a.def(9)"\ 6a\ 5/a\ 6)^\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6.
393
394 \ 5img class="anchor" src="icons/tick.png" id="ex1"\ 6example ex1 : \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter10/equiv.def(9)"\ 6equiv\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter10/exp8.def(10)"\ 6exp8\ 5/a\ 6\ 5a title="re or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/exp9.def(10)"\ 6exp9\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter10/exp9.def(10)"\ 6exp9\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
395 normalize // qed.