From fe7d9f4665e92d9c6934988b2b215547ab7ecf3f Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 4 May 2012 15:14:44 +0000
Subject: [PATCH]

---
 matita/matita/lib/basics/bool.ma |  2 +-
 matita/matita/lib/basics/sets.ma | 36 +++++++++++++--------------
 matita/matita/lib/re/lang.ma     | 22 ++++++++---------
 matita/matita/lib/re/moves.ma    | 17 +++++--------
 matita/matita/lib/re/re.ma       | 42 ++++++++++++++++----------------
 matita/matita/lib/re/reb.ma      |  6 ++---
 6 files changed, 60 insertions(+), 65 deletions(-)

diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma
index 587ab9ed6..0d790efc5 100644
--- a/matita/matita/lib/basics/bool.ma
+++ b/matita/matita/lib/basics/bool.ma
@@ -97,7 +97,7 @@ definition xorb : bool → bool → bool ≝
 notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
  for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
 notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46
- for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
+ for @{ match $e return $T with [ true ⇒ $t | false ⇒ $f]  }.
 
 theorem bool_to_decidable_eq: 
   ∀b1,b2:bool. decidable (b1=b2).
diff --git a/matita/matita/lib/basics/sets.ma b/matita/matita/lib/basics/sets.ma
index 4d77f6c2f..7c791da41 100644
--- a/matita/matita/lib/basics/sets.ma
+++ b/matita/matita/lib/basics/sets.ma
@@ -38,81 +38,81 @@ interpretation "subset" 'subseteq a b = (subset ? a b).
 
 (* extensional equality *)
 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
-notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
+notation "A ≐ B" non associative with precedence 45 for @{'eqP $A $B}.
 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
 
 lemma eqP_sym: ∀U.∀A,B:U →Prop. 
-  A =1 B → B =1 A.
+  A ≐ B → B ≐ A.
 #U #A #B #eqAB #a @iff_sym @eqAB qed.
  
 lemma eqP_trans: ∀U.∀A,B,C:U →Prop. 
-  A =1 B → B =1 C → A =1 C.
+  A ≐ B → B ≐ C → A ≐ C.
 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
 
 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
-  A =1 C  → A ∪ B =1 C ∪ B.
+  A ≐ C  → A ∪ B ≐ C ∪ B.
 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
   
 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. 
-  B =1 C  → A ∪ B =1 A ∪ C.
+  B ≐ C  → A ∪ B ≐ A ∪ C.
 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
   
 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop. 
-  A =1 C  → A ∩ B =1 C ∩ B.
+  A ≐ C  → A ∩ B ≐ C ∩ B.
 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
   
 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. 
-  B =1 C  → A ∩ B =1 A ∩ C.
+  B ≐ C  → A ∩ B ≐ A ∩ C.
 #U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
 
 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. 
-  A =1 C  → A - B =1 C - B.
+  A ≐ C  → A - B ≐ C - B.
 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
   
 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. 
-  B =1 C  → A - B =1 A - C.
+  B ≐ C  → A - B ≐ A - C.
 #U #A #B #C #eqBC #a @iff_and_l /2/ qed.
 
 (* set equalities *)
 lemma union_empty_r: ∀U.∀A:U→Prop. 
-  A ∪ ∅ =1 A.
+  A ∪ ∅ ≐ A.
 #U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
 qed.
 
 lemma union_comm : ∀U.∀A,B:U →Prop. 
-  A ∪ B =1 B ∪ A.
+  A ∪ B ≐ B ∪ A.
 #U #A #B #a % * /2/ qed. 
 
 lemma union_assoc: ∀U.∀A,B,C:U → Prop. 
-  A ∪ B ∪ C =1 A ∪ (B ∪ C).
+  A ∪ B ∪ C ≐ A ∪ (B ∪ C).
 #S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
 qed.   
 
 lemma cap_comm : ∀U.∀A,B:U →Prop. 
-  A ∩ B =1 B ∩ A.
+  A ∩ B ≐ B ∩ A.
 #U #A #B #a % * /2/ qed. 
 
 lemma union_idemp: ∀U.∀A:U →Prop. 
-  A ∪ A =1 A.
+  A ∪ A ≐ A.
 #U #A #a % [* // | /2/] qed. 
 
 lemma cap_idemp: ∀U.∀A:U →Prop. 
-  A ∩ A =1 A.
+  A ∩ A ≐ A.
 #U #A #a % [* // | /2/] qed. 
 
 (*distributivities *)
 
 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop. 
-  (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
+  (A ∪ B) ∩ C ≐ (A ∩ C) ∪ (B ∩ C).
 #U #A #B #C #w % [* * /3/ | * * /3/] 
 qed.
   
 lemma distribute_substract : ∀U.∀A,B,C:U→Prop. 
-  (A ∪ B) - C =1 (A - C) ∪ (B - C).
+  (A ∪ B) - C ≐ (A - C) ∪ (B - C).
 #U #A #B #C #w % [* * /3/ | * * /3/] 
 qed.
 
 (* substraction *)
-lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
+lemma substract_def:∀U.∀A,B:U→Prop. A-B ≐ A ∩ ¬B.
 #U #A #B #w normalize /2/
 qed.
\ No newline at end of file
diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma
index aedf4c131..9f40045ae 100644
--- a/matita/matita/lib/re/lang.ma
+++ b/matita/matita/lib/re/lang.ma
@@ -42,23 +42,23 @@ notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
 interpretation "star lang" 'star l = (star ? l).
 
 lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop. 
-  A =1 C  → A · B =1 C · B.
+  A ≐ C  → A · B ≐ C · B.
 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
 cases (H w1) /6/ 
 qed.
 
 lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop. 
-  B =1 C → A · B =1 A · C.
+  B ≐ C → A · B ≐ A · C.
 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
 cases (H w2) /6/ 
 qed.
   
-lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅.
+lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A ≐ ∅.
 #S #A #w % [|*] * #w1 * #w2 * * #_ *
 qed.
 
 lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
-  (A ∪ B) · C =1  A · C ∪ B · C. 
+  (A ∪ B) · C ≐  A · C ∪ B · C. 
 #S #A #B #C #w %
   [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/] 
 qed.
@@ -68,7 +68,7 @@ qed.
 definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
 
 lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ → 
-  deriv S (A·B) a =1 (deriv S A a) · B.
+  deriv S (A·B) a ≐ (deriv S A a) · B.
 #S #A #B #a #noteps #w normalize %
   [* #w1 cases w1 
     [* #w2 * * #_ #Aeps @False_ind /2/
@@ -93,7 +93,7 @@ lemma cat_to_star:∀S.∀A:word S → Prop.
 qed.
 
 lemma fix_star: ∀S.∀A:word S → Prop. 
-  A^* =1 A · A^* ∪ {ϵ}.
+  A^* ≐ A · A^* ∪ {ϵ}.
 #S #A #w %
   [* #l generalize in match w; -w cases l [normalize #w * /2/]
    #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
@@ -105,7 +105,7 @@ lemma fix_star: ∀S.∀A:word S → Prop.
 qed.
 
 lemma star_fix_eps : ∀S.∀A:word S → Prop.
-  A^* =1 (A - {ϵ}) · A^* ∪ {ϵ}.  
+  A^* ≐ (A - {ϵ}) · A^* ∪ {ϵ}.  
 #S #A #w %
   [* #l elim l 
     [* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw // 
@@ -122,12 +122,12 @@ lemma star_fix_eps : ∀S.∀A:word S → Prop.
 qed. 
      
 lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
-  A^* ∪ {ϵ} =1 A^*.
+  A^* ∪ {ϵ} ≐ A^*.
 #S #A #w % /2/ * // 
 qed.
   
 lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
-   A · {ϵ} =1  A. 
+   A · {ϵ} ≐  A. 
 #S #A #w %
   [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
   |#inA @(ex_intro … w) @(ex_intro … [ ]) /3/
@@ -135,7 +135,7 @@ lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
 qed.
 
 lemma epsilon_cat_l: ∀S.∀A:word S →Prop.
-   {ϵ} · A =1  A. 
+   {ϵ} · A ≐  A. 
 #S #A #w %
   [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
   |#inA @(ex_intro … ϵ) @(ex_intro … w) /3/
@@ -143,7 +143,7 @@ lemma epsilon_cat_l: ∀S.∀A:word S →Prop.
 qed.
 
 lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop.
-  (A ∪ {ϵ}) · C =1  A · C ∪ C. 
+  (A ∪ {ϵ}) · C ≐  A · C ∪ C. 
 #S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
 qed.
 
diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma
index 582531777..3445d9472 100644
--- a/matita/matita/lib/re/moves.ma
+++ b/matita/matita/lib/re/moves.ma
@@ -211,7 +211,7 @@ e1 and e2 are equivalent iff for any word w the states reachable
 through w are cofinal. *)
 
 theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S. 
-  \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+  \sem{e1} ≐ \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
 #S #e1 #e2 % 
 [#same_sem #w 
   cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2)) 
@@ -244,7 +244,7 @@ occurring the given regular expressions. *)
 
 lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
-→ \sem{e1}=1\sem{e2}.
+→ \sem{e1}≐\sem{e2}.
 #S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H 
 qed.
 
@@ -273,7 +273,7 @@ definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
 (* Using lemma equiv_sem_occ it is easy to prove the following result: *)
 
 lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S. 
-  is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
+  is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}≐\sem{e2}.
 #S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ 
 #w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
 lapply Hsub @(list_elim_left … w) [//]
@@ -428,7 +428,7 @@ uniqueb ? l = true ∧
 definition disjoint ≝ λS:DeqSet.λl1,l2.
   ∀p:S. memb S p l1 = true →  memb S p l2 = false.
         
-lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} → 
+lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}≐\sem{e2} → 
  ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
  |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
  all_reachable S e1 e2 visited →  
@@ -544,7 +544,7 @@ definition equiv ≝ λSig.λre1,re2:re Sig.
   (bisim ? sig n [〈e1,e2〉] []).
 
 theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
-   \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
+   \fst (equiv ? e1 e2) = true ↔ \sem{e1} ≐ \sem{e2}.
 #Sig #re1 #re2 %
   [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
    cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
@@ -611,9 +611,4 @@ definition exp10 ≝ a·a·a·a·a·a·a·a·a·a·a·a·(a^* ).
 definition exp11 ≝ (a·a·a·a·a + a·a·a·a·a·a·a)^*.
 
 example ex2 : \fst (equiv ? (exp10+exp11) exp10) = true.
-normalize // qed.
-
-
-
-
-\v
\ No newline at end of file
+normalize // qed.
\ No newline at end of file
diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma
index 60c200e6c..af0e921a6 100644
--- a/matita/matita/lib/re/re.ma
+++ b/matita/matita/lib/re/re.ma
@@ -274,8 +274,8 @@ lemma sem_star_w : ∀S.∀i:pitem S.∀w.
 (* Below are a few, simple, semantic properties of items. In particular:
 - not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
 - epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
-- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
-- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} ≐ \sem{e}-{[ ]}.
 The first property is proved by a simple induction on $i$; the other
 results are easy corollaries. We need an auxiliary lemma first. *)
 
@@ -299,14 +299,14 @@ lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
 #S * #i #b #btrue normalize in btrue; >btrue %2 // 
 qed.
 
-lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
 #S #i #w % 
   [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
   |* //
   ]
 qed.
 
-lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} ≐ \sem{e}-{[ ]}.
 #S * #i * 
   [>sem_pre_true normalize in ⊢ (??%?); #w % 
     [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
@@ -374,11 +374,11 @@ interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
 (* The behaviour of ◃ is summarized by the following, easy lemma: *)
 
 lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop. 
-  A = B → A =1 B. 
+  A = B → A ≐ B. 
 #S #A #B #H >H /2/ qed.
 
 lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
-  \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
+  \sem{i ◃ e} ≐ \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
 #S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //] 
 >sem_pre_true >sem_cat >sem_pre_true /2/ 
 qed.
@@ -471,14 +471,14 @@ qed.
 
 (* 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|}
+sem_oplus:     \sem{e1 ⊕ e2} ≐ \sem{e1} ∪ \sem{e2} 
+sem_pcl:       \sem{e1 ▹ i2} ≐  \sem{e1} · \sem{|i2|} ∪ \sem{i2}
+sem_bullet     \sem{•i} ≐ \sem{i} ∪ \sem{|i|}
 
 The proof of sem_oplus is straightforward. *)
 
 lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
-  \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}. 
+  \sem{e1 ⊕ e2} ≐ \sem{e1} ∪ \sem{e2}. 
 #S * #i1 #b1 * #i2 #b2 #w %
   [cases b1 cases b2 normalize /2/ * /3/ * /3/
   |cases b1 cases b2 normalize /2/ * /3/ * /3/
@@ -489,8 +489,8 @@ qed.
 auxiliary lemma, that assumes sem_bullet:
 
 sem_pcl_aux: 
-   \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
-   \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+   \sem{•i2} ≐  \sem{i2} ∪ \sem{|i2|} →
+   \sem{e1 ▹ i2} ≐  \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. *)
@@ -500,8 +500,8 @@ lemma LcatE : ∀S.∀e1,e2:pitem S.
 // qed.
 
 lemma odot_dot_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}.
+   \sem{•i2} ≐  \sem{i2} ∪ \sem{|i2|} →
+   \sem{e1 ▹ i2} ≐  \sem{e1} · \sem{|i2|} ∪ \sem{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 …))
@@ -512,7 +512,7 @@ lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
 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 - {[ ]}).
