X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream_coafter.ma;h=7758003287dde4ed294fe85588d6a93d4b589aa9;hp=66ba11b18284e3bc6de75181fb03b46a545ccdac;hb=a77d0bd6a04e94f765d329d47b37d9e04d349b14;hpb=b598b37379baabef24ae511596be7f740cbb0c2e

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
index 66ba11b18..775800328 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
@@ -24,13 +24,13 @@ rec definition fun0 (n1:nat) on n1: rtmap → nat.
 defined.
 
 rec definition fun2 (n1:nat) on n1: rtmap → rtmap.
-* * [ | #n2 #f2 @(n2@f2) ]
+* * [ | #n2 #f2 @(n2⨮f2) ]
 #f2 cases n1 -n1 [ @f2 ]
 #n1 @(fun2 n1 f2)
 defined.
 
 rec definition fun1 (n1:nat) (f1:rtmap) on n1: rtmap → rtmap.
-* * [ | #n2 #f2 @(n1@f1) ]
+* * [ | #n2 #f2 @(n1⨮f1) ]
 #f2 cases n1 -n1 [ @f1 ]
 #n1 @(fun1 n1 f1 f2)
 defined.
@@ -53,35 +53,35 @@ lemma fun2_xn: ∀f2,n1. f2 = fun2 n1 (↑f2).
 * #n2 #f2 * //
 qed.
 
-lemma fun1_xxn: ∀f2,f1,n1. fun1 n1 f1 (↑f2) = n1@f1.
+lemma fun1_xxn: ∀f2,f1,n1. fun1 n1 f1 (↑f2) = n1⨮f1.
 * #n2 #f2 #f1 * //
 qed.
 
 (* Basic properies on cocompose *********************************************)
 
-lemma cocompose_rew: ∀f2,f1,n1. (fun0 n1 f2)@(fun2 n1 f2)~∘(fun1 n1 f1 f2) = f2 ~∘ (n1@f1).
-#f2 #f1 #n1 <(stream_rew … (f2~∘(n1@f1))) normalize //
+lemma cocompose_rew: ∀f2,f1,n1. (fun0 n1 f2)⨮(fun2 n1 f2)~∘(fun1 n1 f1 f2) = f2 ~∘ (n1⨮f1).
+#f2 #f1 #n1 <(stream_rew … (f2~∘(n1⨮f1))) normalize //
 qed.
 
 (* Basic inversion lemmas on compose ****************************************)
 
-lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x@f →
+lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x⨮f →
                          0 = x ∧ f2 ~∘ f1 = f.
 #f2 #f1 #f #x
 <cocompose_rew #H destruct
 normalize /2 width=1 by conj/
 qed-.
 
-lemma cocompose_inv_pnx: ∀f2,f1,f,n1,x. (⫯f2) ~∘ ((↑n1)@f1) = x@f →
-                         ∃∃n. ↑n = x & f2 ~∘ (n1@f1) = n@f.
+lemma cocompose_inv_pnx: ∀f2,f1,f,n1,x. (⫯f2) ~∘ (↑n1⨮f1) = x⨮f →
+                         ∃∃n. ↑n = x & f2 ~∘ (n1⨮f1) = n⨮f.
 #f2 #f1 #f #n1 #x
 <cocompose_rew #H destruct
 @(ex2_intro … (fun0 n1 f2)) // <cocompose_rew
 /3 width=1 by eq_f2/
 qed-.
 
-lemma cocompose_inv_nxx: ∀f2,f1,f,n1,x. (↑f2) ~∘ (n1@f1) = x@f →
-                         0 = x ∧ f2 ~∘ (n1@f1) = f.
+lemma cocompose_inv_nxx: ∀f2,f1,f,n1,x. (↑f2) ~∘ (n1⨮f1) = x⨮f →
+                         0 = x ∧ f2 ~∘ (n1⨮f1) = f.
 #f2 #f1 #f #n1 #x
 <cocompose_rew #H destruct
 /2 width=1 by conj/