--- /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/lsubr_lbotr.ma".
+include "basic_2/relocation/ldrop_ldrop.ma".
+
+(* DROPPING *****************************************************************)
+
+(* Inversion lemmas about local env. full refinement for substitution *******)
+
+(* Note: ldrop_ldrop not needed *)
+lemma lbotr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ⊒[d, e] L →
+ d ≤ i → i < d + e → I = Abbr.
+#I #L elim L -L
+[ #K #V #i #H
+ lapply (ldrop_inv_atom1 … H) -H #H destruct
+| #L #J #W #IHL #K #V #i #H
+ elim (ldrop_inv_O1 … H) -H *
+ [ -IHL #H1 #H2 #d #e #HL #Hdi #Hide destruct
+ lapply (le_n_O_to_eq … Hdi) -Hdi #H destruct
+ lapply (HL … (L.ⓓW) ?) -HL /2 width=1/ #H
+ elim (lsubr_inv_abbr2 … H ?) -H // -Hide #K #_ #H destruct //
+ | #Hi #HLK #d @(nat_ind_plus … d) -d
+ [ #e #H #_ #Hide
+ elim (lbotr_inv_bind … H ?) -H [2: /2 width=2/ ] #HL #H destruct
+ @(IHL … HLK … HL) -IHL -HLK -HL // /2 width=1/
+ | #d #_ #e #H #Hdi #Hide
+ lapply (lbotr_inv_skip … H ?) -H // #HL
+ @(IHL … HLK … HL) -IHL -HLK -HL /2 width=1/
+ ]
+ ]
+]
+qed-.
+
+(* Properties about local env. full refinement for substitution *************)
+
+(* Note: ldrop_ldrop not needed *)
+lemma lbotr_ldrop: ∀L,d,e.
+ (∀I,K,V,i. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓑ{I}V → I = Abbr) →
+ ⊒[d, e] L.
+#L elim L -L //
+#L #I #V #IHL #d @(nat_ind_plus … d) -d
+[ #e @(nat_ind_plus … e) -e //
+ #e #_ #H0
+ >(H0 I L V 0 ? ? ?) //
+ /5 width=6 by lbotr_abbr, ldrop_ldrop, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *)
+| #d #_ #e #H0
+ /5 width=6 by lbotr_skip, ldrop_ldrop, le_S_S, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *)
+]
+qed.
+
+lemma lbotr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ⊒[dd, ee] L1 →
+ dd + ee ≤ d → ⊒[dd, ee] L2.
+#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
+@lbotr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
+lapply (lt_to_le_to_lt … Hiddee Hddee) -Hddee #Hid
+elim (ldrop_trans_le … HL12 … HLK2 ?) -L2 /2 width=2/ #X #HLK1 #H
+elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K1 #V1 #HK12 #HV21 #H destruct
+@(lbotr_inv_ldrop … HLK1 … HL1) -L1 -K1 -V1 //
+qed.
+
+lemma lbotr_ldrop_trans_be_up: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
+ ∀dd,ee. ⊒[dd, ee] L1 →
+ dd ≤ d + e → d + e ≤ dd + ee →
+ ⊒[d, dd + ee - d - e] L2.
+#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hdde #Hddee
+@lbotr_ldrop #I #K2 #V2 #i #Hdi #Hiddee #HLK2
+lapply (transitive_le ? ? (i+e)… Hdde ?) -Hdde /2 width=1/ #Hddie
+>commutative_plus in Hiddee; >minus_minus_comm <plus_minus_m_m /2 width=1/ -Hddee #Hiddee
+lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hdi #HL1K2
+@(lbotr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus // -Hddie /2 width=1/
+qed.
+
+lemma lbotr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ⊒[dd, ee] L1 →
+ d + e ≤ dd → ⊒[dd - e, ee] L2.
+#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
+@lbotr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
+elim (le_inv_plus_l … Hddee) -Hddee #Hdde #Hedd
+>plus_minus in Hiddee; // #Hiddee
+lapply (transitive_le … Hdde Hddi) -Hdde #Hid
+lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hid #HL1K2
+@(lbotr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus /2 width=1/
+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_px.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* DROPPING *****************************************************************)
+
+(* Properties on pointwise extension ****************************************)
+
+lemma lpx_deliftable_dropable: ∀R. t_deliftable_sn R → dropable_sn (lpx R).
+#R #HR #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H >(lpx_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #X #H
+ elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
+ elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (IHLK1 … HL12) -L1 /3 width=3/
+| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
+ elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (HR … HV12 … HWV1) -V1
+ elim (IHLK1 … HL12) -L1 /3 width=5/
+]
+qed.
+
+lemma lpx_liftable_dedropable: ∀R. reflexive ? R →
+ t_liftable R → dedropable_sn (lpx R).
+#R #H1R #H2R #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H >(lpx_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #X #H
+ elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
+ elim (IHLK1 … HK12) -K1 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
+ elim (lpx_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (lift_total W2 d e) #V2 #HWV2
+ lapply (H2R … HW12 … HWV1 … HWV2) -W1
+ elim (IHLK1 … HK12) -K1 /3 width=5/
+]
+qed.
+
+fact lpx_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx R L1 L2 →
+ d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & lpx R K1 K2.
+#R #L2 #K2 #d #e #H elim H -L2 -K2 -d -e
+[ #d #e #X #H >(lpx_inv_atom2 … H) -H /2 width=3/
+| #K2 #I #V2 #X #H
+ elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/
+| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_
+ elim (lpx_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct
+ elim (IHLK2 … HL12 ?) -L2 // /3 width=3/
+| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
+ >commutative_plus normalize #H destruct
+]
+qed-.
+
+lemma lpx_dropable: ∀R. dropable_dx (lpx R).
+/2 width=5 by lpx_dropable_aux/ 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_append.ma".
+
+(* POINTWISE EXTENSION OF A CONTEXT-FREE REALTION FOR TERMS *****************)
+
+inductive lpx (R:relation term): relation lenv ≝
+| lpx_stom: lpx R (⋆) (⋆)
+| lpx_pair: ∀I,K1,K2,V1,V2.
+ lpx R K1 K2 → R V1 V2 → lpx R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
+.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lpx_inv_atom1_aux: ∀R,L1,L2. lpx R L1 L2 → L1 = ⋆ → L2 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_inv_atom1: ∀R,L2. lpx R (⋆) L2 → L2 = ⋆.
+/2 width=4 by lpx_inv_atom1_aux/ qed-.
+
+fact lpx_inv_pair1_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. lpx R K1 K2 & R 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/
+]
+qed-.
+
+lemma lpx_inv_pair1: ∀R,I,K1,V1,L2. lpx R (K1. ⓑ{I} V1) L2 →
+ ∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_inv_pair1_aux/ qed-.
+
+fact lpx_inv_atom2_aux: ∀R,L1,L2. lpx R L1 L2 → L2 = ⋆ → L1 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_inv_atom2: ∀R,L1. lpx R L1 (⋆) → L1 = ⋆.
+/2 width=4 by lpx_inv_atom2_aux/ qed-.
+
+fact lpx_inv_pair2_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. lpx R K1 K2 & R 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/
+]
+qed-.
+
+lemma lpx_inv_pair2: ∀R,I,L1,K2,V2. lpx R L1 (K2. ⓑ{I} V2) →
+ ∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_fwd_length: ∀R,L1,L2. lpx R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H -L1 -L2 normalize //
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lpx_inv_append1: ∀R,L1,K1,L. lpx R (K1 @@ L1) L →
+ ∃∃K2,L2. lpx R K1 K2 & lpx R L1 L2 & L = K2 @@ L2.
+#R #L1 elim L1 -L1 normalize
+[ #K1 #K2 #HK12
+ @(ex3_2_intro … K2 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *)
+| #L1 #I #V1 #IH #K1 #X #H
+ elim (lpx_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct
+ elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #HL12 #H destruct
+ @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *)
+]
+qed-.
+
+lemma lpx_inv_append2: ∀R,L2,K2,L. lpx R L (K2 @@ L2) →
+ ∃∃K1,L1. lpx R K1 K2 & lpx R L1 L2 & L = K1 @@ L1.
+#R #L2 elim L2 -L2 normalize
+[ #K2 #K1 #HK12
+ @(ex3_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *)
+| #L2 #I #V2 #IH #K2 #X #H
+ elim (lpx_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct
+ elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #HL12 #H destruct
+ @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *)
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R).
+#R #HR #L elim L -L // /2 width=1/
+qed.
+
+lemma lpx_sym: ∀R. symmetric ? R → symmetric … (lpx R).
+#R #HR #L1 #L2 #H elim H -H // /3 width=1/
+qed.
+
+lemma lpx_trans: ∀R. Transitive ? R → Transitive … (lpx R).
+#R #HR #L1 #L #H elim H -L //
+#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
+elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/
+qed.
+
+lemma lpx_conf: ∀R. confluent ? R → confluent … (lpx R).
+#R #HR #L0 #L1 #H elim H -L1
+[ #X #H >(lpx_inv_atom1 … H) -X /2 width=3/
+| #I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #X #H
+ elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK02 #HV02 #H destruct
+ elim (IHK01 … HK02) -K0 #K #HK1 #HK2
+ elim (HR … HV01 … HV02) -HR -V0 /3 width=5/
+]
+qed.
+
+lemma lpx_TC_inj: ∀R,L1,L2. lpx R L1 L2 → lpx (TC … R) L1 L2.
+#R #L1 #L2 #H elim H -L1 -L2 // /3 width=1/
+qed.
+
+lemma lpx_TC_step: ∀R,L1,L. lpx (TC … R) L1 L →
+ ∀L2. lpx R L L2 → lpx (TC … R) L1 L2.
+#R #L1 #L #H elim H -L /2 width=1/
+#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
+elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/
+qed.
+
+lemma TC_lpx_pair_dx: ∀R. reflexive ? R →
+ ∀I,K,V1,V2. TC … R V1 V2 →
+ TC … (lpx R) (K.ⓑ{I}V1) (K.ⓑ{I}V2).
+#R #HR #I #K #V1 #V2 #H elim H -V2
+/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *)
+qed.
+
+lemma TC_lpx_pair_sn: ∀R. reflexive ? R →
+ ∀I,V,K1,K2. TC … (lpx R) K1 K2 →
+ TC … (lpx R) (K1.ⓑ{I}V) (K2.ⓑ{I}V).
+#R #HR #I #V #K1 #K2 #H elim H -K2
+/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *)
+qed.
+
+lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2.
+#R #L1 #L2 #H elim H -L2 /2 width=1/ /2 width=3/
+qed.
+
+lemma lpx_inv_TC: ∀R. reflexive ? R →
+ ∀L1,L2. lpx (TC … R) L1 L2 → TC … (lpx R) L1 L2.
+#R #HR #L1 #L2 #H elim H -L1 -L2 /3 width=1/ /3 width=3/
+qed.
+
+lemma lpx_append: ∀R,K1,K2. lpx R K1 K2 → ∀L1,L2. lpx R L1 L2 →
+ lpx R (L1 @@ K1) (L2 @@ K2).
+#R #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
+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/computation/ltprs.ma".
+include "basic_2/computation/lfprs.ma".
+
+(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
+
+(* Properties on context-free parallel computation for local environments ***)
+
+lemma ltprs_lfprs: ∀L1,L2. L1 ➡* L2 → ⦃L1⦄ ➡* ⦃L2⦄.
+/3 width=3/ qed.
--- /dev/null
+definition t_liftable: relation term → Prop ≝
+ λR. ∀T1,T2. R T1 T2 → ∀U1,d,e. ⇧[d, e] T1 ≡ U1 →
+ ∀U2. ⇧[d, e] T2 ≡ U2 → R U1 U2.
+
+definition t_deliftable_sn: relation term → Prop ≝
+ λR. ∀U1,U2. R U1 U2 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
+ ∃∃T2. ⇧[d, e] T2 ≡ U2 & R T1 T2.
+
+lemma t_liftable_TC: ∀R. t_liftable R → t_liftable (TC … R).
+#R #HR #T1 #T2 #H elim H -T2
+[ /3 width=7/
+| #T #T2 #_ #HT2 #IHT1 #U1 #d #e #HTU1 #U2 #HTU2
+ elim (lift_total T d e) /3 width=9/
+]
+qed.
+
+lemma t_deliftable_sn_TC: ∀R. t_deliftable_sn R → t_deliftable_sn (TC … R).
+#R #HR #U1 #U2 #H elim H -U2
+[ #U2 #HU12 #T1 #d #e #HTU1
+ elim (HR … HU12 … HTU1) -U1 /3 width=3/
+| #U #U2 #_ #HU2 #IHU1 #T1 #d #e #HTU1
+ elim (IHU1 … HTU1) -U1 #T #HTU #HT1
+ elim (HR … HU2 … HTU) -U /3 width=5/
+]
+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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( L1 break ⊑ [ term 46 d , break term 46 e ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'SubEq $L1 $d $e $L2 }.
+
+include "basic_2/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+inductive lsubr: nat → nat → relation lenv ≝
+| lsubr_sort: ∀d,e. lsubr d e (⋆) (⋆)
+| lsubr_OO: ∀L1,L2. lsubr 0 0 L1 L2
+| lsubr_abbr: ∀L1,L2,V,e. lsubr 0 e L1 L2 →
+ lsubr 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
+| lsubr_abst: ∀L1,L2,I,V1,V2,e. lsubr 0 e L1 L2 →
+ lsubr 0 (e + 1) (L1. ⓑ{I}V1) (L2. ⓛV2)
+| lsubr_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
+ lsubr d e L1 L2 → lsubr (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
+.
+
+interpretation
+ "local environment refinement (substitution)"
+ 'SubEq L1 d e L2 = (lsubr d e L1 L2).
+
+definition lsubr_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+ ∀L2,s1,s2. R L2 s1 s2 →
+ ∀L1,d,e. L1 ⊑ [d, e] L2 → R L1 s1 s2.
+
+(* Basic properties *********************************************************)
+
+lemma lsubr_bind_eq: ∀L1,L2,e. L1 ⊑ [0, e] L2 → ∀I,V.
+ L1. ⓑ{I} V ⊑ [0, e + 1] L2.ⓑ{I} V.
+#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
+qed.
+
+lemma lsubr_abbr_lt: ∀L1,L2,V,e. L1 ⊑ [0, e - 1] L2 → 0 < e →
+ L1. ⓓV ⊑ [0, e] L2.ⓓV.
+#L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
+qed.
+
+lemma lsubr_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ⊑ [0, e - 1] L2 → 0 < e →
+ L1. ⓑ{I}V1 ⊑ [0, e] L2. ⓛV2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
+qed.
+
+lemma lsubr_skip_lt: ∀L1,L2,d,e. L1 ⊑ [d - 1, e] L2 → 0 < d →
+ ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 ⊑ [d, e] L2. ⓑ{I2} V2.
+#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
+qed.
+
+lemma lsubr_bind_lt: ∀I,L1,L2,V,e. L1 ⊑ [0, e - 1] L2 → 0 < e →
+ L1. ⓓV ⊑ [0, e] L2. ⓑ{I}V.
+* /2 width=1/ qed.
+
+lemma lsubr_refl: ∀d,e,L. L ⊑ [d, e] L.
+#d elim d -d
+[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
+| #d #IHd #e #L elim L -L // /2 width=1/
+]
+qed.
+
+lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (λL. (TC … (R L))).
+#S #R #HR #L1 #s1 #s2 #H elim H -s2
+[ /3 width=5/
+| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
+ lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubr_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → L1 = ⋆ →
+ L2 = ⋆ ∨ (d = 0 ∧ e = 0).
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ /2 width=1/
+| /3 width=1/
+| #L1 #L2 #W #e #_ #H destruct
+| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
+]
+qed.
+
+lemma lsubr_inv_atom1: ∀L2,d,e. ⋆ ⊑ [d, e] L2 →
+ L2 = ⋆ ∨ (d = 0 ∧ e = 0).
+/2 width=3/ qed-.
+
+fact lsubr_inv_skip1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
+ ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
+ ∃∃I2,K2,V2. K1 ⊑ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #I1 #K1 #V1 #H destruct
+| #L1 #L2 #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
+]
+qed.
+
+lemma lsubr_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ⊑ [d, e] L2 → 0 < d →
+ ∃∃I2,K2,V2. K1 ⊑ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=5/ qed-.
+
+fact lsubr_inv_atom2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → L2 = ⋆ →
+ L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ /2 width=1/
+| /3 width=1/
+| #L1 #L2 #W #e #_ #H destruct
+| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
+]
+qed.
+
+lemma lsubr_inv_atom2: ∀L1,d,e. L1 ⊑ [d, e] ⋆ →
+ L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+/2 width=3/ qed-.
+
+fact lsubr_inv_abbr2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
+ ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
+ ∃∃K1. K1 ⊑ [0, e - 1] K2 & L1 = K1.ⓓV.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #K1 #V #H destruct
+| #L1 #L2 #K1 #V #_ #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #W #e #HL12 #K1 #V #H #_ #_ destruct /2 width=3/
+| #L1 #L2 #I #W1 #W2 #e #_ #K1 #V #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #K1 #V #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma lsubr_inv_abbr2: ∀L1,K2,V,e. L1 ⊑ [0, e] K2.ⓓV → 0 < e →
+ ∃∃K1. K1 ⊑ [0, e - 1] K2 & L1 = K1.ⓓV.
+/2 width=5/ qed-.
+
+fact lsubr_inv_skip2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
+ ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
+ ∃∃I1,K1,V1. K1 ⊑ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #I1 #K1 #V1 #H destruct
+| #L1 #L2 #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
+]
+qed.
+
+lemma lsubr_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ⊑ [d, e] K2.ⓑ{I2}V2 → 0 < d →
+ ∃∃I1,K1,V1. K1 ⊑ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
+/2 width=5/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+fact lsubr_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
+ d = 0 → e = |L1| → |L1| ≤ |L2|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
+[ //
+| /2 width=1/
+| /3 width=1/
+| /3 width=1/
+| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma lsubr_fwd_length_full1: ∀L1,L2. L1 ⊑ [0, |L1|] L2 → |L1| ≤ |L2|.
+/2 width=5/ qed-.
+
+fact lsubr_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
+ d = 0 → e = |L2| → |L2| ≤ |L1|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
+[ //
+| /2 width=1/
+| /3 width=1/
+| /3 width=1/
+| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma lsubr_fwd_length_full2: ∀L1,L2. L1 ⊑ [0, |L2|] L2 → |L2| ≤ |L1|.
+/2 width=5/ 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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( ⊒ [ term 46 d , break term 46 e ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'SubEqBottom $d $e $L2 }.
+
+include "basic_2/relocation/lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+(* bottom element of the refinement *)
+definition lbotr: nat → nat → predicate lenv ≝
+ λd,e. NF_sn … (lsubr d e) (lsubr d e …).
+
+interpretation
+ "local environment full refinement (substitution)"
+ 'SubEqBottom d e L = (lbotr d e L).
+
+(* Basic properties *********************************************************)
+
+lemma lbotr_atom: ∀d,e. ⊒[d, e] ⋆.
+#d #e #L #H
+elim (lsubr_inv_atom2 … H) -H
+[ #H destruct //
+| * #H1 #H2 destruct //
+]
+qed.
+
+lemma lbotr_OO: ∀L. ⊒[0, 0] L.
+// qed.
+
+lemma lbotr_abbr: ∀L,V,e. ⊒[0, e] L → ⊒[0, e + 1] L.ⓓV.
+#L #V #e #HL #K #H
+elim (lsubr_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
+lapply (HL … HLX) -HL -HLX /2 width=1/
+qed.
+
+lemma lbotr_abbr_O: ∀L,V. ⊒[0,1] L.ⓓV.
+#L #V
+@(lbotr_abbr … 0) //
+qed.
+
+lemma lbotr_skip: ∀I,L,V,d,e. ⊒[d, e] L → ⊒[d + 1, e] L.ⓑ{I}V.
+#I #L #V #d #e #HL #K #H
+elim (lsubr_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
+lapply (HL … HLX) -HL -HLX /2 width=1/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lbotr_inv_bind: ∀I,L,V,e. ⊒[0, e] L.ⓑ{I}V → 0 < e →
+ ⊒[0, e - 1] L ∧ I = Abbr.
+#I #L #V #e #HL #He
+lapply (HL (L.ⓓV) ?) /2 width=1/ #H
+elim (lsubr_inv_abbr2 … H ?) -H // #K #_ #H destruct
+@conj // #L #HKL
+lapply (HL (L.ⓓV) ?) -HL /2 width=1/ -HKL #H
+elim (lsubr_inv_abbr2 … H ?) -H // -He #X #HLX #H destruct //
+qed-.
+
+lemma lbotr_inv_skip: ∀I,L,V,d,e. ⊒[d, e] L.ⓑ{I}V → 0 < d → ⊒[d - 1, e] L.
+#I #L #V #d #e #HL #Hd #K #HLK
+lapply (HL (K.ⓑ{I}V) ?) -HL /2 width=1/ -HLK #H
+elim (lsubr_inv_skip2 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
+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/reducibility/ltpr.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+definition ltprs: relation lenv ≝ TC … ltpr.
+
+interpretation
+ "context-free parallel computation (environment)"
+ 'PRedStar L1 L2 = (ltprs L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma ltprs_ind: ∀L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. L1 ➡* L → L ➡ L2 → R L → R L2) →
+ ∀L2. L1 ➡* L2 → R L2.
+#L1 #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma ltprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. L1 ➡ L → L ➡* L2 → R L → R L1) →
+ ∀L1. L1 ➡* L2 → R L1.
+#L2 #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma ltprs_refl: reflexive … ltprs.
+/2 width=1/ qed.
+
+lemma ltpr_ltprs: ∀L1,L2. L1 ➡ L2 → L1 ➡* L2.
+/2 width=1/ qed.
+
+lemma ltprs_strap1: ∀L1,L,L2. L1 ➡* L → L ➡ L2 → L1 ➡* L2.
+/2 width=3/ qed.
+
+lemma ltprs_strap2: ∀L1,L,L2. L1 ➡ L → L ➡* L2 → L1 ➡* L2.
+/2 width=3/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltprs_inv_atom1: ∀L2. ⋆ ➡* L2 → L2 = ⋆.
+#L2 #H @(ltprs_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL1 destruct
+>(ltpr_inv_atom1 … HL2) -L2 //
+qed-.
+
+lemma ltprs_inv_pair1: ∀I,K1,L2,V1. K1. ⓑ{I} V1 ➡* L2 →
+ ∃∃K2,V2. K1 ➡* K2 & V1 ➡* V2 & L2 = K2. ⓑ{I} V2.
+#I #K1 #L2 #V1 #H @(ltprs_ind … H) -L2 /2 width=5/
+#L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
+elim (ltpr_inv_pair1 … HL2) -HL2 #K2 #V2 #HK2 #HV2 #H destruct /3 width=5/
+qed-.
+
+lemma ltprs_inv_atom2: ∀L1. L1 ➡* ⋆ → L1 = ⋆.
+#L1 #H @(ltprs_ind_dx … H) -L1 //
+#L1 #L #HL1 #_ #IHL2 destruct
+>(ltpr_inv_atom2 … HL1) -L1 //
+qed-.
+
+lemma ltprs_inv_pair2: ∀I,L1,K2,V2. L1 ➡* K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ➡* K2 & V1 ➡* V2 & L1 = K1. ⓑ{I} V1.
+#I #L1 #K2 #V2 #H @(ltprs_ind_dx … H) -L1 /2 width=5/
+#L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
+elim (ltpr_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct /3 width=5/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltprs_fwd_length: ∀L1,L2. L1 ➡* L2 → |L1| = |L2|.
+#L1 #L2 #H @(ltprs_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL1
+>IHL1 -L1 >(ltpr_fwd_length … HL2) -HL2 //
+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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( T1 ➡ ➡ * break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStarAlt $T1 $T2 }.
+
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+(* alternative definition of ltprs *)
+definition ltprsa: relation lenv ≝ lpx tprs.
+
+interpretation
+ "context-free parallel computation (environment) alternative"
+ 'PRedStarAlt L1 L2 = (ltprsa L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltprs_ltprsa: ∀L1,L2. L1 ➡* L2 → L1 ➡➡* L2.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltprsa_ltprs: ∀L1,L2. L1 ➡➡* L2 → L1 ➡* L2.
+/2 width=1/ 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/reducibility/ltpr_ldrop.ma".
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+lemma ltprs_ldrop_conf: dropable_sn ltprs.
+/2 width=3/ qed.
+
+lemma ldrop_ltprs_trans: dedropable_sn ltprs.
+/2 width=3/ qed.
+
+lemma ltprs_ldrop_trans_O1: dropable_dx ltprs.
+/2 width=3/ 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/reducibility/ltpr_ltpr.ma".
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+(* Advanced properties ******************************************************)
+
+lemma ltprs_strip: ∀L1. ∀L:lenv. L ➡* L1 → ∀L2. L ➡ L2 →
+ ∃∃L0. L1 ➡ L0 & L2 ➡* L0.
+/3 width=3/ qed.
+
+(* Main properties **********************************************************)
+
+theorem ltprs_conf: confluent … ltprs.
+/3 width=3/ qed.
+
+theorem ltprs_trans: Transitive … ltprs.
+/2 width=3/ 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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( T1 ➡ * break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStar $T1 $T2 }.
+
+include "basic_2/reducibility/tpr.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Basic_1: includes: pr1_pr0 *)
+definition tprs: relation term ≝ TC … tpr.
+
+interpretation "context-free parallel computation (term)"
+ 'PRedStar T1 T2 = (tprs T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma tprs_ind: ∀T1. ∀R:predicate term. R T1 →
+ (∀T,T2. T1 ➡* T → T ➡ T2 → R T → R T2) →
+ ∀T2. T1 ➡* T2 → R T2.
+#T1 #R #HT1 #IHT1 #T2 #HT12
+@(TC_star_ind … HT1 IHT1 … HT12) //
+qed-.
+
+lemma tprs_ind_dx: ∀T2. ∀R:predicate term. R T2 →
+ (∀T1,T. T1 ➡ T → T ➡* T2 → R T → R T1) →
+ ∀T1. T1 ➡* T2 → R T1.
+#T2 #R #HT2 #IHT2 #T1 #HT12
+@(TC_star_ind_dx … HT2 IHT2 … HT12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma tprs_refl: reflexive … tprs.
+/2 width=1/ qed.
+
+lemma tpr_tprs: ∀T1,T2. T1 ➡ T2 → T2 ➡* T2.
+/2 width=1/ qed.
+
+lemma tprs_strap1: ∀T1,T,T2. T1 ➡* T → T ➡ T2 → T1 ➡* T2.
+/2 width=3/ qed.
+
+lemma tprs_strap2: ∀T1,T,T2. T1 ➡ T → T ➡* T2 → T1 ➡* T2.
+/2 width=3/ qed.
+
+(* Basic_1: was only: pr1_head_1 *)
+lemma tprs_pair_sn: ∀I,T1,T2. T1 ➡ T2 → ∀V1,V2. V1 ➡* V2 →
+ ②{I} V1. T1 ➡* ②{I} V2. T2.
+* [ #a ] #I #T1 #T2 #HT12 #V1 #V2 #H @(tprs_ind … H) -V2
+[1,3: /3 width=1/
+|2,4: #V #V2 #_ #HV2 #IHV1
+ @(tprs_strap1 … IHV1) -IHV1 /2 width=1/
+]
+qed.
+
+(* Basic_1: was only: pr1_head_2 *)
+lemma tprs_pair_dx: ∀I,V1,V2. V1 ➡ V2 → ∀T1,T2. T1 ➡* T2 →
+ ②{I} V1. T1 ➡* ②{I} V2. T2.
+* [ #a ] #I #V1 #V2 #HV12 #T1 #T2 #H @(tprs_ind … H) -T2
+[1,3: /3 width=1/
+|2,4: #T #T2 #_ #HT2 #IHT1
+ @(tprs_strap1 … IHT1) -IHT1 /2 width=1/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma tprs_inv_atom1: ∀U2,k. ⋆k ➡* U2 → U2 = ⋆k.
+#U2 #k #H @(tprs_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU1 destruct
+>(tpr_inv_atom1 … HU2) -HU2 //
+qed-.
+
+lemma tprs_inv_cast1: ∀W1,T1,U2. ⓝW1.T1 ➡* U2 → T1 ➡* U2 ∨
+ ∃∃W2,T2. W1 ➡* W2 & T1 ➡* T2 & U2 = ⓝW2.T2.
+#W1 #T1 #U2 #H @(tprs_ind … H) -U2 /3 width=5/
+#U #U2 #_ #HU2 * /3 width=3/ *
+#W #T #HW1 #HT1 #H destruct
+elim (tpr_inv_cast1 … HU2) -HU2 /3 width=3/ *
+#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+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/reducibility/tpr_lift.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma tprs_inv_abst1: ∀a,V1,T1,U2. ⓛ{a}V1. T1 ➡* U2 →
+ ∃∃V2,T2. V1 ➡* V2 & T1 ➡* T2 & U2 = ⓛ{a}V2. T2.
+#a #V1 #T1 #U2 #H @(tprs_ind … H) -U2 /2 width=5/
+#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
+elim (tpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+qed-.
+
+lemma tprs_inv_abst: ∀a,V1,V2,T1,T2. ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 →
+ V1 ➡* V2 ∧ T1 ➡* T2.
+#a #V1 #V2 #T1 #T2 #H
+elim (tprs_inv_abst1 … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/
+qed-.
+
+(* Relocation properties ****************************************************)
+
+(* Note: this was missing in basic_1 *)
+lemma tprs_lift: t_liftable tprs.
+/3 width=7/ qed.
+
+(* Note: this was missing in basic_1 *)
+lemma tprs_inv_lift1: t_deliftable_sn tprs.
+/3 width=3 by tpr_inv_lift1, t_deliftable_sn_TC/ 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/reducibility/tpr_tpr.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was: pr1_strip *)
+lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 →
+ ∃∃T0. T1 ➡ T0 & T2 ➡* T0.
+/3 width=3 by TC_strip1, tpr_conf/ qed.
+
+(* Main propertis ***********************************************************)
+
+(* Basic_1: was: pr1_confluence *)
+theorem tprs_conf: confluent … tprs.
+/3 width=3/ qed.
+
+(* Basic_1: was: pr1_t *)
+theorem tprs_trans: Transitive … tprs.
+/2 width=3/ qed.
+
+(* Basic_1: was: pr1_comp *)
+lemma tprs_pair: ∀I,V1,V2. V1 ➡* V2 → ∀T1,T2. T1 ➡* T2 →
+ ②{I} V1. T1 ➡* ②{I} V2. T2.
+#I #V1 #V2 #H @(tprs_ind … H) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12
+@(tprs_trans … (②{I}V.T2)) /2 width=1/
+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/reducibility/cpr_delift.ma".
+include "basic_2/reducibility/cpr_cpr.ma".
+include "basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties on inverse basic term relocation ******************************)
+
+(* Note: this should be stated with tprs *)
+lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → L ⊢ +ⓓV.T1 ➡* T2.
+#L #V #T1 #T2 * #T #HT1 #HT2
+@(cprs_strap2 … (+ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *)
+qed.
+
+(* Basic_1: was only: pr3_gen_cabbr *)
+lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 →
+ ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 →
+ ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ ▼*[d, e] U2 ≡ T2.
+#L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/
+#U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT
+elim (thin_cpr_delift_conf … HU2 … HLK … HUT) -U -HLK /3 width=3/
+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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ * break ⦃ term 46 L2 , term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRedStar $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ ➡ * break ⦃ term 46 L2 , term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }.
+
+include "basic_2/reducibility/fpr.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+definition fprs: bi_relation lenv term ≝ bi_TC … fpr.
+
+interpretation "context-free parallel computation (closure)"
+ 'FocalizedPRedStar L1 T1 L2 T2 = (fprs L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma fprs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 →
+ (∀L,L2,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → R L T → R L2 T2) →
+ ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L2 T2.
+/3 width=7 by bi_TC_star_ind/ qed-.
+
+lemma fprs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 →
+ (∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → R L T → R L1 T1) →
+ ∀L1,T1. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L1 T1.
+/3 width=7 by bi_TC_star_ind_dx/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fpr_fprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma fprs_refl: bi_reflexive … fprs.
+/2 width=1/ qed.
+
+lemma fprs_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fprs_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+/2 width=4/ 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/reducibility/cfpr_aaa.ma".
+include "basic_2/computation/fprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_fprs_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A →
+ ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L2 ⊢ T2 ⁝ A.
+#L1 #T1 #A #HT1 #L2 #T2 #HLT12
+@(bi_TC_Conf3 … HT1 ?? HLT12) /2 width=4/
+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/reducibility/fpr_cpr.ma".
+include "basic_2/computation/cprs_lfprs.ma".
+include "basic_2/computation/lfprs_ltprs.ma".
+include "basic_2/computation/lfprs_fprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma fprs_flat_dx_tpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ∀V1,V2. V1 ➡ V2 →
+ ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ➡* ⦃L2, ⓕ{I}V2.T2⦄.
+#L1 #L2 #T1 #T2 #HT12 @(fprs_ind … HT12) -L2 -T2 /3 width=1/
+#L #L2 #T #T2 #_ #HT2 #IHT2 #V1 #V2 #HV12 #I
+lapply (IHT2 … HV12 I) -IHT2 -HV12 /3 width=6/
+qed.
+
+lemma fprs_bind2_minus: ∀I,L1,L2,V1,T1,U2. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L2, U2⦄ →
+ ∃∃V2,T2. ⦃L1.ⓑ{I}V1, T1⦄ ➡* ⦃L2.ⓑ{I}V2, T2⦄ &
+ U2 = -ⓑ{I}V2.T2.
+#I #L1 #L2 #V1 #T1 #U2 #H @(fprs_ind … H) -L2 -U2 /2 width=4/
+#L #L2 #U #U2 #_ #HU2 * #V #T #HT1 #H destruct
+elim (fpr_bind2_minus … HU2) -HU2 /3 width=4/
+qed-.
+
+lemma fprs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ➡* ⦃K2, T2⦄ →
+ ∀d,e,L1. ⇩[d, e] L1 ≡ K1 →
+ ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
+ ∃∃L2. ⦃L1, U1⦄ ➡* ⦃L2, U2⦄ & ⇩[d, e] L2 ≡ K2.
+#K1 #K2 #T1 #T2 #HT12 @(fprs_ind … HT12) -K2 -T2
+[ #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2
+ >(lift_mono … HTU2 … HTU1) -U2 /2 width=3/
+| #K #K2 #T #T2 #_ #HT2 #IHT1 #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2
+ elim (lift_total T d e) #U #HTU
+ elim (IHT1 … HLK1 … HTU1 HTU) -K1 -T1 #L #HU1 #HKL
+ elim (fpr_lift … HT2 … HKL … HTU HTU2) -K -T -T2 /3 width=4/
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma fprs_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ →
+ ∃∃K2,V2. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ &
+ ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄ &
+ L2 = K2.ⓑ{I}V2.
+#I #K1 #L2 #V1 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /2 width=5/
+#L #L2 #T #T2 #_ #HT2 * #K #V #HV1 #HT1 #H destruct
+elim (fpr_inv_pair1 … HT2) -HT2 #K2 #V2 #HV2 #HT2 #H destruct /3 width=5/
+qed-.
+
+lemma fprs_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡* ⦃K2.ⓑ{I}V2, T2⦄ →
+ ∃∃K1,V1. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ &
+ ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄ &
+ L1 = K1.ⓑ{I}V1.
+#I2 #L1 #K2 #V2 #T1 #T2 #H @(fprs_ind_dx … H) -L1 -T1 /2 width=5/
+#L1 #L #T1 #T #HT1 #_ * #K #V #HV2 #HT2 #H destruct
+elim (fpr_inv_pair3 … HT1) -HT1 #K1 #V1 #HV1 #HT1 #H destruct /3 width=5/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma fprs_fwd_bind2_minus: ∀I,L1,L,V1,T1,T. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L, T⦄ → ∀b.
+ ∃∃V2,T2. ⦃L1, ⓑ{b,I}V1.T1⦄ ➡* ⦃L, ⓑ{b,I}V2.T2⦄ &
+ T = -ⓑ{I}V2.T2.
+#I #L1 #L #V1 #T1 #T #H1 #b @(fprs_ind … H1) -L -T /2 width=4/
+#L0 #L #T0 #T #_ #H0 * #W1 #U1 #HTU1 #H destruct
+elim (fpr_fwd_bind2_minus … H0 b) -H0 /3 width=4/
+qed-.
+
+lemma fprs_fwd_pair1_full: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ →
+ ∀b. ∃∃K2,V2. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ &
+ ⦃K1, ⓑ{b,I}V1.T1⦄ ➡* ⦃K2, ⓑ{b,I}V2.T2⦄ &
+ L2 = K2.ⓑ{I}V2.
+#I #K1 #L2 #V1 #T1 #T2 #H #b
+elim (fprs_inv_pair1 … H) -H #K2 #V2 #HV12 #HT12 #H destruct
+elim (fprs_fwd_bind2_minus … HT12 b) -HT12 #W1 #U1 #HTU1 #H destruct /2 width=5/
+qed-.
+
+lemma fprs_fwd_abst2: ∀a,L1,L2,V1,T1,U2. ⦃L1, ⓛ{a}V1.T1⦄ ➡* ⦃L2, U2⦄ → ∀b,I,W.
+ ∃∃V2,T2. ⦃L1, ⓑ{b,I}W.T1⦄ ➡* ⦃L2, ⓑ{b,I}W.T2⦄ &
+ U2 = ⓛ{a}V2.T2.
+#a #L1 #L2 #V1 #T1 #U2 #H #b #I #W @(fprs_ind … H) -L2 -U2 /2 width=4/
+#L #L2 #U #U2 #_ #H2 * #V #T #HT1 #H destruct
+elim (fpr_fwd_abst2 … H2 b I W) -H2 /3 width=4/
+qed-.
+
+(* Properties on context-sensitive parallel computation for terms ***********)
+
+lemma cprs_fprs: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ⦃L, T1⦄ ➡* ⦃L, T2⦄.
+#L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4/
+qed.
+
+(* Forward lemmas on context-sensitive parallel computation for terms *******)
+
+lemma fprs_fwd_cprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 //
+#L #L2 #T #T2 #H1 #H2 #IH1
+elim (fpr_inv_all … H2) -H2 #L0 #HL0 #HT2 #_ -L2
+lapply (lfprs_cpr_trans L1 … HT2) -HT2 /3 width=3/
+qed-.
+(*
+(* Advanced properties ******************************************************)
+
+lamma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 →
+ ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄.
+#L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I
+elim (fpr_inv_all … H) /3 width=4/
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lamma fpr_fwd_shift_bind_minus: ∀I1,I2,L1,L2,V1,V2,T1,T2.
+ ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ →
+ ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ ∧ I1 = I2.
+* #I2 #L1 #L2 #V1 #V2 #T1 #T2 #H
+elim (fpr_inv_all … H) -H #L #HL1 #H #HL2
+[ elim (cpr_inv_abbr1 … H) -H *
+ [ #V #V0 #T #HV1 #HV0 #_ #H destruct /4 width=4/
+ | #T #_ #_ #H destruct
+ ]
+| elim (cpr_inv_abst1 … H Abst V2) -H
+ #V #T #HV1 #_ #H destruct /3 width=4/
+]
+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/reducibility/fpr_fpr.ma".
+include "basic_2/computation/fprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma fprs_strip: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ➡ ⦃L1, T1⦄ →
+ ∀L2,T2. ⦃L0, T0⦄ ➡* ⦃L2, T2⦄ →
+ ∃∃L,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ & ⦃L2, T2⦄ ➡ ⦃L, T⦄.
+#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8
+/2 width=4/ qed.
+
+(* Main propertis ***********************************************************)
+
+theorem fprs_conf: bi_confluent … fprs.
+/2 width=4/ qed.
+
+theorem fprs_trans: bi_transitive … fprs.
+/2 width=4/ 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".
+
+(* POINTWISE EXTENSION OF A FOCALIZED REALTION FOR TERMS ********************)
+
+inductive lpx_bi (R:bi_relation lenv term): relation lenv ≝
+| lpx_bi_stom: lpx_bi R (⋆) (⋆)
+| lpx_bi_pair: ∀I,K1,K2,V1,V2.
+ lpx_bi R K1 K2 → R K1 V1 K2 V2 →
+ lpx_bi R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
+.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lpx_bi_inv_atom1_aux: ∀R,L1,L2. lpx_bi R L1 L2 → L1 = ⋆ → L2 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_bi_inv_atom1: ∀R,L2. lpx_bi R (⋆) L2 → L2 = ⋆.
+/2 width=4 by lpx_bi_inv_atom1_aux/ qed-.
+
+fact lpx_bi_inv_pair1_aux: ∀R,L1,L2. lpx_bi R L1 L2 →
+ ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. lpx_bi R K1 K2 &
+ R K1 V1 K2 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/
+]
+qed-.
+
+lemma lpx_bi_inv_pair1: ∀R,I,K1,V1,L2. lpx_bi R (K1. ⓑ{I} V1) L2 →
+ ∃∃K2,V2. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+ L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_bi_inv_pair1_aux/ qed-.
+
+fact lpx_bi_inv_atom2_aux: ∀R,L1,L2. lpx_bi R L1 L2 → L2 = ⋆ → L1 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_bi_inv_atom2: ∀R,L1. lpx_bi R L1 (⋆) → L1 = ⋆.
+/2 width=4 by lpx_bi_inv_atom2_aux/ qed-.
+
+fact lpx_bi_inv_pair2_aux: ∀R,L1,L2. lpx_bi R L1 L2 →
+ ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. lpx_bi R K1 K2 & R K1 V1 K2 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/
+]
+qed-.
+
+lemma lpx_bi_inv_pair2: ∀R,I,L1,K2,V2. lpx_bi R L1 (K2. ⓑ{I} V2) →
+ ∃∃K1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+ L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_bi_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_bi_fwd_length: ∀R,L1,L2. lpx_bi R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H -L1 -L2 normalize //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_bi_refl: ∀R. bi_reflexive ? ? R → reflexive … (lpx_bi R).
+#R #HR #L elim L -L // /2 width=1/
+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/reducibility/lfpr_fpr.ma".
+include "basic_2/computation/fprs_fprs.ma".
+include "basic_2/computation/lfprs.ma".
+
+(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
+
+(* Inversion lemmas on context-free parallel reduction for closures *********)
+
+lemma lfprs_inv_fprs: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀T. ⦃L1, T⦄ ➡* ⦃L2, T⦄.
+#L1 #L2 #H @(lfprs_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL1 #T
+lapply (lfpr_inv_fpr … HL2 T) -HL2 /3 width=4/
+qed-.
+
+(* Properties on context-free parallel computation for closures *************)
+
+lemma fprs_lfprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1⦄ ➡* ⦃L2⦄.
+#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 // /3 width=5/
+qed.
+
+lemma lfprs_fprs_trans: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+#L1 #L #L2 #T1 #T2 #HL1 #HL2
+lapply (lfprs_inv_fprs … HL1 T1) -HL1 /2 width=4/
+qed.
+(*
+lamma lfprs_cprs_conf: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L2⦄ → L1 ⊢ T1 ➡* T2 → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+*)
--- /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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'HdNormal $L $T }.
+
+include "basic_2/reduction/cpr_tshf.ma".
+
+(* CONTEXT-SENSITIVE WEAK HEAD NORMAL TERMS *********************************)
+
+definition chnf: lenv → predicate term ≝ λL. NF … (cpr L) tshf.
+
+interpretation
+ "context-sensitive head normality (term)"
+ 'HdNormal L T = (chnf L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma chnf_inv_tshf: ∀L,T. L ⊢ 𝐇𝐍⦃T⦄ → T ≈ T.
+normalize /2 width=1/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma tshf_thnf: ∀T. T ≈ T → ⋆ ⊢ 𝐇𝐍⦃T⦄.
+#T #HT #T2 #H elim (cpr_fwd_tshf1 … H) -H //
+#H elim H //
+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/tshf.ma".
+include "basic_2/reduction/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
+
+(* Forward lemmas on same head forms for terms ******************************)
+
+lemma cpr_fwd_tshf1: ∀L,T1,T2. L ⊢ T1 ➡ T2 → T1 ≈ T1 →
+ T2 ≈ T1 ∨ (L = ⋆ → ⊥).
+#L #T1 #T2 #H elim H -L -T1 -T2
+[ /2 width=1/
+| #L #K #V1 #V2 #W2 #i #HLK #_ #_ #_ #_
+ @or_intror #H destruct
+ lapply (ldrop_inv_atom1 … HLK) -HLK #H destruct
+| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #_ #_ #H
+ elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct /2 width=1/
+| #I #L #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H
+ elim (tshf_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct
+ lapply (IHT12 HT1U2) -IHT12 -HT1U2 * #HUT2 /3 width=1/
+ lapply (simple_tshf_repl_sn … HUT2 HT1) /3 width=1/
+| #L #V #T #T1 #T2 #_ #_ #_ #H
+ elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct
+| #L #V #T1 #T2 #_ #_ #H
+ elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct
+| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+ elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #H
+ elim (simple_inv_bind … H)
+| #a #L #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
+ elim (tshf_inv_flat1 … H) -H #U1 #U2 #_ #H
+ elim (simple_inv_bind … H)
+]
+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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( L ⊢ break term 46 T1 ≈ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'Hom $L $T1 $T2 }.
+
+notation "hvbox( L ⊢ break 𝐇𝐑 ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'HdReducible $L $T }.
+
+notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'NotHdReducible $L $T }.
+
+include "basic_2/grammar/term_simple.ma".
+
+(* SAME HEAD TERM FORMS *****************************************************)
+
+inductive tshf: relation term ≝
+ | tshf_atom: ∀I. tshf (⓪{I}) (⓪{I})
+ | tshf_abbr: ∀V1,V2,T1,T2. tshf (-ⓓV1. T1) (-ⓓV2. T2)
+ | tshf_abst: ∀a,V1,V2,T1,T2. tshf (ⓛ{a}V1. T1) (ⓛ{a}V2. T2)
+ | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄ →
+ tshf (ⓐV1. T1) (ⓐV2. T2)
+.
+
+interpretation "same head form (term)" 'napart T1 T2 = (tshf T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma tshf_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1.
+#T1 #T2 #H elim H -T1 -T2 /2 width=1/
+qed.
+
+lemma tshf_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2.
+#T1 #T2 #H elim H -T1 -T2 // /2 width=1/
+qed.
+
+lemma tshf_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1.
+/3 width=2/ qed.
+
+lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
+#T1 #T2 #H elim H -T1 -T2 //
+[ #V1 #V2 #T1 #T2 #H
+ elim (simple_inv_bind … H)
+| #a #V1 #V2 #T1 #T2 #H
+ elim (simple_inv_bind … H)
+]
+qed. (**) (* remove from index *)
+
+lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
+/3 width=3/ qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact tshf_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀a,I,W1,U1. T1 = ⓑ{a,I}W1.U1 →
+ ∃∃W2,U2. T2 = ⓑ{a,I}W2. U2 &
+ (Bind2 a I = Bind2 false Abbr ∨ I = Abst).
+#T1 #T2 * -T1 -T2
+[ #J #a #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #a #I #W1 #U1 #H destruct /3 width=3/
+| #b #V1 #V2 #T1 #T2 #a #I #W1 #U1 #H destruct /3 width=3/
+| #V1 #V2 #T1 #T2 #_ #_ #_ #a #I #W1 #U1 #H destruct
+]
+qed.
+
+lemma tshf_inv_bind1: ∀a,I,W1,U1,T2. ⓑ{a,I}W1.U1 ≈ T2 →
+ ∃∃W2,U2. T2 = ⓑ{a,I}W2. U2 &
+ (Bind2 a I = Bind2 false Abbr ∨ I = Abst).
+/2 width=5/ qed-.
+
+fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
+ ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ &
+ I = Appl & T2 = ⓐW2. U2.
+#T1 #T2 * -T1 -T2
+[ #J #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
+| #a #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/
+]
+qed.
+
+lemma tshf_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
+ ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ &
+ I = Appl & T2 = ⓐW2. U2.
+/2 width=4/ 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_append.ma".
-
-(* POINTWISE EXTENSION OF A CONTEXT-FREE REALTION FOR TERMS *****************)
-
-inductive lpx (R:relation term): relation lenv ≝
-| lpx_stom: lpx R (⋆) (⋆)
-| lpx_pair: ∀I,K1,K2,V1,V2.
- lpx R K1 K2 → R V1 V2 → lpx R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lpx_inv_atom1_aux: ∀R,L1,L2. lpx R L1 L2 → L1 = ⋆ → L2 = ⋆.
-#R #L1 #L2 * -L1 -L2
-[ //
-| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
-]
-qed-.
-
-lemma lpx_inv_atom1: ∀R,L2. lpx R (⋆) L2 → L2 = ⋆.
-/2 width=4 by lpx_inv_atom1_aux/ qed-.
-
-fact lpx_inv_pair1_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
- ∃∃K2,V2. lpx R K1 K2 & R 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/
-]
-qed-.
-
-lemma lpx_inv_pair1: ∀R,I,K1,V1,L2. lpx R (K1. ⓑ{I} V1) L2 →
- ∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2.
-/2 width=3 by lpx_inv_pair1_aux/ qed-.
-
-fact lpx_inv_atom2_aux: ∀R,L1,L2. lpx R L1 L2 → L2 = ⋆ → L1 = ⋆.
-#R #L1 #L2 * -L1 -L2
-[ //
-| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
-]
-qed-.
-
-lemma lpx_inv_atom2: ∀R,L1. lpx R L1 (⋆) → L1 = ⋆.
-/2 width=4 by lpx_inv_atom2_aux/ qed-.
-
-fact lpx_inv_pair2_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
- ∃∃K1,V1. lpx R K1 K2 & R 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/
-]
-qed-.
-
-lemma lpx_inv_pair2: ∀R,I,L1,K2,V2. lpx R L1 (K2. ⓑ{I} V2) →
- ∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1.
-/2 width=3 by lpx_inv_pair2_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lpx_fwd_length: ∀R,L1,L2. lpx R L1 L2 → |L1| = |L2|.
-#R #L1 #L2 #H elim H -L1 -L2 normalize //
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma lpx_inv_append1: ∀R,L1,K1,L. lpx R (K1 @@ L1) L →
- ∃∃K2,L2. lpx R K1 K2 & lpx R L1 L2 & L = K2 @@ L2.
-#R #L1 elim L1 -L1 normalize
-[ #K1 #K2 #HK12
- @(ex3_2_intro … K2 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *)
-| #L1 #I #V1 #IH #K1 #X #H
- elim (lpx_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct
- elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #HL12 #H destruct
- @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *)
-]
-qed-.
-
-lemma lpx_inv_append2: ∀R,L2,K2,L. lpx R L (K2 @@ L2) →
- ∃∃K1,L1. lpx R K1 K2 & lpx R L1 L2 & L = K1 @@ L1.
-#R #L2 elim L2 -L2 normalize
-[ #K2 #K1 #HK12
- @(ex3_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *)
-| #L2 #I #V2 #IH #K2 #X #H
- elim (lpx_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct
- elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #HL12 #H destruct
- @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *)
-]
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R).
-#R #HR #L elim L -L // /2 width=1/
-qed.
-
-lemma lpx_sym: ∀R. symmetric ? R → symmetric … (lpx R).
-#R #HR #L1 #L2 #H elim H -H // /3 width=1/
-qed.
-
-lemma lpx_trans: ∀R. Transitive ? R → Transitive … (lpx R).
-#R #HR #L1 #L #H elim H -L //
-#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
-elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/
-qed.
-
-lemma lpx_conf: ∀R. confluent ? R → confluent … (lpx R).
-#R #HR #L0 #L1 #H elim H -L1
-[ #X #H >(lpx_inv_atom1 … H) -X /2 width=3/
-| #I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #X #H
- elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK02 #HV02 #H destruct
- elim (IHK01 … HK02) -K0 #K #HK1 #HK2
- elim (HR … HV01 … HV02) -HR -V0 /3 width=5/
-]
-qed.
-
-lemma lpx_TC_inj: ∀R,L1,L2. lpx R L1 L2 → lpx (TC … R) L1 L2.
-#R #L1 #L2 #H elim H -L1 -L2 // /3 width=1/
-qed.
-
-lemma lpx_TC_step: ∀R,L1,L. lpx (TC … R) L1 L →
- ∀L2. lpx R L L2 → lpx (TC … R) L1 L2.
-#R #L1 #L #H elim H -L /2 width=1/
-#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
-elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/
-qed.
-
-lemma TC_lpx_pair_dx: ∀R. reflexive ? R →
- ∀I,K,V1,V2. TC … R V1 V2 →
- TC … (lpx R) (K.ⓑ{I}V1) (K.ⓑ{I}V2).
-#R #HR #I #K #V1 #V2 #H elim H -V2
-/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *)
-qed.
-
-lemma TC_lpx_pair_sn: ∀R. reflexive ? R →
- ∀I,V,K1,K2. TC … (lpx R) K1 K2 →
- TC … (lpx R) (K1.ⓑ{I}V) (K2.ⓑ{I}V).
-#R #HR #I #V #K1 #K2 #H elim H -K2
-/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *)
-qed.
-
-lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2.
-#R #L1 #L2 #H elim H -L2 /2 width=1/ /2 width=3/
-qed.
-
-lemma lpx_inv_TC: ∀R. reflexive ? R →
- ∀L1,L2. lpx (TC … R) L1 L2 → TC … (lpx R) L1 L2.
-#R #HR #L1 #L2 #H elim H -L1 -L2 /3 width=1/ /3 width=3/
-qed.
-
-lemma lpx_append: ∀R,K1,K2. lpx R K1 K2 → ∀L1,L2. lpx R L1 L2 →
- lpx R (L1 @@ K1) (L2 @@ K2).
-#R #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
-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".
-
-(* POINTWISE EXTENSION OF A FOCALIZED REALTION FOR TERMS ********************)
-
-inductive lpx_bi (R:bi_relation lenv term): relation lenv ≝
-| lpx_bi_stom: lpx_bi R (⋆) (⋆)
-| lpx_bi_pair: ∀I,K1,K2,V1,V2.
- lpx_bi R K1 K2 → R K1 V1 K2 V2 →
- lpx_bi R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lpx_bi_inv_atom1_aux: ∀R,L1,L2. lpx_bi R L1 L2 → L1 = ⋆ → L2 = ⋆.
-#R #L1 #L2 * -L1 -L2
-[ //
-| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
-]
-qed-.
-
-lemma lpx_bi_inv_atom1: ∀R,L2. lpx_bi R (⋆) L2 → L2 = ⋆.
-/2 width=4 by lpx_bi_inv_atom1_aux/ qed-.
-
-fact lpx_bi_inv_pair1_aux: ∀R,L1,L2. lpx_bi R L1 L2 →
- ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
- ∃∃K2,V2. lpx_bi R K1 K2 &
- R K1 V1 K2 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/
-]
-qed-.
-
-lemma lpx_bi_inv_pair1: ∀R,I,K1,V1,L2. lpx_bi R (K1. ⓑ{I} V1) L2 →
- ∃∃K2,V2. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
- L2 = K2. ⓑ{I} V2.
-/2 width=3 by lpx_bi_inv_pair1_aux/ qed-.
-
-fact lpx_bi_inv_atom2_aux: ∀R,L1,L2. lpx_bi R L1 L2 → L2 = ⋆ → L1 = ⋆.
-#R #L1 #L2 * -L1 -L2
-[ //
-| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
-]
-qed-.
-
-lemma lpx_bi_inv_atom2: ∀R,L1. lpx_bi R L1 (⋆) → L1 = ⋆.
-/2 width=4 by lpx_bi_inv_atom2_aux/ qed-.
-
-fact lpx_bi_inv_pair2_aux: ∀R,L1,L2. lpx_bi R L1 L2 →
- ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
- ∃∃K1,V1. lpx_bi R K1 K2 & R K1 V1 K2 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/
-]
-qed-.
-
-lemma lpx_bi_inv_pair2: ∀R,I,L1,K2,V2. lpx_bi R L1 (K2. ⓑ{I} V2) →
- ∃∃K1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
- L1 = K1. ⓑ{I} V1.
-/2 width=3 by lpx_bi_inv_pair2_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lpx_bi_fwd_length: ∀R,L1,L2. lpx_bi R L1 L2 → |L1| = |L2|.
-#R #L1 #L2 #H elim H -L1 -L2 normalize //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lpx_bi_refl: ∀R. bi_reflexive ? ? R → reflexive … (lpx_bi R).
-#R #HR #L elim L -L // /2 width=1/
-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_append.ma".
-
-(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
-
-inductive lpx_sn (R:lenv→relation term): relation lenv ≝
-| lpx_sn_stom: 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)
-.
-
-definition lpx_sn_confluent: relation (lenv→relation term) ≝ λR1,R2.
- ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
- ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 →
- ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
-
-definition lpx_sn_transitive: relation (lenv→relation term) ≝ λR1,R2.
- ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 →
- ∀T2. R2 L2 T T2 → R1 L1 T1 T2.
-
-(* 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/
-]
-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/
-]
-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-.
-
-(* 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 normalize //
-qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma lpx_sn_fwd_append1: ∀R,L1,K1,L. lpx_sn R (K1 @@ L1) L →
- ∃∃K2,L2. lpx_sn R K1 K2 & L = K2 @@ L2.
-#R #L1 elim L1 -L1
-[ #K1 #K2 #HK12
- @(ex2_2_intro … K2 (⋆)) // (* explicit constructor, /2 width=4/ does not work *)
-| #L1 #I #V1 #IH #K1 #X #H
- elim (lpx_sn_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct
- elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #H destruct
- @(ex2_2_intro … (L2.ⓑ{I}V2) HK12) // (* explicit constructor, /2 width=4/ does not work *)
-]
-qed-.
-
-lemma lpx_sn_fwd_append2: ∀R,L2,K2,L. lpx_sn R L (K2 @@ L2) →
- ∃∃K1,L1. lpx_sn R K1 K2 & L = K1 @@ L1.
-#R #L2 elim L2 -L2
-[ #K2 #K1 #HK12
- @(ex2_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=4/ does not work *)
-| #L2 #I #V2 #IH #K2 #X #H
- elim (lpx_sn_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct
- elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #H destruct
- @(ex2_2_intro … (L1.ⓑ{I}V1) HK12) // (* explicit constructor, /2 width=4/ does not work *)
-]
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R).
-#R #HR #L elim L -L // /2 width=1/
-qed-.
-
-lemma lpx_sn_append: ∀R. l_appendable_sn R →
- ∀K1,K2. lpx_sn R K1 K2 → ∀L1,L2. lpx_sn R L1 L2 →
- lpx_sn R (L1 @@ K1) (L2 @@ K2).
-#R #HR #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R).
-#R #HR #L1 #L #H elim H -L1 -L //
-#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H
-elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5/
-qed-.
-
-lemma lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 →
- confluent2 … (lpx_sn R1) (lpx_sn R2).
-#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH *
-[ #_ #X1 #H1 #X2 #H2 -n
- >(lpx_sn_inv_atom1 … H1) -X1
- >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/
-| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
- elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
- elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
- elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
- elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/
-]
-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_append.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+inductive lpx_sn (R:lenv→relation term): relation lenv ≝
+| lpx_sn_stom: 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 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/
+]
+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/
+]
+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-.
+
+(* 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 normalize //
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lpx_sn_fwd_append1: ∀R,L1,K1,L. lpx_sn R (K1 @@ L1) L →
+ ∃∃K2,L2. lpx_sn R K1 K2 & L = K2 @@ L2.
+#R #L1 elim L1 -L1
+[ #K1 #K2 #HK12
+ @(ex2_2_intro … K2 (⋆)) // (* explicit constructor, /2 width=4/ does not work *)
+| #L1 #I #V1 #IH #K1 #X #H
+ elim (lpx_sn_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct
+ elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #H destruct
+ @(ex2_2_intro … (L2.ⓑ{I}V2) HK12) // (* explicit constructor, /2 width=4/ does not work *)
+]
+qed-.
+
+lemma lpx_sn_fwd_append2: ∀R,L2,K2,L. lpx_sn R L (K2 @@ L2) →
+ ∃∃K1,L1. lpx_sn R K1 K2 & L = K1 @@ L1.
+#R #L2 elim L2 -L2
+[ #K2 #K1 #HK12
+ @(ex2_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=4/ does not work *)
+| #L2 #I #V2 #IH #K2 #X #H
+ elim (lpx_sn_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct
+ elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #H destruct
+ @(ex2_2_intro … (L1.ⓑ{I}V1) HK12) // (* explicit constructor, /2 width=4/ does not work *)
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R).
+#R #HR #L elim L -L // /2 width=1/
+qed-.
+
+lemma lpx_sn_append: ∀R. l_appendable_sn R →
+ ∀K1,K2. lpx_sn R K1 K2 → ∀L1,L2. lpx_sn R L1 L2 →
+ lpx_sn R (L1 @@ K1) (L2 @@ K2).
+#R #HR #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
+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/lpx_sn.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+definition lpx_sn_confluent: relation (lenv→relation term) ≝ λR1,R2.
+ ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+ ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 →
+ ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+
+definition lpx_sn_transitive: relation (lenv→relation term) ≝ λR1,R2.
+ ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 →
+ ∀T2. R2 L2 T T2 → R1 L1 T1 T2.
+
+(* Main properties **********************************************************)
+
+theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R).
+#R #HR #L1 #L #H elim H -L1 -L //
+#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H
+elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5/
+qed-.
+
+theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 →
+ confluent2 … (lpx_sn R1) (lpx_sn R2).
+#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH *
+[ #_ #X1 #H1 #X2 #H2 -n
+ >(lpx_sn_inv_atom1 … H1) -X1
+ >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/
+| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
+ elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
+ elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
+ elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
+ elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/
+]
+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/lpx_sn.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+(* Properties on transitive_closure *****************************************)
+
+lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) →
+ ∀L1,L2. TC … (lpx_sn R) L1 L2 →
+ ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V).
+#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2
+[ /2 width=1 by lpx_sn_refl/
+| /3 width=1 by TC_reflexive, lpx_sn_refl/
+| /3 width=5/
+]
+qed-.
+
+lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) →
+ ∀I,L1,L2. TC … (lpx_sn R) L1 L2 →
+ ∀V1,V2. LTC … R L1 V1 V2 →
+ TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2).
+#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 //
+[ /2 width=1 by TC_lpx_sn_pair_refl/
+| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/
+]
+qed-.
+
+lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) →
+ ∀L1,L2. lpx_sn (LTC … R) L1 L2 →
+ TC … (lpx_sn R) L1 L2.
+#R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1/
+/2 width=1 by TC_lpx_sn_pair/
+qed-.
+
+(* Inversion lemmas on transitive closure ***********************************)
+
+lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆.
+#R #L1 #H @(TC_ind_dx … L1 H) -L1
+[ #L1 #H lapply (lpx_sn_inv_atom2 … H) -H //
+| #L1 #L #HL1 #_ #IHL2 destruct
+ lapply (lpx_sn_inv_atom2 … HL1) -HL1 //
+]
+qed-.
+
+lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_trans … 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
+[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5/
+| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
+ elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct
+ lapply (HR … HV2 … HK1) -HR -HV2 #HV2 /3 width=5/
+]
+qed-.
+
+lemma TC_lpx_sn_ind: ∀R. s_rs_trans … R (lpx_sn R) →
+ ∀S:relation lenv.
+ S (⋆) (⋆) → (
+ ∀I,K1,K2,V1,V2.
+ TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 →
+ S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ ) →
+ ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2.
+#R #HR #S #IH1 #IH2 #L2 elim L2 -L2
+[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X //
+| #L2 #I #V2 #IHL2 #X #H
+ elim (TC_lpx_sn_inv_pair2 … H) // -H -HR
+ #L1 #V1 #HL12 #HV12 #H destruct /3 width=1/
+]
+qed-.
+
+lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆.
+#R #L2 #H elim H -L2
+[ #L2 #H lapply (lpx_sn_inv_atom1 … H) -H //
+| #L #L2 #_ #HL2 #IHL1 destruct
+ lapply (lpx_sn_inv_atom1 … HL2) -HL2 //
+]
+qed-.
+
+fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_trans … 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.
+#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2
+[ #J #K #W #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_trans … 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_trans … R (lpx_sn R) →
+ ∀L1,L2. TC … (lpx_sn R) L1 L2 →
+ lpx_sn (LTC … R) L1 L2.
+#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 /2 width=1/
+qed-.
+
+(* Forward lemmas on transitive closure *************************************)
+
+lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H -L2
+[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 //
+| #L #L2 #_ #HL2 #IHL1
+ >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 //
+]
+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/term_simple.ma".
-
-(* SAME HEAD TERM FORMS *****************************************************)
-
-inductive tshf: relation term ≝
- | tshf_atom: ∀I. tshf (⓪{I}) (⓪{I})
- | tshf_abbr: ∀V1,V2,T1,T2. tshf (-ⓓV1. T1) (-ⓓV2. T2)
- | tshf_abst: ∀a,V1,V2,T1,T2. tshf (ⓛ{a}V1. T1) (ⓛ{a}V2. T2)
- | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄ →
- tshf (ⓐV1. T1) (ⓐV2. T2)
-.
-
-interpretation "same head form (term)" 'napart T1 T2 = (tshf T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma tshf_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1.
-#T1 #T2 #H elim H -T1 -T2 /2 width=1/
-qed.
-
-lemma tshf_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2.
-#T1 #T2 #H elim H -T1 -T2 // /2 width=1/
-qed.
-
-lemma tshf_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1.
-/3 width=2/ qed.
-
-lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
-#T1 #T2 #H elim H -T1 -T2 //
-[ #V1 #V2 #T1 #T2 #H
- elim (simple_inv_bind … H)
-| #a #V1 #V2 #T1 #T2 #H
- elim (simple_inv_bind … H)
-]
-qed. (**) (* remove from index *)
-
-lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
-/3 width=3/ qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact tshf_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀a,I,W1,U1. T1 = ⓑ{a,I}W1.U1 →
- ∃∃W2,U2. T2 = ⓑ{a,I}W2. U2 &
- (Bind2 a I = Bind2 false Abbr ∨ I = Abst).
-#T1 #T2 * -T1 -T2
-[ #J #a #I #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #a #I #W1 #U1 #H destruct /3 width=3/
-| #b #V1 #V2 #T1 #T2 #a #I #W1 #U1 #H destruct /3 width=3/
-| #V1 #V2 #T1 #T2 #_ #_ #_ #a #I #W1 #U1 #H destruct
-]
-qed.
-
-lemma tshf_inv_bind1: ∀a,I,W1,U1,T2. ⓑ{a,I}W1.U1 ≈ T2 →
- ∃∃W2,U2. T2 = ⓑ{a,I}W2. U2 &
- (Bind2 a I = Bind2 false Abbr ∨ I = Abst).
-/2 width=5/ qed-.
-
-fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
- ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ &
- I = Appl & T2 = ⓐW2. U2.
-#T1 #T2 * -T1 -T2
-[ #J #I #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
-| #a #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/
-]
-qed.
-
-lemma tshf_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
- ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ &
- I = Appl & T2 = ⓐW2. U2.
-/2 width=4/ qed-.
left associative with precedence 49
for @{ 'DxAbst $T1 $T2 }.
-notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 T2 , break term 46 T3 } )"
- non associative with precedence 50
- for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
-
notation "hvbox( ♯ { term 46 x } )"
non associative with precedence 90
for @{ 'Weight $x }.
non associative with precedence 45
for @{ 'Simple $T }.
-notation "hvbox( L ⊢ break term 46 T1 ≈ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'Hom $L $T1 $T2 }.
-
notation "hvbox( T1 ≃ break term 46 T2 )"
non associative with precedence 45
for @{ 'Iso $T1 $T2 }.
non associative with precedence 45
for @{ 'RLift $d $e $T1 $T2 }.
-notation "hvbox( L1 break ⊑ [ term 46 d , break term 46 e ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'SubEq $L1 $d $e $L2 }.
-
-notation "hvbox( ⊒ [ term 46 d , break term 46 e ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'SubEqBottom $d $e $L2 }.
-
notation "hvbox( ⇩ [ term 46 e ] break term 46 L1 ≡ break term 46 L2 )"
non associative with precedence 45
for @{ 'RDrop $e $L1 $L2 }.
non associative with precedence 45
for @{ 'SupTermStar $L1 $T1 $L2 $T2 }.
+notation "hvbox( L1 ⊑ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'SubEq $L1 $L2 }.
+
notation "hvbox( L ⊢ break term 46 T1 ▶* break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubstStar $L $T1 $T2 }.
non associative with precedence 45
for @{ 'Normal $L $T }.
-(* this might be removed *)
-notation "hvbox( 𝐇𝐑 ⦃ term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'HdReducible $T }.
-
-(* this might be removed *)
-notation "hvbox( L ⊢ break 𝐇𝐑 ⦃ term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'HdReducible $L $T }.
-
-(* this might be removed *)
-notation "hvbox( 𝐇𝐈 ⦃ term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'NotHdReducible $T }.
-
-(* this might be removed *)
-notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'NotHdReducible $L $T }.
-
-(* this might be removed *)
-notation "hvbox( 𝐇𝐍 ⦃ term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'HdNormal $T }.
-
-(* this might be removed *)
-notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'HdNormal $L $T }.
-
notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )"
non associative with precedence 45
for @{ 'PRed $L $T1 $T2 }.
non associative with precedence 45
for @{ 'PRedSnStar $L1 $L2 }.
+notation "hvbox( L1 ⊢ ➡➡* break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedSnStarAlt $L1 $L2 }.
+
notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'PEval $L $T1 $T2 }.
+++ /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/reduction/cpr_tshf.ma".
-
-(* CONTEXT-SENSITIVE WEAK HEAD NORMAL TERMS *********************************)
-
-definition chnf: lenv → predicate term ≝ λL. NF … (cpr L) tshf.
-
-interpretation
- "context-sensitive head normality (term)"
- 'HdNormal L T = (chnf L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma chnf_inv_tshf: ∀L,T. L ⊢ 𝐇𝐍⦃T⦄ → T ≈ T.
-normalize /2 width=1/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma tshf_thnf: ∀T. T ≈ T → ⋆ ⊢ 𝐇𝐍⦃T⦄.
-#T #HT #T2 #H elim (cpr_fwd_tshf1 … H) -H //
-#H elim H //
-qed.
(* Basic properties *********************************************************)
-(* Note: it does not hold replacing |L1| with |L2| *)
-lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
- ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
+lemma cpr_lsubr_trans: lsubr_trans … cpr.
#L1 #T1 #T2 #H elim H -L1 -T1 -T2
[ //
| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi
- lapply (ldrop_fwd_O1_length … HLK1) #H2i
- elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi
- <H2i -H2i <minus_plus_m_m /3 width=6/
+ elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -HL12 -HLK1 /3 width=6/
|3,7: /4 width=1/
|4,6: /3 width=1/
|5,8: /4 width=3/
+++ /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/tshf.ma".
-include "basic_2/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
-
-(* Forward lemmas on same head forms for terms ******************************)
-
-lemma cpr_fwd_tshf1: ∀L,T1,T2. L ⊢ T1 ➡ T2 → T1 ≈ T1 →
- T2 ≈ T1 ∨ (L = ⋆ → ⊥).
-#L #T1 #T2 #H elim H -L -T1 -T2
-[ /2 width=1/
-| #L #K #V1 #V2 #W2 #i #HLK #_ #_ #_ #_
- @or_intror #H destruct
- lapply (ldrop_inv_atom1 … HLK) -HLK #H destruct
-| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #_ #_ #H
- elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct /2 width=1/
-| #I #L #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H
- elim (tshf_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct
- lapply (IHT12 HT1U2) -IHT12 -HT1U2 * #HUT2 /3 width=1/
- lapply (simple_tshf_repl_sn … HUT2 HT1) /3 width=1/
-| #L #V #T #T1 #T2 #_ #_ #_ #H
- elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct
-| #L #V #T1 #T2 #_ #_ #H
- elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct
-| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
- elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #H
- elim (simple_inv_bind … H)
-| #a #L #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
- elim (tshf_inv_flat1 … H) -H #U1 #U2 #_ #H
- elim (simple_inv_bind … H)
-]
-qed-.
lemma lpr_refl: ∀L. L ⊢ ➡ L.
/2 width=1 by lpx_sn_refl/ qed.
+lemma lpr_pair: ∀I,K1,K2,V1,V2. K1 ⊢ ➡ K2 → K1 ⊢ V1 ➡ V2 →
+ K1.ⓑ{I}V1 ⊢ ➡ K2.ⓑ{I}V2.
+/2 width=1/ qed.
+
lemma lpr_append: ∀K1,K2. K1 ⊢ ➡ K2 → ∀L1,L2. L1 ⊢ ➡ L2 →
L1 @@ K1 ⊢ ➡ L2 @@ K2.
/3 width=1 by lpx_sn_append, cpr_append/ qed.
(* *)
(**************************************************************************)
+include "basic_2/grammar/lpx_sn_lpx_sn.ma".
include "basic_2/relocation/fsup.ma".
include "basic_2/reduction/lpr_ldrop.ma".
(* *)
(**************************************************************************)
+include "basic_2/grammar/lpx_sn_lpx_sn.ma".
include "basic_2/substitution/lpss_ldrop.ma".
include "basic_2/reduction/lpr_ldrop.ma".
include "basic_2/grammar/cl_weight.ma".
include "basic_2/relocation/lift.ma".
-include "basic_2/relocation/lsubr.ma".
(* LOCAL ENVIRONMENT SLICING ************************************************)
interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2).
-definition l_liftable: (lenv → relation term) → Prop ≝
+definition l_liftable: predicate (lenv → relation term) ≝
λR. ∀K,T1,T2. R K T1 T2 → ∀L,d,e. ⇩[d, e] L ≡ K →
∀U1. ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → R L U1 U2.
-definition l_deliftable_sn: (lenv → relation term) → Prop ≝
+definition l_deliftable_sn: predicate (lenv → relation term) ≝
λR. ∀L,U1,U2. R L U1 U2 → ∀K,d,e. ⇩[d, e] L ≡ K →
∀T1. ⇧[d, e] T1 ≡ U1 →
∃∃T2. ⇧[d, e] T2 ≡ U2 & R K T1 T2.
-definition dropable_sn: relation lenv → Prop ≝
+definition dropable_sn: predicate (relation lenv) ≝
λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. R L1 L2 →
∃∃K2. R K1 K2 & ⇩[d, e] L2 ≡ K2.
-definition dedropable_sn: relation lenv → Prop ≝
+definition dedropable_sn: predicate (relation lenv) ≝
λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. R K1 K2 →
∃∃L2. R L1 L2 & ⇩[d, e] L2 ≡ K2.
-definition dropable_dx: relation lenv → Prop ≝
+definition dropable_dx: predicate (relation lenv) ≝
λR. ∀L1,L2. R L1 L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
∃∃K1. ⇩[0, e] L1 ≡ K1 & R K1 K2.
]
qed.
-lemma ldrop_lsubr_ldrop2_abbr: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
- ∀K2,V,i. ⇩[0, i] L2 ≡ K2. ⓓV →
- d ≤ i → i < d + e →
- ∃∃K1. K1 ⊑ [0, d + e - i - 1] K2 &
- ⇩[0, i] L1 ≡ K1. ⓓV.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #d #e #K1 #V #i #H
- lapply (ldrop_inv_atom1 … H) -H #H destruct
-| #L1 #L2 #K1 #V #i #_ #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #V #e #HL12 #IHL12 #K1 #W #i #H #_ #Hie
- elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
- [ -IHL12 -Hie destruct
- <minus_n_O <minus_plus_m_m // /2 width=3/
- | -HL12
- elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /4 width=3/
- ]
-| #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie
- elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
- [ -IHL12 -Hie -Hi destruct
- | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /3 width=3/
- ]
-| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
- elim (le_inv_plus_l … Hdi) #Hdim #Hi
- lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1
- elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hdi -Hide >minus_minus_comm >arith_b1 // /3 width=3/
+lemma l_liftable_LTC: ∀R. l_liftable R → l_liftable (LTC … R).
+#R #HR #K #T1 #T2 #H elim H -T2
+[ /3 width=9/
+| #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2
+ elim (lift_total T d e) /4 width=11 by step/ (**) (* auto too slow without trace *)
+]
+qed.
+
+lemma l_deliftable_sn_LTC: ∀R. l_deliftable_sn R → l_deliftable_sn (LTC … R).
+#R #HR #L #U1 #U2 #H elim H -U2
+[ #U2 #HU12 #K #d #e #HLK #T1 #HTU1
+ elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3/
+| #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+ elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
+ elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5/
]
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/relocation/lsubr_lbotr.ma".
-include "basic_2/relocation/ldrop_ldrop.ma".
-
-(* DROPPING *****************************************************************)
-
-(* Inversion lemmas about local env. full refinement for substitution *******)
-
-(* Note: ldrop_ldrop not needed *)
-lemma lbotr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ⊒[d, e] L →
- d ≤ i → i < d + e → I = Abbr.
-#I #L elim L -L
-[ #K #V #i #H
- lapply (ldrop_inv_atom1 … H) -H #H destruct
-| #L #J #W #IHL #K #V #i #H
- elim (ldrop_inv_O1 … H) -H *
- [ -IHL #H1 #H2 #d #e #HL #Hdi #Hide destruct
- lapply (le_n_O_to_eq … Hdi) -Hdi #H destruct
- lapply (HL … (L.ⓓW) ?) -HL /2 width=1/ #H
- elim (lsubr_inv_abbr2 … H ?) -H // -Hide #K #_ #H destruct //
- | #Hi #HLK #d @(nat_ind_plus … d) -d
- [ #e #H #_ #Hide
- elim (lbotr_inv_bind … H ?) -H [2: /2 width=2/ ] #HL #H destruct
- @(IHL … HLK … HL) -IHL -HLK -HL // /2 width=1/
- | #d #_ #e #H #Hdi #Hide
- lapply (lbotr_inv_skip … H ?) -H // #HL
- @(IHL … HLK … HL) -IHL -HLK -HL /2 width=1/
- ]
- ]
-]
-qed-.
-
-(* Properties about local env. full refinement for substitution *************)
-
-(* Note: ldrop_ldrop not needed *)
-lemma lbotr_ldrop: ∀L,d,e.
- (∀I,K,V,i. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓑ{I}V → I = Abbr) →
- ⊒[d, e] L.
-#L elim L -L //
-#L #I #V #IHL #d @(nat_ind_plus … d) -d
-[ #e @(nat_ind_plus … e) -e //
- #e #_ #H0
- >(H0 I L V 0 ? ? ?) //
- /5 width=6 by lbotr_abbr, ldrop_ldrop, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *)
-| #d #_ #e #H0
- /5 width=6 by lbotr_skip, ldrop_ldrop, le_S_S, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *)
-]
-qed.
-
-lemma lbotr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ⊒[dd, ee] L1 →
- dd + ee ≤ d → ⊒[dd, ee] L2.
-#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
-@lbotr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
-lapply (lt_to_le_to_lt … Hiddee Hddee) -Hddee #Hid
-elim (ldrop_trans_le … HL12 … HLK2 ?) -L2 /2 width=2/ #X #HLK1 #H
-elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K1 #V1 #HK12 #HV21 #H destruct
-@(lbotr_inv_ldrop … HLK1 … HL1) -L1 -K1 -V1 //
-qed.
-
-lemma lbotr_ldrop_trans_be_up: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
- ∀dd,ee. ⊒[dd, ee] L1 →
- dd ≤ d + e → d + e ≤ dd + ee →
- ⊒[d, dd + ee - d - e] L2.
-#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hdde #Hddee
-@lbotr_ldrop #I #K2 #V2 #i #Hdi #Hiddee #HLK2
-lapply (transitive_le ? ? (i+e)… Hdde ?) -Hdde /2 width=1/ #Hddie
->commutative_plus in Hiddee; >minus_minus_comm <plus_minus_m_m /2 width=1/ -Hddee #Hiddee
-lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hdi #HL1K2
-@(lbotr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus // -Hddie /2 width=1/
-qed.
-
-lemma lbotr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ⊒[dd, ee] L1 →
- d + e ≤ dd → ⊒[dd - e, ee] L2.
-#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
-@lbotr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
-elim (le_inv_plus_l … Hddee) -Hddee #Hdde #Hedd
->plus_minus in Hiddee; // #Hiddee
-lapply (transitive_le … Hdde Hddi) -Hdde #Hid
-lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hid #HL1K2
-@(lbotr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus /2 width=1/
-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_px.ma".
-include "basic_2/relocation/ldrop.ma".
-
-(* DROPPING *****************************************************************)
-
-(* Properties on pointwise extension ****************************************)
-
-lemma lpx_deliftable_dropable: ∀R. t_deliftable_sn R → dropable_sn (lpx R).
-#R #HR #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
-[ #d #e #X #H >(lpx_inv_atom1 … H) -H /2 width=3/
-| #K1 #I #V1 #X #H
- elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
- elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
- elim (IHLK1 … HL12) -L1 /3 width=3/
-| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
- elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
- elim (HR … HV12 … HWV1) -V1
- elim (IHLK1 … HL12) -L1 /3 width=5/
-]
-qed.
-
-lemma lpx_liftable_dedropable: ∀R. reflexive ? R →
- t_liftable R → dedropable_sn (lpx R).
-#R #H1R #H2R #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
-[ #d #e #X #H >(lpx_inv_atom1 … H) -H /2 width=3/
-| #K1 #I #V1 #X #H
- elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
- elim (IHLK1 … HK12) -K1 /3 width=5/
-| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
- elim (lpx_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
- elim (lift_total W2 d e) #V2 #HWV2
- lapply (H2R … HW12 … HWV1 … HWV2) -W1
- elim (IHLK1 … HK12) -K1 /3 width=5/
-]
-qed.
-
-fact lpx_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx R L1 L2 →
- d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & lpx R K1 K2.
-#R #L2 #K2 #d #e #H elim H -L2 -K2 -d -e
-[ #d #e #X #H >(lpx_inv_atom2 … H) -H /2 width=3/
-| #K2 #I #V2 #X #H
- elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/
-| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_
- elim (lpx_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct
- elim (IHLK2 … HL12 ?) -L2 // /3 width=3/
-| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
- >commutative_plus normalize #H destruct
-]
-qed-.
-
-lemma lpx_dropable: ∀R. dropable_dx (lpx R).
-/2 width=5 by lpx_dropable_aux/ qed.
(* *)
(**************************************************************************)
-include "basic_2/grammar/lenv_px_sn.ma".
+include "basic_2/grammar/lpx_sn.ma".
include "basic_2/relocation/ldrop.ma".
(* DROPPING *****************************************************************)
interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2).
-definition t_liftable: relation term → Prop ≝
- λR. ∀T1,T2. R T1 T2 → ∀U1,d,e. ⇧[d, e] T1 ≡ U1 →
- ∀U2. ⇧[d, e] T2 ≡ U2 → R U1 U2.
-
-definition t_deliftable_sn: relation term → Prop ≝
- λR. ∀U1,U2. R U1 U2 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
- ∃∃T2. ⇧[d, e] T2 ≡ U2 & R T1 T2.
-
(* Basic inversion lemmas ***************************************************)
fact lift_inv_refl_O2_aux: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
]
qed.
-lemma t_liftable_TC: ∀R. t_liftable R → t_liftable (TC … R).
-#R #HR #T1 #T2 #H elim H -T2
-[ /3 width=7/
-| #T #T2 #_ #HT2 #IHT1 #U1 #d #e #HTU1 #U2 #HTU2
- elim (lift_total T d e) /3 width=9/
-]
-qed.
-
-lemma t_deliftable_sn_TC: ∀R. t_deliftable_sn R → t_deliftable_sn (TC … R).
-#R #HR #U1 #U2 #H elim H -U2
-[ #U2 #HU12 #T1 #d #e #HTU1
- elim (HR … HU12 … HTU1) -U1 /3 width=3/
-| #U #U2 #_ #HU2 #IHU1 #T1 #d #e #HTU1
- elim (IHU1 … HTU1) -U1 #T #HTU #HT1
- elim (HR … HU2 … HTU) -U /3 width=5/
-]
-qed-.
-
(* Basic_1: removed theorems 7:
lift_head lift_gen_head
lift_weight_map lift_weight lift_weight_add lift_weight_add_O
+++ /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".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
-
-inductive lsubr: nat → nat → relation lenv ≝
-| lsubr_sort: ∀d,e. lsubr d e (⋆) (⋆)
-| lsubr_OO: ∀L1,L2. lsubr 0 0 L1 L2
-| lsubr_abbr: ∀L1,L2,V,e. lsubr 0 e L1 L2 →
- lsubr 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
-| lsubr_abst: ∀L1,L2,I,V1,V2,e. lsubr 0 e L1 L2 →
- lsubr 0 (e + 1) (L1. ⓑ{I}V1) (L2. ⓛV2)
-| lsubr_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
- lsubr d e L1 L2 → lsubr (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
-.
-
-interpretation
- "local environment refinement (substitution)"
- 'SubEq L1 d e L2 = (lsubr d e L1 L2).
-
-definition lsubr_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
- ∀L2,s1,s2. R L2 s1 s2 →
- ∀L1,d,e. L1 ⊑ [d, e] L2 → R L1 s1 s2.
-
-(* Basic properties *********************************************************)
-
-lemma lsubr_bind_eq: ∀L1,L2,e. L1 ⊑ [0, e] L2 → ∀I,V.
- L1. ⓑ{I} V ⊑ [0, e + 1] L2.ⓑ{I} V.
-#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
-qed.
-
-lemma lsubr_abbr_lt: ∀L1,L2,V,e. L1 ⊑ [0, e - 1] L2 → 0 < e →
- L1. ⓓV ⊑ [0, e] L2.ⓓV.
-#L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
-qed.
-
-lemma lsubr_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ⊑ [0, e - 1] L2 → 0 < e →
- L1. ⓑ{I}V1 ⊑ [0, e] L2. ⓛV2.
-#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
-qed.
-
-lemma lsubr_skip_lt: ∀L1,L2,d,e. L1 ⊑ [d - 1, e] L2 → 0 < d →
- ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 ⊑ [d, e] L2. ⓑ{I2} V2.
-#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
-qed.
-
-lemma lsubr_bind_lt: ∀I,L1,L2,V,e. L1 ⊑ [0, e - 1] L2 → 0 < e →
- L1. ⓓV ⊑ [0, e] L2. ⓑ{I}V.
-* /2 width=1/ qed.
-
-lemma lsubr_refl: ∀d,e,L. L ⊑ [d, e] L.
-#d elim d -d
-[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
-| #d #IHd #e #L elim L -L // /2 width=1/
-]
-qed.
-
-lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (λL. (TC … (R L))).
-#S #R #HR #L1 #s1 #s2 #H elim H -s2
-[ /3 width=5/
-| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
- lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/
-]
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubr_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → L1 = ⋆ →
- L2 = ⋆ ∨ (d = 0 ∧ e = 0).
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ /2 width=1/
-| /3 width=1/
-| #L1 #L2 #W #e #_ #H destruct
-| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
-| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
-]
-qed.
-
-lemma lsubr_inv_atom1: ∀L2,d,e. ⋆ ⊑ [d, e] L2 →
- L2 = ⋆ ∨ (d = 0 ∧ e = 0).
-/2 width=3/ qed-.
-
-fact lsubr_inv_skip1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
- ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
- ∃∃I2,K2,V2. K1 ⊑ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ #d #e #I1 #K1 #V1 #H destruct
-| #L1 #L2 #I1 #K1 #V1 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
-]
-qed.
-
-lemma lsubr_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ⊑ [d, e] L2 → 0 < d →
- ∃∃I2,K2,V2. K1 ⊑ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
-/2 width=5/ qed-.
-
-fact lsubr_inv_atom2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → L2 = ⋆ →
- L1 = ⋆ ∨ (d = 0 ∧ e = 0).
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ /2 width=1/
-| /3 width=1/
-| #L1 #L2 #W #e #_ #H destruct
-| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
-| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
-]
-qed.
-
-lemma lsubr_inv_atom2: ∀L1,d,e. L1 ⊑ [d, e] ⋆ →
- L1 = ⋆ ∨ (d = 0 ∧ e = 0).
-/2 width=3/ qed-.
-
-fact lsubr_inv_abbr2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
- ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
- ∃∃K1. K1 ⊑ [0, e - 1] K2 & L1 = K1.ⓓV.
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ #d #e #K1 #V #H destruct
-| #L1 #L2 #K1 #V #_ #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #W #e #HL12 #K1 #V #H #_ #_ destruct /2 width=3/
-| #L1 #L2 #I #W1 #W2 #e #_ #K1 #V #H destruct
-| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #K1 #V #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma lsubr_inv_abbr2: ∀L1,K2,V,e. L1 ⊑ [0, e] K2.ⓓV → 0 < e →
- ∃∃K1. K1 ⊑ [0, e - 1] K2 & L1 = K1.ⓓV.
-/2 width=5/ qed-.
-
-fact lsubr_inv_skip2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
- ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
- ∃∃I1,K1,V1. K1 ⊑ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ #d #e #I1 #K1 #V1 #H destruct
-| #L1 #L2 #I1 #K1 #V1 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
-]
-qed.
-
-lemma lsubr_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ⊑ [d, e] K2.ⓑ{I2}V2 → 0 < d →
- ∃∃I1,K1,V1. K1 ⊑ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
-/2 width=5/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-fact lsubr_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
- d = 0 → e = |L1| → |L1| ≤ |L2|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
-[ //
-| /2 width=1/
-| /3 width=1/
-| /3 width=1/
-| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma lsubr_fwd_length_full1: ∀L1,L2. L1 ⊑ [0, |L1|] L2 → |L1| ≤ |L2|.
-/2 width=5/ qed-.
-
-fact lsubr_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
- d = 0 → e = |L2| → |L2| ≤ |L1|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
-[ //
-| /2 width=1/
-| /3 width=1/
-| /3 width=1/
-| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma lsubr_fwd_length_full2: ∀L1,L2. L1 ⊑ [0, |L2|] L2 → |L2| ≤ |L1|.
-/2 width=5/ 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/relocation/lsubr.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
-
-(* bottom element of the refinement *)
-definition lbotr: nat → nat → predicate lenv ≝
- λd,e. NF_sn … (lsubr d e) (lsubr d e …).
-
-interpretation
- "local environment full refinement (substitution)"
- 'SubEqBottom d e L = (lbotr d e L).
-
-(* Basic properties *********************************************************)
-
-lemma lbotr_atom: ∀d,e. ⊒[d, e] ⋆.
-#d #e #L #H
-elim (lsubr_inv_atom2 … H) -H
-[ #H destruct //
-| * #H1 #H2 destruct //
-]
-qed.
-
-lemma lbotr_OO: ∀L. ⊒[0, 0] L.
-// qed.
-
-lemma lbotr_abbr: ∀L,V,e. ⊒[0, e] L → ⊒[0, e + 1] L.ⓓV.
-#L #V #e #HL #K #H
-elim (lsubr_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
-lapply (HL … HLX) -HL -HLX /2 width=1/
-qed.
-
-lemma lbotr_abbr_O: ∀L,V. ⊒[0,1] L.ⓓV.
-#L #V
-@(lbotr_abbr … 0) //
-qed.
-
-lemma lbotr_skip: ∀I,L,V,d,e. ⊒[d, e] L → ⊒[d + 1, e] L.ⓑ{I}V.
-#I #L #V #d #e #HL #K #H
-elim (lsubr_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
-lapply (HL … HLX) -HL -HLX /2 width=1/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lbotr_inv_bind: ∀I,L,V,e. ⊒[0, e] L.ⓑ{I}V → 0 < e →
- ⊒[0, e - 1] L ∧ I = Abbr.
-#I #L #V #e #HL #He
-lapply (HL (L.ⓓV) ?) /2 width=1/ #H
-elim (lsubr_inv_abbr2 … H ?) -H // #K #_ #H destruct
-@conj // #L #HKL
-lapply (HL (L.ⓓV) ?) -HL /2 width=1/ -HKL #H
-elim (lsubr_inv_abbr2 … H ?) -H // -He #X #HLX #H destruct //
-qed-.
-
-lemma lbotr_inv_skip: ∀I,L,V,d,e. ⊒[d, e] L.ⓑ{I}V → 0 < d → ⊒[d - 1, e] L.
-#I #L #V #d #e #HL #Hd #K #HLK
-lapply (HL (K.ⓑ{I}V) ?) -HL /2 width=1/ -HLK #H
-elim (lsubr_inv_skip2 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
-qed-.
(**************************************************************************)
include "basic_2/relocation/ldrop_append.ma".
+include "basic_2/substitution/lsubr.ma".
(* CONTEXT-SENSITIVE PARALLEL SUBSTITUTION FOR TERMS ************************)
(* Basic properties *********************************************************)
-(* Note: it does not hold replacing |L1| with |L2| *)
-lemma cpss_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ▶* T2 →
- ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ▶* T2.
+lemma cpss_lsubr_trans: lsubr_trans … cpss.
#L1 #T1 #T2 #H elim H -L1 -T1 -T2
[ //
| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi
- lapply (ldrop_fwd_O1_length … HLK1) #H2i
- elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi
- <H2i -H2i <minus_plus_m_m /3 width=6/
+ elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -HL12 -HLK1 /3 width=6/
| /4 width=1/
| /3 width=1/
]
elim (lt_or_eq_or_gt i d) #Hid /3 width=4/
destruct
elim (lift_total V 0 (i+1)) #W #HVW
- elim (lift_split … HVW i i ? ? ?) // /3 width=6/
+ elim (lift_split … HVW i i) // /3 width=6/
| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
- [ elim (IHU1 (L. ⓑ{I} W1) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=9/
+ [ elim (IHU1 (L. ⓑ{I} W1) (d+1)) -IHU1 /2 width=1/ -HLK /3 width=9/
| elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/
]
]
(* *)
(**************************************************************************)
-include "basic_2/grammar/lenv_px_sn.ma".
+include "basic_2/grammar/lpx_sn.ma".
include "basic_2/substitution/cpss.ma".
(* SN PARALLEL SUBSTITUTION FOR LOCAL ENVIRONMENTS **************************)
lemma lpss_refl: ∀L. L ⊢ ▶* L.
/2 width=1 by lpx_sn_refl/ qed.
+lemma lpss_pair: ∀I,K1,K2,V1,V2. K1 ⊢ ▶* K2 → K1 ⊢ V1 ▶* V2 →
+ K1.ⓑ{I}V1 ⊢ ▶* K2.ⓑ{I}V2.
+/2 width=1/ qed.
+
lemma lpss_append: ∀K1,K2. K1 ⊢ ▶* K2 → ∀L1,L2. L1 ⊢ ▶* L2 →
L1 @@ K1 ⊢ ▶* L2 @@ K2.
/3 width=1 by lpx_sn_append, cpss_append/ qed.
(* *)
(**************************************************************************)
+include "basic_2/grammar/lpx_sn_lpx_sn.ma".
include "basic_2/relocation/fsup.ma".
include "basic_2/substitution/lpss_ldrop.ma".
--- /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/ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+inductive lsubr: relation lenv ≝
+| lsubr_sort: ∀L. lsubr L (⋆)
+| lsubr_abbr: ∀L1,L2,V. lsubr L1 L2 → lsubr (L1. ⓓV) (L2.ⓓV)
+| lsubr_abst: ∀I,L1,L2,V1,V2. lsubr L1 L2 → lsubr (L1. ⓑ{I}V1) (L2. ⓛV2)
+.
+
+interpretation
+ "local environment refinement (substitution)"
+ 'SubEq L1 L2 = (lsubr L1 L2).
+
+definition lsubr_trans: ∀S. predicate (lenv → relation S) ≝ λS,R.
+ ∀L2,s1,s2. R L2 s1 s2 → ∀L1. L1 ⊑ L2 → R L1 s1 s2.
+
+(* Basic properties *********************************************************)
+
+lemma lsubr_bind: ∀I,L1,L2,V. L1 ⊑ L2 → L1. ⓑ{I} V ⊑ L2.ⓑ{I} V.
+* /2 width=1/ qed.
+
+lemma lsubr_abbr: ∀I,L1,L2,V. L1 ⊑ L2 → L1. ⓓV ⊑ L2. ⓑ{I}V.
+* /2 width=1/ qed.
+
+lemma lsubr_refl: ∀L. L ⊑ L.
+#L elim L -L // /2 width=1/
+qed.
+
+lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (LTC … R).
+#S #R #HR #L1 #s1 #s2 #H elim H -s2
+[ /3 width=3/
+| #s #s2 #_ #Hs2 #IHs1 #L2 #HL12
+ lapply (HR … Hs2 … HL12) -HR -Hs2 /3 width=3/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubr_inv_atom1_aux: ∀L1,L2. L1 ⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 -L2 //
+[ #L1 #L2 #V #_ #H destruct
+| #I #L1 #L2 #V1 #V2 #_ #H destruct
+]
+qed-.
+
+lemma lsubr_inv_atom1: ∀L2. ⋆ ⊑ L2 → L2 = ⋆.
+/2 width=3 by lsubr_inv_atom1_aux/ qed-.
+
+fact lsubr_inv_abbr2_aux: ∀L1,L2. L1 ⊑ L2 → ∀K2,W. L2 = K2.ⓓW →
+ ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
+#L1 #L2 * -L1 -L2
+[ #L #K2 #W #H destruct
+| #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3/
+| #I #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
+]
+qed-.
+
+lemma lsubr_inv_abbr2: ∀L1,K2,W. L1 ⊑ K2.ⓓW →
+ ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
+/2 width=3 by lsubr_inv_abbr2_aux/ qed-.
+
+fact lsubr_inv_abst2_aux: ∀L1,L2. L1 ⊑ L2 → ∀K2,W2. L2 = K2.ⓛW2 →
+ ∃∃I,K1,W1. K1 ⊑ K2 & L1 = K1.ⓑ{I}W1.
+#L1 #L2 * -L1 -L2
+[ #L #K2 #W2 #H destruct
+| #L1 #L2 #V #_ #K2 #W2 #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #K2 #W2 #H destruct /2 width=5/
+]
+qed-.
+
+lemma lsubr_inv_abst2: ∀L1,K2,W2. L1 ⊑ K2.ⓛW2 →
+ ∃∃I,K1,W1. K1 ⊑ K2 & L1 = K1.ⓑ{I}W1.
+/2 width=4 by lsubr_inv_abst2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsubr_fwd_length: ∀L1,L2. L1 ⊑ L2 → |L2| ≤ |L1|.
+#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubr_fwd_ldrop2_abbr: ∀L1,L2. L1 ⊑ L2 →
+ ∀K2,W,i. ⇩[0, i] L2 ≡ K2. ⓓW →
+ ∃∃K1. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1. ⓓW.
+#L1 #L2 #H elim H -L1 -L2
+[ #L #K2 #W #i #H
+ lapply (ldrop_inv_atom1 … H) -H #H destruct
+| #L1 #L2 #V #HL12 #IHL12 #K2 #W #i #H
+ elim (ldrop_inv_O1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+ [ /2 width=3/
+ | elim (IHL12 … HLK2) -IHL12 -HLK2 /3 width=3/
+ ]
+| #I #L1 #L2 #V1 #V2 #_ #IHL12 #K2 #W #i #H
+ elim (ldrop_inv_O1 … H) -H * #Hi #HLK2 destruct
+ elim (IHL12 … HLK2) -IHL12 -HLK2 /3 width=3/
+]
+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/lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+fact lsubr_inv_abbr1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W. L1 = K1.ⓓW →
+ ∨∨ L2 = ⋆
+ | ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓓW
+ | ∃∃K2,W2. K1 ⊑ K2 & L2 = K2.ⓛW2.
+#L1 #L2 * -L1 -L2
+[ #L #K1 #W #H destruct /2 width=1/
+| #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3/
+| #I #L1 #L2 #V1 #V2 #HL12 #K1 #W #H destruct /3 width=4/
+]
+qed-.
+
+lemma lsubr_inv_abbr1: ∀K1,L2,W. K1.ⓓW ⊑ L2 →
+ ∨∨ L2 = ⋆
+ | ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓓW
+ | ∃∃K2,W2. K1 ⊑ K2 & L2 = K2.ⓛW2.
+/2 width=3 by lsubr_inv_abbr1_aux/ qed-.
+
+fact lsubr_inv_abst1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W1. L1 = K1.ⓛW1 →
+ L2 = ⋆ ∨
+ ∃∃K2,W2. K1 ⊑ K2 & L2 = K2.ⓛW2.
+#L1 #L2 * -L1 -L2
+[ #L #K1 #W1 #H destruct /2 width=1/
+| #L1 #L2 #V #_ #K1 #W1 #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #K1 #W1 #H destruct /3 width=4/
+]
+qed-.
+
+lemma lsubr_inv_abst1: ∀K1,L2,W1. K1.ⓛW1 ⊑ L2 →
+ L2 = ⋆ ∨
+ ∃∃K2,W2. K1 ⊑ K2 & L2 = K2.ⓛW2.
+/2 width=4 by lsubr_inv_abst1_aux/ qed-.
+
+(* Main properties **********************************************************)
+
+theorem lsubr_trans: Transitive … lsubr.
+#L1 #L #H elim H -L1 -L
+[ #L1 #X #H
+ lapply (lsubr_inv_atom1 … H) -H //
+| #L1 #L #V #_ #IHL1 #X #H
+ elim (lsubr_inv_abbr1 … H) -H // *
+ #L2 [2: #V2 ] #HL2 #H destruct /3 width=1/
+| #I #L1 #L #V1 #V #_ #IHL1 #X #H
+ elim (lsubr_inv_abst1 … H) -H // *
+ #L2 #V2 #HL2 #H destruct /3 width=1/
+]
+qed-.
(* Basic properties *********************************************************)
-(* Note: it does not hold replacing |L1| with |L2| *)
-lemma cpqs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➤* T2 →
- ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➤* T2.
+lemma cpqs_lsubr_trans: lsubr_trans … cpqs.
#L1 #T1 #T2 #H elim H -L1 -T1 -T2
[ //
| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi
- lapply (ldrop_fwd_O1_length … HLK1) #H2i
- elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi
- <H2i -H2i <minus_plus_m_m /3 width=6/
+ elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -HL12 -HLK1 /3 width=6/
| /4 width=1/
|4,6: /3 width=1/
| /4 width=3/
lemma lpqs_refl: ∀L. L ⊢ ➤* L.
/2 width=1 by lpx_sn_refl/ qed.
+lemma lpqs_pair: ∀I,K1,K2,V1,V2. K1 ⊢ ➤* K2 → K1 ⊢ V1 ➤* V2 →
+ K1.ⓑ{I}V1 ⊢ ➤* K2.ⓑ{I}V2.
+/2 width=1/ qed.
+
lemma lpqs_append: ∀K1,K2. K1 ⊢ ➤* K2 → ∀L1,L2. L1 ⊢ ➤* L2 →
L1 @@ K1 ⊢ ➤* L2 @@ K2.
/3 width=1 by lpx_sn_append, cpqs_append/ qed.
(* *)
(**************************************************************************)
+include "basic_2/grammar/lpx_sn_lpx_sn.ma".
include "basic_2/relocation/fsup.ma".
include "basic_2/unfold/lpqs_ldrop.ma".
}
]
[ { "context-sensitive computation" * } {
- [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_tpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_delift" + "cprs_aaa" + "cprs_ltpr" + "cprs_lfpr" + "cprs_cprs" + "cprs_lfprs" + "cprs_tstc" + "cprs_tstc_vector" * ]
- }
- ]
- [ { "context-free computation" * } {
- [ "ltprs ( ? ➡* ? )" "ltprs_alt ( ? ➡➡* ? )" "ltprs_ldrop" + "ltprs_ltprs" * ]
- [ "tprs ( ? ➡* ?)" "tprs_lift" + "tprs_tprs" * ]
+ [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_aaa" + "lprs_cprs" + "lprs_lprs" * ]
+ [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_tpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_aaa" + "cprs_lpr" + "cprs_cprs" + "cprs_tstc" + "cprs_tstc_vector" * ]
}
]
[ { "local env. ref. for abstract candidates of reducibility" * } {
[ { "reduction" * } {
[ { "context-sensitive normal forms" * } {
[ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_liftt" + "cnf_crf" + "cnf_cif" * ]
- [ "chnf ( ? ⊢ 𝐇𝐍⦃?⦄ )" * ]
}
]
[ { "context-sensitive reduction" * } {
[ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_cpss" + "lpr_lpss" + "lpr_aaa" + "lpr_cpr" + "lpr_lpr" * ]
- [ "cpr ( ? ⊢ ? ➡ ? )" "lpr_tshf" + "cpr_lift" + "cpr_cif" * ]
+ [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cif" * ]
}
]
[ { "context-sensitive reducible forms" * } {
[ "cpss ( ? ⊢ ? ▶* ? )" "cpss_lift" * ]
}
]
+ [ { "local env. ref. for substitution" * } {
+ [ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ]
+ }
+ ]
[ { "iterated structural successor for closures" * } {
[ "fsups ( ⦃?,?⦄ ⊃* ⦃?,?⦄ )" "fsups_fsups" * ]
[ "fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )" "fsupp_fsupp" * ]
}
]
[ { "basic local env. slicing" * } {
- [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx" + "ldrop_lpx_sn" + "ldrop_lbotr" + "ldrop_ldrop" * ]
- }
- ]
- [ { "local env. ref. for substitution" * } {
- [ "lsubr ( ? ⊑[?,?] ? )" "(lsubr_lsubr)" "lsubr_lbotr ( ⊒[?,?] ? )" * ]
+ [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
}
]
[ { "basic term relocation" * } {
]
class "red"
[ { "grammar" * } {
- [ { "same head term form" * } {
- [ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ]
+ [ { "pointwise extension of a relation" * } {
+ [ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ]
}
]
[ { "same top term constructor" * } {
]
[ { "internal syntax" * } {
[ "genv" * ]
- [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" + "lenv_px_sn" + "lenv_px_bi" * ]
+ [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" * ]
[ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
[ "item" * ]
}
∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 →
∃∃a,b. R a1 b1 a b & R a2 b2 a b.
+definition LTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝
+ λA,B,R,a. TC … (R a).
+
+definition s_r_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2.
+ ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2.
+
+definition s_rs_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2.
+ ∀L2,T1,T2. LTC … R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2.
+
lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 →
∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
∃∃a. R2 a1 a & TC … R1 a2 a.
lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
#A #R #S #a1 #Ha1
@SN_intro #a2 #HRa12 #HSa12
-elim (HSa12 ?) -HSa12 /2 width=1/
+elim HSa12 -HSa12 /2 width=1/
qed.
definition NF_sn: ∀A. relation A → relation A → predicate A ≝
lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.
#A #R #S #a2 #Ha2
@SN_sn_intro #a1 #HRa12 #HSa12
-elim (HSa12 ?) -HSa12 /2 width=1/
+elim HSa12 -HSa12 /2 width=1/
qed.
lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R →
∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
R a1 b1 a2 b2 ∨
∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2.
-#A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx ?????????? H) -a1 -b1
+#A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx … a1 b1 H) -a1 -b1
[ /2 width=1/
| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4/
]
qed-.
+
+lemma s_r_trans_TC1: ∀A,B,R,S. s_r_trans A B R S → s_rs_trans A B R S.
+#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ]
+#T #T2 #_ #HT2 #IHT1 #L1 #HL12
+lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/
+qed-.
+
+lemma s_r_trans_TC2: ∀A,B,R,S. s_rs_trans A B R S → s_r_trans A B R (TC … S).
+#A #B #R #S #HRS #L2 #T1 #T2 #HT12 #L1 #H @(TC_ind_dx … L1 H) -L1 /2 width=3/ /3 width=3/
+qed-.
projects / helm.git / commitdiff