notational update in ground_2 and basic_2

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

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 321773c634594c788e54fbedf1d3340968970ea8..4724aa8be738ff5188d13a38b15343457621bd81 100644 (file)
--- 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
-@(â\86\93*[⫯n1] f2)
+@(â«°*[â\86\91n1] f2)
 defined.
 
 interpretation "functional composition (nstream)"
@@ -27,11 +27,11 @@ interpretation "functional composition (nstream)"
 
 (* Basic properies on compose ***********************************************)
 
-lemma compose_rew: â\88\80f2,f1,n1. f2@â\9d´n1â\9dµ@(â\86\93*[⫯n1]f2)∘f1 = f2∘(n1@f1).
+lemma compose_rew: â\88\80f2,f1,n1. f2@â\9d´n1â\9dµ@(â«°*[â\86\91n1]f2)∘f1 = f2∘(n1@f1).
 #f2 #f1 #n1 <(stream_rew … (f2∘(n1@f1))) normalize //
 qed.
 
-lemma compose_next: â\88\80f2,f1,f. f2â\88\98f1 = f â\86\92 (⫯f2)â\88\98f1 = ⫯f.
+lemma compose_next: â\88\80f2,f1,f. f2â\88\98f1 = f â\86\92 (â\86\91f2)â\88\98f1 = â\86\91f.
 #f2 * #n1 #f1 #f <compose_rew <compose_rew
 * -f <tls_S1 /2 width=1 by eq_f2/
 qed.
@@ -39,25 +39,25 @@ qed.
 (* Basic inversion lemmas on compose ****************************************)
 
 lemma compose_inv_rew: ∀f2,f1,f,n1,n. f2∘(n1@f1) = n@f →
-                       f2@â\9d´n1â\9dµ = n â\88§ (â\86\93*[⫯n1]f2)∘f1 = f.
+                       f2@â\9d´n1â\9dµ = n â\88§ (â«°*[â\86\91n1]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: â\88\80f2,f1,f,n2,n. (n2@f2)â\88\98(â\86\91f1) = n@f →
+lemma compose_inv_O2: â\88\80f2,f1,f,n2,n. (n2@f2)â\88\98(⫯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: â\88\80f2,f1,f,n2,n1,n. (n2@f2)â\88\98(⫯n1@f1) = n@f →
-                      ⫯(n2+f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+lemma compose_inv_S2: â\88\80f2,f1,f,n2,n1,n. (n2@f2)â\88\98(â\86\91n1@f1) = n@f →
+                      â\86\91(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: â\88\80f2,f1,f,n1,n. (⫯f2)∘(n1@f1) = n@f →
-                      ⫯(f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+lemma compose_inv_S1: â\88\80f2,f1,f,n1,n. (â\86\91f2)∘(n1@f1) = n@f →
+                      â\86\91(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-.
@@ -65,16 +65,16 @@ qed-.
 (* Specific properties on after *********************************************)
 
 lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
-                â\88\80n. n@f2 â\8a\9a â\86\91f1 ≘ n@f.
+                â\88\80n. n@f2 â\8a\9a ⫯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 →
-                â\88\80n2. n2@f2 â\8a\9a ⫯n1@f1 â\89\98 ⫯(n2+n)@f.
+                â\88\80n2. n2@f2 â\8a\9a â\86\91n1@f1 â\89\98 â\86\91(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: â\88\80n1,f2,f1,f. (â\86\93*[⫯n1] f2) ⊚ f1 ≘ f → f2 ⊚ n1@f1 ≘ f2@❴n1❵@f.
+lemma after_apply: â\88\80n1,f2,f1,f. (â«°*[â\86\91n1] 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/
@@ -96,7 +96,7 @@ theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
 
 (* Specific inversion lemmas on after ***************************************)
 
-lemma after_inv_xpx: â\88\80f2,g2,f,n2,n. n2@f2 â\8a\9a g2 â\89\98 n@f â\86\92 â\88\80f1. â\86\91f1 = g2 →
+lemma after_inv_xpx: â\88\80f2,g2,f,n2,n. n2@f2 â\8a\9a g2 â\89\98 n@f â\86\92 â\88\80f1. ⫯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: // ]
@@ -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: â\88\80f2,g2,f,n2,n. n2@f2 â\8a\9a g2 â\89\98 n@f â\86\92 â\88\80f1. ⫯f1 = g2 →
-                     â\88\83â\88\83m. f2 â\8a\9a f1 â\89\98 m@f & ⫯(n2+m) = n.
+lemma after_inv_xnx: â\88\80f2,g2,f,n2,n. n2@f2 â\8a\9a g2 â\89\98 n@f â\86\92 â\88\80f1. â\86\91f1 = g2 →
+                     â\88\83â\88\83m. f2 â\8a\9a f1 â\89\98 m@f & â\86\91(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
@@ -129,7 +129,7 @@ lemma after_inv_const: ∀f2,f1,f,n1,n. n@f2 ⊚ n1@f1 ≘ n@f → f2 ⊚ f1 ≘
 ]
 qed-.
 
-lemma after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89\97 f.
+lemma after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89¡ f.
 /2 width=4 by after_mono/ qed-.
 
 (* Specific forward lemmas on after *****************************************)
@@ -140,7 +140,7 @@ lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≘ n@f → f2@❴n1❵ = n.
 qed-.
 
 lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2@f2 ⊚ n1@f1 ≘ n@f →
-                     (â\86\93*[n1]f2) ⊚ f1 ≘ 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: // ]
@@ -149,5 +149,5 @@ 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)@â\9d´n1â\9dµ = n â\88§ (â\86\93*[n1]f2) ⊚ f1 ≘ f.
+                       (n2@f2)@â\9d´n1â\9dµ = n â\88§ (â«°*[n1]f2) ⊚ f1 ≘ f.
 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.