notational update in lambdadelta completed

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

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 c158f25930fe6d454e3b0f6884e7d3b3358b0126..7758003287dde4ed294fe85588d6a93d4b589aa9 100644 (file)
--- 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 @(â\86\91(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.
@@ -45,43 +45,43 @@ interpretation "functional co-composition (nstream)"
 (* Basic properties on funs *************************************************)
 
 (* Note: we need theese since matita blocks recursive δ when ι is blocked *)  
-lemma fun0_xn: â\88\80f2,n1. 0 = fun0 n1 (⫯f2).
+lemma fun0_xn: â\88\80f2,n1. 0 = fun0 n1 (â\86\91f2).
 * #n2 #f2 * //
 qed.
 
-lemma fun2_xn: â\88\80f2,n1. f2 = fun2 n1 (⫯f2).
+lemma fun2_xn: â\88\80f2,n1. f2 = fun2 n1 (â\86\91f2).
 * #n2 #f2 * //
 qed.
 
-lemma fun1_xxn: â\88\80f2,f1,n1. fun1 n1 f1 (⫯f2) = n1@f1.
+lemma fun1_xxn: â\88\80f2,f1,n1. fun1 n1 f1 (â\86\91f2) = 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: â\88\80f2,f1,f,x. (â\86\91f2) ~â\88\98 (â\86\91f1) = x@f →
+lemma cocompose_inv_ppx: â\88\80f2,f1,f,x. (⫯f2) ~â\88\98 (⫯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: â\88\80f2,f1,f,n1,x. (â\86\91f2) ~â\88\98 ((⫯n1)@f1) = x@f →
-                         â\88\83â\88\83n. ⫯n = x & f2 ~â\88\98 (n1@f1) = n@f.
+lemma cocompose_inv_pnx: â\88\80f2,f1,f,n1,x. (⫯f2) ~â\88\98 (â\86\91n1⨮f1) = x⨮f →
+                         â\88\83â\88\83n. â\86\91n = x & f2 ~â\88\98 (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: â\88\80f2,f1,f,n1,x. (⫯f2) ~â\88\98 (n1@f1) = x@f →
-                         0 = x ∧ f2 ~∘ (n1@f1) = f.
+lemma cocompose_inv_nxx: â\88\80f2,f1,f,n1,x. (â\86\91f2) ~â\88\98 (n1⨮f1) = x⨮f →
+                         0 = x ∧ f2 ~∘ (n1⨮f1) = f.
 #f2 #f1 #f #n1 #x
 <cocompose_rew #H destruct
 /2 width=1 by conj/