update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / nstream_istot.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
index 9d2f3cd2b0e74dd8dabf2c7788b3281a57d01845..3a19d81a0f355a306cb9dc2c3402caaa87fd453e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
@@ -31,49 +31,49 @@ interpretation "functional application (nstream)"
 
 (* Specific properties on at ************************************************)
 
-lemma at_O1: â\88\80i2,f. @â¦\830, i2⨮fâ¦\84 ≘ i2.
+lemma at_O1: â\88\80i2,f. @â\9dª0, i2⨮fâ\9d« ≘ i2.
 #i2 elim i2 -i2 /2 width=5 by at_refl, at_next/
 qed.
 
-lemma at_S1: â\88\80n,f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 @â¦\83â\86\91i1, n⨮fâ¦\84 ≘ ↑(n+i2).
+lemma at_S1: â\88\80n,f,i1,i2. @â\9dªi1, fâ\9d« â\89\98 i2 â\86\92 @â\9dªâ\86\91i1, n⨮fâ\9d« ≘ ↑(n+i2).
 #n elim n -n /3 width=7 by at_push, at_next/
 qed.
 
-lemma at_total: â\88\80i1,f. @â¦\83i1, fâ¦\84 â\89\98 f@â\9d´i1â\9dµ.
+lemma at_total: â\88\80i1,f. @â\9dªi1, fâ\9d« â\89\98 f@â\9d¨i1â\9d©.
 #i1 elim i1 -i1
 [ * // | #i #IH * /3 width=1 by at_S1/ ]
 qed.
 
-lemma at_istot: â\88\80f. ð\9d\90\93â¦\83fâ¦\84.
+lemma at_istot: â\88\80f. ð\9d\90\93â\9dªfâ\9d«.
 /2 width=2 by ex_intro/ qed.
 
-lemma at_plus2: â\88\80f,i1,i,n,m. @â¦\83i1, n⨮fâ¦\84 â\89\98 i â\86\92 @â¦\83i1, (m+n)⨮fâ¦\84 ≘ m+i.
+lemma at_plus2: â\88\80f,i1,i,n,m. @â\9dªi1, n⨮fâ\9d« â\89\98 i â\86\92 @â\9dªi1, (m+n)⨮fâ\9d« ≘ m+i.
 #f #i1 #i #n #m #H elim m -m //
 #m <plus_S1 /2 width=5 by at_next/ (**) (* full auto fails *)
 qed.
 
 (* Specific inversion lemmas on at ******************************************)
 
-lemma at_inv_O1: â\88\80f,n,i2. @â¦\830, n⨮fâ¦\84 ≘ i2 → n = i2.
+lemma at_inv_O1: â\88\80f,n,i2. @â\9dª0, n⨮fâ\9d« ≘ i2 → n = i2.
 #f #n elim n -n /2 width=6 by at_inv_ppx/
 #n #IH #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
 #j2 #Hj * -i2 /3 width=1 by eq_f/
 qed-.
 
-lemma at_inv_S1: â\88\80f,n,j1,i2. @â¦\83â\86\91j1, n⨮fâ¦\84 ≘ i2 →
-                 â\88\83â\88\83j2. @â¦\83j1, fâ¦\84 ≘ j2 & ↑(n+j2) = i2.
+lemma at_inv_S1: â\88\80f,n,j1,i2. @â\9dªâ\86\91j1, n⨮fâ\9d« ≘ i2 →
+                 â\88\83â\88\83j2. @â\9dªj1, fâ\9d« ≘ j2 & ↑(n+j2) = i2.
 #f #n elim n -n /2 width=5 by at_inv_npx/
 #n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
 #j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
 #i2 #Hi * -j2 /2 width=3 by ex2_intro/
 qed-.
 
-lemma at_inv_total: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89\98 i2 â\86\92 f@â\9d´i1â\9dµ = i2.
+lemma at_inv_total: â\88\80f,i1,i2. @â\9dªi1, fâ\9d« â\89\98 i2 â\86\92 f@â\9d¨i1â\9d© = i2.
 /2 width=6 by at_mono/ qed-.
 
 (* Spercific forward lemmas on at *******************************************)
 
-lemma at_increasing_plus: â\88\80f,n,i1,i2. @â¦\83i1, n⨮fâ¦\84 ≘ i2 → i1 + n ≤ i2.
+lemma at_increasing_plus: â\88\80f,n,i1,i2. @â\9dªi1, n⨮fâ\9d« ≘ i2 → i1 + n ≤ i2.
 #f #n *
 [ #i2 #H <(at_inv_O1 … H) -i2 //
 | #i1 #i2 #H elim (at_inv_S1 … H) -H
@@ -81,35 +81,35 @@ lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n⨮f⦄ ≘ i2 → i1 + n ≤ i
 ]
 qed-.
 
-lemma at_fwd_id: â\88\80f,n,i. @â¦\83i, n⨮fâ¦\84 ≘ i → 0 = n.
+lemma at_fwd_id: â\88\80f,n,i. @â\9dªi, n⨮fâ\9d« ≘ i → 0 = n.
 #f #n #i #H elim (at_fwd_id_ex … H) -H
 #g #H elim (push_inv_seq_dx … H) -H //
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma apply_O1: â\88\80n,f. (n⨮f)@â\9d´0â\9dµ = n.
+lemma apply_O1: â\88\80n,f. (n⨮f)@â\9d¨0â\9d© = n.
 // qed.
 
-lemma apply_S1: â\88\80n,f,i. (n⨮f)@â\9d´â\86\91iâ\9dµ = â\86\91(n+f@â\9d´iâ\9dµ).
+lemma apply_S1: â\88\80n,f,i. (n⨮f)@â\9d¨â\86\91iâ\9d© = â\86\91(n+f@â\9d¨iâ\9d©).
 // qed.
 
-lemma apply_eq_repl (i): eq_repl â\80¦ (λf1,f2. f1@â\9d´iâ\9dµ = f2@â\9d´iâ\9dµ).
+lemma apply_eq_repl (i): eq_repl â\80¦ (λf1,f2. f1@â\9d¨iâ\9d© = f2@â\9d¨iâ\9d©).
 #i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H
 elim (eq_inv_seq_aux … H) -H normalize //
 #Hn #Hf /4 width=1 by eq_f2, eq_f/
 qed.
 
-lemma apply_S2: â\88\80f,i. (â\86\91f)@â\9d´iâ\9dµ = â\86\91(f@â\9d´iâ\9dµ).
+lemma apply_S2: â\88\80f,i. (â\86\91f)@â\9d¨iâ\9d© = â\86\91(f@â\9d¨iâ\9d©).
 * #n #f * //
 qed.
 
 (* Main inversion lemmas ****************************************************)
 
-theorem apply_inj: â\88\80f,i1,i2,j. f@â\9d´i1â\9dµ = j â\86\92 f@â\9d´i2â\9dµ = j → i1 = i2.
+theorem apply_inj: â\88\80f,i1,i2,j. f@â\9d¨i1â\9d© = j â\86\92 f@â\9d¨i2â\9d© = j → i1 = i2.
 /2 width=4 by at_inj/ qed-.
 
-corec theorem nstream_eq_inv_ext: â\88\80f1,f2. (â\88\80i. f1@â\9d´iâ\9dµ = f2@â\9d´iâ\9dµ) → f1 ≗ f2.
+corec theorem nstream_eq_inv_ext: â\88\80f1,f2. (â\88\80i. f1@â\9d¨iâ\9d© = f2@â\9d¨iâ\9d©) → f1 ≗ f2.
 * #n1 #f1 * #n2 #f2 #Hf @eq_seq
 [ @(Hf 0)
 | @nstream_eq_inv_ext -nstream_eq_inv_ext #i