(* RELOCATION N-STREAM ******************************************************)
corec definition compose: rtmap → rtmap → rtmap.
-#f2 * #n1 #f1 @(seq â\80¦ (f2@â\9d´n1â\9dµ)) @(compose ? f1) -compose -f1
+#f2 * #n1 #f1 @(seq â\80¦ (f2@â\9d¨n1â\9d©)) @(compose ? f1) -compose -f1
@(⫰*[↑n1] f2)
defined.
(* Basic properies on compose ***********************************************)
-lemma compose_rew: â\88\80f2,f1,n1. f2@â\9d´n1â\9dµ⨮(⫰*[↑n1]f2)∘f1 = f2∘(n1⨮f1).
+lemma compose_rew: â\88\80f2,f1,n1. f2@â\9d¨n1â\9d©⨮(⫰*[↑n1]f2)∘f1 = f2∘(n1⨮f1).
#f2 #f1 #n1 <(stream_rew … (f2∘(n1⨮f1))) normalize //
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 ∧ (⫰*[↑n1]f2)∘f1 = f.
+ f2@â\9d¨n1â\9d© = n ∧ (⫰*[↑n1]f2)∘f1 = f.
#f2 #f1 #f #n1 #n <(stream_rew … (f2∘(n1⨮f1))) normalize
#H destruct /2 width=1 by conj/
qed-.
qed-.
lemma compose_inv_S2: ∀f2,f1,f,n2,n1,n. (n2⨮f2)∘(↑n1⨮f1) = n⨮f →
- â\86\91(n2+f2@â\9d´n1â\9dµ) = n â\88§ f2â\88\98(n1⨮f1) = f2@â\9d´n1â\9dµ⨮f.
+ â\86\91(n2+f2@â\9d¨n1â\9d©) = n â\88§ f2â\88\98(n1⨮f1) = f2@â\9d¨n1â\9d©⨮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 →
- â\86\91(f2@â\9d´n1â\9dµ) = n â\88§ f2â\88\98(n1⨮f1) = f2@â\9d´n1â\9dµ⨮f.
+ â\86\91(f2@â\9d¨n1â\9d©) = n â\88§ f2â\88\98(n1⨮f1) = f2@â\9d¨n1â\9d©⨮f.
#f2 #f1 #f #n1 #n <compose_rew
#H destruct <tls_S1 /2 width=1 by conj/
qed-.
#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\91n1] f2) â\8a\9a f1 â\89\98 f â\86\92 f2 â\8a\9a n1⨮f1 â\89\98 f2@â\9d´n1â\9dµ⨮f.
+lemma after_apply: â\88\80n1,f2,f1,f. (â«°*[â\86\91n1] f2) â\8a\9a f1 â\89\98 f â\86\92 f2 â\8a\9a n1⨮f1 â\89\98 f2@â\9d¨n1â\9d©⨮f.
#n1 elim n1 -n1
[ * /2 width=1 by after_O2/
| #n1 #IH * /3 width=1 by after_S2/
(* Specific forward lemmas on after *****************************************)
-lemma after_fwd_hd: â\88\80f2,f1,f,n1,n. f2 â\8a\9a n1⨮f1 â\89\98 n⨮f â\86\92 f2@â\9d´n1â\9dµ = n.
+lemma after_fwd_hd: â\88\80f2,f1,f,n1,n. f2 â\8a\9a n1⨮f1 â\89\98 n⨮f â\86\92 f2@â\9d¨n1â\9d© = 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-.
qed-.
lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
- (n2⨮f2)@â\9d´n1â\9dµ = n ∧ (⫰*[n1]f2) ⊚ f1 ≘ f.
+ (n2⨮f2)@â\9d¨n1â\9d© = 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@â\9d´f1@â\9d´iâ\9dµâ\9dµ = (f2â\88\98f1)@â\9d´iâ\9dµ.
+lemma compose_apply (f2) (f1) (i): f2@â\9d¨f1@â\9d¨iâ\9d©â\9d© = (f2â\88\98f1)@â\9d¨iâ\9d©.
/4 width=6 by after_fwd_at, at_inv_total, sym_eq/ qed.