1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/notation/relations/rafter_3.ma".
16 include "ground_2/lib/streams_hdtl.ma".
17 include "ground_2/relocation/nstream_at.ma".
19 (* RELOCATION N-STREAM ******************************************************)
21 let corec compose: rtmap → rtmap → rtmap ≝ ?.
22 #f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2
26 interpretation "functional composition (nstream)"
27 'compose f1 f2 = (compose f1 f2).
29 coinductive after: relation3 rtmap rtmap rtmap ≝
30 | after_refl: ∀f1,f2,f,g1,g2,g.
31 after f1 f2 f → g1 = ↑f1 → g2 = ↑f2 → g = ↑f → after g1 g2 g
32 | after_push: ∀f1,f2,f,g1,g2,g.
33 after f1 f2 f → g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → after g1 g2 g
34 | after_next: ∀f1,f2,f,g1,g.
35 after f1 f2 f → g1 = ⫯f1 → g = ⫯f → after g1 f2 g
38 interpretation "relational composition (nstream)"
39 'RAfter f1 f2 f = (after f1 f2 f).
41 (* Basic properies on compose ***********************************************)
43 lemma compose_unfold: ∀f1,f2,n2. f1∘(n2@f2) = f1@❴n2❵@tln … (⫯n2) f1∘f2.
44 #f1 #f2 #n2 >(stream_expand … (f1∘(n2@f2))) normalize //
47 lemma compose_next: ∀f1,f2,f. f1∘f2 = f → (⫯f1)∘f2 = ⫯f.
48 * #n1 #f1 * #n2 #f2 #f >compose_unfold >compose_unfold
49 #H destruct normalize //
52 (* Basic inversion lemmas on compose ****************************************)
54 lemma compose_inv_unfold: ∀f1,f2,f,n2,n. f1∘(n2@f2) = n@f →
55 f1@❴n2❵ = n ∧ tln … (⫯n2) f1∘f2 = f.
56 #f1 #f2 #f #n2 #n >(stream_expand … (f1∘(n2@f2))) normalize
57 #H destruct /2 width=1 by conj/
60 lemma compose_inv_O2: ∀f1,f2,f,n1,n. (n1@f1)∘(↑f2) = n@f →
62 #f1 #f2 #f #n1 #n >compose_unfold
63 #H destruct /2 width=1 by conj/
66 lemma compose_inv_S2: ∀f1,f2,f,n1,n2,n. (n1@f1)∘(⫯n2@f2) = n@f →
67 n = ⫯(n1+f1@❴n2❵) ∧ f1∘(n2@f2) = f1@❴n2❵@f.
68 #f1 #f2 #f #n1 #n2 #n >compose_unfold
69 #H destruct /2 width=1 by conj/
72 lemma compose_inv_S1: ∀f1,f2,f,n1,n2,n. (⫯n1@f1)∘(n2@f2) = n@f →
73 n = ⫯((n1@f1)@❴n2❵) ∧ (n1@f1)∘(n2@f2) = (n1@f1)@❴n2❵@f.
74 #f1 #f2 #f #n1 #n2 #n >compose_unfold
75 #H destruct /2 width=1 by conj/
78 (* Basic properties on after ************************************************)
80 lemma after_O2: ∀f1,f2,f. f1 ⊚ f2 ≡ f →
82 #f1 #f2 #f #Ht #n elim n -n /2 width=7 by after_refl, after_next/
85 lemma after_S2: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f →
86 ∀n1. n1@f1 ⊚ ⫯n2@f2 ≡ ⫯(n1+n)@f.
87 #f1 #f2 #f #n2 #n #Ht #n1 elim n1 -n1 /2 width=7 by after_next, after_push/
90 lemma after_apply: ∀n2,f1,f2,f. (tln … (⫯n2) f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ≡ f1@❴n2❵@f.
92 [ * /2 width=1 by after_O2/
93 | #n2 #IH * /3 width=1 by after_S2/
97 let corec after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f ≝ ?.
98 * #n1 #f1 * #n2 #f2 * #n #f cases n1 -n1
100 [ #H cases (compose_inv_O2 … H) -H
101 /3 width=7 by after_refl, eq_f2/
102 | #n2 #H cases (compose_inv_S2 … H) -H
103 /3 width=7 by after_push/
105 | #n1 #H cases (compose_inv_S1 … H) -H
106 /4 width=7 by after_next, next_rew_sn/
110 theorem after_total: ∀f2,f1. f1 ⊚ f2 ≡ f1 ∘ f2.
111 /2 width=1 by after_total_aux/ qed.
113 (* Basic inversion lemmas on after ******************************************)
115 fact after_inv_OOx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ↑f2 →
116 ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f.
117 #g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
118 [ #g2 #g #Hf #H1 #H2 #H #x1 #x2 #Hx1 #Hx2 destruct
119 <(injective_push … Hx1) <(injective_push … Hx2) -x2 -x1
120 /2 width=3 by ex2_intro/
121 | #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
122 elim (discr_next_push … Hx2)
123 | #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
124 elim (discr_next_push … Hx1)
128 lemma after_inv_OOx: ∀f1,f2,g. ↑f1 ⊚ ↑f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f.
129 /2 width=5 by after_inv_OOx_aux/ qed-.
131 fact after_inv_OSx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ⫯f2 →
132 ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
133 #g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
134 [ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
135 elim (discr_push_next … Hx2)
136 | #g2 #g #Hf #H1 #H2 #H3 #x1 #x2 #Hx1 #Hx2 destruct
137 <(injective_push … Hx1) <(injective_next … Hx2) -x2 -x1
138 /2 width=3 by ex2_intro/
139 | #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
140 elim (discr_next_push … Hx1)
144 lemma after_inv_OSx: ∀f1,f2,g. ↑f1 ⊚ ⫯f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
145 /2 width=5 by after_inv_OSx_aux/ qed-.
147 fact after_inv_Sxx_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g → ∀f1. g1 = ⫯f1 →
148 ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
149 #g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1
150 [ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
151 elim (discr_push_next … Hx1)
152 | #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
153 elim (discr_push_next … Hx1)
154 | #g #Hf #H1 #H #x1 #Hx1 destruct
155 <(injective_next … Hx1) -x1
156 /2 width=3 by ex2_intro/
160 lemma after_inv_Sxx: ∀f1,f2,g. ⫯f1 ⊚ f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
161 /2 width=5 by after_inv_Sxx_aux/ qed-.
163 (* Advanced inversion lemmas on after ***************************************)
165 fact after_inv_OOO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
166 ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ↑f → f1 ⊚ f2 ≡ f.
167 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
168 #x #Hf #Hx destruct >(injective_push … Hx) -f //
171 fact after_inv_OOS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
172 ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ⫯f → ⊥.
173 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
174 #x #Hf #Hx destruct elim (discr_next_push … Hx)
177 fact after_inv_OSS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
178 ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → f1 ⊚ f2 ≡ f.
179 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
180 #x #Hf #Hx destruct >(injective_next … Hx) -f //
183 fact after_inv_OSO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
184 ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ↑f → ⊥.
185 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
186 #x #Hf #Hx destruct elim (discr_push_next … Hx)
189 fact after_inv_SxS_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g →
190 ∀f1,f. g1 = ⫯f1 → g = ⫯f → f1 ⊚ f2 ≡ f.
191 #g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1
192 #x #Hf #Hx destruct >(injective_next … Hx) -f //
195 fact after_inv_SxO_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g →
196 ∀f1,f. g1 = ⫯f1 → g = ↑f → ⊥.
197 #g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1
198 #x #Hf #Hx destruct elim (discr_push_next … Hx)
201 fact after_inv_OxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
202 ∀f1,f. g1 = ↑f1 → g = ↑f →
203 ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2.
204 #g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H
205 [ elim (after_inv_OSO_aux … Hg … H1 … H) -g1 -g -f1 -f //
206 | lapply (after_inv_OOO_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/
210 lemma after_inv_OxO: ∀f1,g2,f. ↑f1 ⊚ g2 ≡ ↑f →
211 ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2.
212 /2 width=5 by after_inv_OxO_aux/ qed-.
214 fact after_inv_OxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
215 ∀f1,f. g1 = ↑f1 → g = ⫯f →
216 ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ⫯f2.
217 #g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H
218 [ lapply (after_inv_OSS_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/
219 | elim (after_inv_OOS_aux … Hg … H1 … H) -g1 -g -f1 -f //
223 fact after_inv_xxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ↑f →
224 ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2.
225 * * [2: #m1 ] #g1 #g2 #g #Hg #f #H
226 [ elim (after_inv_SxO_aux … Hg … H) -g2 -g -f //
227 | elim (after_inv_OxO_aux … Hg … H) -g /2 width=5 by ex3_2_intro/
231 lemma after_inv_xxO: ∀g1,g2,f. g1 ⊚ g2 ≡ ↑f →
232 ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2.
233 /2 width=3 by after_inv_xxO_aux/ qed-.
235 fact after_inv_xxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ⫯f →
236 (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨
237 ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1.
238 * * [2: #m1 ] #g1 #g2 #g #Hg #f #H
239 [ /4 width=5 by after_inv_SxS_aux, or_intror, ex2_intro/
240 | elim (after_inv_OxS_aux … Hg … H) -g
241 /3 width=5 by or_introl, ex3_2_intro/
245 lemma after_inv_xxS: ∀g1,g2,f. g1 ⊚ g2 ≡ ⫯f →
246 (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨
247 ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1.
248 /2 width=3 by after_inv_xxS_aux/ qed-.
250 fact after_inv_xOx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ↑f2 →
251 f1 ⊚ f2 ≡ f ∧ n1 = n.
252 #f1 #g2 #f #n1 elim n1 -n1
253 [ #n #Hf #f2 #H2 elim (after_inv_OOx_aux … Hf … H2) -g2 [3: // |2: skip ]
254 #g #Hf #H elim (push_inv_seq_sn … H) -H destruct /2 width=1 by conj/
255 | #n1 #IH #n #Hf #f2 #H2 elim (after_inv_Sxx_aux … Hf) -Hf [3: // |2: skip ]
256 #g1 #Hg #H1 elim (next_inv_seq_sn … H1) -H1
257 #x #Hx #H destruct elim (IH … Hg) [2: // |3: skip ] -IH -Hg
258 #H destruct /2 width=1 by conj/
262 lemma after_inv_xOx: ∀f1,f2,f,n1,n. n1@f1 ⊚ ↑f2 ≡ n@f →
263 f1 ⊚ f2 ≡ f ∧ n1 = n.
264 /2 width=3 by after_inv_xOx_aux/ qed-.
266 fact after_inv_xSx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ⫯f2 →
267 ∃∃m. f1 ⊚ f2 ≡ m@f & n = ⫯(n1+m).
268 #f1 #g2 #f #n1 elim n1 -n1
269 [ #n #Hf #f2 #H2 elim (after_inv_OSx_aux … Hf … H2) -g2 [3: // |2: skip ]
270 #g #Hf #H elim (next_inv_seq_sn … H) -H
271 #x #Hx #Hg destruct /2 width=3 by ex2_intro/
272 | #n1 #IH #n #Hf #f2 #H2 elim (after_inv_Sxx_aux … Hf) -Hf [3: // |2: skip ]
273 #g #Hg #H elim (next_inv_seq_sn … H) -H
274 #x #Hx #H destruct elim (IH … Hg) -IH -Hg [3: // |2: skip ]
275 #m #Hf #Hm destruct /2 width=3 by ex2_intro/
279 lemma after_inv_xSx: ∀f1,f2,f,n1,n. n1@f1 ⊚ ⫯f2 ≡ n@f →
280 ∃∃m. f1 ⊚ f2 ≡ m@f & n = ⫯(n1+m).
281 /2 width=3 by after_inv_xSx_aux/ qed-.
283 lemma after_inv_const: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡ f ∧ n2 = 0.
284 #f1 #f2 #f #n2 #n elim n -n
285 [ #H elim (after_inv_OxO … H) -H
286 #g2 #Hf #H elim (push_inv_seq_sn … H) -H /2 width=1 by conj/
287 | #n #IH #H lapply (after_inv_SxS_aux … H ????) -H /2 width=5 by/
291 (* Forward lemmas on application ********************************************)
293 lemma after_at_fwd: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f →
294 ∃∃i2. @⦃i1, f1⦄ ≡ i2 & @⦃i2, f2⦄ ≡ i.
295 #f #i1 #i #H elim H -f -i1 -i
296 [ #f #f2 #f1 #H elim (after_inv_xxO … H) -H
297 /2 width=3 by at_refl, ex2_intro/
298 | #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_xxO … H) -H
299 #g2 #g1 #Hg #H1 #H2 destruct elim (IH … Hg) -f
300 /3 width=3 by at_S1, ex2_intro/
301 | #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_xxS … H) -H *
302 [ #g2 #g1 #Hg #H2 #H1 destruct elim (IH … Hg) -f
303 /3 width=3 by at_S1, at_next, ex2_intro/
304 | #g1 #Hg #H destruct elim (IH … Hg) -f
305 /3 width=3 by at_next, ex2_intro/
310 lemma after_at1_fwd: ∀f1,i1,i2. @⦃i1, f1⦄ ≡ i2 → ∀f2,f. f2 ⊚ f1 ≡ f →
311 ∃∃i. @⦃i2, f2⦄ ≡ i & @⦃i1, f⦄ ≡ i.
312 #f1 #i1 #i2 #H elim H -f1 -i1 -i2
313 [ #f1 * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H /2 width=3 by ex2_intro/
314 | #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H
315 #Hf #H destruct elim (IH … Hf) -f1 /3 width=3 by at_S1, ex2_intro/
316 | #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xSx … H) -H
317 #m #Hf #Hm destruct elim (IH … Hf) -f1
318 /4 width=3 by at_plus2, at_S1, at_next, ex2_intro/
322 lemma after_fwd_at: ∀f1,f2,i1,i2,i. @⦃i1, f1⦄ ≡ i2 → @⦃i2, f2⦄ ≡ i →
323 ∀f. f2 ⊚ f1 ≡ f → @⦃i1, f⦄ ≡ i.
324 #f1 #f2 #i1 #i2 #i #Hi1 #Hi2 #f #Ht elim (after_at1_fwd … Hi1 … Ht) -f1
325 #j #H #Hj >(at_mono … H … Hi2) -i2 //
328 lemma after_fwd_at1: ∀f2,f,i1,i2,i. @⦃i1, f⦄ ≡ i → @⦃i2, f2⦄ ≡ i →
329 ∀f1. f2 ⊚ f1 ≡ f → @⦃i1, f1⦄ ≡ i2.
330 #f2 #f #i1 #i2 #i #Hi1 #Hi2 #f1 #Ht elim (after_at_fwd … Hi1 … Ht) -f
331 #j1 #Hij1 #H >(at_inj … Hi2 … H) -i //
334 lemma after_fwd_at2: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f1,i2. @⦃i1, f1⦄ ≡ i2 →
335 ∀f2. f2 ⊚ f1 ≡ f → @⦃i2, f2⦄ ≡ i.
336 #f #i1 #i #H elim H -f -i1 -i
337 [ #f #f1 #i2 #Ht1 #f2 #H elim (after_inv_xxO … H) -H
338 #g2 #g1 #_ #H1 #H2 destruct >(at_inv_OOx … Ht1) -f -g1 -i2 //
339 | #f #i1 #i #_ #IH #f1 #i2 #Ht1 #f2 #H elim (after_inv_xxO … H) -H
340 #g2 #g1 #Hu #H1 #H2 destruct elim (at_inv_SOx … Ht1) -Ht1
341 /3 width=3 by at_push/
342 | #f #i1 #i #_ #IH #f1 #i2 #Hf1 #f2 #H elim (after_inv_xxS … H) -H *
343 [ #g2 #g1 #Hg #H2 #H1 destruct elim (at_inv_xSx … Hf1) -Hf1
344 /3 width=3 by at_push/
345 | #g2 #Hg #H destruct /3 width=3 by at_next/
350 (* Advanced forward lemmas on after *****************************************)
352 lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → n = f1@❴n2❵.
353 #f1 #f2 #f #n2 #n #H lapply (after_fwd_at … 0 … H) -H [1,4: // |2,3: skip ]
354 /3 width=2 by at_inv_O1, sym_eq/
357 lemma after_fwd_tl: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f →
358 tln … n2 f1 ⊚ f2 ≡ f.
359 #f #f2 #n2 elim n2 -n2
360 [ #f1 #n1 #n #H elim (after_inv_xOx … H) -H //
361 | #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xSx_aux … H ??) -H [3: // |2: skip ]
362 #m #Hm #H destruct /2 width=3 by/
366 lemma after_inv_apply: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f →
367 a = (a1@f1)@❴a2❵ ∧ tln … a2 f1 ⊚ f2 ≡ f.
368 /3 width=3 by after_fwd_tl, after_fwd_hd, conj/ qed-.
370 (* Main properties on after *************************************************)
372 let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 →
373 ∀f1,f2. f1 ⊚ f2 ≡ f0 →
374 ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?.
375 #f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4
376 [ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
377 cases (after_inv_xxO_aux … Hg0 … H0) -g0
379 cases (after_inv_OOx_aux … Hg … H2 H3) -g2 -g3
380 #f #Hf #H /3 width=7 by after_refl/
381 | #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
382 cases (after_inv_xxO_aux … Hg0 … H0) -g0
384 cases (after_inv_OSx_aux … Hg … H2 H3) -g2 -g3
385 #f #Hf #H /3 width=7 by after_push/
386 | #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg
387 cases (after_inv_xxS_aux … Hg0 … H0) -g0 *
388 [ #f1 #f2 #Hf0 #H1 #H2
389 cases (after_inv_Sxx_aux … Hg … H2) -g2
390 #f #Hf #H /3 width=7 by after_push/
391 | #f1 #Hf0 #H1 /3 width=6 by after_next/
396 let corec after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 →
397 ∀f2, f3. f2 ⊚ f3 ≡ f0 →
398 ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4 ≝ ?.
399 #f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4
400 [ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
401 cases (after_inv_xxO_aux … Hg0 … H0) -g0
403 cases (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
404 #f #Hf #H /3 width=7 by after_refl/
405 | #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
406 cases (after_inv_xxS_aux … Hg0 … H0) -g0 *
407 [ #f2 #f3 #Hf0 #H2 #H3
408 cases (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
409 #f #Hf #H /3 width=7 by after_push/
411 cases (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
412 #f #Hf #H /3 width=6 by after_next/
414 | #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg
415 cases (after_inv_Sxx_aux … Hg … H1) -g1
416 #f #Hg #H /3 width=6 by after_next/
420 (* Main inversion lemmas on after *******************************************)
422 let corec after_mono: ∀f1,f2,x. f1 ⊚ f2 ≡ x → ∀y. f1 ⊚ f2 ≡ y → x ≐ y ≝ ?.
423 * #n1 #f1 * #n2 #f2 * #n #x #Hx * #m #y #Hy
424 cases (after_inv_apply … Hx) -Hx #Hn #Hx
425 cases (after_inv_apply … Hy) -Hy #Hm #Hy
426 /3 width=4 by eq_seq/
429 let corec after_inj: ∀f1,x,f. f1 ⊚ x ≡ f → ∀y. f1 ⊚ y ≡ f → x ≐ y ≝ ?.
430 * #n1 #f1 * #n2 #x * #n #f #Hx * #m2 #y #Hy
431 cases (after_inv_apply … Hx) -Hx #Hn2 #Hx
432 cases (after_inv_apply … Hy) -Hy #Hm2
433 cases (apply_inj_aux … Hn2 Hm2) -n -m2 /3 width=4 by eq_seq/
436 theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f.
437 /2 width=4 by after_mono/ qed-.