include "tutorial/chapter8.ma".
-let rec move (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (x:S) (E: \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on E : \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
+\ 5img class="anchor" src="icons/tick.png" id="move"\ 6let rec move (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (x:S) (E: \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on E : \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
match E with
- [ pz ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"\ 6pz\ 5/a\ 6 S, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 〉
- | pe ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 〉
- | ps y ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem ps" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6y, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 〉
- | pp y ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem ps" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6y, x \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= y 〉
+ [ pz ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"\ 6pz\ 5/a\ 6 S, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
+ | pe ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem epsilon" 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="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
+ | ps y ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem ps" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6y, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
+ | pp y ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem ps" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6y, x \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
| po e1 e2 ⇒ (move ? x e1) \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 (move ? x e2)
| pc e1 e2 ⇒ (move ? x e1) \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 (move ? x e2)
- | pk e ⇒ (move ? x e)\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛ ].
+ | pk e ⇒ (move ? x e)\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6⊛\ 5/a\ 6 ].
-lemma move_plus: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+\ 5img class="anchor" src="icons/tick.png" id="move_plus"\ 6lemma move_plus: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x (i1 \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x i1) \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x i2).
// qed.
-lemma move_cat: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+\ 5img class="anchor" src="icons/tick.png" id="move_cat"\ 6lemma move_cat: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x (i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x i1) \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x i2).
// qed.
-lemma move_star: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
- \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x i)\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛.
+\ 5img class="anchor" src="icons/tick.png" id="move_star"\ 6lemma move_star: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x i)\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6⊛\ 5/a\ 6.
// qed.
(*
point stops in front of the final b, while the other one broadcast inside (b^*a + b)b,
so
- move((•a + ϵ)((•b)*•a + •b)b,a) = 〈(a + ϵ)((•b)^*•a + •b)•b, false〉
+ move((•a + ϵ)((•b)*•a + •b)b,a) = 〈(a + ϵ)((•b)^*•a + •b)•b, false〉
For b, we have two positions too. The innermost point stops in front of the final b too,
while the other point reaches the end of b* and must go back through b*a:
- move((•a + ϵ)((•b)*•a + •b)b ,b) = 〈(a + ϵ)((•b)*•a + b)•b, false〉
+ move((•a + ϵ)((•b)*•a + •b)b ,b) = 〈(a + ϵ)((•b)*•a + b)•b, false〉
*)
-definition pmove ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λx:S.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).
+\ 5img class="anchor" src="icons/tick.png" id="pmove"\ 6definition pmove ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λx:S.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).
-lemma pmove_def : ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀b.
- \ 5a href="cic:/matita/tutorial/chapter9/pmove.def(7)"\ 6pmove\ 5/a\ 6 ? x \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,b〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x i.
+\ 5img class="anchor" src="icons/tick.png" id="pmove_def"\ 6lemma pmove_def : ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀b.
+ \ 5a href="cic:/matita/tutorial/chapter9/pmove.def(7)"\ 6pmove\ 5/a\ 6 ? x \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,b\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x i.
// qed.
-lemma eq_to_eq_hd: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a,b.
- a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l2 → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
+\ 5img class="anchor" src="icons/tick.png" id="eq_to_eq_hd"\ 6lemma eq_to_eq_hd: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a,b.
+ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2 → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
#A #l1 #l2 #a #b #H destruct //
qed.
(* Obviously, a move does not change the carrier of the item, as one can easily
prove by induction on the item. *)
-lemma same_kernel: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 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 (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? a i)| \ 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\ 6i|.
+\ 5img class="anchor" src="icons/tick.png" id="same_kernel"\ 6lemma same_kernel: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 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 (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? a i)\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
#S #a #i elim i //
[#i1 #i2 #H1 #H2 >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter8/erase_odot.def(7)"\ 6erase_odot\ 5/a\ 6 //
|#i1 #i2 #H1 #H2 >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6 whd in ⊢ (??%%); //
(* Here is our first, major result, stating the correctness of the
move operation. The proof is a simple induction on i. *)
-theorem move_ok:
+\ 5img class="anchor" src="icons/tick.png" id="move_ok"\ 6theorem move_ok:
∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S.
- \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? a i} w \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w).
+ \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? a i\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 w \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w).
#S #a #i elim i
[normalize /\ 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/
|normalize /\ 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/
|normalize /\ 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/
- |normalize #x #w cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x)) #H >H normalize
+ |normalize #x #w cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)) #H >H normalize
[>(\P H) % [* // #bot @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 //| #H1 destruct /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
|% [@\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 |#H1 cases (\Pf H) #H2 @H2 destruct //]
]
notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
-let rec moves (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) w e on w : \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
+\ 5img class="anchor" src="icons/tick.png" id="moves"\ 6let rec moves (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) w e on w : \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
match w with
[ nil ⇒ e
| cons x w' ⇒ w' ↦* (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e))].
-lemma moves_empty: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
- \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 e.
+\ 5img class="anchor" src="icons/tick.png" id="moves_empty"\ 6lemma moves_empty: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 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 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 e.
// qed.
-lemma moves_cons: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀w.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
- \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w) e \ 5a title="leibnitz's equality" 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 (\ 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 e)).
+\ 5img class="anchor" src="icons/tick.png" id="moves_cons"\ 6lemma moves_cons: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀w.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w) e \ 5a title="leibnitz's equality" 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 (\ 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 e)).
// qed.
-lemma moves_left : ∀S,a,w,e.
- \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S (w\ 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])) e \ 5a title="leibnitz's equality" 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 href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e)).
+\ 5img class="anchor" src="icons/tick.png" id="moves_left"\ 6lemma moves_left : ∀S,a,w,e.
+ \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S (w\ 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="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)) e \ 5a title="leibnitz's equality" 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 href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e)).
#S #a #w elim w // #x #tl #Hind #e >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 //
qed.
-lemma not_epsilon_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. ∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
- \ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 ((a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w) \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e) ((a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w) \ 5a title="in_pl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).
+\ 5img class="anchor" src="icons/tick.png" id="not_epsilon_sem"\ 6lemma not_epsilon_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. ∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ \ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 ((a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w) \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e) ((a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w) \ 5a title="in_pl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).
#S #a #w * #i #b cases b normalize
[% /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * // #H destruct |% normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/]
qed.
-lemma same_kernel_moves: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀w.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 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 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e)| \ 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 e|.
+\ 5img class="anchor" src="icons/tick.png" id="same_kernel_moves"\ 6lemma same_kernel_moves: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀w.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 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 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e)\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
#S #w elim w //
qed.
-theorem decidable_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. ∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
- (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w 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) \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e} w.
+\ 5img class="anchor" src="icons/tick.png" id="decidable_sem"\ 6theorem decidable_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. ∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w 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) \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 w.
#S #w elim w
[* #i #b >\ 5a href="cic:/matita/tutorial/chapter9/moves_empty.def(8)"\ 6moves_empty\ 5/a\ 6 cases b % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter7/true_to_epsilon.def(9)"\ 6true_to_epsilon\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/\ 5span class="error" title="error location"\ 6\ 5/span\ 6 #H @\ 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/
|#a #w1 #Hind #e >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6
qed.
(* It is now clear that we can build a DFA D_e for e by taking pre as states,
-and move as transition function; the initial state is •(e) and a state 〈i,b〉 is
+and move as transition function; the initial state is •(e) and a state 〈i,b〉 is
final if and only if b is true. The fact that states in D_e are finite is obvious:
in fact, their cardinality is at most 2^{n+1} where n is the number of symbols in
e. This is one of the advantages of pointed regular expressions w.r.t. derivatives,
The graphical description of the automaton is the traditional one, with nodes for
states and labelled arcs for transitions. Unreachable states are not shown.
-Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
+Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
only if b is true, we may just label nodes with the item.
The automaton is not minimal: it is easy to see that the two states corresponding to
the items (a•c +bc)* and (ac+b•c)* are equivalent (a way to prove it is to observe
We conclude this chapter with a few properties of the move opertions in relation
with the pit state. *)
-definition pit_pre ≝ λS.λi.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i|), \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉.
+\ 5img class="anchor" src="icons/tick.png" id="pit_pre"\ 6definition pit_pre ≝ λS.λi.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6), \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6.
(* The following function compute the list of characters occurring in a given
item i. *)
-let rec occur (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (i: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on i ≝
+\ 5img class="anchor" src="icons/tick.png" id="occur"\ 6let rec occur (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (i: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on i ≝
match i with
- [ z ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
- | e ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
- | s y ⇒ 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]
+ [ z ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
+ | e ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
+ | s y ⇒ y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
| o e1 e2 ⇒ \ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 ? (occur S e1) (occur S e2)
| c e1 e2 ⇒ \ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 ? (occur S e1) (occur S e2)
| k e ⇒ occur S e].
(* If a symbol a does not occur in i, then move(i,a) gets to the
pit state. *)
-lemma not_occur_to_pit: ∀S,a.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 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\ 6i|)) \ 5a title="leibnitz's non-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 →
+\ 5img class="anchor" src="icons/tick.png" id="not_occur_to_pit"\ 6lemma not_occur_to_pit: ∀S,a.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 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\ 6i\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) \ 5a title="leibnitz's non-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/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.
#S #a #i elim i //
- [#x normalize cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x) normalize // #H @\ 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/
+ [#x normalize cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x) normalize // #H @\ 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/
|#i1 #i2 #Hind1 #Hind2 #H >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6
>Hind1 [2:@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"\ 6sublist_unique_append_l1\ 5/a\ 6 //]
>Hind2 [2:@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"\ 6sublist_unique_append_l2\ 5/a\ 6 //] //
(* We cannot escape form the pit state. *)
-lemma move_pit: ∀S,a,i. \ 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 href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.
+\ 5img class="anchor" src="icons/tick.png" id="move_pit"\ 6lemma move_pit: ∀S,a,i. \ 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 href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.
#S #a #i elim i //
[#i1 #i2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6 >Hind1 >Hind2 //
|#i1 #i2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6 >Hind1 >Hind2 //
]
qed.
-lemma moves_pit: ∀S,w,i. \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.
+\ 5img class="anchor" src="icons/tick.png" id="moves_pit"\ 6lemma moves_pit: ∀S,w,i. \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.
#S #w #i elim w //
qed.
(* If any character in w does not occur in i, then moves(i,w) gets
to the pit state. *)
-lemma to_pit: ∀S,w,e. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S w (\ 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 e|)) →
+\ 5img class="anchor" src="icons/tick.png" id="to_pit"\ 6lemma to_pit: ∀S,w,e. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S w (\ 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 e\ 5a title="forget" 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 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).
#S #w elim w
[#e * #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @H normalize #a #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/
- |#a #tl #Hind #e #H 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 S a (\ 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 e|))))
+ |#a #tl #Hind #e #H 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 S a (\ 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 e\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))))
[#Htrue >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 whd in ⊢ (???%); <(\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"\ 6same_kernel\ 5/a\ 6 … a)
@Hind >\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"\ 6same_kernel\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 #b #memb cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … memb)
[#H2 >(\P H2) // |#H2 @H1 //]
projects / helm.git / blobdiff