-lemma after_inv_apply: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f →
- a = (a1@f1)@❴a2❵ ∧ tln … a2 f1 ⊚ f2 ≡ f.
-/3 width=3 by after_fwd_tl, after_fwd_hd, conj/ qed-.
-
-(* Main properties on after *************************************************)
-
-let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 →
- ∀f1,f2. f1 ⊚ f2 ≡ f0 →
- ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?.
-#f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4
-[ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
- cases (after_inv_xxO_aux … Hg0 … H0) -g0
- #f1 #f2 #Hf0 #H1 #H2
- cases (after_inv_OOx_aux … Hg … H2 H3) -g2 -g3
- #f #Hf #H /3 width=7 by after_refl/
-| #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
- cases (after_inv_xxO_aux … Hg0 … H0) -g0
- #f1 #f2 #Hf0 #H1 #H2
- cases (after_inv_OSx_aux … Hg … H2 H3) -g2 -g3
- #f #Hf #H /3 width=7 by after_push/
-| #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg
- cases (after_inv_xxS_aux … Hg0 … H0) -g0 *
- [ #f1 #f2 #Hf0 #H1 #H2
- cases (after_inv_Sxx_aux … Hg … H2) -g2
- #f #Hf #H /3 width=7 by after_push/
- | #f1 #Hf0 #H1 /3 width=6 by after_next/
- ]
-]
-qed-.
-
-let corec after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 →
- ∀f2, f3. f2 ⊚ f3 ≡ f0 →
- ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4 ≝ ?.
-#f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4
-[ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
- cases (after_inv_xxO_aux … Hg0 … H0) -g0
- #f2 #f3 #Hf0 #H2 #H3
- cases (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
- #f #Hf #H /3 width=7 by after_refl/
-| #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
- cases (after_inv_xxS_aux … Hg0 … H0) -g0 *
- [ #f2 #f3 #Hf0 #H2 #H3
- cases (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
- #f #Hf #H /3 width=7 by after_push/
- | #f2 #Hf0 #H2
- cases (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
- #f #Hf #H /3 width=6 by after_next/
- ]
-| #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg
- cases (after_inv_Sxx_aux … Hg … H1) -g1
- #f #Hg #H /3 width=6 by after_next/
-]
-qed-.
-
-(* Main inversion lemmas on after *******************************************)
-
-let corec after_mono: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g →
- f1 ≐ g1 → f2 ≐ g2 → f ≐ g ≝ ?.
-* #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2
-cases (after_inv_apply … Hf) -Hf #Hn #Hf
-cases (after_inv_apply … Hg) -Hg #Hm #Hg
-cases (eq_stream_inv_seq ????? H1) -H1
-cases (eq_stream_inv_seq ????? H2) -H2
-/4 width=8 by apply_eq_repl, tln_eq_repl, eq_seq/
-qed-.
-
-let corec after_inj: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g →
- f1 ≐ g1 → f ≐ g → f2 ≐ g2 ≝ ?.
-* #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2
-cases (after_inv_apply … Hf) -Hf #Hn #Hf
-cases (after_inv_apply … Hg) -Hg #Hm #Hg
-cases (eq_stream_inv_seq ????? H1) -H1 #Hnm1 #Hfg1
-cases (eq_stream_inv_seq ????? H2) -H2 #Hnm #Hfg
-lapply (apply_inj_aux … Hn Hm Hnm ?) -n -m
-/4 width=8 by tln_eq_repl, eq_seq/
-qed-.
-
-theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f.
-/2 width=8 by after_mono/ qed-.
-
-(* Properties on after ******************************************************)
-
-lemma after_isid_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ≐ f → 𝐈⦃f1⦄.
-#f2 #f1 #f #Ht #H2 @isid_at_total
-#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -f1
-/3 width=6 by at_inj, eq_stream_sym/
-qed.
-
-lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄.
-#f2 #f1 #f #Ht #H1 @isid_at_total
-#i2 #i #Hi2 lapply (at_total i2 f1)
-#H0 lapply (at_increasing … H0)
-#Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht)
-/3 width=7 by at_eq_repl_back, at_mono, at_id_le/
-qed.
-
-(* Inversion lemmas on after ************************************************)
-
-let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?.
-* #n1 #f1 * * [ | #n2 ] #f2 #H cases (isid_inv_seq … H) -H
-/3 width=7 by after_push, after_refl/
-qed-.
-
-let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?.
-* #n2 #f2 * *
-[ #f1 #H cases (isid_inv_seq … H) -H
- /3 width=7 by after_refl/
-| #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/
-]
-qed-.
-
-lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f.
-/3 width=8 by isid_after_sn, after_mono/
-qed-.
-
-lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≐ f.
-/3 width=8 by isid_after_dx, after_mono/
-qed-.
-
-axiom after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄.