(* Specific properties on after *********************************************)
-lemma after_O2: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89¡ f →
- â\88\80n. n@f2 â\8a\9a â\86\91f1 â\89¡ n@f.
+lemma after_O2: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f →
+ â\88\80n. n@f2 â\8a\9a â\86\91f1 â\89\98 n@f.
#f2 #f1 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
qed.
-lemma after_S2: â\88\80f2,f1,f,n1,n. f2 â\8a\9a n1@f1 â\89¡ n@f →
- â\88\80n2. n2@f2 â\8a\9a ⫯n1@f1 â\89¡ ⫯(n2+n)@f.
+lemma after_S2: â\88\80f2,f1,f,n1,n. f2 â\8a\9a n1@f1 â\89\98 n@f →
+ â\88\80n2. n2@f2 â\8a\9a ⫯n1@f1 â\89\98 ⫯(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) â\8a\9a f1 â\89¡ f â\86\92 f2 â\8a\9a n1@f1 â\89¡ f2@❴n1❵@f.
+lemma after_apply: â\88\80n1,f2,f1,f. (â\86\93*[⫯n1] f2) â\8a\9a f1 â\89\98 f â\86\92 f2 â\8a\9a n1@f1 â\89\98 f2@❴n1❵@f.
#n1 elim n1 -n1
[ * /2 width=1 by after_O2/
| #n1 #IH * /3 width=1 by after_S2/
]
qed-.
-corec lemma after_total_aux: â\88\80f2,f1,f. f2 â\88\98 f1 = f â\86\92 f2 â\8a\9a f1 â\89¡ f.
+corec lemma after_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 (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
]
qed-.
-theorem after_total: â\88\80f1,f2. f2 â\8a\9a f1 â\89¡ f2 ∘ f1.
+theorem after_total: â\88\80f1,f2. f2 â\8a\9a f1 â\89\98 f2 ∘ f1.
/2 width=1 by after_total_aux/ qed.
(* Specific inversion lemmas on after ***************************************)
-lemma after_inv_xpx: â\88\80f2,g2,f,n2,n. n2@f2 â\8a\9a g2 â\89¡ n@f → ∀f1. ↑f1 = g2 →
- f2 â\8a\9a f1 â\89¡ f ∧ n2 = n.
+lemma after_inv_xpx: â\88\80f2,g2,f,n2,n. n2@f2 â\8a\9a g2 â\89\98 n@f → ∀f1. ↑f1 = g2 →
+ f2 â\8a\9a f1 â\89\98 f ∧ n2 = n.
#f2 #g2 #f #n2 elim n2 -n2
[ #n #Hf #f1 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ]
#g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
]
qed-.
-lemma after_inv_xnx: â\88\80f2,g2,f,n2,n. n2@f2 â\8a\9a g2 â\89¡ n@f → ∀f1. ⫯f1 = g2 →
- â\88\83â\88\83m. f2 â\8a\9a f1 â\89¡ m@f & ⫯(n2+m) = n.
+lemma after_inv_xnx: â\88\80f2,g2,f,n2,n. n2@f2 â\8a\9a g2 â\89\98 n@f → ∀f1. ⫯f1 = g2 →
+ â\88\83â\88\83m. f2 â\8a\9a f1 â\89\98 m@f & ⫯(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
]
qed-.
-lemma after_inv_const: â\88\80f2,f1,f,n1,n. n@f2 â\8a\9a n1@f1 â\89¡ n@f â\86\92 f2 â\8a\9a f1 â\89¡ f ∧ 0 = n1.
+lemma after_inv_const: â\88\80f2,f1,f,n1,n. n@f2 â\8a\9a n1@f1 â\89\98 n@f â\86\92 f2 â\8a\9a f1 â\89\98 f ∧ 0 = n1.
#f2 #f1 #f #n1 #n elim n -n
[ #H elim (after_inv_pxp … H) -H [ |*: // ]
#g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
]
qed-.
-lemma after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89¡ f → f2 ∘ f1 ≗ f.
+lemma after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f → f2 ∘ f1 ≗ f.
/2 width=4 by after_mono/ qed-.
(* Specific forward lemmas on after *****************************************)
-lemma after_fwd_hd: â\88\80f2,f1,f,n1,n. f2 â\8a\9a n1@f1 â\89¡ n@f → f2@❴n1❵ = n.
+lemma after_fwd_hd: â\88\80f2,f1,f,n1,n. f2 â\8a\9a n1@f1 â\89\98 n@f → f2@❴n1❵ = 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-.
-lemma after_fwd_tls: â\88\80f,f1,n1,f2,n2,n. n2@f2 â\8a\9a n1@f1 â\89¡ n@f →
- (â\86\93*[n1]f2) â\8a\9a f1 â\89¡ f.
+lemma after_fwd_tls: â\88\80f,f1,n1,f2,n2,n. n2@f2 â\8a\9a n1@f1 â\89\98 n@f →
+ (â\86\93*[n1]f2) â\8a\9a f1 â\89\98 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: // ]
]
qed-.
-lemma after_inv_apply: â\88\80f2,f1,f,n2,n1,n. n2@f2 â\8a\9a n1@f1 â\89¡ n@f →
- (n2@f2)@â\9d´n1â\9dµ = n â\88§ (â\86\93*[n1]f2) â\8a\9a f1 â\89¡ f.
+lemma after_inv_apply: â\88\80f2,f1,f,n2,n1,n. n2@f2 â\8a\9a n1@f1 â\89\98 n@f →
+ (n2@f2)@â\9d´n1â\9dµ = n â\88§ (â\86\93*[n1]f2) â\8a\9a f1 â\89\98 f.
/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.