(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps.ma".
+include "Basic_2/substitution/tps.ma".
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
-(* Basic-1: includes: csubst1_bind *)
+(* Basic_1: includes: csubst1_bind *)
inductive ltps: nat → nat → relation lenv ≝
| ltps_atom: ∀d,e. ltps d e (⋆) (⋆)
| ltps_pair: ∀L,I,V. ltps 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
>(plus_minus_m_m d 1) /2/
qed.
-(* Basic-1: was by definition: csubst1_refl *)
+(* Basic_1: was by definition: csubst1_refl *)
lemma ltps_refl: ∀L,d,e. L [d, e] ≫ L.
#L elim L -L //
#L #I #V #IHL * /2/ * /2/
qed.
lemma ltps_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ≫ L2 → L1 = L2.
-/2/ qed.
+/2/ qed-.
fact ltps_inv_atom1_aux: ∀d,e,L1,L2.
L1 [d, e] ≫ L2 → L1 = ⋆ → L2 = ⋆.
qed.
lemma ltps_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫ L2 → L2 = ⋆.
-/2 width=5/ qed.
+/2 width=5/ qed-.
fact ltps_inv_tps21_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e →
∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
lemma ltps_inv_tps21: ∀e,K1,I,V1,L2. K1. 𝕓{I} V1 [0, e] ≫ L2 → 0 < e →
∃∃K2,V2. K1 [0, e - 1] ≫ K2 & K2 ⊢ V1 [0, e - 1] ≫ V2 &
L2 = K2. 𝕓{I} V2.
-/2 width=5/ qed.
+/2 width=5/ qed-.
fact ltps_inv_tps11_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d →
∀I,K1,V1. L1 = K1. 𝕓{I} V1 →
∃∃K2,V2. K1 [d - 1, e] ≫ K2 &
K2 ⊢ V1 [d - 1, e] ≫ V2 &
L2 = K2. 𝕓{I} V2.
-/2/ qed.
+/2/ qed-.
fact ltps_inv_atom2_aux: ∀d,e,L1,L2.
L1 [d, e] ≫ L2 → L2 = ⋆ → L1 = ⋆.
qed.
lemma ltps_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆.
-/2 width=5/ qed.
+/2 width=5/ qed-.
fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e →
∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ≫ K2. 𝕓{I} V2 → 0 < e →
∃∃K1,V1. K1 [0, e - 1] ≫ K2 & K2 ⊢ V1 [0, e - 1] ≫ V2 &
L1 = K1. 𝕓{I} V1.
-/2 width=5/ qed.
+/2 width=5/ qed-.
fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d →
∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
∃∃K1,V1. K1 [d - 1, e] ≫ K2 &
K2 ⊢ V1 [d - 1, e] ≫ V2 &
L1 = K1. 𝕓{I} V1.
-/2/ qed.
+/2/ qed-.
-(* Basic-1: removed theorems 27:
- csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
+(* Basic_1: removed theorems 27:
+ csubst0_clear_O csubst0_ldrop_lt csubst0_ldrop_gt csubst0_ldrop_eq
csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
- csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back
+ csubst0_ldrop_gt_back csubst0_ldrop_eq_back csubst0_ldrop_lt_back
csubst0_gen_sort csubst0_gen_head csubst0_getl_ge csubst0_getl_lt
csubst0_gen_S_bind_2 csubst0_getl_ge_back csubst0_getl_lt_back
csubst0_snd_bind csubst0_fst_bind csubst0_both_bind