X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream_after.ma;h=6ce6fa476a68bc4e2ed4587653a9f4e0d25b2677;hb=053be41a8db6aa0ca7cc06fb569ec284a9bcc5ef;hp=977a0ca023eeab6e57f90f744303bfcb4c03ebe3;hpb=5b93ea047903b606979705ed25a6df6504fd027c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
index 977a0ca02..6ce6fa476 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
@@ -19,7 +19,7 @@ include "ground_2/relocation/rtmap_after.ma".
 
 corec definition compose: rtmap → rtmap → rtmap.
 #f2 * #n1 #f1 @(seq … (f2@❴n1❵)) @(compose ? f1) -compose -f1
-@(↓*[⫯n1] f2)
+@(⫰*[↑n1] f2)
 defined.
 
 interpretation "functional composition (nstream)"
@@ -27,61 +27,61 @@ interpretation "functional composition (nstream)"
 
 (* Basic properies on compose ***********************************************)
 
-lemma compose_rew: ∀f2,f1,n1. f2@❴n1❵@(↓*[⫯n1]f2)∘f1 = f2∘(n1@f1).
-#f2 #f1 #n1 <(stream_rew … (f2∘(n1@f1))) normalize //
+lemma compose_rew: ∀f2,f1,n1. f2@❴n1❵⨮(⫰*[↑n1]f2)∘f1 = f2∘(n1⨮f1).
+#f2 #f1 #n1 <(stream_rew … (f2∘(n1⨮f1))) normalize //
 qed.
 
-lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (⫯f2)∘f1 = ⫯f.
+lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
 #f2 * #n1 #f1 #f <compose_rew <compose_rew
 * -f <tls_S1 /2 width=1 by eq_f2/
 qed.
 
 (* Basic inversion lemmas on compose ****************************************)
 
-lemma compose_inv_rew: ∀f2,f1,f,n1,n. f2∘(n1@f1) = n@f →
-                       f2@❴n1❵ = n ∧ (↓*[⫯n1]f2)∘f1 = f.
-#f2 #f1 #f #n1 #n <(stream_rew … (f2∘(n1@f1))) normalize
+lemma compose_inv_rew: ∀f2,f1,f,n1,n. f2∘(n1⨮f1) = n⨮f →
+                       f2@❴n1❵ = n ∧ (⫰*[↑n1]f2)∘f1 = f.
+#f2 #f1 #f #n1 #n <(stream_rew … (f2∘(n1⨮f1))) normalize
 #H destruct /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_O2: ∀f2,f1,f,n2,n. (n2@f2)∘(↑f1) = n@f →
+lemma compose_inv_O2: ∀f2,f1,f,n2,n. (n2⨮f2)∘(⫯f1) = n⨮f →
                       n2 = n ∧ f2∘f1 = f.
 #f2 #f1 #f #n2 #n <compose_rew
 #H destruct /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_S2: ∀f2,f1,f,n2,n1,n. (n2@f2)∘(⫯n1@f1) = n@f →