+ \sem{e} ≐ \sem{i} ∪ A → \sem{\fst e} ≐ \sem{i} ∪ (A - {[ ]}).
 #S #e #i #A #seme
 @eqP_trans [|@minus_eps_pre]
 @eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
@@ -520,7 +520,7 @@ lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
 @eqP_substract_r //
 qed.
 
-theorem sem_bull: ∀S:DeqSet. ∀i:pitem S.  \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
+theorem sem_bull: ∀S:DeqSet. ∀i:pitem S.  \sem{•i} ≐ \sem{i} ∪ \sem{|i|}.
 #S #e elim e 
   [#w normalize % [/2/ | * //]
   |/2/ 
@@ -583,7 +583,7 @@ lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
 #S #e elim e normalize //
 qed.
 
-lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
+lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} ≐ ∅.
 #S #e elim e 
   [1,2:@eq_to_ex_eq // 
   |#s @eq_to_ex_eq //
@@ -600,7 +600,7 @@ lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
 qed.
    
 theorem re_embedding: ∀S.∀e:re S. 
-  \sem{•(blank S e)} =1 \sem{e}.
+  \sem{•(blank S e)} ≐ \sem{e}.
 #S #e @eqP_trans [|@sem_bull] >forget_blank 
 @eqP_trans [|@eqP_union_r [|@sem_blank]]
 @eqP_trans [|@union_comm] @union_empty_r.
@@ -663,7 +663,7 @@ lemma erase_ostar: ∀S.∀e:pre S.
 #S * #i * // qed.
 
 lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i. 
-  \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
+  \sem{e1 ⊙ 〈i,true〉} ≐ \sem{e1 ▹ i} ∪ { [ ] }.
 #S #e1 #i 
 cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
 #H >H cases (e1 ▹ i) #i1 #b1 cases b1 
@@ -684,7 +684,7 @@ qed.
 of ⊙ and ⊛. *)
 
 lemma sem_odot: 
-  ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
+  ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} ≐ \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
 #S #e1 * #i2 * 
   [>sem_pre_true 
    @eqP_trans [|@sem_odot_true]
@@ -694,7 +694,7 @@ lemma sem_odot:
 qed.
       
 theorem sem_ostar: ∀S.∀e:pre S. 
-  \sem{e^⊛} =1  \sem{e} · \sem{|\fst e|}^*.
+  \sem{e^⊛} ≐  \sem{e} · \sem{|\fst e|}^*.
 #S * #i #b cases b
   [(* lhs = \sem{〈i,true〉^⊛} *)
    >sem_pre_true (* >sem_pre_true *) 
diff --git a/matita/matita/lib/re/reb.ma b/matita/matita/lib/re/reb.ma
index e1d85641f..f4cd2e6c1 100644
--- a/matita/matita/lib/re/reb.ma
+++ b/matita/matita/lib/re/reb.ma
@@ -253,11 +253,11 @@ definition reclose ≝ lift eclose.
 interpretation "reclose" 'eclose x = (reclose ? x).
 
 definition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w.
-notation "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
+notation "A ≐ B" non associative with precedence 45 for @{'eq_f1 $A $B}.
 interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b).
 
 (*
-lemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) =1 ϵ b1 ∪ ϵ b2. 
+lemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) ≐ ϵ b1 ∪ ϵ b2. 
 ##[##2: napply S]
 #S b1 b2; ncases b1; ncases b2; napply extP; #w; nnormalize; @; /2/; *; //; *;
 nqed.
@@ -269,7 +269,7 @@ nlemma cupC : ∀S. ∀a,b:word S → Prop.a ∪ b = b ∪ a.
 #S a b; napply extP; #w; @; *; nnormalize; /2/; nqed.*)
 
 (* theorem 16: 2 *)
-lemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.\sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+lemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.\sem{e1 ⊕ e2} ≐ \sem{e1} ∪ \sem{e2}.
 #S * #i1 #b1  * #i2 #b2 >lo_def normalize in ⊢ (?%?);
 
 #w cases b1 cases b2 normalize % #w r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2;
-- 
2.39.2