matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  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".
  18
  19 (* RELOCATION N-STREAM ******************************************************)
  20
  21 let corec compose: rtmap → rtmap → rtmap ≝ ?.
  22 #f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2
  23 @(tln … (⫯n2) f1)
  24 defined.
  25
  26 interpretation "functional composition (nstream)"
  27    'compose f1 f2 = (compose f1 f2).
  28
  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
  36 .
  37
  38 interpretation "relational composition (nstream)"
  39    'RAfter f1 f2 f = (after f1 f2 f).
  40
  41 (* Basic properies on compose ***********************************************)
  42
  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 //
  45 qed.
  46
  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 //
  50 qed.
  51
  52 (* Basic inversion lemmas on compose ****************************************)
  53
  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/
  58 qed-.
  59
  60 lemma compose_inv_O2: ∀f1,f2,f,n1,n. (n1@f1)∘(↑f2) = n@f →
  61                       n = n1 ∧ f1∘f2 = f.
  62 #f1 #f2 #f #n1 #n >compose_unfold
  63 #H destruct /2 width=1 by conj/
  64 qed-.
  65
  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/
  70 qed-.
  71
  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/
  76 qed-.
  77
  78 (* Basic properties on after ************************************************)
  79
  80 lemma after_O2: ∀f1,f2,f. f1 ⊚ f2 ≡ f →
  81                 ∀n. n@f1 ⊚ ↑f2 ≡ n@f.
  82 #f1 #f2 #f #Ht #n elim n -n /2 width=7 by after_refl, after_next/
  83 qed.
  84
  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/
  88 qed.
  89
  90 lemma after_apply: ∀n2,f1,f2,f. (tln … (⫯n2) f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ≡ f1@❴n2❵@f.
  91 #n2 elim n2 -n2
  92 [ * /2 width=1 by after_O2/
  93 | #n2 #IH * /3 width=1 by after_S2/
  94 ]
  95 qed-.
  96
  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
  99 [ cases n2 -n2
 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/
 104   ]
 105 | #n1 #H cases (compose_inv_S1 … H) -H
 106   /4 width=7 by after_next, next_rew_sn/
 107 ]
 108 qed-.
 109
 110 theorem after_total: ∀f2,f1. f1 ⊚ f2 ≡ f1 ∘ f2.
 111 /2 width=1 by after_total_aux/ qed.
 112
 113 (* Basic inversion lemmas on after ******************************************)
 114
 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)
 125 ]
 126 qed-.
 127
 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-.
 130
 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)
 141 ]
 142 qed-.
 143
 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-.
 146
 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/
 157 ]
 158 qed-.
 159
 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-.
 162
 163 (* Advanced inversion lemmas on after ***************************************)
 164
 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 //
 169 qed-.
 170
 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)
 175 qed-.
 176
 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 //
 181 qed-.
 182
 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)
 187 qed-.
 188
 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 //
 193 qed-.
 194
 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)
 199 qed-.
 200
 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/
 207 ]
 208 qed-.
 209
 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-.
 213
 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 //
 220 ]
 221 qed-.
 222
 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/
 228 ]
 229 qed-.
 230
 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-.
 234
 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/
 242 ]
 243 qed-.
 244
 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-.
 249
 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/
 259 ]
 260 qed-.
 261
 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-.
 265
 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/
 276 ]
 277 qed-.
 278
 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-.
 282
 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/
 288 ]
 289 qed-.
 290
 291 (* Forward lemmas on application ********************************************)
 292
 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/
 306   ]
 307 ]
 308 qed-.
 309
 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/
 319 ]
 320 qed-.
 321
 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 //
 326 qed-.
 327
 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 //
 332 qed-.
 333
 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/
 346   ]
 347 ]
 348 qed-.
 349
 350 (* Advanced forward lemmas on after *****************************************)
 351
 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/
 355 qed-.
 356
 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/
 363 ]
 364 qed-.
 365
 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-.
 369
 370 (* Main properties on after *************************************************)
 371
 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
 378   #f1 #f2 #Hf0 #H1 #H2
 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
 383   #f1 #f2 #Hf0 #H1 #H2
 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/
 392   ]
 393 ]
 394 qed-.
 395
 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
 402   #f2 #f3 #Hf0 #H2 #H3
 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/
 410   | #f2 #Hf0 #H2
 411     cases (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
 412     #f #Hf #H /3 width=6 by after_next/
 413   ]
 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/
 417 ]
 418 qed-.
 419
 420 (* Main inversion lemmas on after *******************************************)
 421
 422 let corec after_mono: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g →
 423                       f1 ≐ g1 → f2 ≐ g2 → f ≐ g ≝ ?.
 424 * #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2
 425 cases (after_inv_apply … Hf) -Hf #Hn #Hf
 426 cases (after_inv_apply … Hg) -Hg #Hm #Hg
 427 cases (eq_stream_inv_seq ????? H1) -H1
 428 cases (eq_stream_inv_seq ????? H2) -H2
 429 /4 width=8 by apply_eq_repl, tln_eq_repl, eq_seq/
 430 qed-.
 431
 432 let corec after_inj: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g →
 433                      f1 ≐ g1 → f ≐ g → f2 ≐ g2 ≝ ?.
 434 * #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2
 435 cases (after_inv_apply … Hf) -Hf #Hn #Hf
 436 cases (after_inv_apply … Hg) -Hg #Hm #Hg
 437 cases (eq_stream_inv_seq ????? H1) -H1 #Hnm1 #Hfg1
 438 cases (eq_stream_inv_seq ????? H2) -H2 #Hnm #Hfg
 439 lapply (apply_inj_aux … Hn Hm Hnm ?) -n -m
 440 /4 width=8 by tln_eq_repl, eq_seq/
 441 qed-.
 442
 443 theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f.
 444 /2 width=8 by after_mono/ qed-.