]> matita.cs.unibo.it Git - helm.git/commitdiff
urgent partial commit ... to be fixed later ...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 10 Apr 2012 13:48:26 +0000 (13:48 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 10 Apr 2012 13:48:26 +0000 (13:48 +0000)
matita/matita/contribs/lambda_delta/basic_2/notation.ma
matita/matita/contribs/lambda_delta/basic_2/substitution/ltps.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_ldrop.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_tps.ma [deleted file]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_ltps.ma [deleted file]

index 06d7d9ed37e8bfa31ffaade0cd5a3f20df321b7e..d8ab202ff553b1a52230969997da012b1c42ed4a 100644 (file)
@@ -150,10 +150,6 @@ notation "hvbox( L ⊢ break ⌘ [ T ] ≡ break k )"
    non associative with precedence 45
    for @{ 'ICM $L $T $k }.
 
-notation "hvbox( T1 break [ d , break e ] ▶ break T2 )"
-   non associative with precedence 45
-   for @{ 'PSubst $T1 $d $e $T2 }.
-
 notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ▶ break T2 )"
    non associative with precedence 45
    for @{ 'PSubst $L $T1 $d $e $T2 }.
@@ -184,6 +180,14 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ▶* break T2 )"
    non associative with precedence 45
    for @{ 'PSubstStar $L $T1 $d $e $T2 }.
 
+notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ▶▶* break T2 )"
+   non associative with precedence 45
+   for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
+
+notation "hvbox( T1 break [ d , break e ] ▶** break T2 )"
+   non associative with precedence 45
+   for @{ 'PSubstStars $T1 $d $e $T2 }.
+
 notation "hvbox( T1 break [ d , break e ] ≡ break T2 )"
    non associative with precedence 45
    for @{ 'TSubst $T1 $d $e $T2 }.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps.ma
deleted file mode 100644 (file)
index b1d4353..0000000
+++ /dev/null
@@ -1,191 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/tps.ma".
-
-(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
-
-(* 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)
-| ltps_tps2: ∀L1,L2,I,V1,V2,e.
-             ltps 0 e L1 L2 → L2 ⊢ V1 [0, e] ▶ V2 →
-             ltps 0 (e + 1) (L1. ⓑ{I} V1) L2. ⓑ{I} V2
-| ltps_tps1: ∀L1,L2,I,V1,V2,d,e.
-             ltps d e L1 L2 → L2 ⊢ V1 [d, e] ▶ V2 →
-             ltps (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
-.
-
-interpretation "parallel substritution (local environment)"
-   'PSubst L1 d e L2 = (ltps d e L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma ltps_tps2_lt: ∀L1,L2,I,V1,V2,e.
-                    L1 [0, e - 1] ▶ L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
-                    0 < e → L1. ⓑ{I} V1 [0, e] ▶ L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(plus_minus_m_m e 1) /2 width=1/
-qed.
-
-lemma ltps_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
-                    L1 [d - 1, e] ▶ L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 →
-                    0 < d → L1. ⓑ{I} V1 [d, e] ▶ L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
->(plus_minus_m_m d 1) /2 width=1/
-qed.
-
-(* 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 width=1/ * /2 width=1/
-qed.
-
-lemma ltps_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶ L2 → L1 [0, |L2|] ▶ L2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-// /3 width=2/ /3 width=3/
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma ltps_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶ L2 → |L1| = |L2|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-normalize //
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact ltps_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → e = 0 → L1 = L2.
-#d #e #L1 #L2 #H elim H -d -e -L1 -L2 //
-[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct
-  >(IHL12 ?) -IHL12 // >(tps_inv_refl_O2 … HV12) //
-]
-qed.
-
-lemma ltps_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶ L2 → L1 = L2.
-/2 width=4/ qed-.
-
-fact ltps_inv_atom1_aux: ∀d,e,L1,L2.
-                         L1 [d, e] ▶ L2 → L1 = ⋆ → L2 = ⋆.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ //
-| #L #I #V #H destruct
-| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
-]
-qed.
-
-lemma ltps_inv_atom1: ∀d,e,L2. ⋆ [d, e] ▶ L2 → L2 = ⋆.
-/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 →
-                         ∃∃K2,V2. K1 [0, e - 1] ▶ K2 &
-                                  K2 ⊢ V1 [0, e - 1] ▶ V2 &
-                                  L2 = K2. ⓑ{I} V2.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #e #_ #_ #K1 #I #V1 #H destruct
-| #L1 #I #V #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct /2 width=5/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-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-.
-
-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.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #e #_ #I #K1 #V1 #H destruct
-| #L #I #V #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K1 #W1 #H destruct /2 width=5/
-]
-qed.
-
-lemma ltps_inv_tps11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 [d, e] ▶ L2 → 0 < d →
-                      ∃∃K2,V2. K1 [d - 1, e] ▶ K2 &
-                                  K2 ⊢ V1 [d - 1, e] ▶ V2 &
-                                  L2 = K2. ⓑ{I} V2.
-/2 width=3/ qed-.
-
-fact ltps_inv_atom2_aux: ∀d,e,L1,L2.
-                         L1 [d, e] ▶ L2 → L2 = ⋆ → L1 = ⋆.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ //
-| #L #I #V #H destruct
-| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
-]
-qed.
-
-lemma ltps_inv_atom2: ∀d,e,L1. L1 [d, e] ▶ ⋆ → L1 = ⋆.
-/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 →
-                         ∃∃K1,V1. K1 [0, e - 1] ▶ K2 &
-                                  K2 ⊢ V1 [0, e - 1] ▶ V2 &
-                                  L1 = K1. ⓑ{I} V1.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #e #_ #_ #K1 #I #V1 #H destruct
-| #L1 #I #V #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct /2 width=5/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-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-.
-
-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.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #e #_ #I #K2 #V2 #H destruct
-| #L #I #V #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct /2 width=5/
-]
-qed.
-
-lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. ⓑ{I} V2 → 0 < d →
-                      ∃∃K1,V1. K1 [d - 1, e] ▶ K2 &
-                                  K2 ⊢ V1 [d - 1, e] ▶ V2 &
-                                  L1 = K1. ⓑ{I} V1.
-/2 width=3/ qed-.
-
-(* Basic_1: removed theorems 27:
-            csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
-            csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
-            csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_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
-            csubst1_head csubst1_flat csubst1_gen_head
-            csubst1_getl_ge csubst1_getl_lt csubst1_getl_ge_back getl_csubst1
-
-*)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_ldrop.ma
deleted file mode 100644 (file)
index e94aec4..0000000
+++ /dev/null
@@ -1,131 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/ltps.ma".
-
-(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
-
-lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶ L1 →
-                          ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
-                          d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
-#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
-| //
-| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
-  elim (le_inv_plus_l … He12) #_ #He2
-  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
-  lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
-| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
-  elim (le_inv_plus_l … Hd1e2) #_ #He2
-  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
-  lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
-]
-qed.
-
-lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶ L0 →
-                           ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
-                           d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
-#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
-| //
-| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
-  elim (le_inv_plus_l … He12) #_ #He2
-  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
-  lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
-| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
-  elim (le_inv_plus_l … Hd1e2) #_ #He2
-  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
-  lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
-]
-qed.
-
-lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶ L1 →
-                          ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
-                          ∃∃L. L2 [0, d1 + e1 - e2] ▶ L & ⇩[0, e2] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
-| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
-  lapply (le_n_O_to_eq … He2) -He2 #H destruct
-  lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
-| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
-  lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
-  [ -IHK01 -He21 destruct <minus_n_O /3 width=3/
-  | -HK01 -HV01 <minus_le_minus_minus_comm //
-    elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
-  ]
-| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
-  elim (le_inv_plus_l … Hd1e2) #_ #He2
-  <minus_le_minus_minus_comm //
-  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
-  elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
-]
-qed.
-
-lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶ L0 →
-                           ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
-                           ∃∃L. L [0, d1 + e1 - e2] ▶ L2 & ⇩[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
-| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
-  lapply (le_n_O_to_eq … He2) -He2 #H destruct
-  lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
-| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
-  lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
-  [ -IHK10 -He21 destruct <minus_n_O /3 width=3/
-  | -HK10 -HV10 <minus_le_minus_minus_comm //
-    elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
-  ]
-| #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
-  elim (le_inv_plus_l … Hd1e2) #_ #He2
-  <minus_le_minus_minus_comm //
-  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
-  elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
-]
-qed.
-
-lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶ L1 →
-                          ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
-                          ∃∃L. L2 [d1 - e2, e1] ▶ L & ⇩[0, e2] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
-| /2 width=3/
-| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
-  lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
-  lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
-| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
-  lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
-  [ -IHK01 -He2d1 destruct <minus_n_O /3 width=3/
-  | -HK01 -HV01 <minus_le_minus_minus_comm //
-    elim (IHK01 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
-  ]
-]
-qed.
-
-lemma ltps_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ▶ L0 →
-                           ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
-                           ∃∃L. L [d1 - e2, e1] ▶ L2 & ⇩[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
-| /2 width=3/
-| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
-  lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
-  lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
-| #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
-  lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
-  [ -IHK10 -He2d1 destruct <minus_n_O /3 width=3/
-  | -HK10 -HV10 <minus_le_minus_minus_comm //
-    elim (IHK10 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
-  ]
-]
-qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_tps.ma
deleted file mode 100644 (file)
index 9627335..0000000
+++ /dev/null
@@ -1,112 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/tps_lift.ma".
-include "basic_2/substitution/ltps_ldrop.ma".
-
-(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
-
-lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
-                        ∀L1,d1,e1. L0 [d1, e1] ▶ L1 → d1 + e1 ≤ d2 →
-                        L1 ⊢ T2 [d2, e2] ▶ U2.
-#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
-[ //
-| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
-  lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
-  lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /2 width=4/
-| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
-  @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltps_tps1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
-| /3 width=4/
-]
-qed.
-
-(* Basic_1: was: subst1_subst1_back *)
-lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
-                     ∀L1,d1,e1. L0 [d1, e1] ▶ L1 →
-                     ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T &
-                          L1 ⊢ U2 [d1, e1] ▶ T.
-#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
-[ /2 width=3/
-| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
-  elim (lt_or_ge i2 d1) #Hi2d1
-  [ elim (ltps_ldrop_conf_le … HL01 … HLK0 ?) -L0 /2 width=2/ #X #H #HLK1
-    elim (ltps_inv_tps11 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
-    lapply (ldrop_fwd_ldrop2 … HLK1) #H
-    elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
-    lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // >minus_plus <plus_minus_m_m // /3 width=4/
-  | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
-    [ elim (ltps_ldrop_conf_be … HL01 … HLK0 ? ?) -L0 // /2 width=2/ #X #H #HLK1
-      elim (ltps_inv_tps21 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
-      lapply (ldrop_fwd_ldrop2 … HLK1) #H
-      elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
-      lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // normalize #HW01
-      lapply (tps_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
-    | lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/
-    ]
-  ]
-| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
-  elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
-  elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/
-| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
-  elim (IHVW2 … HL01) -IHVW2
-  elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
-]
-qed.
-
-lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
-                         ∀L1,d1,e1. L1 [d1, e1] ▶ L0 → d1 + e1 ≤ d2 →
-                         L1 ⊢ T2 [d2, e2] ▶ U2.
-#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
-[ //
-| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2
-  lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
-  lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/
-| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2
-  @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltps_tps1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
-| /3 width=4/
-]
-qed.
-
-(* Basic_1: was: subst1_subst1 *)
-lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
-                      ∀L1,d1,e1. L1 [d1, e1] ▶ L0 →
-                      ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T &
-                           L0 ⊢ T [d1, e1] ▶ U2.
-#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
-[ /2 width=3/
-| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10
-  elim (lt_or_ge i2 d1) #Hi2d1
-  [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=2/ #X #H #HLK1
-    elim (ltps_inv_tps12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
-    lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
-    elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
-    lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // >minus_plus <plus_minus_m_m /2 width=1/ /3 width=4/
-  | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
-    [ elim (ltps_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 // /2 width=2/ #X #H #HLK1
-      elim (ltps_inv_tps22 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
-      lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
-      elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
-      lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // normalize #HW01
-      lapply (tps_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
-    | lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/
-    ]
-  ]
-| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
-  elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
-  elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/
-| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
-  elim (IHVW2 … HL10) -IHVW2
-  elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/
-]
-qed.
index e992e2a77b63a4ecbf8d301991b16798103931e8..a520f2e6f2f5c9c380fb20c14f64dff15c0c3fb1 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ltps.ma".
 include "basic_2/unfold/tpss.ma".
 
-(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
-
-definition ltpss: nat → nat → relation lenv ≝
-                  λd,e. TC … (ltps d e).
-
-interpretation "partial unfold (local environment)"
+(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************)
+
+(* Basic_1: includes: csubst1_bind *)
+inductive ltpss: nat → nat → relation lenv ≝
+| ltpss_atom : ∀d,e. ltpss d e (⋆) (⋆)
+| ltpss_pair : ∀L,I,V. ltpss 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
+| ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
+               ltpss 0 e L1 L2 → L2 ⊢ V1 [0, e] ▶* V2 →
+               ltpss 0 (e + 1) (L1. ⓑ{I} V1) L2. ⓑ{I} V2
+| ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
+               ltpss d e L1 L2 → L2 ⊢ V1 [d, e] ▶* V2 →
+               ltpss (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
+.
+
+interpretation "parallel unfold (local environment)"
    'PSubstStar L1 d e L2 = (ltpss d e L1 L2).
 
-(* Basic eliminators ********************************************************)
-
-lemma ltpss_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 →
-                 (∀L,L2. L1 [d, e] ▶* L → L [d, e] ▶ L2 → R L → R L2) →
-                 ∀L2. L1 [d, e] ▶* L2 → R L2.
-#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
-qed-.
-
-lemma ltpss_ind_dx: ∀d,e,L2. ∀R:predicate lenv. R L2 →
-                    (∀L1,L. L1 [d, e] ▶ L → L [d, e] ▶* L2 → R L → R L1) →
-                    ∀L1. L1 [d, e] ▶* L2 → R L1.
-#d #e #L2 #R #HL2 #IHL2 #L1 #HL12 @(TC_star_ind_dx … HL2 IHL2 … HL12) //
-qed-.
-
 (* Basic properties *********************************************************)
 
-lemma ltpss_strap: ∀L1,L,L2,d,e.
-                   L1 [d, e] ▶ L → L [d, e] ▶* L2 → L1 [d, e] ▶* L2. 
-/2 width=3/ qed.
+lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
+                      L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
+                      0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
+>(plus_minus_m_m e 1) /2 width=1/
+qed.
+
+lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
+                      L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 →
+                      0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
+>(plus_minus_m_m d 1) /2 width=1/
+qed.
 
+(* Basic_1: was by definition: csubst1_refl *)
 lemma ltpss_refl: ∀L,d,e. L [d, e] ▶* L.
-/2 width=1/ qed.
+#L elim L -L //
+#L #I #V #IHL * /2 width=1/ * /2 width=1/
+qed.
 
 lemma ltpss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → L1 [0, |L2|] ▶* L2.
-#L1 #L2 #d #e #H @(ltpss_ind … H) -L2 //
-#L #L2 #_ #HL2
->(ltps_fwd_length … HL2) /3 width=5/
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+// /3 width=2/ /3 width=3/
 qed.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma ltpss_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → |L1| = |L2|.
-#L1 #L2 #d #e #H @(ltpss_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL12 >IHL12 -IHL12
-/2 width=3 by ltps_fwd_length/
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+normalize //
 qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
+fact ltpss_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → e = 0 → L1 = L2.
+#d #e #L1 #L2 #H elim H -d -e -L1 -L2 //
+[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct
+  >(IHL12 ?) -IHL12 // >(tpss_inv_refl_O2 … HV12) //
+]
+qed.
+
 lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶* L2 → L1 = L2.
-#d #L1 #L2 #H @(ltpss_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL <(ltps_inv_refl_O2 … HL2) -HL2 //
-qed-.
+/2 width=4/ qed-.
+
+fact ltpss_inv_atom1_aux: ∀d,e,L1,L2.
+                          L1 [d, e] ▶* L2 → L1 = ⋆ → L2 = ⋆.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ //
+| #L #I #V #H destruct
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+]
+qed.
 
 lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ▶* L2 → L2 = ⋆.
-#d #e #L2 #H @(ltpss_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL destruct
->(ltps_inv_atom1 … HL2) -HL2 //
-qed-.
+/2 width=5/ qed-.
 
-fact ltpss_inv_atom2_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → L2 = ⋆ → L1 = ⋆.
-#d #e #L1 #L2 #H @(ltpss_ind … H) -L2 //
-#L2 #L #_ #HL2 #IHL2 #H destruct
-lapply (ltps_inv_atom2 … HL2) -HL2 /2 width=1/
+fact ltpss_inv_tpss21_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → d = 0 → 0 < e →
+                           ∀K1,I,V1. L1 = K1. ⓑ{I} V1 →
+                           ∃∃K2,V2. K1 [0, e - 1] ▶* K2 &
+                                    K2 ⊢ V1 [0, e - 1] ▶* V2 &
+                                    L2 = K2. ⓑ{I} V2.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ #d #e #_ #_ #K1 #I #V1 #H destruct
+| #L1 #I #V #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma ltpss_inv_tpss21: ∀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-.
+
+fact ltpss_inv_tpss11_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.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ #d #e #_ #I #K1 #V1 #H destruct
+| #L #I #V #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K1 #W1 #H destruct /2 width=5/
+]
+qed.
+
+lemma ltpss_inv_tpss11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 [d, e] ▶* L2 → 0 < d →
+                        ∃∃K2,V2. K1 [d - 1, e] ▶* K2 &
+                                 K2 ⊢ V1 [d - 1, e] ▶* V2 &
+                                 L2 = K2. ⓑ{I} V2.
+/2 width=3/ qed-.
+
+fact ltpss_inv_atom2_aux: ∀d,e,L1,L2.
+                          L1 [d, e] ▶* L2 → L2 = ⋆ → L1 = ⋆.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ //
+| #L #I #V #H destruct
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+]
 qed.
 
 lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ▶* ⋆ → L1 = ⋆.
 /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 →
-                         ∃∃K1,V1. K1 [0, e - 1] ▶ K2 &
-                                  K2 ⊢ V1 [0, e - 1] ▶ V2 &
-                                  L1 = K1. ⓑ{I} V1.
-#d #e #L1 #L2 * -d e L1 L2
+
+fact ltpss_inv_tpss22_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → d = 0 → 0 < e →
+                           ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
+                           ∃∃K1,V1. K1 [0, e - 1] ▶* K2 &
+                                    K2 ⊢ V1 [0, e - 1] ▶* V2 &
+                                    L1 = K1. ⓑ{I} V1.
+#d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #_ #K1 #I #V1 #H destruct
 | #L1 #I #V #_ #H elim (lt_refl_false … H)
 | #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct /2 width=5/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
 ]
 qed.
 
-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.
+lemma ltpss_inv_tpss22: ∀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-.
 
-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 &
+fact ltpss_inv_tpss12_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.
-#d #e #L1 #L2 * -d e L1 L2
+#d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #I #K2 #V2 #H destruct
 | #L #I #V #H elim (lt_refl_false … H)
 | #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
@@ -113,9 +172,20 @@ fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → 0 < d →
 ]
 qed.
 
-lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. ⓑ{I} V2 → 0 < d →
-                      ∃∃K1,V1. K1 [d - 1, e] ▶ K2 &
-                                  K2 ⊢ V1 [d - 1, e] ▶ V2 &
-                                  L1 = K1. ⓑ{I} V1.
-/2 width=1/ qed.
+lemma ltpss_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶* K2. ⓑ{I} V2 → 0 < d →
+                        ∃∃K1,V1. K1 [d - 1, e] ▶* K2 &
+                                 K2 ⊢ V1 [d - 1, e] ▶* V2 &
+                                 L1 = K1. ⓑ{I} V1.
+/2 width=3/ qed-.
+
+(* Basic_1: removed theorems 27:
+            csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
+            csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
+            csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_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
+            csubst1_head csubst1_flat csubst1_gen_head
+            csubst1_getl_ge csubst1_getl_lt csubst1_getl_ge_back getl_csubst1
+
 *)
index 59269ef11da415f15821b19c9851bd95a8766c7f..4d223834e3f27030fe704461249f70e15a8b7001 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ltps_ldrop.ma".
 include "basic_2/unfold/ltpss.ma".
 
-(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
+(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************)
 
 lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
                            ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
                            d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
-#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 // /3 width=6/
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
+| //
+| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
+  elim (le_inv_plus_l … He12) #_ #He2
+  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+  lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
+  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+  lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
+]
 qed.
 
 lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
                             ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
                             d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
-#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 // /3 width=6/
+#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
+| //
+| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
+  elim (le_inv_plus_l … He12) #_ #He2
+  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+  lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
+| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
+  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+  lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
+]
 qed.
 
 lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
                            ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
                            ∃∃L. L2 [0, d1 + e1 - e2] ▶* L & ⇩[0, e2] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
-[ /2 width=3/
-| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
-  elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0
-  elim (ltps_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3 width=3/
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+  lapply (le_n_O_to_eq … He2) -He2 #H destruct
+  lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
+| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
+  lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+  [ -IHK01 -He21 destruct <minus_n_O /3 width=3/
+  | -HK01 -HV01 <minus_le_minus_minus_comm //
+    elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
+  ]
+| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
+  <minus_le_minus_minus_comm //
+  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+  elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
 ]
 qed.
 
 lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
                             ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
                             ∃∃L. L [0, d1 + e1 - e2] ▶* L2 & ⇩[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
-[ /2 width=3/
-| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
-  elim (ltps_ldrop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0
-  elim (IHL … HL0 Hd1e2 He2de1) -L /3 width=3/
+#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+  lapply (le_n_O_to_eq … He2) -He2 #H destruct
+  lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
+| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
+  lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+  [ -IHK10 -He21 destruct <minus_n_O /3 width=3/
+  | -HK10 -HV10 <minus_le_minus_minus_comm //
+    elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
+  ]
+| #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
+  <minus_le_minus_minus_comm //
+  lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+  elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
 ]
 qed.
 
 lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
                            ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
                            ∃∃L. L2 [d1 - e2, e1] ▶* L & ⇩[0, e2] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
-[ /2 width=3/
-| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
-  elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0
-  elim (ltps_ldrop_conf_le … HL1 … HL0 He2d1) -L /3 width=3/
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
+  lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
+  lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
+  lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+  [ -IHK01 -He2d1 destruct <minus_n_O /3 width=3/
+  | -HK01 -HV01 <minus_le_minus_minus_comm //
+    elim (IHK01 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
+  ]
 ]
 qed.
 
 lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
                             ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
                             ∃∃L. L [d1 - e2, e1] ▶* L2 & ⇩[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
-[ /2 width=3/
-| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1
-  elim (ltps_ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0
-  elim (IHL … HL0 He2d1) -L /3 width=3/
+#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
+  lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
+  lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
+| #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
+  lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+  [ -IHK10 -He2d1 destruct <minus_n_O /3 width=3/
+  | -HK10 -HV10 <minus_le_minus_minus_comm //
+    elim (IHK10 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
+  ]
 ]
 qed.
index faa3ce6e5c8adab4063abe3a79c5d8824d85ceba..ce2271b705f0b8f4b3622b0c593718a57b845021 100644 (file)
@@ -19,122 +19,82 @@ include "basic_2/unfold/ltpss_tpss.ma".
 
 (* Advanced properties ******************************************************)
 
-(* Main properties **********************************************************)
-
-theorem ltpss_trans_eq: ∀L1,L,L2,d,e.
-                        L1 [d, e] ▶* L → L [d, e] ▶* L2 → L1 [d, e] ▶* L2. 
-/2 width=3/ qed.
-
-lemma ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
-                   L1 [0, e] ▶* L2 → L2 ⊢ V1 [0, e] ▶* V2 →
-                   L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
-[ /2 width=1/
-| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
-]
+lemma ltpss_tpss_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 →
+                       ∀L1,d1,e1. L0 [d1, e1] ▶* L1 →
+                       ∃∃T. L1 ⊢ T2 [d2, e2] ▶* T &
+                            L1 ⊢ U2 [d1, e1] ▶* T.
+#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 @(tpss_ind … H) -U2 /2 width=3/
+#U #U2 #_ #HU2 * #X2 #HTX2 #HUX2
+elim (ltpss_tps_conf … HU2 … HL01) -L0 #X1 #HUX1 #HU2X1
+elim (tpss_strip_eq … HUX2 … HUX1) -U #X #HX2 #HX1
+lapply (tpss_trans_eq … HU2X1 … HX1) -X1 /3 width=3/
 qed.
 
-lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
-                      L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
-                      0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(plus_minus_m_m e 1) // /2 width=1/
-qed.
-
-lemma ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
-                   L1 [d, e] ▶* L2 → L2 ⊢ V1 [d, e] ▶* V2 →
-                   L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
-[ /2 width=1/
-| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
+lemma ltpss_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 →
+                             L1 [d1, e1] ▶* L0 → L0 ⊢ T2 [d2, e2] ▶* U2 →
+                             ∃∃T. L1 ⊢ T2 [d2, e2] ▶* T & L0 ⊢ T [d1, e1] ▶* U2.
+#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #HL10 #H @(tpss_ind … H) -U2
+[ /2 width=3/
+| #U #U2 #_ #HU2 * #T #HT2 #HTU
+  elim (tpss_strap1_down … HTU … HU2 ?) -U // #U #HTU #HU2
+  elim (ltpss_tps_trans … HTU … HL10) -HTU -HL10 #X #HTX #HXU
+  lapply (tpss_trans_eq … HXU HU2) -U /3 width=3/
 ]
 qed.
 
-lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
-                      L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 →
-                      0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
->(plus_minus_m_m d 1) // /2 width=1/
-qed.
+(* Main properties **********************************************************)
 
-fact ltps_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶ L1 →
-                    ∀K2,L2,d2,e2. K2 [d2, e2] ▶ L2 → K1 = K → K2 = K →
-                    ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
+fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶* L1 →
+                     ∀K2,L2,d2,e2. K2 [d2, e2] ▶* L2 → K1 = K → K2 = K →
+                     ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
 #K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
-[ -IH /3 width=3/
+[ -IH /2 width=3/
 | -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
   [ /2 width=3/
   | #K2 #I2 #V2 #H1 #H2 destruct /2 width=3/
-  | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /4 width=3/
-  | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /4 width=3/
+  | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
+  | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
   ]
 | #K1 #L1 #I1 #W1 #V1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
   [ -IH #d2 #e2 #H1 #H2 destruct
-  | -IH #K2 #I2 #V2 #H1 #H2 destruct
-    @ex2_1_intro [2,3: @inj ] /3 width=5/ (**) (* /4 width=5/ is too slow *)
+  | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
   | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
     elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
-    elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
-    elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+    elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+    elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
     elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
-    @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
-    [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
-    | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
-    ]
+    lapply (tpss_trans_eq … HVU1 HU1W) -U1
+    lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
   | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
     elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
-    elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
-    elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+    elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+    elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
     elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
-    @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
-    [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
-    | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
-    ]
+    lapply (tpss_trans_eq … HVU1 HU1W) -U1
+    lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
   ]
 | #K1 #L1 #I1 #W1 #V1 #d1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
   [ -IH #d2 #e2 #H1 #H2 destruct
-  | -IH #K2 #I2 #V2 #H1 #H2 destruct
-    @ex2_1_intro [2,3: @inj ] /3 width=5/ (**) (* /4 width=5/ is too slow *)
+  | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
   | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
     elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
-    elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
-    elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+    elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+    elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
     elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
-    @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
-    [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
-    | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
-    ]
+    lapply (tpss_trans_eq … HVU1 HU1W) -U1
+    lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
   | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
     elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
-    elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
-    elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+    elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+    elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
     elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
-    @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
-    [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
-    | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
-    ]
+    lapply (tpss_trans_eq … HVU1 HU1W) -U1
+    lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
   ]
 ]
 qed.
 
-lemma ltps_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶ L1 →
-                 ∀L2,d2,e2. L0 [d2, e2] ▶ L2 →
-                 ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
-/2 width=7/ qed.
-
-axiom ltpss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
+lemma ltpss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
                   ∀L2,d2,e2. L0 [d2, e2] ▶* L2 →
                   ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
-(*
-fact ltpss_conf_aux: ∀K1,L1,d1,e1. K1 [d1, e1] ▶* L1 →
-                     ∀K2,L2,d2,e2. K2 [d2, e2] ▶* L2 → K1 = K2 →
-                     ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
-#K1 #L1 #d1 #e1 #H @(ltpss_ind_dx … H) -K1 /2 width=3/
-#X1 #K1 #HXK1 #HKL1 #IHKL1 #K2 #L2 #d2 #e2 #H @(ltpss_ind_dx … H) -K2
-[ -IHKL1 #H destruct
-  lapply (ltpss_strap … HXK1 HKL1) -K1 /2 width=3/
-| #X2 #K2 #HXK2 #HKL2 #_ #H destruct
-  elim (ltps_conf … HXK1 … HXK2) -X2 #K #HK1 #HK2
-  elim (IHKL1 … HK1 ?) // -K1 #L #HL1 #HKL
-  @(ex2_1_intro … K) //
-*)
\ No newline at end of file
+/2 width=7/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma
new file mode 100644 (file)
index 0000000..9c670a8
--- /dev/null
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unfold/ltpss_ldrop.ma".
+
+(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************)
+
+(* Properties concerning partial substitution on terms **********************)
+
+lemma ltpss_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
+                         ∀L1,d1,e1. L0 [d1, e1] ▶* L1 → d1 + e1 ≤ d2 →
+                         L1 ⊢ T2 [d2, e2] ▶ U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ //
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
+  lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
+  lapply (ltpss_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /2 width=4/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
+  @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
+| /3 width=4/
+]
+qed.
+
+lemma ltpss_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
+                          ∀L1,d1,e1. L1 [d1, e1] ▶* L0 → d1 + e1 ≤ d2 →
+                          L1 ⊢ T2 [d2, e2] ▶ U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ //
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2
+  lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
+  lapply (ltpss_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2
+  @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
+| /3 width=4/
+]
+qed.
index 3e4dba50d49913349fe311ce84df035db638fdc6..2b1b8377c2f5c128f871e87917b1a9eeb2a7872c 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/tpss_ltps.ma".
-include "basic_2/unfold/ltpss.ma".
+include "basic_2/unfold/tpss_lift.ma".
+include "basic_2/unfold/ltpss_tps.ma".
 
-(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
+(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************)
 
 (* Properties concerning partial unfold on terms ****************************)
 
-lemma ltpss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
-                           ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 →
-                           d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2.
-#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 //
-#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
-lapply (ltps_tpss_trans_ge … HL0 HTU2) -HL0 -HTU2 /2 width=1/
-qed.
-
-lemma ltpss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
-                          ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
-                          d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2.
-#L1 #L0 #d1 #e1 #HL10 #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
-@(ltpss_tpss_trans_ge … HL10 … Hde1d2) /2 width=1/ (**) (* /3 width=6/ is too slow *)
-qed.
-
-lemma ltpss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶* L1 →
-                           ∀T2,U2. L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2.
-#L0 #L1 #d #e #H @(ltpss_ind … H) -L1
-[ /2 width=1/
-| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2
-  lapply (ltps_tpss_trans_eq … HL1 HTU2) -HL1 -HTU2 /2 width=1/
-]
-qed.
-
-lemma ltpss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶* L1 →
-                          ∀T2,U2. L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2.
-/3 width=3/ qed.
-
-lemma ltpss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → 
-                          L0 ⊢ T2 [d2, e2] ▶* U2 → L0 [d1, e1] ▶* L1 →
+lemma ltpss_tpss_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 →
+                          ∀L1,d1,e1. L0 [d1, e1] ▶* L1 → d1 + e1 ≤ d2 →
                           L1 ⊢ T2 [d2, e2] ▶* U2.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpss_ind … H) -L1
-[ //
-| -HTU2 #L #L1 #_ #HL1 #IHL
-  lapply (ltps_tpss_conf_ge … HL1 IHL) -HL1 -IHL //
-]
+#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU
+lapply (ltpss_tps_conf_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
 qed.
 
-lemma ltpss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → 
-                         L0 ⊢ T2 [d2, e2] ▶ U2 → L0 [d1, e1] ▶* L1 →
-                         L1 ⊢ T2 [d2, e2] ▶* U2.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #HL01
-@(ltpss_tpss_conf_ge … Hde1d2 … HL01) /2 width=1/ (**) (* /3 width=6/ is too slow *)
-qed.
-
-lemma ltpss_tpss_conf_eq: ∀L0,L1,T2,U2,d,e.
-                          L0 ⊢ T2 [d, e] ▶* U2 → L0 [d, e] ▶* L1 →
-                          ∃∃T. L1 ⊢ T2 [d, e] ▶* T & L1 ⊢ U2 [d, e] ▶* T.
-#L0 #L1 #T2 #U2 #d #e #HTU2 #H @(ltpss_ind … H) -L1
+(* Basic_1: was: subst1_subst1_back *)
+lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
+                      ∀L1,d1,e1. L0 [d1, e1] ▶* L1 →
+                      ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T &
+                           L1 ⊢ U2 [d1, e1] ▶* T.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
 [ /2 width=3/
-| -HTU2 #L #L1 #_ #HL1 * #W2 #HTW2 #HUW2
-  elim (ltps_tpss_conf … HL1 HTW2) -HTW2 #T #HT2 #HW2T
-  elim (ltps_tpss_conf … HL1 HUW2) -HL1 -HUW2 #U #HU2 #HW2U
-  elim (tpss_conf_eq … HW2T … HW2U) -HW2T -HW2U #V #HTV #HUV
-  lapply (tpss_trans_eq … HT2 … HTV) -T
-  lapply (tpss_trans_eq … HU2 … HUV) -U /2 width=3/
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
+  elim (lt_or_ge i2 d1) #Hi2d1
+  [ elim (ltpss_ldrop_conf_le … HL01 … HLK0 ?) -L0 /2 width=2/ #X #H #HLK1
+    elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+    lapply (ldrop_fwd_ldrop2 … HLK1) #H
+    elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+    lapply (tpss_lift_ge … HV01 … H HVW0 … HVW1) -V0 -H // >minus_plus <plus_minus_m_m // /3 width=4/
+  | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
+    [ elim (ltpss_ldrop_conf_be … HL01 … HLK0 ? ?) -L0 // /2 width=2/ #X #H #HLK1
+      elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+      lapply (ldrop_fwd_ldrop2 … HLK1) #H
+      elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+      lapply (tpss_lift_ge … HV01 … H HVW0 … HVW1) -V0 -H // normalize #HW01
+      lapply (tpss_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
+    | lapply (ltpss_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/
+    ]
+  ]
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
+  elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
+  elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
+  elim (IHVW2 … HL01) -IHVW2
+  elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
 ]
 qed.
-
-lemma ltpss_tps_conf_eq: ∀L0,L1,T2,U2,d,e.
-                         L0 ⊢ T2 [d, e] ▶ U2 → L0 [d, e] ▶* L1 →
-                         ∃∃T. L1 ⊢ T2 [d, e] ▶* T & L1 ⊢ U2 [d, e] ▶* T.
-/3 width=3/ qed.
-
-lemma ltpss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 →
-                       ∀L2,ds,es. L1 [ds, es] ▶* L2 → 
-                       ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T.
-#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpss_ind … H) -L2
-[ /3 width=3/
-| #L #L2 #HL1 #HL2 * #T #HT1 #HT2
-  elim (ltps_tpss_conf … HL2 HT1) -HT1 #T0 #HT10 #HT0
-  lapply (ltps_tpss_trans_eq … HL2 … HT0) -HL2 -HT0 #HT0
-  lapply (ltpss_tpss_trans_eq … HL1 … HT0) -HL1 -HT0 #HT0
-  lapply (tpss_trans_eq … HT2 … HT0) -T /2 width=3/
-]
+  
+lemma ltpss_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 →
+                           ∀L1,d1,e1. L1 [d1, e1] ▶* L0 → d1 + e1 ≤ d2 →
+                           L1 ⊢ T2 [d2, e2] ▶* U2.
+#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU
+lapply (ltpss_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
 qed.
 
-lemma ltpss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 →
-                      ∀L2,ds,es. L1 [ds, es] ▶* L2 → 
-                      ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T.
-/3 width=1/ qed.
-
-(* Advanced properties ******************************************************)
-
-lemma ltpss_tps2: ∀L1,L2,I,e.
-                  L1 [0, e] ▶* L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ▶ V2 →
-                  L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2.
-#L1 #L2 #I #e #H @(ltpss_ind … H) -L2
-[ /3 width=1/
-| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
-  elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
-  lapply (IHL … HV1) -IHL -HV1 #HL1
-  @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+(* Basic_1: was: subst1_subst1 *)
+lemma ltpss_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
+                       ∀L1,d1,e1. L1 [d1, e1] ▶* L0 →
+                       ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T &
+                            L0 ⊢ T [d1, e1] ▶* U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ /2 width=3/
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10
+  elim (lt_or_ge i2 d1) #Hi2d1
+  [ elim (ltpss_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=2/ #X #H #HLK1
+    elim (ltpss_inv_tpss12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+    lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
+    elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+    lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // >minus_plus <plus_minus_m_m /2 width=1/ /3 width=4/
+  | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
+    [ elim (ltpss_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 // /2 width=2/ #X #H #HLK1
+      elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+      lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
+      elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+      lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // normalize #HW01
+      lapply (tpss_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
+    | lapply (ltpss_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/
+    ]
+  ]
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
+  elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
+  elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
+  elim (IHVW2 … HL10) -IHVW2
+  elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/
 ]
 qed.
 
-lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e.
-                     L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
-                     0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(plus_minus_m_m e 1) // /2 width=1/
-qed.
-
-lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶* L2 →
-                  ∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 →
-                  L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2.
-#L1 #L2 #I #d #e #H @(ltpss_ind … H) -L2
-[ /3 width=1/
-| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
-  elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
-  lapply (IHL … HV1) -IHL -HV1 #HL1
-  @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+fact ltpss_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
+                             L1 ⊢ T2 [d, e] ▶ U2 → ∀L0. L0 [d, e] ▶* L1 →
+                             Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ▶* U2.
+#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
+#L1 #T2 #U2 #d #e * -L1 -T2 -U2 -d -e
+[ //
+| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct
+  lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
+  elim (ltpss_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0
+  elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
+  lapply (tpss_fwd_tw … HV01) #H2
+  lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H
+  lapply (IH … HV01 … HK01 ? ?) -IH -HV01 -HK01
+  [1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ]
+| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
+  lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
+  lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
+  lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
+  lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
+| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
+  lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
+  lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
 ]
 qed.
 
-lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
-                     L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 →
-                     0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
->(plus_minus_m_m d 1) // /2 width=1/
-qed.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. ⓑ{I} V1 [0, e] ▶* L2 →
-                        ∃∃K2,V2. K1 [0, e - 1] ▶* K2 & K1 ⊢ V1 [0, e - 1] ▶* V2 &
-                                 L2 = K2. ⓑ{I} V2.
-#e #K1 #I #V1 #L2 #He #H @(ltpss_ind … H) -L2
-[ /2 width=5/
-| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
-  elim (ltps_inv_tps21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
-  lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
-  lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
-]
-qed-.
+lemma ltps_tps_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 [d, e] ▶ U2 →
+                         ∀L0. L0 [d, e] ▶ L1 → L0 ⊢ T2 [d, e] ▶* U2.
+/2 width=5/ qed.
 
-lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. ⓑ{I} V1 [d, e] ▶* L2 →
-                        ∃∃K2,V2. K1 [d - 1, e] ▶* K2 &
-                                 K1 ⊢ V1 [d - 1, e] ▶* V2 &
-                                 L2 = K2. ⓑ{I} V2.
-#d #e #K1 #I #V1 #L2 #Hd #H @(ltpss_ind … H) -L2
-[ /2 width=5/
-| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
-  elim (ltps_inv_tps11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
-  lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
-  lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
-]
-qed-.
+lemma ltps_tpss_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ▶ L1 →
+                          L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2.
+#L0 #L1 #T2 #U2 #d #e #HL01 #H @(tpss_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU @(tpss_trans_eq … IHU) /2 width=3/
+qed.
+*)
index 707e469596d8d1a2213280446efc597b7b8fd557..fc74d802ca9a48c1f790a4db731287a990be849c 100644 (file)
@@ -144,3 +144,12 @@ lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ▶* T2 → T1 = T2.
 | #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 //
 ]
 qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → #[T1] ≤ #[T2].
+#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1
+lapply (tps_fwd_tw … HT2) -HT2 #HT2
+@(transitive_le … IHT1) //
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_ltps.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_ltps.ma
deleted file mode 100644 (file)
index efaf3f5..0000000
+++ /dev/null
@@ -1,95 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/ltps_tps.ma".
-include "basic_2/unfold/tpss_tpss.ma".
-
-(* PARTIAL UNFOLD ON TERMS **************************************************)
-
-(* Properties concerning parallel substitution on local environments ********)
-
-lemma ltps_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2.
-                         d1 + e1 ≤ d2 → L0 [d1, e1] ▶ L1 →
-                         L0 ⊢ T2 [d2, e2] ▶* U2 → L1 ⊢ T2 [d2, e2] ▶* U2.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HL01 #H @(tpss_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU
-lapply (ltps_tps_conf_ge … HU2 … HL01 ?) -HU2 -HL01 // /2 width=3/
-qed.
-
-lemma ltps_tpss_conf: ∀L0,L1,T2,U2,d1,e1,d2,e2.
-                      L0 [d1, e1] ▶ L1 → L0 ⊢ T2 [d2, e2] ▶* U2 →
-                      ∃∃T. L1 ⊢ T2 [d2, e2] ▶* T & L1 ⊢ U2 [d1, e1] ▶* T.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #HL01 #H @(tpss_ind … H) -U2
-[ /3 width=3/
-| #U #U2 #_ #HU2 * #T #HT2 #HUT
-  elim (ltps_tps_conf … HU2 … HL01) -HU2 -HL01 #W #HUW #HU2W
-  elim (tpss_strip_eq … HUT … HUW) -U
-  /3 width=5 by ex2_1_intro, step, tpss_strap/ (**) (* just /3 width=5/ is too slow *)
-]
-qed.
-
-lemma ltps_tpss_trans_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2.
-                          d1 + e1 ≤ d2 → L1 [d1, e1] ▶ L0 →
-                          L0 ⊢ T2 [d2, e2] ▶* U2 → L1 ⊢ T2 [d2, e2] ▶* U2.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HL10 #H @(tpss_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU
-lapply (ltps_tps_trans_ge … HU2 … HL10 ?) -HU2 -HL10 // /2 width=3/
-qed.
-
-lemma ltps_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 →
-                            L1 [d1, e1] ▶ L0 → L0 ⊢ T2 [d2, e2] ▶* U2 →
-                            ∃∃T. L1 ⊢ T2 [d2, e2] ▶* T & L0 ⊢ T [d1, e1] ▶* U2.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #HL10 #H @(tpss_ind … H) -U2
-[ /3 width=3/
-| #U #U2 #_ #HU2 * #T #HT2 #HTU
-  elim (tpss_strap1_down … HTU … HU2 ?) -U // #U #HTU #HU2
-  elim (ltps_tps_trans … HTU … HL10) -HTU -HL10 #W #HTW #HWU
-  @(ex2_1_intro … W) /2 width=3/ (**) (* /3 width=5/ does not work as in ltps_tpss_conf *)
-]
-qed.
-
-fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
-                            L1 ⊢ T2 [d, e] ▶ U2 → ∀L0. L0 [d, e] ▶ L1 →
-                            Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ▶* U2.
-#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
-#L1 #T2 #U2 #d #e * -L1 -T2 -U2 -d -e
-[ //
-| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct
-  lapply (ldrop_fwd_lw … HLK1) normalize #H1
-  elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0
-  elim (ltps_inv_tps22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
-  lapply (tps_fwd_tw … HV01) #H2
-  lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H
-  lapply (IH … HV01 … HK01 ? ?) -IH -HV01 -HK01
-  [1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ]
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
-  lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
-  lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
-  lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
-  lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
-  lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
-  lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
-]
-qed.
-
-lemma ltps_tps_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 [d, e] ▶ U2 →
-                         ∀L0. L0 [d, e] ▶ L1 → L0 ⊢ T2 [d, e] ▶* U2.
-/2 width=5/ qed.
-
-lemma ltps_tpss_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ▶ L1 →
-                          L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2.
-#L0 #L1 #T2 #U2 #d #e #HL01 #H @(tpss_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU @(tpss_trans_eq … IHU) /2 width=3/
-qed.