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