(* Here are a few simple properties of ▹ and •(-) *)
-lemma pcl_true :
- ∀S.∀i1,i2:pitem S.
- 〈i1,true〉 ▸ i2 = i1 ◂ (•i2).
+lemma pcl_true : ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i1 \ 5a title="pre_concat_r" href="cic:/fakeuri.def(1)"\ 6◃\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2).
// qed.
-lemma pcl_true_bis :
- ∀S.∀i1,i2:pitem S.
- 〈i1,true〉 ▸ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉.
-#S #i1 #i2 normalize cases (•i2) // qed.
+lemma pcl_true_bis : ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉 \ 5a title="item-pre concat" 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 title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2), \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2)〉.
+#S #i1 #i2 normalize cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2) // qed.
-lemma pcl_false:
- ∀S.∀i1,i2:pitem S.
- 〈i1,false〉 ▸ i2 = 〈i1 · i2, false〉.
+lemma pcl_false: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉 \ 5a title="item-pre concat" 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 title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉.
// qed.
-lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
- •(i1 + i2) = •i1 ⊕ •i2.
+lemma eclose_plus: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6(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 title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i1 \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2.
// qed.
-lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S.
- •(i1 · i2) = •i1 ▹ i2.
+lemma eclose_dot: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6(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 title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i2.
// qed.
-lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
- •i^* = 〈(\fst(•i))^*,true〉.
+lemma eclose_star: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i\ 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 title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6(\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i))\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉.
// qed.
(* The definition of •(-) (eclose) can then be lifted from items to pres
in the obvious way. *)
-definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
+definition lift ≝ λS.λf:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S →\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
match e with
- [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
+ [ mk_Prod i b ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (f i), \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (f i) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b〉].
-definition preclose ≝ λS. lift S (eclose S).
+definition preclose ≝ λS. \ 5a href="cic:/matita/tutorial/chapter8/lift.def(2)"\ 6lift\ 5/a\ 6 S (\ 5a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"\ 6eclose\ 5/a\ 6 S).
interpretation "preclose" 'eclose x = (preclose ? x).
(* Obviously, broadcasting does not change the carrier of the item,
as it is easily proved by structural induction. *)
-lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
+lemma erase_bull : ∀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 title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i)| \ 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|.
#S #i elim i //
- [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
- cases (•i1) #i11 #b1 cases b1 // <IH2 >odot_true_bis //
- | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
- cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //
- | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
+ [ #i1 #i2 #IH1 #IH2 >\ 5a href="cic:/matita/tutorial/chapter7/erase_dot.def(4)"\ 6erase_dot\ 5/a\ 6 <IH1 >\ 5a href="cic:/matita/tutorial/chapter8/eclose_dot.def(5)"\ 6eclose_dot\ 5/a\ 6
+ cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i1) #i11 #b1 cases b1 // <IH2 >\ 5a href="cic:/matita/tutorial/chapter8/pcl_true_bis.def(5)"\ 6pcl_true_bis\ 5/a\ 6 //
+ | #i1 #i2 #IH1 #IH2 >\ 5a href="cic:/matita/tutorial/chapter8/eclose_plus.def(5)"\ 6eclose_plus\ 5/a\ 6 >(\ 5a href="cic:/matita/tutorial/chapter7/erase_plus.def(4)"\ 6erase_plus\ 5/a\ 6 … i1) <IH1 <IH2
+ cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i1) #i11 #b1 cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2) #i21 #b2 //
+ | #i #IH >\ 5a href="cic:/matita/tutorial/chapter8/eclose_star.def(5)"\ 6eclose_star\ 5/a\ 6 >(\ 5a href="cic:/matita/tutorial/chapter7/erase_star.def(4)"\ 6erase_star\ 5/a\ 6 … i) <IH cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i) //
]
qed.
-(* We are now ready to state the main semantic properties of $\oplus,
-\triangleleft$ and $\bullet(-)$:
-
-\begin{lstlisting}[language=grafite]
-lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
- \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
-lemma sem_pcl : ∀S.∀e1:pre S.∀i2:pitem S.
- \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
-theorem sem_bullet: ∀S:DeqSet. ∀i:pitem S.
- \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
-\end{lstlisting}
-The proof of \verb+sem_oplus+ is straightforward. *)
-
-lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
- \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+(* We are now ready to state the main semantic properties of ⊕, ◃ and •(-):
+
+sem_oplus: \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}
+sem_pcl: \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}
+sem_bullet \sem{•i} =1 \sem{i} ∪ \sem{|i|}
+
+The proof of sem_oplus is straightforward. *)
+
+lemma sem_oplus: ∀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.
+ \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 e2} \ 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{e1} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2}.
#S * #i1 #b1 * #i2 #b2 #w %
- [cases b1 cases b2 normalize /2/ * /3/ * /3/
- |cases b1 cases b2 normalize /2/ * /3/ * /3/
+ [cases b1 cases b2 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |cases b1 cases b2 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
qed.
(* For the others, we proceed as follow: we first prove the following
auxiliary lemma, that assumes sem_bullet:
-lemma sem_pcl_aux: ∀S.∀e1:pre S.∀i2:pitem S.
+sem_pcl_aux:
\sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
\sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
Then, using the previous result, we prove sem_bullet by induction
on i. Finally, sem_pcl_aux and sem_bullet give sem_pcl. *)
-lemma LcatE : ∀S.∀e1,e2:pitem S.
- \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
+lemma LcatE : ∀S.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 e2} \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6e2|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2}.
// qed.
-lemma sem_pcl_aux : ∀S.∀e1:pre S.∀i2:pitem S.
- \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
- \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+lemma sem_pcl_aux : ∀S.∀e1:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.∀i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2|} →
+ \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i2} \ 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{e1} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2}.
#S * #i1 #b1 #i2 cases b1
- [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
- |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
- >erase_bull @eqP_trans [|@(eqP_union_l … H)]
- @eqP_trans [|@eqP_union_l[|@union_comm ]]
- @eqP_trans [|@eqP_sym @union_assoc ] /3/
+ [2:#th >\ 5a href="cic:/matita/tutorial/chapter8/pcl_false.def(5)"\ 6pcl_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"\ 6sem_cat\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#H >\ 5a href="cic:/matita/tutorial/chapter8/pcl_true.def(5)"\ 6pcl_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 @(\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter8/sem_pre_concat_r.def(10)"\ 6sem_pre_concat_r\ 5/a\ 6 …))
+ >\ 5a href="cic:/matita/tutorial/chapter8/erase_bull.def(6)"\ 6erase_bull\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@(\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 … H)]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6[|@\ 5a href="cic:/matita/tutorial/chapter4/union_comm.def(3)"\ 6union_comm\ 5/a\ 6 ]]
+ @\ 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/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6 ] /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
qed.
-lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
- \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
+lemma minus_eps_pre_aux: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀A.
+ \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 A → \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]}).
#S #e #i #A #seme
-@eqP_trans [|@minus_eps_pre]
-@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
-@eqP_trans [||@distribute_substract]
-@eqP_substract_r //
+@\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter7/minus_eps_pre.def(10)"\ 6minus_eps_pre\ 5/a\ 6]
+@\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter7/minus_eps_item.def(9)"\ 6minus_eps_item\ 5/a\ 6]]
+@\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/distribute_substract.def(3)"\ 6distribute_substract\ 5/a\ 6]
+@\ 5a href="cic:/matita/tutorial/chapter4/eqP_substract_r.def(3)"\ 6eqP_substract_r\ 5/a\ 6 //
qed.
-(* theorem 16: 1 *)
-theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
+theorem sem_bull: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6. ∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i|}.
#S #e elim e
- [#w normalize % [/2/ | * //]
- |/2/
- |#x normalize #w % [ /2/ | * [@False_ind | //]]
- |#x normalize #w % [ /2/ | * // ]
- |#i1 #i2 #IH1 #IH2 >eclose_dot
- @eqP_trans [|@odot_dot_aux //] >sem_cat
- @eqP_trans
- [|@eqP_union_r
- [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
- @eqP_trans [|@union_assoc]
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l //
- |#i1 #i2 #IH1 #IH2 >eclose_plus
- @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
- @eqP_trans [|@(eqP_union_l … IH2)]
- @eqP_trans [|@eqP_sym @union_assoc]
- @eqP_trans [||@union_assoc] @eqP_union_r
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_trans [||@eqP_union_l [|@union_comm]]
- @eqP_trans [||@union_assoc] /2/
- |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
- @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
- @eqP_sym @star_fix_eps
+ [#w normalize % [/\ 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/ | * //]
+ |/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#x normalize #w % [ /\ 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 | //]]
+ |#x normalize #w % [ /\ 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/ | * // ]
+ |#i1 #i2 #IH1 #IH2 >\ 5a href="cic:/matita/tutorial/chapter8/eclose_dot.def(5)"\ 6eclose_dot\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_pcl_aux.def(11)"\ 6sem_pcl_aux\ 5/a\ 6 //] >\ 5a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"\ 6sem_cat\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6
+ [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6
+ [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@(\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 … IH1)] @\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6]]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
+ @\ 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/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 //
+ |#i1 #i2 #IH1 #IH2 >\ 5a href="cic:/matita/tutorial/chapter8/eclose_plus.def(5)"\ 6eclose_plus\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_oplus.def(9)"\ 6sem_oplus\ 5/a\ 6] >\ 5a href="cic:/matita/tutorial/chapter7/sem_plus.def(8)"\ 6sem_plus\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/erase_plus.def(4)"\ 6erase_plus\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@(\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 … IH2)]
+ @\ 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/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6
+ @\ 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/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_comm.def(3)"\ 6union_comm\ 5/a\ 6]]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#i #H >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter8/erase_bull.def(6)"\ 6erase_bull\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/minus_eps_pre_aux.def(11)"\ 6minus_eps_pre_aux\ 5/a\ 6 //]]]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6]]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/erase_star.def(4)"\ 6erase_star\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/star_fix_eps.def(7)"\ 6star_fix_eps\ 5/a\ 6
]
qed.
-(* blank item *)
-let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
+(*
+\ 5h2\ 6Blank item\ 5/h2\ 6
+*)
+
+let rec blank (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 :\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S ≝
match i with
- [ z ⇒ `∅
- | e ⇒ ϵ
- | s y ⇒ `y
- | o e1 e2 ⇒ (blank S e1) + (blank S e2)
- | c e1 e2 ⇒ (blank S e1) · (blank S e2)
- | k e ⇒ (blank S e)^* ].
+ [ z ⇒ \ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"\ 6pz\ 5/a\ 6 ?
+ | e ⇒ \ 5a title="pitem epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6
+ | s y ⇒ \ 5a title="pitem ps" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6y
+ | o e1 e2 ⇒ (blank S e1) \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (blank S e2)
+ | c e1 e2 ⇒ (blank S e1) \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (blank S e2)
+ | k e ⇒ (blank S e)\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* ].
-lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
+lemma forget_blank: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S.\ 5a title="forget" 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 e| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 e.
#S #e elim e normalize //
qed.
-lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
+lemma sem_blank: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S.\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 S e} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6.
#S #e elim e
- [1,2:@eq_to_ex_eq //
- |#s @eq_to_ex_eq //
- |#e1 #e2 #Hind1 #Hind2 >sem_cat
- @eqP_trans [||@(union_empty_r … ∅)]
- @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
- @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1
- |#e1 #e2 #Hind1 #Hind2 >sem_plus
- @eqP_trans [||@(union_empty_r … ∅)]
- @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
- |#e #Hind >sem_star
- @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind
+ [1,2:@\ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6 //
+ |#s @\ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6 //
+ |#e1 #e2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"\ 6sem_cat\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@(\ 5a href="cic:/matita/tutorial/chapter4/union_empty_r.def(3)"\ 6union_empty_r\ 5/a\ 6 … \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6)]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6[|@Hind2]] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@(\ 5a href="cic:/matita/tutorial/chapter6/cat_empty_l.def(5)"\ 6cat_empty_l\ 5/a\ 6 … ?)] @\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 @Hind1
+ |#e1 #e2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter7/sem_plus.def(8)"\ 6sem_plus\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@(\ 5a href="cic:/matita/tutorial/chapter4/union_empty_r.def(3)"\ 6union_empty_r\ 5/a\ 6 … \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6)]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6[|@Hind2]] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 @Hind1
+ |#e #Hind >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@(\ 5a href="cic:/matita/tutorial/chapter6/cat_empty_l.def(5)"\ 6cat_empty_l\ 5/a\ 6 … ?)] @\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 @Hind
]
qed.
-theorem re_embedding: ∀S.∀e:re S.
- \sem{•(blank S e)} =1 \sem{e}.
-#S #e @eqP_trans [|@sem_bull] >forget_blank
-@eqP_trans [|@eqP_union_r [|@sem_blank]]
-@eqP_trans [|@union_comm] @union_empty_r.
+theorem re_embedding: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S.
+ \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 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 S e)} \ 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{e}.
+#S #e @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_bull.def(12)"\ 6sem_bull\ 5/a\ 6] >\ 5a href="cic:/matita/tutorial/chapter8/forget_blank.def(4)"\ 6forget_blank\ 5/a\ 6
+@\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_blank.def(9)"\ 6sem_blank\ 5/a\ 6]]
+@\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_comm.def(3)"\ 6union_comm\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/union_empty_r.def(3)"\ 6union_empty_r\ 5/a\ 6.
qed.
-(* lefted operations *)
-definition lifted_cat ≝ λS:DeqSet.λe:pre S.
- lift S (pre_concat_l S eclose e).
+(*
+\ 5h2\ 6Lifted Operators\ 5/h2\ 6
+*)
+
+definition lifted_cat ≝ λ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/chapter8/lift.def(2)"\ 6lift\ 5/a\ 6 S (\ 5a href="cic:/matita/tutorial/chapter8/pre_concat_l.def(3)"\ 6pre_concat_l\ 5/a\ 6 S \ 5a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"\ 6eclose\ 5/a\ 6 e).
notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
-lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
- 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
-#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
+lemma odot_true_b : ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀b.
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i2,b〉 \ 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\ 6i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2)),\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b〉.
+#S #i1 #i2 #b normalize in ⊢ (??%?); cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2) //
qed.
-lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
- 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
+lemma odot_false_b : ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀b.
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i2,b〉 \ 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\ 6i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2 ,b〉.
//
qed.
-lemma erase_odot:∀S.∀e1,e2:pre S.
- |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
-#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //
+lemma erase_odot:∀S.∀e1,e2:\ 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 (e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 e2)| \ 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="re cat" 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|).
+#S * #i1 * * #i2 #b2 // >\ 5a href="cic:/matita/tutorial/chapter8/odot_true_b.def(6)"\ 6odot_true_b\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/erase_dot.def(4)"\ 6erase_dot\ 5/a\ 6 //
qed.
-definition lk ≝ λS:DeqSet.λe:pre S.
+definition lk ≝ λ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.
match e with
[ mk_Prod i1 b1 ⇒
match b1 with
- [true ⇒ 〈(\fst (eclose ? i1))^*, true〉
- |false ⇒ 〈i1^*,false〉
+ [true ⇒ \ 5a title="Pair construction" 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/chapter8/eclose.fix(0,1,4)"\ 6eclose\ 5/a\ 6 ? i1))\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*, \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉
+ |false ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉
]
].
notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
-lemma ostar_true: ∀S.∀i:pitem S.
- 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
+lemma ostar_true: ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛ \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i))\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*, \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉.
// qed.
-lemma ostar_false: ∀S.∀i:pitem S.
- 〈i,false〉^⊛ = 〈i^*, false〉.
+lemma ostar_false: ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛ \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉.
// qed.
-lemma erase_ostar: ∀S.∀e:pre S.
- |\fst (e^⊛)| = |\fst e|^*.
+lemma erase_ostar: ∀S.∀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 (e\ 5a title="lk" 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="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
#S * #i * // qed.
-lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
- \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
+lemma sem_odot_true: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e1:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.∀i.
+ \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] }.
#S #e1 #i
-cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
-#H >H cases (e1 ▹ i) #i1 #b1 cases b1
- [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l /2/
- |/2/
+cut (e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉 \ 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 title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i), \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6(e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉) [//]
+#H >H cases (e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i) #i1 #b1 cases b1
+ [>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 @\ 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/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
qed.
-lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i.
- e1 ⊙ 〈i,false〉 = e1 ▹ i.
+lemma eq_odot_false: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e1:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.∀i.
+ e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i.
#S #e1 #i
-cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//]
-cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
+cut (e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉 \ 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 title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i), \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6(e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉) [//]
+cases (e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i) #i1 #b1 cases b1 #H @H
qed.
lemma sem_odot:
- ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
+ ∀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="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 e2} \ 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{e1}\ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e2|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2}.
#S #e1 * #i2 *
- [>sem_pre_true
- @eqP_trans [|@sem_odot_true]
- @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux //
- |>sem_pre_false >eq_odot_false @odot_dot_aux //
+ [>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_odot_true.def(10)"\ 6sem_odot_true\ 5/a\ 6]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter8/sem_pcl_aux.def(11)"\ 6sem_pcl_aux\ 5/a\ 6 //
+ |>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter8/eq_odot_false.def(6)"\ 6eq_odot_false\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter8/sem_pcl_aux.def(11)"\ 6sem_pcl_aux\ 5/a\ 6 //
]
qed.
-(* theorem 16: 4 *)
-theorem sem_ostar: ∀S.∀e:pre S.
- \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*.
+theorem sem_ostar: ∀S.∀e:\ 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{e\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 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="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
#S * #i #b cases b
- [>sem_pre_true >sem_pre_true >sem_star >erase_bull
- @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [||@eqP_sym @distr_cat_r]
- @eqP_trans [|@union_assoc] @eqP_union_l
- @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
- |>sem_pre_false >sem_pre_false >sem_star /2/
+ [>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter8/erase_bull.def(6)"\ 6erase_bull\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6[|@\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/minus_eps_pre_aux.def(11)"\ 6minus_eps_pre_aux\ 5/a\ 6 //]]]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6]]
+ @\ 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/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6
+ @\ 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/chapter6/epsilon_cat_l.def(5)"\ 6epsilon_cat_l\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/star_fix_eps.def(7)"\ 6star_fix_eps\ 5/a\ 6
+ |>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
-qed.
\ No newline at end of file
+qed.
\ No newline at end of file
projects / helm.git / commitdiff