2 \ 5h1
\ 6Regular Expressions Equivalence
\ 5/h1
\ 6*)
4 include "tutorial/chapter9.ma".
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
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).
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. *)
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〉.
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]
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. *)
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|)).
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〉.
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 //]
46 (* The following is a stronger version of equiv_sem, relative to characters
47 occurring the given regular expressions. *)
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
56 \ 5h2
\ 6Bisimulations
\ 5/h2
\ 6
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.
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.
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]
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).
76 (* Using lemma equiv_sem_occ it is easy to prove the following result: *)
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)
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
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
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.
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.
113 Here is the extremely simple algorithm: *)
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 ≝
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 *)
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〉
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〉
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.
134 The following results explicitly state the behaviour of bisim is the general
135 case and in some relevant instances *)
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
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 *)
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〉
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〉
151 #S #l #n cases n // qed.
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 //
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 //
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 //
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 //
177 (* In order to prove termination of bisim we must be able to effectively
178 enumerate all possible pres: *)
180 (* lemma notb_eq_true_l: ∀b. notb b = true → b = false.
181 #b cases b normalize //
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 ≝
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)
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.
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)) //
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 title="cons" 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/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6].
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 //
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).
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〉))
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).
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.
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. *)
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
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]
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.dec"
\ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6a]))
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 //
267 |@
\ 5a href="cic:/matita/tutorial/chapter5/unique_append_elim.dec"
\ 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/filter_true.def(5)"
\ 6filter_true
\ 5/a
\ 6 … H)
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 //
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. *)
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).
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.
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.
295 [#fron #vis #vis_res #_ #_ >
\ 5a href="cic:/matita/tutorial/chapter10/bisim_never.def(10)"
\ 6bisim_never
\ 5/a
\ 6 #H destruct
297 [(* case empty frontier *)
298 -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?);
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 //
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 //
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)
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
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
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
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. *)
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="cons" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6e1,e2〉]
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]).
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}.
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)〉)
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
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/
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.
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]
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.
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)).
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*.
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*.
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*.
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.