-                      ⫯(n2+f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+lemma compose_inv_S2: ∀f2,f1,f,n2,n1,n. (n2⨮f2)∘(↑n1⨮f1) = n⨮f →
+                      ↑(n2+f2@❴n1❵) = n ∧ f2∘(n1⨮f1) = f2@❴n1❵⨮f.
 #f2 #f1 #f #n2 #n1 #n <compose_rew
 #H destruct <tls_S1 /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_S1: ∀f2,f1,f,n1,n. (⫯f2)∘(n1@f1) = n@f →
-                      ⫯(f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+lemma compose_inv_S1: ∀f2,f1,f,n1,n. (↑f2)∘(n1⨮f1) = n⨮f →
+                      ↑(f2@❴n1❵) = n ∧ f2∘(n1⨮f1) = f2@❴n1❵⨮f.
 #f2 #f1 #f #n1 #n <compose_rew
 #H destruct <tls_S1 /2 width=1 by conj/
 qed-.
 
 (* Specific properties on after *********************************************)
 
-lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≡ f →
-                ∀n. n@f2 ⊚ ↑f1 ≡ n@f.
+lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
+                ∀n. n⨮f2 ⊚ ⫯f1 ≘ n⨮f.
 #f2 #f1 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
 qed.
 
-lemma after_S2: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≡ n@f →
-                ∀n2. n2@f2 ⊚ ⫯n1@f1 ≡ ⫯(n2+n)@f.
+lemma after_S2: ∀f2,f1,f,n1,n. f2 ⊚ n1⨮f1 ≘ n⨮f →
+                ∀n2. n2⨮f2 ⊚ ↑n1⨮f1 ≘ ↑(n2+n)⨮f.
 #f2 #f1 #f #n1 #n #Hf #n2 elim n2 -n2 /2 width=7 by after_next, after_push/
 qed.
 
-lemma after_apply: ∀n1,f2,f1,f. (↓*[⫯n1] f2) ⊚ f1 ≡ f → f2 ⊚ n1@f1 ≡ f2@❴n1❵@f.
+lemma after_apply: ∀n1,f2,f1,f. (⫰*[↑n1] f2) ⊚ f1 ≘ f → f2 ⊚ n1⨮f1 ≘ f2@❴n1❵⨮f.
 #n1 elim n1 -n1
 [ * /2 width=1 by after_O2/
 | #n1 #IH * /3 width=1 by after_S2/
 ]
 qed-.
 
-corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≡ f.
+corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
 * #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
 [ cases n1 -n1
   [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
@@ -91,13 +91,13 @@ corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≡ f.
 ]
 qed-.
 
-theorem after_total: ∀f1,f2. f2 ⊚ f1 ≡ f2 ∘ f1.
+theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
 /2 width=1 by after_total_aux/ qed.
 
 (* Specific inversion lemmas on after ***************************************)
 
-lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≡ n@f → ∀f1. ↑f1 = g2 →
-                     f2 ⊚ f1 ≡ f ∧ n2 = n.
+lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2⨮f2 ⊚ g2 ≘ n⨮f → ∀f1. ⫯f1 = g2 →
+                     f2 ⊚ f1 ≘ f ∧ n2 = n.
 #f2 #g2 #f #n2 elim n2 -n2
 [ #n #Hf #f1 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ]
   #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
@@ -108,8 +108,8 @@ lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≡ n@f → ∀f1. ↑f1 = g2
 ]
 qed-.
 
-lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≡ n@f → ∀f1. ⫯f1 = g2 →
-                     ∃∃m. f2 ⊚ f1 ≡ m@f & ⫯(n2+m) = n.
+lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2⨮f2 ⊚ g2 ≘ n⨮f → ∀f1. ↑f1 = g2 →
+                     ∃∃m. f2 ⊚ f1 ≘ m⨮f & ↑(n2+m) = n.
 #f2 #g2 #f #n2 elim n2 -n2
 [ #n #Hf #f1 #H2 elim (after_inv_pnx … Hf … H2) -g2 [2,3: // ]
   #g #Hf #H elim (next_inv_seq_dx … H) -H
@@ -121,7 +121,7 @@ lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≡ n@f → ∀f1. ⫯f1 = g2
 ]
 qed-.
 
-lemma after_inv_const: ∀f2,f1,f,n1,n. n@f2 ⊚ n1@f1 ≡ n@f → f2 ⊚ f1 ≡ f ∧ 0 = n1.
+lemma after_inv_const: ∀f2,f1,f,n1,n. n⨮f2 ⊚ n1⨮f1 ≘ n⨮f → f2 ⊚ f1 ≘ f ∧ 0 = n1.
 #f2 #f1 #f #n1 #n elim n -n
 [ #H elim (after_inv_pxp … H) -H [ |*: // ]
   #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
@@ -129,18 +129,18 @@ lemma after_inv_const: ∀f2,f1,f,n1,n. n@f2 ⊚ n1@f1 ≡ n@f → f2 ⊚ f1 ≡
 ]
 qed-.
 
-lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ∘ f1 ≗ f.
+lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
 /2 width=4 by after_mono/ qed-.
 
 (* Specific forward lemmas on after *****************************************)
 
-lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≡ n@f → f2@❴n1❵ = n.
+lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1⨮f1 ≘ n⨮f → f2@❴n1❵ = n.
 #f2 #f1 #f #n1 #n #H lapply (after_fwd_at ? n1 0 … H) -H [1,2,3: // ]
 /3 width=2 by at_inv_O1, sym_eq/
 qed-.
 
-lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2@f2 ⊚ n1@f1 ≡ n@f →
-                     (↓*[n1]f2) ⊚ f1 ≡ f.
+lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
+                     (⫰*[n1]f2) ⊚ f1 ≘ f.
 #f #f1 #n1 elim n1 -n1
 [ #f2 #n2 #n #H elim (after_inv_xpx … H) -H //
 | #n1 #IH * #m1 #f2 #n2 #n #H elim (after_inv_xnx … H) -H [2,3: // ]
@@ -148,6 +148,11 @@ lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2@f2 ⊚ n1@f1 ≡ n@f →
 ]
 qed-.
 
-lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2@f2 ⊚ n1@f1 ≡ n@f →
-                       (n2@f2)@❴n1❵ = n ∧ (↓*[n1]f2) ⊚ f1 ≡ f.
+lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
+                       (n2⨮f2)@❴n1❵ = n ∧ (⫰*[n1]f2) ⊚ f1 ≘ f.
 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
+
+(* Properties on apply ******************************************************)
+
+lemma compose_apply (f2) (f1) (i): f2@❴f1@❴i❵❵ = (f2∘f1)@❴i❵.
+/4 width=6 by after_fwd_at, at_inv_total, sym_eq/ qed.