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.
(* 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/
(* Specific properties on coafter *******************************************)
-corec lemma coafter_total_aux: â\88\80f2,f1,f. f2 ~â\88\98 f1 = f â\86\92 f2 ~â\8a\9a f1 â\89¡ f.
+corec lemma coafter_total_aux: â\88\80f2,f1,f. f2 ~â\88\98 f1 = f â\86\92 f2 ~â\8a\9a f1 â\89\98 f.
* #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
[ cases n1 -n1
[ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by coafter_refl, eq_f2/
]
qed-.
-theorem coafter_total: â\88\80f2,f1. f2 ~â\8a\9a f1 â\89¡ f2 ~∘ f1.
+theorem coafter_total: â\88\80f2,f1. f2 ~â\8a\9a f1 â\89\98 f2 ~∘ f1.
/2 width=1 by coafter_total_aux/ qed.