X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fmodels%2Fincreasing_supremum_stabilizes.ma;h=fc4424e5ec7cde8616c68e0d96d237cfc37baa4e;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=f84b740441602122456119aa101139489fb58c86;hpb=fdab21f9db0c8536718001e38213c34595170182;p=helm.git

diff --git a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
index f84b74044..fc4424e5e 100644
--- a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
+++ b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
@@ -35,7 +35,7 @@ lemma increasing_supremum_stabilizes:
 intros 4; cases X (x Hx); clear X; letin X ≝ ≪x,Hx≫; 
 fold normalize X; intros; cases H1; 
 alias symbol "N" = "Natural numbers".
-letin spec ≝ (λi,j:ℕ.(𝕦_sg ≤ i ∧ x = \fst (a j)) ∨ (i < 𝕦_sg ∧ x + i ≤ 𝕦_sg + \fst (a j))); 
+letin spec ≝ (λi,j:ℕ.(𝕦_ sg ≤ i ∧ x = \fst (a j)) ∨ (i < 𝕦_ sg ∧ x + i ≤ 𝕦_ sg + \fst (a j))); 
 (* x - aj <= max 0 (u - i) *)  
 letin m ≝ (hide ? (
   let rec aux i ≝
@@ -52,7 +52,7 @@ letin m ≝ (hide ? (
    ∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %;
 [3: unfold X in H2; clear H4 n aux spec H3 H1 H X;
     cases (cases_in_segment ??? Hx);
-    elim 𝕦_sg in H1 ⊢ %; intros (a Hs H);
+    elim 𝕦_ sg in H1 ⊢ %; intros (a Hs H);
     [1: left; split; [apply le_n]
         generalize in match H;
         generalize in match Hx;
@@ -77,9 +77,9 @@ letin m ≝ (hide ? (
     cases H5; clear H5; cases H7; clear H7;
     [1: left; split; [ apply (le_S ?? H5); | assumption]
     |3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
-    |*: cases (cmp_nat 𝕦_sg (S n1));
+    |*: cases (cmp_nat 𝕦_ sg (S n1));
         [1,3: left; split; [1,3: assumption |2: assumption]
-            cut (𝕦_sg = S n1); [2: apply le_to_le_to_eq; assumption ]
+            cut (𝕦_ sg = S n1); [2: apply le_to_le_to_eq; assumption ]
             clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
             cut (x = S (\fst (a w)));
             [2: apply le_to_le_to_eq; [2: assumption]
@@ -95,7 +95,7 @@ letin m ≝ (hide ? (
             [1: rewrite > sym_plus in ⊢ (? ? %);
                 rewrite < H6; apply le_plus_r; assumption;
             |2: cases (H3 (a w) H6);
-                change with (x + S n1 ≤ 𝕦_sg + \fst (a w1));rewrite < plus_n_Sm;
+                change with (x + S n1 ≤ 𝕦_ sg + \fst (a w1));rewrite < plus_n_Sm;
                 apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
                 apply (le_plus ???? (le_n ?) H9);]]]]
 clearbody m; unfold spec in m; clear spec;
@@ -109,14 +109,14 @@ letin find ≝ (
           | false ⇒ find (S i) w]]
  in find
  :
-  ∀i,bound.∃j.i + bound = 𝕦_sg → x = \fst (a j));
+  ∀i,bound.∃j.i + bound = 𝕦_ sg → x = \fst (a j));
 [1: cases (find (S n) n2); intro; change with (x = \fst (a w));
     apply H6; rewrite < H7; simplify; apply plus_n_Sm;
 |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
 |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
-    cases (m 𝕦_sg); cases H4; clear H4; cases H5; clear H5; [assumption]
+    cases (m 𝕦_ sg); cases H4; clear H4; cases H5; clear H5; [assumption]
     cases (not_le_Sn_n ? H4)]
-clearbody find; cases (find O 𝕦_sg);
+clearbody find; cases (find O 𝕦_ sg);
 exists [apply w]; intros; change with (x = \fst (a j));
 rewrite > (H4 ?); [2: reflexivity]
 apply le_to_le_to_eq;