X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Fitem_sd.ma;h=15be7977f97603926763746d5b563629c498c1d3;hp=3387066d34e65bc6805a86051e04442258d442eb;hb=222044da28742b24584549ba86b1805a87def070;hpb=09b4420070d6a71990e16211e499b51dbb0742cb

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/item_sd.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/item_sd.ma
index 3387066d3..15be7977f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/item_sd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/item_sd.ma
@@ -21,7 +21,7 @@ record sd (h:sh): Type[0] ≝ {
    deg      : relation nat;                            (* degree of the sort *)
    deg_total: ∀s. ∃d. deg s d;                         (* functional relation axioms *)
    deg_mono : ∀s,d1,d2. deg s d1 → deg s d2 → d1 = d2;
-   deg_next : ∀s,d. deg s d → deg (next h s) (⫰d)      (* compatibility condition *)
+   deg_next : ∀s,d. deg s d → deg (next h s) (↓d)      (* compatibility condition *)
 }.
 
 (* Notable specifications ***************************************************)
@@ -33,11 +33,11 @@ definition sd_O: ∀h. sd h ≝ λh. mk_sd h deg_O ….
 
 (* Basic_2A1: includes: deg_SO_pos *)
 inductive deg_SO (h:sh) (s:nat) (s0:nat): predicate nat ≝
-| deg_SO_succ : ∀n. (next h)^n s0 = s → deg_SO h s s0 (⫯n)
+| deg_SO_succ : ∀n. (next h)^n s0 = s → deg_SO h s s0 (↑n)
 | deg_SO_zero: ((∃n. (next h)^n s0 = s) → ⊥) → deg_SO h s s0 0
 .
 
-fact deg_SO_inv_succ_aux: ∀h,s,s0,n0. deg_SO h s s0 n0 → ∀n. n0 = ⫯n →
+fact deg_SO_inv_succ_aux: ∀h,s,s0,n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n →
                           (next h)^n s0 = s.
 #h #s #s0 #n0 * -n0
 [ #n #Hn #x #H destruct //
@@ -46,7 +46,7 @@ fact deg_SO_inv_succ_aux: ∀h,s,s0,n0. deg_SO h s s0 n0 → ∀n. n0 = ⫯n →
 qed-.
 
 (* Basic_2A1: was: deg_SO_inv_pos *)
-lemma deg_SO_inv_succ: ∀h,s,s0,n. deg_SO h s s0 (⫯n) → (next h)^n s0 = s.
+lemma deg_SO_inv_succ: ∀h,s,s0,n. deg_SO h s s0 (↑n) → (next h)^n s0 = s.
 /2 width=3 by deg_SO_inv_succ_aux/ qed-.
 
 lemma deg_SO_refl: ∀h,s. deg_SO h s s 1.
@@ -80,7 +80,7 @@ definition sd_SO: ∀h. nat → sd h ≝ λh,s. mk_sd h (deg_SO h s) ….
   [ #d #H destruct elim d -d normalize
     /2 width=1 by deg_SO_gt, deg_SO_succ, next_lt/
   | #H1 @deg_SO_zero * #d #H2 destruct
-    @H1 -H1 @(ex_intro … (⫯d)) /2 width=1 by sym_eq/ (**) (* explicit constructor *)
+    @H1 -H1 @(ex_intro … (↑d)) /2 width=1 by sym_eq/ (**) (* explicit constructor *)
   ]
 ]
 defined.
@@ -96,14 +96,14 @@ rec definition sd_d (h:sh) (s:nat) (d:nat) on d : sd h ≝
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma deg_inv_pred: ∀h,o,s,d. deg h o (next h s) (⫯d) → deg h o s (⫯⫯d).
+lemma deg_inv_pred: ∀h,o,s,d. deg h o (next h s) (↑d) → deg h o s (↑↑d).
 #h #o #s #d #H1
 elim (deg_total h o s) #n #H0
 lapply (deg_next … H0) #H2
 lapply (deg_mono … H1 H2) -H1 -H2 #H >H >S_pred /2 width=2 by ltn_to_ltO/
 qed-.
 
-lemma deg_inv_prec: ∀h,o,s,n,d. deg h o ((next h)^n s) (⫯d) → deg h o s (⫯(d+n)).
+lemma deg_inv_prec: ∀h,o,s,n,d. deg h o ((next h)^n s) (↑d) → deg h o s (↑(d+n)).
 #h #o #s #n elim n -n normalize /3 width=1 by deg_inv_pred/
 qed-.
 
@@ -113,10 +113,10 @@ lemma deg_iter: ∀h,o,s,d,n. deg h o s d → deg h o ((next h)^n s) (d-n).
 #h #o #s #d #n elim n -n normalize /3 width=1 by deg_next/
 qed.
 
-lemma deg_next_SO: ∀h,o,s,d. deg h o s (⫯d) → deg h o (next h s) d.
+lemma deg_next_SO: ∀h,o,s,d. deg h o s (↑d) → deg h o (next h s) d.
 /2 width=1 by deg_next/ qed-.
 
-lemma sd_d_SS: ∀h,s,d. sd_d h s (⫯⫯d) = sd_d h (next h s) (⫯d).
+lemma sd_d_SS: ∀h,s,d. sd_d h s (↑↑d) = sd_d h (next h s) (↑d).
 // qed.
 
 lemma sd_d_correct: ∀h,d,s. deg h (sd_d h s d) s d.