X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream_after.ma;h=b27633d1187a4b83885090f7d463c7545c7e878c;hb=85ba2f09d81f44b8c75505cc470f1fc5c431b9f2;hp=154ba25e3fbb76df3a449d9ff5eedc5e67833952;hpb=a02ba10c669642bd4b75a5b0ac9351c24ddb724a;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma index 154ba25e3..b27633d11 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma @@ -18,419 +18,443 @@ include "ground_2/relocation/nstream_at.ma". (* RELOCATION N-STREAM ******************************************************) -let corec compose: nstream → nstream → nstream ≝ ?. -#t1 * #b2 #t2 @(seq … (t1@❴b2❵)) @(compose ? t2) -compose -t2 -@(tln … (⫯b2) t1) -qed. +let corec compose: rtmap → rtmap → rtmap ≝ ?. +#f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2 +@(tln … (⫯n2) f1) +defined. interpretation "functional composition (nstream)" - 'compose t1 t2 = (compose t1 t2). - -coinductive after: relation3 nstream nstream nstream ≝ -| after_zero: ∀t1,t2,t,b1,b2,b. - after t1 t2 t → - b1 = 0 → b2 = 0 → b = 0 → - after (b1@t1) (b2@t2) (b@t) -| after_skip: ∀t1,t2,t,b1,b2,b,a2,a. - after t1 (a2@t2) (a@t) → - b1 = 0 → b2 = ⫯a2 → b = ⫯a → - after (b1@t1) (b2@t2) (b@t) -| after_drop: ∀t1,t2,t,b1,b,a1,a. - after (a1@t1) t2 (a@t) → - b1 = ⫯a1 → b = ⫯a → - after (b1@t1) t2 (b@t) + 'compose f1 f2 = (compose f1 f2). + +coinductive after: relation3 rtmap rtmap rtmap ≝ +| after_refl: ∀f1,f2,f,g1,g2,g. + after f1 f2 f → g1 = ↑f1 → g2 = ↑f2 → g = ↑f → after g1 g2 g +| after_push: ∀f1,f2,f,g1,g2,g. + after f1 f2 f → g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → after g1 g2 g +| after_next: ∀f1,f2,f,g1,g. + after f1 f2 f → g1 = ⫯f1 → g = ⫯f → after g1 f2 g . interpretation "relational composition (nstream)" - 'RAfter t1 t2 t = (after t1 t2 t). + 'RAfter f1 f2 f = (after f1 f2 f). (* Basic properies on compose ***********************************************) -lemma compose_unfold: ∀t1,t2,a2. t1∘(a2@t2) = t1@❴a2❵@tln … (⫯a2) t1∘t2. -#t1 #t2 #a2 >(stream_expand … (t1∘(a2@t2))) normalize // +lemma compose_unfold: ∀f1,f2,n2. f1∘(n2@f2) = f1@❴n2❵@tln … (⫯n2) f1∘f2. +#f1 #f2 #n2 >(stream_expand … (f1∘(n2@f2))) normalize // qed. -lemma compose_drop: ∀t1,t2,t,a1,a. (a1@t1)∘t2 = a@t → (⫯a1@t1)∘t2 = ⫯a@t. -#t1 * #a2 #t2 #t #a1 #a >compose_unfold >compose_unfold +lemma compose_next: ∀f1,f2,f. f1∘f2 = f → (⫯f1)∘f2 = ⫯f. +* #n1 #f1 * #n2 #f2 #f >compose_unfold >compose_unfold #H destruct normalize // qed. (* Basic inversion lemmas on compose ****************************************) -lemma compose_inv_unfold: ∀t1,t2,t,a2,a. t1∘(a2@t2) = a@t → - t1@❴a2❵ = a ∧ tln … (⫯a2) t1∘t2 = t. -#t1 #t2 #t #a2 #a >(stream_expand … (t1∘(a2@t2))) normalize +lemma compose_inv_unfold: ∀f1,f2,f,n2,n. f1∘(n2@f2) = n@f → + f1@❴n2❵ = n ∧ tln … (⫯n2) f1∘f2 = f. +#f1 #f2 #f #n2 #n >(stream_expand … (f1∘(n2@f2))) normalize #H destruct /2 width=1 by conj/ qed-. -lemma compose_inv_O2: ∀t1,t2,t,a1,a. (a1@t1)∘(O@t2) = a@t → - a = a1 ∧ t1∘t2 = t. -#t1 #t2 #t #a1 #a >compose_unfold +lemma compose_inv_O2: ∀f1,f2,f,n1,n. (n1@f1)∘(↑f2) = n@f → + n = n1 ∧ f1∘f2 = f. +#f1 #f2 #f #n1 #n >compose_unfold #H destruct /2 width=1 by conj/ qed-. -lemma compose_inv_S2: ∀t1,t2,t,a1,a2,a. (a1@t1)∘(⫯a2@t2) = a@t → - a = ⫯(a1+t1@❴a2❵) ∧ t1∘(a2@t2) = t1@❴a2❵@t. -#t1 #t2 #t #a1 #a2 #a >compose_unfold +lemma compose_inv_S2: ∀f1,f2,f,n1,n2,n. (n1@f1)∘(⫯n2@f2) = n@f → + n = ⫯(n1+f1@❴n2❵) ∧ f1∘(n2@f2) = f1@❴n2❵@f. +#f1 #f2 #f #n1 #n2 #n >compose_unfold #H destruct /2 width=1 by conj/ qed-. -lemma compose_inv_S1: ∀t1,t2,t,a1,a2,a. (⫯a1@t1)∘(a2@t2) = a@t → - a = ⫯((a1@t1)@❴a2❵) ∧ (a1@t1)∘(a2@t2) = (a1@t1)@❴a2❵@t. -#t1 #t2 #t #a1 #a2 #a >compose_unfold +lemma compose_inv_S1: ∀f1,f2,f,n1,n2,n. (⫯n1@f1)∘(n2@f2) = n@f → + n = ⫯((n1@f1)@❴n2❵) ∧ (n1@f1)∘(n2@f2) = (n1@f1)@❴n2❵@f. +#f1 #f2 #f #n1 #n2 #n >compose_unfold #H destruct /2 width=1 by conj/ qed-. (* Basic properties on after ************************************************) -lemma after_O2: ∀t1,t2,t. t1 ⊚ t2 ≡ t → - ∀b. b@t1 ⊚ O@t2 ≡ b@t. -#t1 #t2 #t #Ht #b elim b -b /2 width=5 by after_drop, after_zero/ +lemma after_O2: ∀f1,f2,f. f1 ⊚ f2 ≡ f → + ∀n. n@f1 ⊚ ↑f2 ≡ n@f. +#f1 #f2 #f #Ht #n elim n -n /2 width=7 by after_refl, after_next/ qed. -lemma after_S2: ∀t1,t2,t,b2,b. t1 ⊚ b2@t2 ≡ b@t → - ∀b1. b1@t1 ⊚ ⫯b2@t2 ≡ ⫯(b1+b)@t. -#t1 #t2 #t #b2 #b #Ht #b1 elim b1 -b1 /2 width=5 by after_drop, after_skip/ +lemma after_S2: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → + ∀n1. n1@f1 ⊚ ⫯n2@f2 ≡ ⫯(n1+n)@f. +#f1 #f2 #f #n2 #n #Ht #n1 elim n1 -n1 /2 width=7 by after_next, after_push/ qed. -lemma after_apply: ∀b2,t1,t2,t. (tln … (⫯b2) t1) ⊚ t2 ≡ t → t1 ⊚ b2@t2 ≡ t1@❴b2❵@t. -#b2 elim b2 -b2 +lemma after_apply: ∀n2,f1,f2,f. (tln … (⫯n2) f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ≡ f1@❴n2❵@f. +#n2 elim n2 -n2 [ * /2 width=1 by after_O2/ -| #b2 #IH * /3 width=1 by after_S2/ +| #n2 #IH * /3 width=1 by after_S2/ ] qed-. -let corec after_total_aux: ∀t1,t2,t. t1 ∘ t2 = t → t1 ⊚ t2 ≡ t ≝ ?. -* #a1 #t1 * #a2 #t2 * #a #t cases a1 -a1 -[ cases a2 -a2 +let corec after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f ≝ ?. +* #n1 #f1 * #n2 #f2 * #n #f cases n1 -n1 +[ cases n2 -n2 [ #H cases (compose_inv_O2 … H) -H - /3 width=1 by after_zero/ - | #a2 #H cases (compose_inv_S2 … H) -H - /3 width=5 by after_skip, eq_f/ + /3 width=7 by after_refl, eq_f2/ + | #n2 #H cases (compose_inv_S2 … H) -H + /3 width=7 by after_push/ ] -| #a1 #H cases (compose_inv_S1 … H) -H - /3 width=5 by after_drop, eq_f/ +| #n1 #H cases (compose_inv_S1 … H) -H + /4 width=7 by after_next, next_rew_sn/ ] qed-. -theorem after_total: ∀t2,t1. t1 ⊚ t2 ≡ t1 ∘ t2. +theorem after_total: ∀f2,f1. f1 ⊚ f2 ≡ f1 ∘ f2. /2 width=1 by after_total_aux/ qed. (* Basic inversion lemmas on after ******************************************) -fact after_inv_O1_aux: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u1. t1 = 0@u1 → - (∃∃u2,u. u1 ⊚ u2 ≡ u & t2 = 0@u2 & t = 0@u) ∨ - ∃∃u2,u,b2,b. u1 ⊚ b2@u2 ≡ b@u & t2 = ⫯b2@u2 & t = ⫯b@u. -#t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1 -[ #b2 #b #Ht #H1 #H2 #H3 #u1 #H destruct /3 width=5 by ex3_2_intro, or_introl/ -| #b2 #b #a2 #a #Ht #H1 #H2 #H3 #u1 #H destruct /3 width=7 by ex3_4_intro, or_intror/ -| #b #a1 #a #_ #H1 #H3 #u1 #H destruct +fact after_inv_OOx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ↑f2 → + ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f. +#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1 +[ #g2 #g #Hf #H1 #H2 #H #x1 #x2 #Hx1 #Hx2 destruct + <(injective_push … Hx1) <(injective_push … Hx2) -x2 -x1 + /2 width=3 by ex2_intro/ +| #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct + elim (discr_next_push … Hx2) +| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct + elim (discr_next_push … Hx1) ] qed-. -fact after_inv_O1_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b1 = 0 → - (∧∧ t1 ⊚ t2 ≡ t & b2 = 0 & b = 0) ∨ - ∃∃a2,a. t1 ⊚ a2@t2 ≡ a@t & b2 = ⫯a2 & b = ⫯a. -#t1 #t2 #t #b1 #b2 #b #Ht #H elim (after_inv_O1_aux … Ht) -Ht [4: // |2: skip ] * -[ #u2 #u #Hu #H1 #H2 destruct /3 width=1 by and3_intro, or_introl/ -| #u2 #u #a2 #a #Hu #H1 #H2 destruct /3 width=5 by ex3_2_intro, or_intror/ +lemma after_inv_OOx: ∀f1,f2,g. ↑f1 ⊚ ↑f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f. +/2 width=5 by after_inv_OOx_aux/ qed-. + +fact after_inv_OSx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ⫯f2 → + ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f. +#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1 +[ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct + elim (discr_push_next … Hx2) +| #g2 #g #Hf #H1 #H2 #H3 #x1 #x2 #Hx1 #Hx2 destruct + <(injective_push … Hx1) <(injective_next … Hx2) -x2 -x1 + /2 width=3 by ex2_intro/ +| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct + elim (discr_next_push … Hx1) ] qed-. -lemma after_inv_O1: ∀u1,t2,t. 0@u1 ⊚ t2 ≡ t → - (∃∃u2,u. u1 ⊚ u2 ≡ u & t2 = 0@u2 & t = 0@u) ∨ - ∃∃u2,u,b2,b. u1 ⊚ b2@u2 ≡ b@u & t2 = ⫯b2@u2 & t = ⫯b@u. -/2 width=3 by after_inv_O1_aux/ qed-. +lemma after_inv_OSx: ∀f1,f2,g. ↑f1 ⊚ ⫯f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f. +/2 width=5 by after_inv_OSx_aux/ qed-. -fact after_inv_zero_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b1 = 0 → b2 = 0 → - t1 ⊚ t2 ≡ t ∧ b = 0. -#t1 #t2 #t #b1 #b2 #b #Ht #H1 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 * -[ /2 width=1 by conj/ -| #a1 #a2 #_ #H0 destruct +fact after_inv_Sxx_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g → ∀f1. g1 = ⫯f1 → + ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f. +#g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1 +[ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct + elim (discr_push_next … Hx1) +| #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct + elim (discr_push_next … Hx1) +| #g #Hf #H1 #H #x1 #Hx1 destruct + <(injective_next … Hx1) -x1 + /2 width=3 by ex2_intro/ ] qed-. -lemma after_inv_zero: ∀u1,u2,t. 0@u1 ⊚ 0@u2 ≡ t → - ∃∃u. u1 ⊚ u2 ≡ u & t = 0@u. -#u1 #u2 #t #H elim (after_inv_O1 … H) -H * -[ #x2 #u #Hu #H1 #H2 destruct /2 width=3 by ex2_intro/ -| #x2 #u #a2 #a #Hu #H destruct -] -qed-. +lemma after_inv_Sxx: ∀f1,f2,g. ⫯f1 ⊚ f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f. +/2 width=5 by after_inv_Sxx_aux/ qed-. -fact after_inv_skip_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b1 = 0 → ∀a2. b2 = ⫯a2 → - ∃∃a. t1 ⊚ a2@t2 ≡ a@t & b = ⫯a. -#t1 #t2 #t #b1 #b2 #b #Ht #H1 #a2 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 * -[ #_ #H0 destruct -| #x2 #x #H #H0 #H1 destruct /2 width=3 by ex2_intro/ -] -qed-. +(* Advanced inversion lemmas on after ***************************************) -lemma after_inv_skip: ∀u1,u2,t,b2. 0@u1 ⊚ ⫯b2@u2 ≡ t → - ∃∃u,b. u1 ⊚ b2@u2 ≡ b@u & t = ⫯b@u. -#u1 #u2 * #b #t #b2 #Ht elim (after_inv_skip_aux2 … Ht) [2,4: // |3: skip ] -Ht -#a #Ht #H destruct /2 width=4 by ex2_2_intro/ +fact after_inv_OOO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ↑f → f1 ⊚ f2 ≡ f. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct >(injective_push … Hx) -f // qed-. -fact after_inv_S1_aux: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u1,b1. t1 = ⫯b1@u1 → - ∃∃u,b. b1@u1 ⊚ t2 ≡ b@u & t = ⫯b@u. -#t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1 -[ #b2 #b #_ #H1 #H2 #H3 #u1 #a1 #H destruct -| #b2 #b #a2 #a #_ #H1 #H2 #H3 #u1 #a1 #H destruct -| #b #a1 #a #Ht #H1 #H3 #u1 #x1 #H destruct /2 width=4 by ex2_2_intro/ -] +fact after_inv_OOS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ⫯f → ⊥. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct elim (discr_next_push … Hx) qed-. -fact after_inv_S1_aux2: ∀t1,t2,t,b1,b. b1@t1 ⊚ t2 ≡ b@t → ∀a1. b1 = ⫯a1 → - ∃∃a. a1@t1 ⊚ t2 ≡ a@t & b = ⫯a. -#t1 #t2 #t #b1 #b #Ht #a #H elim (after_inv_S1_aux … Ht) -Ht [4: // |2,3: skip ] -#u #x #Hu #H0 destruct /2 width=3 by ex2_intro/ +fact after_inv_OSS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → f1 ⊚ f2 ≡ f. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct >(injective_next … Hx) -f // qed-. -lemma after_inv_S1: ∀u1,t2,t,b1. ⫯b1@u1 ⊚ t2 ≡ t → - ∃∃u,b. b1@u1 ⊚ t2 ≡ b@u & t = ⫯b@u. -/2 width=3 by after_inv_S1_aux/ qed-. - -fact after_inv_drop_aux2: ∀t1,t2,t,a1,a. a1@t1 ⊚ t2 ≡ a@t → ∀b1,b. a1 = ⫯b1 → a = ⫯b → - b1@t1 ⊚ t2 ≡ b@t. -#t1 #t2 #t #a1 #a #Ht #b1 #b #H1 #H elim (after_inv_S1_aux2 … Ht … H1) -a1 -#x #Ht #Hx destruct // +fact after_inv_OSO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ↑f → ⊥. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct elim (discr_push_next … Hx) qed-. -lemma after_inv_drop: ∀t1,t2,t,b1,b. ⫯b1@t1 ⊚ t2 ≡ ⫯b@t → b1@t1 ⊚ t2 ≡ b@t. -/2 width=5 by after_inv_drop_aux2/ qed-. +fact after_inv_SxS_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g → + ∀f1,f. g1 = ⫯f1 → g = ⫯f → f1 ⊚ f2 ≡ f. +#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1 +#x #Hf #Hx destruct >(injective_next … Hx) -f // +qed-. -fact after_inv_O3_aux1: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u. t = 0@u → - ∃∃u1,u2. u1 ⊚ u2 ≡ u & t1 = 0@u1 & t2 = 0@u2. -#t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1 -[ #b2 #b #Ht #H1 #H2 #H3 #u #H destruct /2 width=5 by ex3_2_intro/ -| #b2 #b #a2 #a #_ #H1 #H2 #H3 #u #H destruct -| #b #a1 #a #_ #H1 #H3 #u #H destruct -] +fact after_inv_SxO_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g → + ∀f1,f. g1 = ⫯f1 → g = ↑f → ⊥. +#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1 +#x #Hf #Hx destruct elim (discr_push_next … Hx) qed-. -fact after_inv_O3_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b = 0 → - ∧∧ t1 ⊚ t2 ≡ t & b1 = 0 & b2 = 0. -#t1 #t2 #t #b1 #b2 #b #Ht #H1 elim (after_inv_O3_aux1 … Ht) [2: // |3: skip ] -b -#u1 #u2 #Ht #H1 #H2 destruct /2 width=1 by and3_intro/ +fact after_inv_OxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f. g1 = ↑f1 → g = ↑f → + ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2. +#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H +[ elim (after_inv_OSO_aux … Hg … H1 … H) -g1 -g -f1 -f // +| lapply (after_inv_OOO_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/ +] qed-. -lemma after_inv_O3: ∀t1,t2,u. t1 ⊚ t2 ≡ 0@u → - ∃∃u1,u2. u1 ⊚ u2 ≡ u & t1 = 0@u1 & t2 = 0@u2. -/2 width=3 by after_inv_O3_aux1/ qed-. +lemma after_inv_OxO: ∀f1,g2,f. ↑f1 ⊚ g2 ≡ ↑f → + ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2. +/2 width=5 by after_inv_OxO_aux/ qed-. -fact after_inv_S3_aux1: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u,b. t = ⫯b@u → - (∃∃u1,u2,b2. u1 ⊚ b2@u2 ≡ b@u & t1 = 0@u1 & t2 = ⫯b2@u2) ∨ - ∃∃u1,b1. b1@u1 ⊚ t2 ≡ b@u & t1 = ⫯b1@u1. -#t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1 -[ #b2 #b #_ #H1 #H2 #H3 #u #a #H destruct -| #b2 #b #a2 #a #HT #H1 #H2 #H3 #u #x #H destruct /3 width=6 by ex3_3_intro, or_introl/ -| #b #a1 #a #HT #H1 #H3 #u #x #H destruct /3 width=4 by ex2_2_intro, or_intror/ +fact after_inv_OxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f. g1 = ↑f1 → g = ⫯f → + ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ⫯f2. +#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H +[ lapply (after_inv_OSS_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/ +| elim (after_inv_OOS_aux … Hg … H1 … H) -g1 -g -f1 -f // ] qed-. -fact after_inv_S3_aux2: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ a2@t2 ≡ a@t → ∀b. a = ⫯b → - (∃∃b2. t1 ⊚ b2@t2 ≡ b@t & a1 = 0 & a2 = ⫯b2) ∨ - ∃∃b1. b1@t1 ⊚ a2@t2 ≡ b@t & a1 = ⫯b1. -#t1 #t2 #t #a1 #a2 #a #Ht #b #H elim (after_inv_S3_aux1 … Ht) [3: // |4,5: skip ] -a * -[ #u1 #u2 #b2 #Ht #H1 #H2 destruct /3 width=3 by ex3_intro, or_introl/ -| #u1 #b1 #Ht #H1 destruct /3 width=3 by ex2_intro, or_intror/ +fact after_inv_xxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ↑f → + ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2. +* * [2: #m1 ] #g1 #g2 #g #Hg #f #H +[ elim (after_inv_SxO_aux … Hg … H) -g2 -g -f // +| elim (after_inv_OxO_aux … Hg … H) -g /2 width=5 by ex3_2_intro/ ] qed-. -lemma after_inv_S3: ∀t1,t2,u,b. t1 ⊚ t2 ≡ ⫯b@u → - (∃∃u1,u2,b2. u1 ⊚ b2@u2 ≡ b@u & t1 = 0@u1 & t2 = ⫯b2@u2) ∨ - ∃∃u1,b1. b1@u1 ⊚ t2 ≡ b@u & t1 = ⫯b1@u1. -/2 width=3 by after_inv_S3_aux1/ qed-. +lemma after_inv_xxO: ∀g1,g2,f. g1 ⊚ g2 ≡ ↑f → + ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2. +/2 width=3 by after_inv_xxO_aux/ qed-. -(* Advanced inversion lemmas on after ***************************************) +fact after_inv_xxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ⫯f → + (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨ + ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1. +* * [2: #m1 ] #g1 #g2 #g #Hg #f #H +[ /4 width=5 by after_inv_SxS_aux, or_intror, ex2_intro/ +| elim (after_inv_OxS_aux … Hg … H) -g + /3 width=5 by or_introl, ex3_2_intro/ +] +qed-. -fact after_inv_O2_aux2: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ a2@t2 ≡ a@t → a2 = 0 → - a1 = a ∧ t1 ⊚ t2 ≡ t. -#t1 #t2 #t #a1 #a2 elim a1 -a1 -[ #a #H #H2 elim (after_inv_zero_aux2 … H … H2) -a2 /2 width=1 by conj/ -| #a1 #IH #a #H #H2 elim (after_inv_S1_aux2 … H) -H [3: // |2: skip ] - #b #H #H1 elim (IH … H) // -a2 - #H2 destruct /2 width=1 by conj/ +lemma after_inv_xxS: ∀g1,g2,f. g1 ⊚ g2 ≡ ⫯f → + (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨ + ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1. +/2 width=3 by after_inv_xxS_aux/ qed-. + +fact after_inv_Oxx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1. g1 = ↑f1 → + (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ↑f2 & g = ↑f) ∨ + (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ⫯f2 & g = ⫯f). +#g1 * * [2: #m2 ] #g2 #g #Hg #f1 #H +[ elim (after_inv_OSx_aux … Hg … H) -g1 + /3 width=5 by or_intror, ex3_2_intro/ +| elim (after_inv_OOx_aux … Hg … H) -g1 + /3 width=5 by or_introl, ex3_2_intro/ ] qed-. -lemma after_inv_O2: ∀t1,u2,t. t1 ⊚ 0@u2 ≡ t → - ∃∃u1,u,a. t1 = a@u1 & t = a@u & u1 ⊚ u2 ≡ u. -* #a1 #t1 #t2 * #a #t #H elim (after_inv_O2_aux2 … H) -H // -/2 width=6 by ex3_3_intro/ +lemma after_inv_Oxx: ∀f1,g2,g. ↑f1 ⊚ g2 ≡ g → + (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ↑f2 & g = ↑f) ∨ + (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ⫯f2 & g = ⫯f). +/2 width=3 by after_inv_Oxx_aux/ qed-. + +fact after_inv_xOx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ↑f2 → + f1 ⊚ f2 ≡ f ∧ n1 = n. +#f1 #g2 #f #n1 elim n1 -n1 +[ #n #Hf #f2 #H2 elim (after_inv_OOx_aux … Hf … H2) -g2 [3: // |2: skip ] + #g #Hf #H elim (push_inv_seq_sn … H) -H destruct /2 width=1 by conj/ +| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_Sxx_aux … Hf) -Hf [3: // |2: skip ] + #g1 #Hg #H1 elim (next_inv_seq_sn … H1) -H1 + #x #Hx #H destruct elim (IH … Hg) [2: // |3: skip ] -IH -Hg + #H destruct /2 width=1 by conj/ +] qed-. -lemma after_inv_const: ∀a,t1,b2,u2,t. a@t1 ⊚ b2@u2 ≡ a@t → b2 = 0. -#a elim a -a -[ #t1 #b2 #u2 #t #H elim (after_inv_O3 … H) -H - #u1 #x2 #_ #_ #H destruct // -| #a #IH #t1 #b2 #u2 #t #H elim (after_inv_S1 … H) -H - #x #b #Hx #H destruct >(IH … Hx) -t1 -u2 -x -b2 -b // +lemma after_inv_xOx: ∀f1,f2,f,n1,n. n1@f1 ⊚ ↑f2 ≡ n@f → + f1 ⊚ f2 ≡ f ∧ n1 = n. +/2 width=3 by after_inv_xOx_aux/ qed-. + +fact after_inv_xSx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ⫯f2 → + ∃∃m. f1 ⊚ f2 ≡ m@f & n = ⫯(n1+m). +#f1 #g2 #f #n1 elim n1 -n1 +[ #n #Hf #f2 #H2 elim (after_inv_OSx_aux … Hf … H2) -g2 [3: // |2: skip ] + #g #Hf #H elim (next_inv_seq_sn … H) -H + #x #Hx #Hg destruct /2 width=3 by ex2_intro/ +| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_Sxx_aux … Hf) -Hf [3: // |2: skip ] + #g #Hg #H elim (next_inv_seq_sn … H) -H + #x #Hx #H destruct elim (IH … Hg) -IH -Hg [3: // |2: skip ] + #m #Hf #Hm destruct /2 width=3 by ex2_intro/ ] qed-. -lemma after_inv_S2: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ ⫯a2@t2 ≡ a@t → ∀b. a = ⫯(a1+b) → - t1 ⊚ a2@t2 ≡ b@t. -#t1 #t2 #t #a1 elim a1 -a1 -[ #a2 #a #Ht #b #Hb - elim (after_inv_skip_aux2 … Ht) -Ht [3,4: // |2: skip ] - #c #Ht #Hc destruct // -| #a1 #IH #a2 #a #Ht #b #Hb - lapply (after_inv_drop_aux2 … Ht … Hb) -a [ // | skip ] - /2 width=3 by/ +lemma after_inv_xSx: ∀f1,f2,f,n1,n. n1@f1 ⊚ ⫯f2 ≡ n@f → + ∃∃m. f1 ⊚ f2 ≡ m@f & n = ⫯(n1+m). +/2 width=3 by after_inv_xSx_aux/ qed-. + +lemma after_inv_const: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡ f ∧ n2 = 0. +#f1 #f2 #f #n2 #n elim n -n +[ #H elim (after_inv_OxO … H) -H + #g2 #Hf #H elim (push_inv_seq_sn … H) -H /2 width=1 by conj/ +| #n #IH #H lapply (after_inv_SxS_aux … H ????) -H /2 width=5 by/ ] qed-. (* Forward lemmas on application ********************************************) -lemma after_at_fwd: ∀t,i1,i. @⦃i1, t⦄ ≡ i → ∀t2,t1. t2 ⊚ t1 ≡ t → - ∃∃i2. @⦃i1, t1⦄ ≡ i2 & @⦃i2, t2⦄ ≡ i. -#t #i1 #i #H elim H -t -i1 -i -[ #t #t2 #t1 #H elim (after_inv_O3 … H) -H - /2 width=3 by at_zero, ex2_intro/ -| #t #i1 #i #_ #IH #t2 #t1 #H elim (after_inv_O3 … H) -H - #u2 #u1 #Hu #H1 #H2 destruct elim (IH … Hu) -t +lemma after_at_fwd: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f → + ∃∃i2. @⦃i1, f1⦄ ≡ i2 & @⦃i2, f2⦄ ≡ i. +#f #i1 #i #H elim H -f -i1 -i +[ #f #f2 #f1 #H elim (after_inv_xxO … H) -H + /2 width=3 by at_refl, ex2_intro/ +| #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_xxO … H) -H + #g2 #g1 #Hg #H1 #H2 destruct elim (IH … Hg) -f /3 width=3 by at_S1, ex2_intro/ -| #t #b #i1 #i #_ #IH #t2 #t1 #H elim (after_inv_S3 … H) -H * - [ #u2 #u1 #b2 #Hu #H1 #H2 destruct elim (IH … Hu) -t -b - /3 width=3 by at_S1, at_lift, ex2_intro/ - | #u1 #b1 #Hu #H destruct elim (IH … Hu) -t -b - /3 width=3 by at_lift, ex2_intro/ +| #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_xxS … H) -H * + [ #g2 #g1 #Hg #H2 #H1 destruct elim (IH … Hg) -f + /3 width=3 by at_S1, at_next, ex2_intro/ + | #g1 #Hg #H destruct elim (IH … Hg) -f + /3 width=3 by at_next, ex2_intro/ ] ] qed-. -lemma after_at1_fwd: ∀t1,i1,i2. @⦃i1, t1⦄ ≡ i2 → ∀t2,t. t2 ⊚ t1 ≡ t → - ∃∃i. @⦃i2, t2⦄ ≡ i & @⦃i1, t⦄ ≡ i. -#t1 #i1 #i2 #H elim H -t1 -i1 -i2 -[ #t1 #t2 #t #H elim (after_inv_O2 … H) -H /2 width=3 by ex2_intro/ -| #t1 #i1 #i2 #_ #IH * #b2 elim b2 -b2 - [ #t2 #t #H elim (after_inv_zero … H) -H - #u #Hu #H destruct elim (IH … Hu) -t1 - /3 width=3 by at_S1, at_skip, ex2_intro/ - | -IH #b2 #IH #t2 #t #H elim (after_inv_S1 … H) -H - #u #b #Hu #H destruct elim (IH … Hu) -t1 - /3 width=3 by at_lift, ex2_intro/ - ] -| #t1 #b1 #i1 #i2 #_ #IH * #b2 elim b2 -b2 - [ #t2 #t #H elim (after_inv_skip … H) -H - #u #a #Hu #H destruct elim (IH … Hu) -t1 -b1 - /3 width=3 by at_S1, at_lift, ex2_intro/ - | -IH #b2 #IH #t2 #t #H elim (after_inv_S1 … H) -H - #u #b #Hu #H destruct elim (IH … Hu) -t1 -b1 - /3 width=3 by at_lift, ex2_intro/ - ] +lemma after_at1_fwd: ∀f1,i1,i2. @⦃i1, f1⦄ ≡ i2 → ∀f2,f. f2 ⊚ f1 ≡ f → + ∃∃i. @⦃i2, f2⦄ ≡ i & @⦃i1, f⦄ ≡ i. +#f1 #i1 #i2 #H elim H -f1 -i1 -i2 +[ #f1 * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H /2 width=3 by ex2_intro/ +| #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H + #Hf #H destruct elim (IH … Hf) -f1 /3 width=3 by at_S1, ex2_intro/ +| #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xSx … H) -H + #m #Hf #Hm destruct elim (IH … Hf) -f1 + /4 width=3 by at_plus2, at_S1, at_next, ex2_intro/ ] qed-. -lemma after_fwd_at: ∀t1,t2,i1,i2,i. @⦃i1, t1⦄ ≡ i2 → @⦃i2, t2⦄ ≡ i → - ∀t. t2 ⊚ t1 ≡ t → @⦃i1, t⦄ ≡ i. -#t1 #t2 #i1 #i2 #i #Hi1 #Hi2 #t #Ht elim (after_at1_fwd … Hi1 … Ht) -t1 +lemma after_fwd_at: ∀f1,f2,i1,i2,i. @⦃i1, f1⦄ ≡ i2 → @⦃i2, f2⦄ ≡ i → + ∀f. f2 ⊚ f1 ≡ f → @⦃i1, f⦄ ≡ i. +#f1 #f2 #i1 #i2 #i #Hi1 #Hi2 #f #Ht elim (after_at1_fwd … Hi1 … Ht) -f1 #j #H #Hj >(at_mono … H … Hi2) -i2 // qed-. -lemma after_fwd_at1: ∀t2,t,i1,i2,i. @⦃i1, t⦄ ≡ i → @⦃i2, t2⦄ ≡ i → - ∀t1. t2 ⊚ t1 ≡ t → @⦃i1, t1⦄ ≡ i2. -#t2 #t #i1 #i2 #i #Hi1 #Hi2 #t1 #Ht elim (after_at_fwd … Hi1 … Ht) -t +lemma after_fwd_at1: ∀f2,f,i1,i2,i. @⦃i1, f⦄ ≡ i → @⦃i2, f2⦄ ≡ i → + ∀f1. f2 ⊚ f1 ≡ f → @⦃i1, f1⦄ ≡ i2. +#f2 #f #i1 #i2 #i #Hi1 #Hi2 #f1 #Ht elim (after_at_fwd … Hi1 … Ht) -f #j1 #Hij1 #H >(at_inj … Hi2 … H) -i // qed-. -lemma after_fwd_at2: ∀t,i1,i. @⦃i1, t⦄ ≡ i → ∀t1,i2. @⦃i1, t1⦄ ≡ i2 → - ∀t2. t2 ⊚ t1 ≡ t → @⦃i2, t2⦄ ≡ i. -#t #i1 #i #H elim H -t -i1 -i -[ #t #t1 #i2 #Ht1 #t2 #H elim (after_inv_O3 … H) -H - #u2 #u1 #_ #H1 #H2 destruct >(at_inv_OOx … Ht1) -t -u1 -i2 // -| #t #i1 #i #_ #IH #t1 #i2 #Ht1 #t2 #H elim (after_inv_O3 … H) -H - #u2 #u1 #Hu #H1 #H2 destruct elim (at_inv_SOx … Ht1) -Ht1 - /3 width=3 by at_skip/ -| #t #b #i1 #i #_ #IH #t1 #i2 #Ht1 #t2 #H elim (after_inv_S3 … H) -H * - [ #u2 #u1 #a1 #Hu #H1 #H2 destruct elim (at_inv_xSx … Ht1) -Ht1 - /3 width=3 by at_skip/ - | #u2 #a2 #Hu #H destruct /3 width=3 by at_lift/ +lemma after_fwd_at2: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f1,i2. @⦃i1, f1⦄ ≡ i2 → + ∀f2. f2 ⊚ f1 ≡ f → @⦃i2, f2⦄ ≡ i. +#f #i1 #i #H elim H -f -i1 -i +[ #f #f1 #i2 #Ht1 #f2 #H elim (after_inv_xxO … H) -H + #g2 #g1 #_ #H1 #H2 destruct >(at_inv_OOx … Ht1) -f -g1 -i2 // +| #f #i1 #i #_ #IH #f1 #i2 #Ht1 #f2 #H elim (after_inv_xxO … H) -H + #g2 #g1 #Hu #H1 #H2 destruct elim (at_inv_SOx … Ht1) -Ht1 + /3 width=3 by at_push/ +| #f #i1 #i #_ #IH #f1 #i2 #Hf1 #f2 #H elim (after_inv_xxS … H) -H * + [ #g2 #g1 #Hg #H2 #H1 destruct elim (at_inv_xSx … Hf1) -Hf1 + /3 width=3 by at_push/ + | #g2 #Hg #H destruct /3 width=3 by at_next/ ] ] qed-. (* Advanced forward lemmas on after *****************************************) -lemma after_fwd_hd: ∀t1,t2,t,a2,a. t1 ⊚ a2@t2 ≡ a@t → a = t1@❴a2❵. -#t1 #t2 #t #a2 #a #Ht lapply (after_fwd_at … 0 … Ht) -Ht [4: // | // |2,3: skip ] +lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → n = f1@❴n2❵. +#f1 #f2 #f #n2 #n #H lapply (after_fwd_at … 0 … H) -H [1,4: // |2,3: skip ] /3 width=2 by at_inv_O1, sym_eq/ qed-. -lemma after_fwd_tl: ∀t,t2,a2,t1,a1,a. a1@t1 ⊚ a2@t2 ≡ a@t → - tln … a2 t1 ⊚ t2 ≡ t. -#t #t2 #a2 elim a2 -a2 -[ #t1 #a1 #a #Ht elim (after_inv_O2_aux2 … Ht) -Ht // -| #a2 #IH * #b1 #t1 #a1 #a #Ht - lapply (after_fwd_hd … Ht) #Ha - lapply (after_inv_S2 … Ht … Ha) -a - /2 width=3 by/ +lemma after_fwd_tl: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f → + tln … n2 f1 ⊚ f2 ≡ f. +#f #f2 #n2 elim n2 -n2 +[ #f1 #n1 #n #H elim (after_inv_xOx … H) -H // +| #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xSx_aux … H ??) -H [3: // |2: skip ] + #m #Hm #H destruct /2 width=3 by/ ] qed-. -lemma after_inv_apply: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ a2@t2 ≡ a@t → - a = (a1@t1)@❴a2❵ ∧ tln … a2 t1 ⊚ t2 ≡ t. -/3 width=3 by after_fwd_tl, after_fwd_hd, conj/ qed-. +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: ∀t1,t2,t0. t1 ⊚ t2 ≡ t0 → - ∀t3,t4. t0 ⊚ t3 ≡ t4 → - ∀t. t2 ⊚ t3 ≡ t → t1 ⊚ t ≡ t4 ≝ ?. -#t1 #t2 #t0 * -t1 -t2 -t0 #t1 #t2 #t0 #b1 [1,2: #b2 ] #b0 -[ #Ht0 #H1 #H2 #H0 * #b3 #t3 * #b4 #t4 #Ht4 * #b #t #Ht - cases (after_inv_O1_aux2 … Ht4 H0) -Ht4 -H0 * - [ #Ht4 #H3 #H4 cases (after_inv_zero_aux2 … Ht H2 H3) -Ht -H2 -H3 - #Ht #H /3 width=6 by after_zero/ - | #a0 #a4 #Ht4 #H3 #H4 cases (after_inv_skip_aux2 … Ht H2 … H3) -Ht -H2 -H3 - #a #Ht3 #H /3 width=6 by after_skip/ +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/ ] -| #a2 #a0 #Ht0 #H1 #H2 #H0 #t3 * #b4 #t4 #Ht4 cases (after_inv_S1_aux2 … Ht4 … H0) -Ht4 -H0 - #a4 #Ht4 #H4 * #b #t #H cases (after_inv_S1_aux2 … H … H2) -H -H2 - #a #Ht3 #H /3 width=6 by after_skip/ -| #a1 #a0 #Ht0 #H1 #H0 #t3 * #b4 #t4 #Ht4 cases (after_inv_S1_aux2 … Ht4 … H0) -Ht4 -H0 - #a4 #Ht4 #H4 * #b #t #Ht /3 width=6 by after_drop/ ] qed-. -let corec after_trans2: ∀t1,t0,t4. t1 ⊚ t0 ≡ t4 → - ∀t2, t3. t2 ⊚ t3 ≡ t0 → - ∀t. t1 ⊚ t2 ≡ t → t ⊚ t3 ≡ t4 ≝ ?. -#t1 #t0 #t4 * -t1 -t0 -t4 #t1 #t0 #t4 #b1 [1,2: #b0 ] #b4 -[ #Ht4 #H1 #H0 #H4 * #b2 #t2 * #b3 #t3 #Ht0 * #b #t #Ht - cases (after_inv_O3_aux2 … Ht0 H0) -b0 - #Ht0 #H2 #H3 cases (after_inv_zero_aux2 … Ht H1 H2) -b1 -b2 - #Ht #H /3 width=6 by after_zero/ -| #a0 #a4 #Ht4 #H1 #H0 #H4 * #b2 #t2 * #b3 #t3 #Ht0 * #b #t #Ht - cases (after_inv_S3_aux2 … Ht0 … H0) -b0 * - [ #a3 #Ht0 #H2 #H3 cases (after_inv_zero_aux2 … Ht H1 H2) -b1 -b2 - #Ht #H /3 width=6 by after_skip/ - | #a2 #Ht0 #H2 cases (after_inv_skip_aux2 … Ht H1 … H2) -b1 -b2 - #a #Ht #H /3 width=6 by after_drop/ +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/ ] -| #a1 #a4 #Ht4 #H1 #H4 * #b2 #t2 * #b3 #t3 #Ht0 * #b #t #Ht - cases (after_inv_S1_aux2 … Ht … H1) -b1 - #a #Ht #H /3 width=6 by after_drop/ +| #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-. -let corec after_mono: ∀t1,t2,x. t1 ⊚ t2 ≡ x → ∀y. t1 ⊚ t2 ≡ y → x ≐ y ≝ ?. -* #a1 #t1 * #a2 #t2 * #c #x #Hx * #d #y #Hy -cases (after_inv_apply … Hx) -Hx #Hc #Hx -cases (after_inv_apply … Hy) -Hy #Hd #Hy -/3 width=4 by eq_sec/ -qed-. - -let corec after_inj: ∀t1,x,t. t1 ⊚ x ≡ t → ∀y. t1 ⊚ y ≡ t → x ≐ y ≝ ?. -* #a1 #t1 * #c #x * #a #t #Hx * #d #y #Hy -cases (after_inv_apply … Hx) -Hx #Hc #Hx -cases (after_inv_apply … Hy) -Hy #Hd -cases (apply_inj_aux … Hc Hd) #Hy -a -d /3 width=4 by eq_sec/ -qed-. - (* Main inversion lemmas on after *******************************************) -theorem after_inv_total: ∀t1,t2,t. t1 ⊚ t2 ≡ t → t1 ∘ t2 ≐ t. -/2 width=4 by after_mono/ qed-. +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-.