--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/drop.ma".
+include "basic_2/substitution/lpx_sn.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+(* alternative definition of lpx_sn *)
+definition lpx_sn_alt: relation3 lenv term term → relation lenv ≝
+ λR,L1,L2. |L1| = |L2| ∧
+ (∀I1,I2,K1,K2,V1,V2,i.
+ ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 →
+ I1 = I2 ∧ R K1 V1 V2
+ ).
+
+(* Basic forward lemmas ******************************************************)
+
+lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H //
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpx_sn_alt_inv_atom1: ∀R,L2. lpx_sn_alt R (⋆) L2 → L2 = ⋆.
+#R #L2 #H lapply (lpx_sn_alt_fwd_length … H) -H
+normalize /2 width=1 by length_inv_zero_sn/
+qed-.
+
+lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 →
+ ∃∃K2,V2. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2.
+#R #I1 #L2 #K1 #V1 #H elim H -H
+#H #IH elim (length_inv_pos_sn … H) -H
+#I2 #K2 #V2 #HK12 #H destruct
+elim (IH I1 I2 K1 K2 V1 V2 0) //
+#H #HV12 destruct @(ex3_2_intro … K2 V2) // -HV12
+@conj // -HK12
+#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH
+/2 width=1 by drop_drop, conj/
+qed-.
+
+lemma lpx_sn_alt_inv_atom2: ∀R,L1. lpx_sn_alt R L1 (⋆) → L1 = ⋆.
+#R #L1 #H lapply (lpx_sn_alt_fwd_length … H) -H
+normalize /2 width=1 by length_inv_zero_dx/
+qed-.
+
+lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) →
+ ∃∃K1,V1. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+#R #I2 #L1 #K2 #V2 #H elim H -H
+#H #IH elim (length_inv_pos_dx … H) -H
+#I1 #K1 #V1 #HK12 #H destruct
+elim (IH I1 I2 K1 K2 V1 V2 0) //
+#H #HV12 destruct @(ex3_2_intro … K1 V1) // -HV12
+@conj // -HK12
+#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH
+/2 width=1 by drop_drop, conj/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆).
+#R @conj //
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 elim (drop_inv_atom1 … HLK1) -HLK1
+#H destruct
+qed.
+
+lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2.
+ lpx_sn_alt R L1 L2 → R L1 V1 V2 →
+ lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2).
+#R #I #L1 #L2 #V1 #V2 #H #HV12 elim H -H
+#HL12 #IH @conj //
+#I1 #I2 #K1 #K2 #W1 #W2 #i @(ynat_ind … i) -i
+[ #HLK1 #HLK2
+ lapply (drop_inv_O2 … HLK1) -HLK1 #H destruct
+ lapply (drop_inv_O2 … HLK2) -HLK2 #H destruct
+ /2 width=1 by conj/
+| -HL12 -HV12 /3 width=6 by drop_inv_drop1/
+| #H lapply (drop_fwd_Y2 … H) -H
+ #H elim (ylt_yle_false … H) -H //
+]
+qed.
+
+(* Main properties **********************************************************)
+
+theorem lpx_sn_lpx_sn_alt: ∀R,L1,L2. lpx_sn R L1 L2 → lpx_sn_alt R L1 L2.
+#R #L1 #L2 #H elim H -L1 -L2
+/2 width=1 by lpx_sn_alt_atom, lpx_sn_alt_pair/
+qed.
+
+(* Main inversion lemmas ****************************************************)
+
+theorem lpx_sn_alt_inv_lpx_sn: ∀R,L1,L2. lpx_sn_alt R L1 L2 → lpx_sn R L1 L2.
+#R #L1 elim L1 -L1
+[ #L2 #H lapply (lpx_sn_alt_inv_atom1 … H) -H //
+| #L1 #I #V1 #IH #X #H elim (lpx_sn_alt_inv_pair1 … H) -H
+ #L2 #V2 #HL12 #HV12 #H destruct /3 width=1 by lpx_sn_pair/
+]
+qed-.
+
+(* alternative definition of lpx_sn *****************************************)
+
+lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| →
+ (∀I1,I2,K1,K2,V1,V2,i.
+ ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 →
+ I1 = I2 ∧ R K1 V1 V2
+ ) → lpx_sn R L1 L2.
+/4 width=4 by lpx_sn_alt_inv_lpx_sn, conj/ qed.
+
+lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 →
+ |L1| = |L2| ∧
+ ∀I1,I2,K1,K2,V1,V2,i.
+ ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 →
+ I1 = I2 ∧ R K1 V1 V2.
+#R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H
+#H elim H -H /3 width=4 by conj/
+qed-.
--- /dev/null
+definition dropable_dx: predicate (relation lenv) ≝
+ λR. ∀L1,L2. R L1 L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 →
+ ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & R K1 K2.
+
+lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
+#R #HR #L1 #L2 #H elim H -L2
+[ #L2 #HL12 #K2 #c #k #HLK2 elim (HR … HL12 … HLK2) -HR -L2
+ /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IHL1 #K2 #c #k #HLK2 elim (HR … HL2 … HLK2) -HR -L2
+ #K #HLK #HK2 elim (IHL1 … HLK) -L
+ /3 width=5 by step, ex2_intro/
+]
+qed-.
+
+
+fact lpx_sn_dropable_aux: ∀R,L2,K2,c,l,k. ⬇[c, l, k] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
+ l = 0 → ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & lpx_sn R K1 K2.
+#R #L2 #K2 #c #l #k #H elim H -L2 -K2 -l -k
+[ #l #k #Hm #X #H >(lpx_sn_inv_atom2 … H) -H
+ /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/
+| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H
+ #K1 #V1 #HK12 #HV12 #H destruct
+ /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/
+| #I #L2 #K2 #V2 #k #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H
+ #L1 #V1 #HL12 #HV12 #H destruct
+ elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/
+| #I #L2 #K2 #V2 #W2 #l #k #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H)
+]
+qed-.
+
+lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R).
+/2 width=5 by lpx_sn_dropable_aux/ qed-.
+
+lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 →
+ ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2.
+#R #L1 #L2 #H elim H -L1 -L2
+[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H
+ [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/
+ | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
+ /3 width=5 by drop_drop_lt, ex3_2_intro/
+ ]
+]
+qed-.
+
+lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 →
+ ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 →
+ ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2.
+#R #L1 #L2 #H elim H -L1 -L2
+[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H
+ [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/
+ | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
+ /3 width=5 by drop_drop_lt, ex3_2_intro/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/nstream_sle.ma".
+include "basic_2/notation/relations/relationstar_5.ma".
+include "basic_2/grammar/lenv.ma".
+
+(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *)
+inductive lexs (RS,RO:relation3 lenv term term): rtmap → relation lenv ≝
+| lexs_atom: ∀f. lexs RS RO f (⋆) (⋆)
+| lexs_next: ∀I,L1,L2,V1,V2,f.
+ lexs RS RO f L1 L2 → RS L1 V1 V2 →
+ lexs RS RO (⫯f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2)
+| lexs_push: ∀I,L1,L2,V1,V2,f.
+ lexs RS RO f L1 L2 → RO L1 V1 V2 →
+ lexs RS RO (↑f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2)
+.
+
+interpretation "general entrywise extension (local environment)"
+ 'RelationStar RS RO f L1 L2 = (lexs RS RO f L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lexs_inv_atom1_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → X = ⋆ → Y = ⋆.
+#RS #RO #X #Y #f * -X -Y -f //
+#I #L1 #L2 #V1 #V2 #f #_ #_ #H destruct
+qed-.
+
+(* Basic_2A1: includes lpx_sn_inv_atom1 *)
+lemma lexs_inv_atom1: ∀RS,RO,Y,f. ⋆ ⦻*[RS, RO, f] Y → Y = ⋆.
+/2 width=6 by lexs_inv_atom1_aux/ qed-.
+
+fact lexs_inv_next1_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ⫯g →
+ ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & Y = K2.ⓑ{J}W2.
+#RS #RO #X #Y #f * -X -Y -f
+[ #f #J #K1 #W1 #g #H destruct
+| #I #L1 #L2 #V1 #V2 #f #HL #HS #J #K1 #W1 #g #H1 #H2 <(injective_next … H2) -g destruct
+ /2 width=5 by ex3_2_intro/
+| #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K1 #W1 #g #_ #H elim (discr_push_next … H)
+]
+qed-.
+
+(* Basic_2A1: includes lpx_sn_inv_pair1 *)
+lemma lexs_inv_next1: ∀RS,RO,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[RS, RO, ⫯g] Y →
+ ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & Y = K2.ⓑ{J}W2.
+/2 width=7 by lexs_inv_next1_aux/ qed-.
+
+
+fact lexs_inv_push1_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ↑g →
+ ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & Y = K2.ⓑ{J}W2.
+#RS #RO #X #Y #f * -X -Y -f
+[ #f #J #K1 #W1 #g #H destruct
+| #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K1 #W1 #g #_ #H elim (discr_next_push … H)
+| #I #L1 #L2 #V1 #V2 #f #HL #HO #J #K1 #W1 #g #H1 #H2 <(injective_push … H2) -g destruct
+ /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lexs_inv_push1: ∀RS,RO,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[RS, RO, ↑g] Y →
+ ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & Y = K2.ⓑ{J}W2.
+/2 width=7 by lexs_inv_push1_aux/ qed-.
+
+fact lexs_inv_atom2_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → Y = ⋆ → X = ⋆.
+#RS #RO #X #Y #f * -X -Y -f //
+#I #L1 #L2 #V1 #V2 #f #_ #_ #H destruct
+qed-.
+
+(* Basic_2A1: includes lpx_sn_inv_atom2 *)
+lemma lexs_inv_atom2: ∀RS,RO,X,f. X ⦻*[RS, RO, f] ⋆ → X = ⋆.
+/2 width=6 by lexs_inv_atom2_aux/ qed-.
+
+fact lexs_inv_next2_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ⫯g →
+ ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & X = K1.ⓑ{J}W1.
+#RS #RO #X #Y #f * -X -Y -f
+[ #f #J #K2 #W2 #g #H destruct
+| #I #L1 #L2 #V1 #V2 #f #HL #HS #J #K2 #W2 #g #H1 #H2 <(injective_next … H2) -g destruct
+ /2 width=5 by ex3_2_intro/
+| #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K2 #W2 #g #_ #H elim (discr_push_next … H)
+]
+qed-.
+
+(* Basic_2A1: includes lpx_sn_inv_pair2 *)
+lemma lexs_inv_next2: ∀RS,RO,J,X,K2,W2,g. X ⦻*[RS, RO, ⫯g] K2.ⓑ{J}W2 →
+ ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & X = K1.ⓑ{J}W1.
+/2 width=7 by lexs_inv_next2_aux/ qed-.
+
+fact lexs_inv_push2_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ↑g →
+ ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & X = K1.ⓑ{J}W1.
+#RS #RO #X #Y #f * -X -Y -f
+[ #f #J #K2 #W2 #g #H destruct
+| #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K2 #W2 #g #_ #H elim (discr_next_push … H)
+| #I #L1 #L2 #V1 #V2 #f #HL #HO #J #K2 #W2 #g #H1 #H2 <(injective_push … H2) -g destruct
+ /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lexs_inv_push2: ∀RS,RO,J,X,K2,W2,g. X ⦻*[RS, RO, ↑g] K2.ⓑ{J}W2 →
+ ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & X = K1.ⓑ{J}W1.
+/2 width=7 by lexs_inv_push2_aux/ qed-.
+
+(* Basic_2A1: includes lpx_sn_inv_pair *)
+lemma lexs_inv_next: ∀RS,RO,I1,I2,L1,L2,V1,V2,f.
+ L1.ⓑ{I1}V1 ⦻*[RS, RO, ⫯f] (L2.ⓑ{I2}V2) →
+ ∧∧ L1 ⦻*[RS, RO, f] L2 & RS L1 V1 V2 & I1 = I2.
+#RS #RO #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_next1 … H) -H
+#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/
+qed-.
+
+lemma lexs_inv_push: ∀RS,RO,I1,I2,L1,L2,V1,V2,f.
+ L1.ⓑ{I1}V1 ⦻*[RS, RO, ↑f] (L2.ⓑ{I2}V2) →
+ ∧∧ L1 ⦻*[RS, RO, f] L2 & RO L1 V1 V2 & I1 = I2.
+#RS #RO #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_push1 … H) -H
+#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lexs_eq_repl_back: ∀RS,RO,L1,L2. eq_stream_repl_back … (λf. L1 ⦻*[RS, RO, f] L2).
+#RS #RO #L1 #L2 #f1 #H elim H -L1 -L2 -f1 //
+[ #I #L1 #L2 #V1 #v2 #f1 #_ #HS #IH #f2 #H elim (next_inv_sn … H) -H /3 width=1 by lexs_next/
+| #I #L1 #L2 #V1 #v2 #f1 #_ #HO #IH #f2 #H elim (push_inv_sn … H) -H /3 width=1 by lexs_push/
+]
+qed-.
+
+lemma lexs_eq_repl_fwd: ∀RS,RO,L1,L2. eq_stream_repl_fwd … (λf. L1 ⦻*[RS, RO, f] L2).
+#RS #RO #L1 #L2 @eq_stream_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *)
+qed-.
+
+(* Basic_2A1: includes: lpx_sn_refl *)
+lemma lexs_refl: ∀RS,RO,f.
+ (∀L. reflexive … (RS L)) →
+ (∀L. reflexive … (RO L)) →
+ reflexive … (lexs RS RO f).
+#RS #RO #f #HS #HO #L generalize in match f; -f elim L -L //
+#L #I #V #IH * * /2 width=1 by lexs_next, lexs_push/
+qed.
+
+lemma sle_lexs_trans: ∀RS,RO. (∀L,T1,T2. RO L T1 T2 → RS L T1 T2) →
+ ∀L1,L2,f2. L1 ⦻*[RS, RO, f2] L2 →
+ ∀f1. f1 ⊆ f2 → L1 ⦻*[RS, RO, f1] L2.
+#RS #RO #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 //
+#I #L1 #L2 #V1 #V2 #f2 #_ #HV12 #IH
+[2: * * [2: #n1 ] ] #f1 #H
+[ <next_rew /4 width=5 by lexs_next, sle_inv_SO_aux/
+| /4 width=5 by lexs_push, sle_inv_OO_aux/
+| elim (sle_inv_xS_aux … H) -H [3: // |2: skip ]
+ #g1 #H #H1 destruct /3 width=5 by lexs_next/
+]
+qed-.
+
+lemma sle_lexs_conf: ∀RS,RO. (∀L,T1,T2. RS L T1 T2 → RO L T1 T2) →
+ ∀L1,L2,f1. L1 ⦻*[RS, RO, f1] L2 →
+ ∀f2. f1 ⊆ f2 → L1 ⦻*[RS, RO, f2] L2.
+#RS #RO #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 //
+#I #L1 #L2 #V1 #V2 #f1 #_ #HV12 #IH
+[ * * [2: #n2 ] ] #f2 #H
+[ <next_rew /4 width=5 by lexs_next, sle_inv_SS_aux/
+| /4 width=5 by lexs_push, sle_inv_SO_aux/
+| elim (sle_inv_Ox_aux … H) -H [3: // |2: skip ]
+ #g2 #H #H2 destruct /3 width=5 by lexs_push/
+]
+qed-.
+
+lemma lexs_co: ∀RS1,RS2,RO1,RO2.
+ (∀L1,T1,T2. RS1 L1 T1 T2 → RS2 L1 T1 T2) →
+ (∀L1,T1,T2. RO1 L1 T1 T2 → RO2 L1 T1 T2) →
+ ∀L1,L2,f. L1 ⦻*[RS1, RO1, f] L2 → L1 ⦻*[RS2, RO2, f] L2.
+#RS1 #RS2 #RO1 #RO2 #HS #HO #L1 #L2 #f #H elim H -L1 -L2 -f
+/3 width=1 by lexs_atom, lexs_next, lexs_push/
+qed-.
+
+(* Basic_2A1: removed theorems 17:
+ llpx_sn_inv_bind llpx_sn_inv_flat
+ llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length
+ llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx
+ llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co
+ llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/lpx_sn.ma".
+include "basic_2/relocation/drops.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+(* Properties on general slicing for local environments *********************)
+
+lemma lpx_sn_deliftable_dropable: ∀R. (∀b. d_deliftable2_sn (R b)) → dropable_sn (lpx_sn R).
+#R #HR #L1 #K1 #c #t #H elim H -L1 -K1 -t
+[ #t #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_atom1 … H) -H
+ #H1 #H2 destruct elim (after_inv_empty3 … Hu) -Hu
+ #H1 #H2 destruct /3 width=3 by drops_atom, lpx_sn_atom, ex2_intro/
+| #I #L1 #K1 #V1 #t #_ #IH #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair1 … H) -H
+ #L2 #V2 #y2 #x2 #HL #HV #H1 #H2 destruct elim (after_inv_false1 … Hu) -Hu
+ #u #H1 #Hu destruct elim (IH … HL … Hu) -L1 /3 width=3 by drops_drop, ex2_intro/
+| #I #L1 #K1 #V1 #W1 #t #HLK #HWV #IHLK #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair1 … H) -H
+ #L2 #V2 #y2 #x2 #HL #HV #H1 #H2 destruct elim (after_inv_true1 … Hu) -Hu
+ #y1 #y #x1 #H1 #H2 #Hu destruct elim (HR … HV … HLK … HWV) -V1
+ elim (IHLK … HL … Hu) -L1 /3 width=5 by drops_skip, lpx_sn_pair, ex2_intro/
+]
+qed-.
+(*
+lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
+ d_liftable2 R → dedropable_sn (lpx_sn R).
+#R #H1R #H2R #L1 #K1 #s #l #m #H elim H -L1 -K1 -l -m
+[ #l #m #Hm #X #H >(lpx_sn_inv_atom1 … H) -H
+ /4 width=4 by drop_atom, lpx_sn_atom, ex3_intro/
+| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
+ #K2 #V2 #HK12 #HV12 #H destruct
+ lapply (lpx_sn_fwd_length … HK12)
+ #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *)
+ /3 width=1 by lpx_sn_pair, lreq_O2/
+| #I #L1 #K1 #V1 #m #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1
+ /3 width=5 by drop_drop, lreq_pair, lpx_sn_pair, ex3_intro/
+| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H
+ elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (H2R … HW12 … HLK1 … HWV1) -W1
+ elim (IHLK1 … HK12) -K1
+ /3 width=6 by drop_skip, lreq_succ, lpx_sn_pair, ex3_intro/
+]
+qed-.
+*)
+include "ground_2/relocation/trace_isun.ma".
+
+lemma lpx_sn_dropable: ∀R,L2,K2,c,t. ⬇*[c, t] L2 ≡ K2 → 𝐔⦃t⦄ →
+ ∀L1,u2. lpx_sn R u2 L1 L2 → ∀u1. t ⊚ u1 ≡ u2 →
+ ∃∃K1. ⬇*[c, t] L1 ≡ K1 & lpx_sn R u1 K1 K2.
+#R #L2 #K2 #c #t #H elim H -L2 -K2 -t
+[ #t #Ht #_ #X #u2 #H #u1 #Hu elim (lpx_sn_inv_atom2 … H) -H
+ #H1 #H2 destruct elim (after_inv_empty3 … Hu) -Hu
+ /4 width=3 by drops_atom, lpx_sn_atom, ex2_intro/
+| #I #L2 #K2 #V2 #t #_ #IH #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H
+ #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_false1 … Hu) -Hu
+ #u #H #Hu destruct elim (IH … HL … Hu) -L2 /3 width=3 by drops_drop, isun_inv_false, ex2_intro/
+| #I #L2 #K2 #V2 #W2 #t #_ #HWV #IHLK #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H
+ #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_true1 … Hu) -Hu
+ #y1 #y #x2 #H1 #H2 #Hu destruct lapply (isun_inv_true … Ht) -Ht
+ #Ht elim (IHLK … HL … Hu) -L2 -Hu /2 width=1 by isun_id/
+ #K1 #HLK1 #HK12 lapply (lifts_fwd_isid … HWV ?) // -HWV
+ #H destruct lapply (drops_fwd_isid … HLK1 ?) //
+ #H destruct
+ @ex2_intro
+ [
+ | @(drops_skip … HLK1)
+ | @(lpx_sn_pair … HK12 … HV)
+
+
+ lapply (drops_fwd_isid … HLK1 ?) // -HLK1
+ 2:
+
+
+
+
+ elim (HR … HV … HLK … HWV) -V1
+ elim (IHLK … HL … Hu) -L1 /3 width=5 by drops_skip, lpx_sn_pair, ex2_intro/
+
+
+]
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/grammar/lenv_length.ma".
-
-(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
-
-inductive lpx_sn (R:relation3 lenv term term): relation lenv ≝
-| lpx_sn_atom: lpx_sn R (⋆) (⋆)
-| lpx_sn_pair: ∀I,K1,K2,V1,V2.
- lpx_sn R K1 K2 → R K1 V1 V2 →
- lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
-.
-
-(* Basic properties *********************************************************)
-
-lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R).
-#R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆.
-#R #L1 #L2 * -L1 -L2
-[ //
-| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
-]
-qed-.
-
-lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆.
-/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
-
-fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
- ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
-#R #L1 #L2 * -L1 -L2
-[ #J #K1 #V1 #H destruct
-| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 →
- ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
-/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
-
-fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆.
-#R #L1 #L2 * -L1 -L2
-[ //
-| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
-]
-qed-.
-
-lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆.
-/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
-
-fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
- ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
-#R #L1 #L2 * -L1 -L2
-[ #J #K2 #V2 #H destruct
-| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) →
- ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
-/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
-
-lemma lpx_sn_inv_pair: ∀R,I1,I2,L1,L2,V1,V2.
- lpx_sn R (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) →
- ∧∧ lpx_sn R L1 L2 & R L1 V1 V2 & I1 = I2.
-#R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lpx_sn_inv_pair1 … H) -H
-#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|.
-#R #L1 #L2 #H elim H -L1 -L2 //
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/substitution/drop.ma".
-include "basic_2/substitution/lpx_sn.ma".
-
-(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
-
-(* alternative definition of lpx_sn *)
-definition lpx_sn_alt: relation3 lenv term term → relation lenv ≝
- λR,L1,L2. |L1| = |L2| ∧
- (∀I1,I2,K1,K2,V1,V2,i.
- ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 →
- I1 = I2 ∧ R K1 V1 V2
- ).
-
-(* Basic forward lemmas ******************************************************)
-
-lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|.
-#R #L1 #L2 #H elim H //
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lpx_sn_alt_inv_atom1: ∀R,L2. lpx_sn_alt R (⋆) L2 → L2 = ⋆.
-#R #L2 #H lapply (lpx_sn_alt_fwd_length … H) -H
-normalize /2 width=1 by length_inv_zero_sn/
-qed-.
-
-lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 →
- ∃∃K2,V2. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2.
-#R #I1 #L2 #K1 #V1 #H elim H -H
-#H #IH elim (length_inv_pos_sn … H) -H
-#I2 #K2 #V2 #HK12 #H destruct
-elim (IH I1 I2 K1 K2 V1 V2 0) //
-#H #HV12 destruct @(ex3_2_intro … K2 V2) // -HV12
-@conj // -HK12
-#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH
-/2 width=1 by drop_drop, conj/
-qed-.
-
-lemma lpx_sn_alt_inv_atom2: ∀R,L1. lpx_sn_alt R L1 (⋆) → L1 = ⋆.
-#R #L1 #H lapply (lpx_sn_alt_fwd_length … H) -H
-normalize /2 width=1 by length_inv_zero_dx/
-qed-.
-
-lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) →
- ∃∃K1,V1. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1.
-#R #I2 #L1 #K2 #V2 #H elim H -H
-#H #IH elim (length_inv_pos_dx … H) -H
-#I1 #K1 #V1 #HK12 #H destruct
-elim (IH I1 I2 K1 K2 V1 V2 0) //
-#H #HV12 destruct @(ex3_2_intro … K1 V1) // -HV12
-@conj // -HK12
-#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH
-/2 width=1 by drop_drop, conj/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆).
-#R @conj //
-#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 elim (drop_inv_atom1 … HLK1) -HLK1
-#H destruct
-qed.
-
-lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2.
- lpx_sn_alt R L1 L2 → R L1 V1 V2 →
- lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2).
-#R #I #L1 #L2 #V1 #V2 #H #HV12 elim H -H
-#HL12 #IH @conj //
-#I1 #I2 #K1 #K2 #W1 #W2 #i @(ynat_ind … i) -i
-[ #HLK1 #HLK2
- lapply (drop_inv_O2 … HLK1) -HLK1 #H destruct
- lapply (drop_inv_O2 … HLK2) -HLK2 #H destruct
- /2 width=1 by conj/
-| -HL12 -HV12 /3 width=6 by drop_inv_drop1/
-| #H lapply (drop_fwd_Y2 … H) -H
- #H elim (ylt_yle_false … H) -H //
-]
-qed.
-
-(* Main properties **********************************************************)
-
-theorem lpx_sn_lpx_sn_alt: ∀R,L1,L2. lpx_sn R L1 L2 → lpx_sn_alt R L1 L2.
-#R #L1 #L2 #H elim H -L1 -L2
-/2 width=1 by lpx_sn_alt_atom, lpx_sn_alt_pair/
-qed.
-
-(* Main inversion lemmas ****************************************************)
-
-theorem lpx_sn_alt_inv_lpx_sn: ∀R,L1,L2. lpx_sn_alt R L1 L2 → lpx_sn R L1 L2.
-#R #L1 elim L1 -L1
-[ #L2 #H lapply (lpx_sn_alt_inv_atom1 … H) -H //
-| #L1 #I #V1 #IH #X #H elim (lpx_sn_alt_inv_pair1 … H) -H
- #L2 #V2 #HL12 #HV12 #H destruct /3 width=1 by lpx_sn_pair/
-]
-qed-.
-
-(* alternative definition of lpx_sn *****************************************)
-
-lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| →
- (∀I1,I2,K1,K2,V1,V2,i.
- ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 →
- I1 = I2 ∧ R K1 V1 V2
- ) → lpx_sn R L1 L2.
-/4 width=4 by lpx_sn_alt_inv_lpx_sn, conj/ qed.
-
-lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 →
- |L1| = |L2| ∧
- ∀I1,I2,K1,K2,V1,V2,i.
- ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 →
- I1 = I2 ∧ R K1 V1 V2.
-#R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H
-#H elim H -H /3 width=4 by conj/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/substitution/drop_lreq.ma".
-include "basic_2/substitution/lpx_sn.ma".
-
-(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
-
-(* Properties on dropping ****************************************************)
-
-lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 →
- ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 →
- ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2.
-#R #L1 #L2 #H elim H -L1 -L2
-[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct
-| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H
- [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/
- | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
- /3 width=5 by drop_drop_lt, ex3_2_intro/
- ]
-]
-qed-.
-
-lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 →
- ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2.
-#R #L1 #L2 #H elim H -L1 -L2
-[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct
-| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H
- [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/
- | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
- /3 width=5 by drop_drop_lt, ex3_2_intro/
- ]
-]
-qed-.
-
-lemma lpx_sn_deliftable_dropable: ∀R. d_deliftable_sn R → dropable_sn (lpx_sn R).
-#R #HR #L1 #K1 #s #l #m #H elim H -L1 -K1 -l -m
-[ #l #m #Hm #X #H >(lpx_sn_inv_atom1 … H) -H
- /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/
-| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
- #L2 #V2 #HL12 #HV12 #H destruct
- /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/
-| #I #L1 #K1 #V1 #m #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H
- #L2 #V2 #HL12 #HV12 #H destruct
- elim (IHLK1 … HL12) -L1 /3 width=3 by drop_drop, ex2_intro/
-| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H
- elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
- elim (HR … HV12 … HLK1 … HWV1) -V1
- elim (IHLK1 … HL12) -L1 /3 width=5 by drop_skip, lpx_sn_pair, ex2_intro/
-]
-qed-.
-
-lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
- d_liftable R → dedropable_sn (lpx_sn R).
-#R #H1R #H2R #L1 #K1 #s #l #m #H elim H -L1 -K1 -l -m
-[ #l #m #Hm #X #H >(lpx_sn_inv_atom1 … H) -H
- /4 width=4 by drop_atom, lpx_sn_atom, ex3_intro/
-| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
- #K2 #V2 #HK12 #HV12 #H destruct
- lapply (lpx_sn_fwd_length … HK12)
- #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *)
- /3 width=1 by lpx_sn_pair, lreq_O2/
-| #I #L1 #K1 #V1 #m #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1
- /3 width=5 by drop_drop, lreq_pair, lpx_sn_pair, ex3_intro/
-| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H
- elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
- elim (H2R … HW12 … HLK1 … HWV1) -W1
- elim (IHLK1 … HK12) -K1
- /3 width=6 by drop_skip, lreq_succ, lpx_sn_pair, ex3_intro/
-]
-qed-.
-
-fact lpx_sn_dropable_aux: ∀R,L2,K2,s,l,m. ⬇[s, l, m] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
- l = 0 → ∃∃K1. ⬇[s, 0, m] L1 ≡ K1 & lpx_sn R K1 K2.
-#R #L2 #K2 #s #l #m #H elim H -L2 -K2 -l -m
-[ #l #m #Hm #X #H >(lpx_sn_inv_atom2 … H) -H
- /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/
-| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H
- #K1 #V1 #HK12 #HV12 #H destruct
- /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/
-| #I #L2 #K2 #V2 #m #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H
- #L1 #V1 #HL12 #HV12 #H destruct
- elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/
-| #I #L2 #K2 #V2 #W2 #l #m #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H)
-]
-qed-.
-
-lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R).
-/2 width=5 by lpx_sn_dropable_aux/ qed-.
]
qed-.
-lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
+lemma TC_lpx_sn_inv_pair2: ∀R. c_rs_transitive … R (λ_. lpx_sn R) →
∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) →
∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1
]
qed-.
-lemma TC_lpx_sn_ind: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
+lemma TC_lpx_sn_ind: ∀R. c_rs_transitive … R (λ_. lpx_sn R) →
∀S:relation lenv.
S (⋆) (⋆) → (
∀I,K1,K2,V1,V2.
]
qed-.
-fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
+fact TC_lpx_sn_inv_pair1_aux: ∀R. c_rs_transitive … R (λ_. lpx_sn R) →
∀L1,L2. TC … (lpx_sn R) L1 L2 →
∀I,K1,V1. L1 = K1.ⓑ{I}V1 →
∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
]
qed-.
-lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
+lemma TC_lpx_sn_inv_pair1: ∀R. c_rs_transitive … R (λ_. lpx_sn R) →
∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 →
∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-.
-lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
+lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. c_rs_transitive … R (λ_. lpx_sn R) →
∀L1,L2. TC … (lpx_sn R) L1 L2 →
lpx_sn (LTC … R) L1 L2.
/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-.
projects / helm.git / commitdiff