X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream_coafter.ma;h=f93a968b0f3a373adbe8947ee0db8df00ebc7306;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=c158f25930fe6d454e3b0f6884e7d3b3358b0126;hpb=75f395f0febd02de8e0f881d918a8812b1425c8d;p=helm.git

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 c158f2593..f93a968b0 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
@@ -20,17 +20,17 @@ include "ground_2/relocation/rtmap_coafter.ma".
 rec definition fun0 (n1:nat) on n1: rtmap → nat.
 * * [ | #n2 #f2 @0 ]
 #f2 cases n1 -n1 [ @0 ]
-#n1 @(⫯(fun0 n1 f2))
+#n1 @(↑(fun0 n1 f2))
 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.
@@ -44,44 +44,44 @@ interpretation "functional co-composition (nstream)"
 
 (* Basic properties on funs *************************************************)
 
-(* Note: we need theese since matita blocks recursive δ when ι is blocked *)  
-lemma fun0_xn: ∀f2,n1. 0 = fun0 n1 (⫯f2).
+(* Note: we need theese since matita blocks recursive δ when ι is blocked *)
+lemma fun0_xn: ∀f2,n1. 0 = fun0 n1 (↑f2).
 * #n2 #f2 * //
 qed.
 
-lemma fun2_xn: ∀f2,n1. f2 = fun2 n1 (⫯f2).
+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/