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: nstream → nstream → nstream ≝ ?.
  22 #t1 * #b2 #t2 @(seq … (t1@❴b2❵)) @(compose ? t2) -compose -t2
  23 @(tln … (⫯b2) t1)
  24 qed.
  25
  26 interpretation "functional composition (nstream)"
  27    'compose t1 t2 = (compose t1 t2).
  28
  29 coinductive after: relation3 nstream nstream nstream ≝
  30 | after_zero: ∀t1,t2,t,b1,b2,b.
  31               after t1 t2 t →
  32               b1 = 0 → b2 = 0 → b = 0 →
  33               after (b1@t1) (b2@t2) (b@t)
  34 | after_skip: ∀t1,t2,t,b1,b2,b,a2,a.
  35               after t1 (a2@t2) (a@t) →
  36               b1 = 0 → b2 = ⫯a2 → b = ⫯a →
  37               after (b1@t1) (b2@t2) (b@t)
  38 | after_drop: ∀t1,t2,t,b1,b,a1,a.
  39               after (a1@t1) t2 (a@t) →
  40               b1 = ⫯a1 → b = ⫯a →
  41               after (b1@t1) t2 (b@t)
  42 .
  43
  44 interpretation "relational composition (nstream)"
  45    'RAfter t1 t2 t = (after t1 t2 t).
  46
  47 (* Basic properies on compose ***********************************************)
  48
  49 lemma compose_unfold: ∀t1,t2,a2. t1∘(a2@t2) = t1@❴a2❵@tln … (⫯a2) t1∘t2.
  50 #t1 #t2 #a2 >(stream_expand … (t1∘(a2@t2))) normalize //
  51 qed.
  52
  53 lemma compose_drop: ∀t1,t2,t,a1,a. (a1@t1)∘t2 = a@t → (⫯a1@t1)∘t2 = ⫯a@t.
  54 #t1 * #a2 #t2 #t #a1 #a >compose_unfold >compose_unfold
  55 #H destruct normalize //
  56 qed.
  57
  58 (* Basic inversion lemmas on compose ****************************************)
  59
  60 lemma compose_inv_unfold: ∀t1,t2,t,a2,a. t1∘(a2@t2) = a@t →
  61                           t1@❴a2❵ = a ∧ tln … (⫯a2) t1∘t2 = t.
  62 #t1 #t2 #t #a2 #a >(stream_expand … (t1∘(a2@t2))) normalize
  63 #H destruct /2 width=1 by conj/
  64 qed-.
  65
  66 lemma compose_inv_O2: ∀t1,t2,t,a1,a. (a1@t1)∘(O@t2) = a@t →
  67                       a = a1 ∧ t1∘t2 = t.
  68 #t1 #t2 #t #a1 #a >compose_unfold
  69 #H destruct /2 width=1 by conj/
  70 qed-.
  71
  72 lemma compose_inv_S2: ∀t1,t2,t,a1,a2,a. (a1@t1)∘(⫯a2@t2) = a@t →
  73                       a = ⫯(a1+t1@❴a2❵) ∧ t1∘(a2@t2) = t1@❴a2❵@t.
  74 #t1 #t2 #t #a1 #a2 #a >compose_unfold
  75 #H destruct /2 width=1 by conj/
  76 qed-.
  77
  78 lemma compose_inv_S1: ∀t1,t2,t,a1,a2,a. (⫯a1@t1)∘(a2@t2) = a@t →
  79                       a = ⫯((a1@t1)@❴a2❵) ∧ (a1@t1)∘(a2@t2) = (a1@t1)@❴a2❵@t.
  80 #t1 #t2 #t #a1 #a2 #a >compose_unfold
  81 #H destruct /2 width=1 by conj/
  82 qed-.
  83
  84 (* Basic properties on after ************************************************)
  85
  86 lemma after_O2: ∀t1,t2,t. t1 ⊚ t2 ≡ t →
  87                 ∀b. b@t1 ⊚ O@t2 ≡ b@t.
  88 #t1 #t2 #t #Ht #b elim b -b /2 width=5 by after_drop, after_zero/
  89 qed.
  90
  91 lemma after_S2: ∀t1,t2,t,b2,b. t1 ⊚ b2@t2 ≡ b@t →
  92                 ∀b1. b1@t1 ⊚ ⫯b2@t2 ≡ ⫯(b1+b)@t.
  93 #t1 #t2 #t #b2 #b #Ht #b1 elim b1 -b1 /2 width=5 by after_drop, after_skip/
  94 qed.
  95
  96 lemma after_apply: ∀b2,t1,t2,t. (tln … (⫯b2) t1) ⊚ t2 ≡ t → t1 ⊚ b2@t2 ≡ t1@❴b2❵@t.
  97 #b2 elim b2 -b2
  98 [ * /2 width=1 by after_O2/
  99 | #b2 #IH * /3 width=1 by after_S2/
 100 ]
 101 qed-.
 102
 103 let corec after_total_aux: ∀t1,t2,t. t1 ∘ t2 = t → t1 ⊚ t2 ≡ t ≝ ?.
 104 * #a1 #t1 * #a2 #t2 * #a #t cases a1 -a1
 105 [ cases a2 -a2
 106   [ #H cases (compose_inv_O2 … H) -H
 107     /3 width=1 by after_zero/
 108   | #a2 #H cases (compose_inv_S2 … H) -H
 109     /3 width=5 by after_skip, eq_f/
 110   ]
 111 | #a1 #H cases (compose_inv_S1 … H) -H
 112   /3 width=5 by after_drop, eq_f/
 113 ]
 114 qed-.
 115
 116 theorem after_total: ∀t2,t1. t1 ⊚ t2 ≡ t1 ∘ t2.
 117 /2 width=1 by after_total_aux/ qed.
 118
 119 (* Basic inversion lemmas on after ******************************************)
 120
 121 fact after_inv_O1_aux: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u1. t1 = 0@u1 →
 122                        (∃∃u2,u. u1 ⊚ u2 ≡ u & t2 = 0@u2 & t = 0@u) ∨
 123                        ∃∃u2,u,b2,b. u1 ⊚ b2@u2 ≡ b@u & t2 = ⫯b2@u2 & t = ⫯b@u.
 124 #t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1
 125 [ #b2 #b #Ht #H1 #H2 #H3 #u1 #H destruct /3 width=5 by ex3_2_intro, or_introl/
 126 | #b2 #b #a2 #a #Ht #H1 #H2 #H3 #u1 #H destruct /3 width=7 by ex3_4_intro, or_intror/
 127 | #b #a1 #a #_ #H1 #H3 #u1 #H destruct
 128 ]
 129 qed-.
 130
 131 fact after_inv_O1_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b1 = 0 →
 132                         (∧∧ t1 ⊚ t2 ≡ t & b2 = 0 & b = 0) ∨
 133                         ∃∃a2,a. t1 ⊚ a2@t2 ≡ a@t & b2 = ⫯a2 & b = ⫯a.
 134 #t1 #t2 #t #b1 #b2 #b #Ht #H elim (after_inv_O1_aux … Ht) -Ht [4: // |2: skip ] *
 135 [ #u2 #u #Hu #H1 #H2 destruct /3 width=1 by and3_intro, or_introl/
 136 | #u2 #u #a2 #a #Hu #H1 #H2 destruct /3 width=5 by ex3_2_intro, or_intror/
 137 ]
 138 qed-.
 139
 140 lemma after_inv_O1: ∀u1,t2,t. 0@u1 ⊚ t2 ≡ t →
 141                     (∃∃u2,u. u1 ⊚ u2 ≡ u & t2 = 0@u2 & t = 0@u) ∨
 142                     ∃∃u2,u,b2,b. u1 ⊚ b2@u2 ≡ b@u & t2 = ⫯b2@u2 & t = ⫯b@u.
 143 /2 width=3 by after_inv_O1_aux/ qed-.
 144
 145 fact after_inv_zero_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b1 = 0 → b2 = 0 →
 146                           t1 ⊚ t2 ≡ t ∧ b = 0.
 147 #t1 #t2 #t #b1 #b2 #b #Ht #H1 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 *
 148 [ /2 width=1 by conj/
 149 | #a1 #a2 #_ #H0 destruct
 150 ]
 151 qed-.
 152
 153 lemma after_inv_zero: ∀u1,u2,t. 0@u1 ⊚ 0@u2 ≡ t →
 154                       ∃∃u. u1 ⊚ u2 ≡ u & t = 0@u.
 155 #u1 #u2 #t #H elim (after_inv_O1 … H) -H *
 156 [ #x2 #u #Hu #H1 #H2 destruct /2 width=3 by ex2_intro/
 157 | #x2 #u #a2 #a #Hu #H destruct
 158 ]
 159 qed-.
 160
 161 fact after_inv_skip_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b1 = 0 → ∀a2. b2 = ⫯a2 →
 162                           ∃∃a. t1 ⊚ a2@t2 ≡ a@t & b = ⫯a.
 163 #t1 #t2 #t #b1 #b2 #b #Ht #H1 #a2 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 *
 164 [ #_ #H0 destruct
 165 | #x2 #x #H #H0 #H1 destruct /2 width=3 by ex2_intro/
 166 ]
 167 qed-.
 168
 169 lemma after_inv_skip: ∀u1,u2,t,b2. 0@u1 ⊚ ⫯b2@u2 ≡ t →
 170                       ∃∃u,b. u1 ⊚ b2@u2 ≡ b@u & t = ⫯b@u.
 171 #u1 #u2 * #b #t #b2 #Ht elim (after_inv_skip_aux2 … Ht) [2,4: // |3: skip ] -Ht
 172 #a #Ht #H destruct /2 width=4 by ex2_2_intro/
 173 qed-.
 174
 175 fact after_inv_S1_aux: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u1,b1. t1 = ⫯b1@u1 →
 176                        ∃∃u,b. b1@u1 ⊚ t2 ≡ b@u & t = ⫯b@u.
 177 #t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1
 178 [ #b2 #b #_ #H1 #H2 #H3 #u1 #a1 #H destruct
 179 | #b2 #b #a2 #a #_ #H1 #H2 #H3 #u1 #a1 #H destruct
 180 | #b #a1 #a #Ht #H1 #H3 #u1 #x1 #H destruct /2 width=4 by ex2_2_intro/
 181 ]
 182 qed-.
 183
 184 fact after_inv_S1_aux2: ∀t1,t2,t,b1,b. b1@t1 ⊚ t2 ≡ b@t → ∀a1. b1 = ⫯a1 →
 185                         ∃∃a. a1@t1 ⊚ t2 ≡ a@t & b = ⫯a.
 186 #t1 #t2 #t #b1 #b #Ht #a #H elim (after_inv_S1_aux … Ht) -Ht [4: // |2,3: skip ]
 187 #u #x #Hu #H0 destruct /2 width=3 by ex2_intro/
 188 qed-.
 189
 190 lemma after_inv_S1: ∀u1,t2,t,b1. ⫯b1@u1 ⊚ t2 ≡ t →
 191                     ∃∃u,b. b1@u1 ⊚ t2 ≡ b@u & t = ⫯b@u.
 192 /2 width=3 by after_inv_S1_aux/ qed-.
 193
 194 fact after_inv_drop_aux2: ∀t1,t2,t,a1,a. a1@t1 ⊚ t2 ≡ a@t → ∀b1,b. a1 = ⫯b1 → a = ⫯b →
 195                           b1@t1 ⊚ t2 ≡ b@t.
 196 #t1 #t2 #t #a1 #a #Ht #b1 #b #H1 #H elim (after_inv_S1_aux2 … Ht … H1) -a1
 197 #x #Ht #Hx destruct //
 198 qed-.
 199
 200 lemma after_inv_drop: ∀t1,t2,t,b1,b. ⫯b1@t1 ⊚ t2 ≡ ⫯b@t → b1@t1 ⊚ t2 ≡ b@t.
 201 /2 width=5 by after_inv_drop_aux2/ qed-.
 202
 203 fact after_inv_O3_aux1: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u. t = 0@u →
 204                         ∃∃u1,u2. u1 ⊚ u2 ≡ u & t1 = 0@u1 & t2 = 0@u2.
 205 #t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1
 206 [ #b2 #b #Ht #H1 #H2 #H3 #u #H destruct /2 width=5 by ex3_2_intro/
 207 | #b2 #b #a2 #a #_ #H1 #H2 #H3 #u #H destruct
 208 | #b #a1 #a #_ #H1 #H3 #u #H destruct
 209 ]
 210 qed-.
 211
 212 fact after_inv_O3_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b = 0 →
 213                         ∧∧ t1 ⊚ t2 ≡ t & b1 = 0 & b2 = 0.
 214 #t1 #t2 #t #b1 #b2 #b #Ht #H1 elim (after_inv_O3_aux1 … Ht) [2: // |3: skip ] -b
 215 #u1 #u2 #Ht #H1 #H2 destruct /2 width=1 by and3_intro/
 216 qed-.
 217
 218 lemma after_inv_O3: ∀t1,t2,u. t1 ⊚ t2 ≡ 0@u →
 219                     ∃∃u1,u2. u1 ⊚ u2 ≡ u & t1 = 0@u1 & t2 = 0@u2.
 220 /2 width=3 by after_inv_O3_aux1/ qed-.
 221
 222 fact after_inv_S3_aux1: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u,b. t = ⫯b@u →
 223                         (∃∃u1,u2,b2. u1 ⊚ b2@u2 ≡ b@u & t1 = 0@u1 & t2 = ⫯b2@u2) ∨
 224                         ∃∃u1,b1. b1@u1 ⊚ t2 ≡ b@u & t1 = ⫯b1@u1.
 225 #t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1
 226 [ #b2 #b #_ #H1 #H2 #H3 #u #a #H destruct
 227 | #b2 #b #a2 #a #HT #H1 #H2 #H3 #u #x #H destruct /3 width=6 by ex3_3_intro, or_introl/
 228 | #b #a1 #a #HT #H1 #H3 #u #x #H destruct /3 width=4 by ex2_2_intro, or_intror/
 229 ]
 230 qed-.
 231
 232 fact after_inv_S3_aux2: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ a2@t2 ≡ a@t → ∀b. a = ⫯b →
 233                         (∃∃b2. t1 ⊚ b2@t2 ≡ b@t & a1 = 0 & a2 = ⫯b2) ∨
 234                         ∃∃b1. b1@t1 ⊚ a2@t2 ≡ b@t & a1 = ⫯b1.
 235 #t1 #t2 #t #a1 #a2 #a #Ht #b #H elim (after_inv_S3_aux1 … Ht) [3: // |4,5: skip ] -a *
 236 [ #u1 #u2 #b2 #Ht #H1 #H2 destruct /3 width=3 by ex3_intro, or_introl/
 237 | #u1 #b1 #Ht #H1 destruct /3 width=3 by ex2_intro, or_intror/
 238 ]
 239 qed-.
 240
 241 lemma after_inv_S3: ∀t1,t2,u,b. t1 ⊚ t2 ≡ ⫯b@u →
 242                     (∃∃u1,u2,b2. u1 ⊚ b2@u2 ≡ b@u & t1 = 0@u1 & t2 = ⫯b2@u2) ∨
 243                     ∃∃u1,b1. b1@u1 ⊚ t2 ≡ b@u & t1 = ⫯b1@u1.
 244 /2 width=3 by after_inv_S3_aux1/ qed-.
 245
 246 (* Advanced inversion lemmas on after ***************************************)
 247
 248 fact after_inv_O2_aux2: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ a2@t2 ≡ a@t → a2 = 0 →
 249                          a1 = a ∧ t1 ⊚ t2 ≡ t.
 250 #t1 #t2 #t #a1 #a2 elim a1 -a1
 251 [ #a #H #H2 elim (after_inv_zero_aux2 … H … H2) -a2 /2 width=1 by conj/
 252 | #a1 #IH #a #H #H2 elim (after_inv_S1_aux2 … H) -H [3: // |2: skip ]
 253   #b #H #H1 elim (IH … H) // -a2
 254   #H2 destruct /2 width=1 by conj/
 255 ]
 256 qed-.
 257
 258 lemma after_inv_O2: ∀t1,u2,t. t1 ⊚ 0@u2 ≡ t →
 259                     ∃∃u1,u,a. t1 = a@u1 & t = a@u & u1 ⊚ u2 ≡ u.
 260 * #a1 #t1 #t2 * #a #t #H elim (after_inv_O2_aux2 … H) -H //
 261 /2 width=6 by ex3_3_intro/
 262 qed-.
 263
 264 lemma after_inv_const: ∀a,t1,b2,u2,t. a@t1 ⊚ b2@u2 ≡ a@t → b2 = 0.
 265 #a elim a -a
 266 [ #t1 #b2 #u2 #t #H elim (after_inv_O3 … H) -H
 267   #u1 #x2 #_ #_ #H destruct //
 268 | #a #IH #t1 #b2 #u2 #t #H elim (after_inv_S1 … H) -H
 269   #x #b #Hx #H destruct >(IH … Hx) -t1 -u2 -x -b2 -b //
 270 ]
 271 qed-.
 272
 273 lemma after_inv_S2: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ ⫯a2@t2 ≡ a@t → ∀b. a = ⫯(a1+b) →
 274                     t1 ⊚ a2@t2 ≡ b@t.
 275 #t1 #t2 #t #a1 elim a1 -a1
 276 [ #a2 #a #Ht #b #Hb
 277   elim (after_inv_skip_aux2 … Ht) -Ht [3,4: // |2: skip ]
 278   #c #Ht #Hc destruct //
 279 | #a1 #IH #a2 #a #Ht #b #Hb
 280   lapply (after_inv_drop_aux2 … Ht … Hb) -a [ // | skip ]
 281   /2 width=3 by/
 282 ]
 283 qed-.
 284
 285 (* Forward lemmas on application ********************************************)
 286
 287 lemma after_at_fwd: ∀t,i1,i. @⦃i1, t⦄ ≡ i → ∀t2,t1. t2 ⊚ t1 ≡ t →
 288                     ∃∃i2. @⦃i1, t1⦄ ≡ i2 & @⦃i2, t2⦄ ≡ i.
 289 #t #i1 #i #H elim H -t -i1 -i
 290 [ #t #t2 #t1 #H elim (after_inv_O3 … H) -H
 291   /2 width=3 by at_zero, ex2_intro/
 292 | #t #i1 #i #_ #IH #t2 #t1 #H elim (after_inv_O3 … H) -H
 293   #u2 #u1 #Hu #H1 #H2 destruct elim (IH … Hu) -t
 294   /3 width=3 by at_S1, ex2_intro/
 295 | #t #b #i1 #i #_ #IH #t2 #t1 #H elim (after_inv_S3 … H) -H *
 296   [ #u2 #u1 #b2 #Hu #H1 #H2 destruct elim (IH … Hu) -t -b
 297     /3 width=3 by at_S1, at_lift, ex2_intro/
 298   | #u1 #b1 #Hu #H destruct elim (IH … Hu) -t -b
 299     /3 width=3 by at_lift, ex2_intro/
 300   ]
 301 ]
 302 qed-.
 303
 304 lemma after_at1_fwd: ∀t1,i1,i2. @⦃i1, t1⦄ ≡ i2 → ∀t2,t. t2 ⊚ t1 ≡ t →
 305                      ∃∃i. @⦃i2, t2⦄ ≡ i & @⦃i1, t⦄ ≡ i.
 306 #t1 #i1 #i2 #H elim H -t1 -i1 -i2
 307 [ #t1 #t2 #t #H elim (after_inv_O2 … H) -H /2 width=3 by ex2_intro/
 308 | #t1 #i1 #i2 #_ #IH * #b2 elim b2 -b2
 309   [ #t2 #t #H elim (after_inv_zero … H) -H
 310     #u #Hu #H destruct elim (IH … Hu) -t1
 311     /3 width=3 by at_S1, at_skip, ex2_intro/
 312   | -IH #b2 #IH #t2 #t #H elim (after_inv_S1 … H) -H
 313     #u #b #Hu #H destruct elim (IH … Hu) -t1
 314     /3 width=3 by at_lift, ex2_intro/
 315   ]
 316 | #t1 #b1 #i1 #i2 #_ #IH * #b2 elim b2 -b2
 317   [ #t2 #t #H elim (after_inv_skip … H) -H
 318     #u #a #Hu #H destruct elim (IH … Hu) -t1 -b1
 319     /3 width=3 by at_S1, at_lift, ex2_intro/
 320   | -IH #b2 #IH #t2 #t #H elim (after_inv_S1 … H) -H
 321     #u #b #Hu #H destruct elim (IH … Hu) -t1 -b1
 322     /3 width=3 by at_lift, ex2_intro/
 323   ]
 324 ]
 325 qed-.
 326
 327 lemma after_fwd_at: ∀t1,t2,i1,i2,i. @⦃i1, t1⦄ ≡ i2 → @⦃i2, t2⦄ ≡ i →
 328                     ∀t. t2 ⊚ t1 ≡ t → @⦃i1, t⦄ ≡ i.
 329 #t1 #t2 #i1 #i2 #i #Hi1 #Hi2 #t #Ht elim (after_at1_fwd … Hi1 … Ht) -t1
 330 #j #H #Hj >(at_mono … H … Hi2) -i2 //
 331 qed-.
 332
 333 lemma after_fwd_at1: ∀t2,t,i1,i2,i. @⦃i1, t⦄ ≡ i → @⦃i2, t2⦄ ≡ i →
 334                      ∀t1. t2 ⊚ t1 ≡ t → @⦃i1, t1⦄ ≡ i2.
 335 #t2 #t #i1 #i2 #i #Hi1 #Hi2 #t1 #Ht elim (after_at_fwd … Hi1 … Ht) -t
 336 #j1 #Hij1 #H >(at_inj … Hi2 … H) -i //
 337 qed-.
 338
 339 lemma after_fwd_at2: ∀t,i1,i. @⦃i1, t⦄ ≡ i → ∀t1,i2. @⦃i1, t1⦄ ≡ i2 →
 340                      ∀t2. t2 ⊚ t1 ≡ t → @⦃i2, t2⦄ ≡ i.
 341 #t #i1 #i #H elim H -t -i1 -i
 342 [ #t #t1 #i2 #Ht1 #t2 #H elim (after_inv_O3 … H) -H
 343   #u2 #u1 #_ #H1 #H2 destruct >(at_inv_OOx … Ht1) -t -u1 -i2 //
 344 | #t #i1 #i #_ #IH #t1 #i2 #Ht1 #t2 #H elim (after_inv_O3 … H) -H
 345   #u2 #u1 #Hu #H1 #H2 destruct elim (at_inv_SOx … Ht1) -Ht1
 346   /3 width=3 by at_skip/
 347 | #t #b #i1 #i #_ #IH #t1 #i2 #Ht1 #t2 #H elim (after_inv_S3 … H) -H *
 348   [ #u2 #u1 #a1 #Hu #H1 #H2 destruct elim (at_inv_xSx … Ht1) -Ht1
 349     /3 width=3 by at_skip/
 350   | #u2 #a2 #Hu #H destruct /3 width=3 by at_lift/
 351   ]
 352 ]
 353 qed-.
 354
 355 (* Advanced forward lemmas on after *****************************************)
 356
 357 lemma after_fwd_hd: ∀t1,t2,t,a2,a. t1 ⊚ a2@t2 ≡ a@t → a = t1@❴a2❵.
 358 #t1 #t2 #t #a2 #a #Ht lapply (after_fwd_at … 0 … Ht) -Ht [4: // | // |2,3: skip ]
 359 /3 width=2 by at_inv_O1, sym_eq/
 360 qed-.
 361
 362 lemma after_fwd_tl: ∀t,t2,a2,t1,a1,a. a1@t1 ⊚ a2@t2 ≡ a@t →
 363                     tln … a2 t1 ⊚ t2 ≡ t.
 364 #t #t2 #a2 elim a2 -a2
 365 [ #t1 #a1 #a #Ht elim (after_inv_O2_aux2 … Ht) -Ht //
 366 | #a2 #IH * #b1 #t1 #a1 #a #Ht
 367   lapply (after_fwd_hd … Ht) #Ha
 368   lapply (after_inv_S2 … Ht … Ha) -a
 369   /2 width=3 by/
 370 ]
 371 qed-.
 372
 373 lemma after_inv_apply: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ a2@t2 ≡ a@t →
 374                        a = (a1@t1)@❴a2❵ ∧ tln … a2 t1 ⊚ t2 ≡ t.
 375 /3 width=3 by  after_fwd_tl, after_fwd_hd, conj/ qed-.
 376
 377 (* Main properties on after *************************************************)
 378
 379 let corec after_trans1: ∀t1,t2,t0. t1 ⊚ t2 ≡ t0 →
 380                         ∀t3,t4. t0 ⊚ t3 ≡ t4 →
 381                         ∀t. t2 ⊚ t3 ≡ t → t1 ⊚ t ≡ t4 ≝ ?.
 382 #t1 #t2 #t0 * -t1 -t2 -t0 #t1 #t2 #t0 #b1 [1,2: #b2 ] #b0
 383 [ #Ht0 #H1 #H2 #H0 * #b3 #t3 * #b4 #t4 #Ht4 * #b #t #Ht
 384   cases (after_inv_O1_aux2 … Ht4 H0) -Ht4 -H0 *
 385   [ #Ht4 #H3 #H4 cases (after_inv_zero_aux2 … Ht H2 H3) -Ht -H2 -H3
 386     #Ht #H /3 width=6 by after_zero/
 387   | #a0 #a4 #Ht4 #H3 #H4 cases (after_inv_skip_aux2 … Ht H2 … H3) -Ht -H2 -H3
 388     #a #Ht3 #H /3 width=6 by after_skip/
 389   ]
 390 | #a2 #a0 #Ht0 #H1 #H2 #H0 #t3 * #b4 #t4 #Ht4 cases (after_inv_S1_aux2 … Ht4 … H0) -Ht4 -H0
 391   #a4 #Ht4 #H4 * #b #t #H cases (after_inv_S1_aux2 … H … H2) -H -H2
 392   #a #Ht3 #H /3 width=6 by after_skip/
 393 | #a1 #a0 #Ht0 #H1 #H0 #t3 * #b4 #t4 #Ht4 cases (after_inv_S1_aux2 … Ht4 … H0) -Ht4 -H0
 394   #a4 #Ht4 #H4 * #b #t #Ht /3 width=6 by after_drop/
 395 ]
 396 qed-.
 397
 398 let corec after_trans2: ∀t1,t0,t4. t1 ⊚ t0 ≡ t4 →
 399                         ∀t2, t3. t2 ⊚ t3 ≡ t0 →
 400                         ∀t. t1 ⊚ t2 ≡ t → t ⊚ t3 ≡ t4 ≝ ?.
 401 #t1 #t0 #t4 * -t1 -t0 -t4 #t1 #t0 #t4 #b1 [1,2: #b0 ] #b4
 402 [ #Ht4 #H1 #H0 #H4 * #b2 #t2 * #b3 #t3 #Ht0 * #b #t #Ht
 403   cases (after_inv_O3_aux2 … Ht0 H0) -b0
 404   #Ht0 #H2 #H3 cases (after_inv_zero_aux2 … Ht H1 H2) -b1 -b2
 405   #Ht #H /3 width=6 by after_zero/
 406 | #a0 #a4 #Ht4 #H1 #H0 #H4 * #b2 #t2 * #b3 #t3 #Ht0 * #b #t #Ht
 407   cases (after_inv_S3_aux2 … Ht0 … H0) -b0 *
 408   [ #a3 #Ht0 #H2 #H3 cases (after_inv_zero_aux2 … Ht H1 H2) -b1 -b2
 409     #Ht #H /3 width=6 by after_skip/
 410   | #a2 #Ht0 #H2 cases (after_inv_skip_aux2 … Ht H1 … H2) -b1 -b2
 411     #a #Ht #H /3 width=6 by after_drop/
 412   ]
 413 | #a1 #a4 #Ht4 #H1 #H4 * #b2 #t2 * #b3 #t3 #Ht0 * #b #t #Ht
 414   cases (after_inv_S1_aux2 … Ht … H1) -b1
 415   #a #Ht #H /3 width=6 by after_drop/
 416 ]
 417 qed-.
 418
 419 let corec after_mono: ∀t1,t2,x. t1 ⊚ t2 ≡ x → ∀y. t1 ⊚ t2 ≡ y → x ≐ y ≝ ?.
 420 * #a1 #t1 * #a2 #t2 * #c #x #Hx * #d #y #Hy
 421 cases (after_inv_apply … Hx) -Hx #Hc #Hx
 422 cases (after_inv_apply … Hy) -Hy #Hd #Hy
 423 /3 width=4 by eq_sec/
 424 qed-.
 425
 426 let corec after_inj: ∀t1,x,t. t1 ⊚ x ≡ t → ∀y. t1 ⊚ y ≡ t → x ≐ y ≝ ?.
 427 * #a1 #t1 * #c #x * #a #t #Hx * #d #y #Hy
 428 cases (after_inv_apply … Hx) -Hx #Hc #Hx
 429 cases (after_inv_apply … Hy) -Hy #Hd
 430 cases (apply_inj_aux … Hc Hd) #Hy -a -d /3 width=4 by eq_sec/
 431 qed-.
 432
 433 (* Main inversion lemmas on after *******************************************)
 434
 435 theorem after_inv_total: ∀t1,t2,t. t1 ⊚ t2 ≡ t → t1 ∘ t2 ≐ t.
 436 /2 width=4 by after_mono/ qed-.