X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream_istot.ma;h=3a19d81a0f355a306cb9dc2c3402caaa87fd453e;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hp=759b83a13026dce98c53cf4e8f2b0e9aaae8e55a;hpb=75f395f0febd02de8e0f881d918a8812b1425c8d;p=helm.git

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 759b83a13..3a19d81a0 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
@@ -22,7 +22,7 @@ rec definition apply (i: nat) on i: rtmap → nat ≝ ?.
 * #n #f cases i -i
 [ @n
 | #i lapply (apply i f) -apply -i -f
-  #i @(⫯(n+i))
+  #i @(↑(n+i))
 ]
 defined.
 
@@ -31,49 +31,49 @@ interpretation "functional application (nstream)"
 
 (* Specific properties on at ************************************************)
 
-lemma at_O1: ∀i2,f. @⦃0, i2@f⦄ ≘ i2.
+lemma at_O1: ∀i2,f. @❪0, i2⨮f❫ ≘ i2.
 #i2 elim i2 -i2 /2 width=5 by at_refl, at_next/
 qed.
 
-lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≘ i2 → @⦃⫯i1, n@f⦄ ≘ ⫯(n+i2).
+lemma at_S1: ∀n,f,i1,i2. @❪i1, f❫ ≘ i2 → @❪↑i1, n⨮f❫ ≘ ↑(n+i2).
 #n elim n -n /3 width=7 by at_push, at_next/
 qed.
 
-lemma at_total: ∀i1,f. @⦃i1, f⦄ ≘ f@❴i1❵.
+lemma at_total: ∀i1,f. @❪i1, f❫ ≘ f@❨i1❩.
 #i1 elim i1 -i1
 [ * // | #i #IH * /3 width=1 by at_S1/ ]
 qed.
 
-lemma at_istot: ∀f. 𝐓⦃f⦄.
+lemma at_istot: ∀f. 𝐓❪f❫.
 /2 width=2 by ex_intro/ qed.
 
-lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≘ i → @⦃i1, (m+n)@f⦄ ≘ m+i.
+lemma at_plus2: ∀f,i1,i,n,m. @❪i1, n⨮f❫ ≘ i → @❪i1, (m+n)⨮f❫ ≘ 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: ∀f,n,i2. @⦃0, n@f⦄ ≘ i2 → n = i2.
+lemma at_inv_O1: ∀f,n,i2. @❪0, n⨮f❫ ≘ 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: ∀f,n,j1,i2. @⦃⫯j1, n@f⦄ ≘ i2 →
-                 ∃∃j2. @⦃j1, f⦄ ≘ j2 & ⫯(n+j2) = i2.
+lemma at_inv_S1: ∀f,n,j1,i2. @❪↑j1, n⨮f❫ ≘ i2 →
+                 ∃∃j2. @❪j1, f❫ ≘ 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: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 → f@❴i1❵ = i2.
+lemma at_inv_total: ∀f,i1,i2. @❪i1, f❫ ≘ i2 → f@❨i1❩ = i2.
 /2 width=6 by at_mono/ qed-.
 
 (* Spercific forward lemmas on at *******************************************)
 
-lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n@f⦄ ≘ i2 → i1 + n ≤ i2.
+lemma at_increasing_plus: ∀f,n,i1,i2. @❪i1, n⨮f❫ ≘ i2 → i1 + n ≤ i2.
 #f #n *
 [ #i2 #H <(at_inv_O1 … H) -i2 //
 | #i1 #i2 #H elim (at_inv_S1 … H) -H
@@ -81,24 +81,40 @@ lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n@f⦄ ≘ i2 → i1 + n ≤ i2.
 ]
 qed-.
 
-lemma at_fwd_id: ∀f,n,i. @⦃i, n@f⦄ ≘ i → 0 = n.
+lemma at_fwd_id: ∀f,n,i. @❪i, n⨮f❫ ≘ 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_eq_repl (i): eq_repl … (λf1,f2. f1@❴i❵ = f2@❴i❵).
+lemma apply_O1: ∀n,f. (n⨮f)@❨0❩ = n.
+// qed.
+
+lemma apply_S1: ∀n,f,i. (n⨮f)@❨↑i❩ = ↑(n+f@❨i❩).
+// qed.
+
+lemma apply_eq_repl (i): eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
 #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_S1: ∀f,i. (⫯f)@❴i❵ = ⫯(f@❴i❵).
+lemma apply_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
 * #n #f * //
 qed.
 
 (* Main inversion lemmas ****************************************************)
 
-theorem apply_inj: ∀f,i1,i2,j. f@❴i1❵ = j → f@❴i2❵ = j → i1 = i2.
+theorem apply_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
 /2 width=4 by at_inj/ qed-.
+
+corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
+* #n1 #f1 * #n2 #f2 #Hf @eq_seq
+[ @(Hf 0)
+| @nstream_eq_inv_ext -nstream_eq_inv_ext #i
+  lapply (Hf 0) >apply_O1 >apply_O1 #H destruct
+  lapply (Hf (↑i)) >apply_S1 >apply_S1 #H
+  /3 width=2 by injective_plus_r, injective_S/
+]
+qed-.