(* Advanced properties ******************************************************)
-lemma ltprs_strip: ∀L1. ∀L:term. L ➡* L1 → ∀L2. L ➡ L2 →
+lemma ltprs_strip: ∀L1. ∀L:lenv. L ➡* L1 → ∀L2. L ➡ L2 →
∃∃L0. L1 ➡ L0 & L2 ➡* L0.
/3 width=3/ qed.
(* Basic_1: was: pr1_strip *)
lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 →
∃∃T0. T1 ➡ T0 & T2 ➡* T0.
-/3 width=3/ qed.
+/3 width=3 by TC_strip1, tpr_conf/ qed.
(* Main propertis ***********************************************************)
-(**************************************************************************)
-(* ___ *)
-(* ||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 T1 ⦄ > break ⦃ L2 , break T2 ⦄ )"
- non associative with precedence 45
- for @{ 'SupTerm $L1 $T1 $L2 $T2 }.
-
-include "basic_2/substitution/ldrop.ma".
-
-(* SUPCLOSURE ***************************************************************)
-
-inductive csup: bi_relation lenv term ≝
-| csup_lref : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → csup L (#i) K V
-| csup_bind_sn: ∀a,I,L,V,T. csup L (ⓑ{a,I}V.T) L V
-| csup_bind_dx: ∀a,I,L,V,T. csup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
-| csup_flat_sn: ∀I,L,V,T. csup L (ⓕ{I}V.T) L V
-| csup_flat_dx: ∀I,L,V,T. csup L (ⓕ{I}V.T) L T
-.
-
-interpretation
- "structural predecessor (closure)"
- 'SupTerm L1 T1 L2 T2 = (csup L1 T1 L2 T2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact csup_inv_atom1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ∀J. T1 = ⓪{J} →
- ∃∃I,i. ⇩[0, i] L1 ≡ L2.ⓑ{I}T2 & J = LRef i.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #I #L #K #V #i #HLK #J #H destruct /2 width=4/
-| #a #I #L #V #T #J #H destruct
-| #a #I #L #V #T #J #H destruct
-| #I #L #V #T #J #H destruct
-| #I #L #V #T #J #H destruct
-]
-qed-.
-
-lemma csup_inv_atom1: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ > ⦃L2, T2⦄ →
- ∃∃I,i. ⇩[0, i] L1 ≡ L2.ⓑ{I}T2 & J = LRef i.
-/2 width=3 by csup_inv_atom1_aux/ qed-.
-
-fact csup_inv_bind1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
- ∀b,J,W,U. T1 = ⓑ{b,J}W.U →
- (L2 = L1 ∧ T2 = W) ∨
- (L2 = L1.ⓑ{J}W ∧ T2 = U).
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #I #L #K #V #i #_ #b #J #W #U #H destruct
-| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
-| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
-| #I #L #V #T #b #J #W #U #H destruct
-| #I #L #V #T #b #J #W #U #H destruct
-]
-qed-.
-
-lemma csup_inv_bind1: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ > ⦃L2, T2⦄ →
- (L2 = L1 ∧ T2 = W) ∨
- (L2 = L1.ⓑ{J}W ∧ T2 = U).
-/2 width=4 by csup_inv_bind1_aux/ qed-.
-
-fact csup_inv_flat1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
- ∀J,W,U. T1 = ⓕ{J}W.U →
- L2 = L1 ∧ (T2 = W ∨ T2 = U).
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #I #L #K #V #i #_ #J #W #U #H destruct
-| #a #I #L #V #T #J #W #U #H destruct
-| #a #I #L #V #T #J #W #U #H destruct
-| #I #L #V #T #J #W #U #H destruct /3 width=1/
-| #I #L #V #T #J #W #U #H destruct /3 width=1/
-]
-qed-.
-
-lemma csup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ > ⦃L2, T2⦄ →
- L2 = L1 ∧ (T2 = W ∨ T2 = U).
-/2 width=4 by csup_inv_flat1_aux/ qed-.
-
(* Basic forward lemmas *****************************************************)
-lemma csup_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=4 by ldrop_pair2_fwd_cw/
-qed-.
-
lemma csup_fwd_ldrop: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
∃i. ⇩[0, i] L1 ≡ L2 ∨ ⇩[0, i] L2 ≡ L1.
#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /3 width=2/ /4 width=2/
elim (lift_csup_trans_eq … HTU … H) -H -T #T #H
elim (lift_inv_lref2_be … H ? ?) //
qed-.
+
+
+fact csup_inv_all4_refl_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → L1 = L2 →
+ ∨∨ ∃∃a,I,U. T1 = ⓑ{a,I}T2.U
+ | ∃∃I,W. T1 = ⓕ{I}W.T2
+ | ∃∃I,U. T1 = ⓕ{I}T2.U.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /3 width=3/ /3 width=4/
+[ #I #L #K #V #i #HLK #H destruct
+ lapply (ldrop_pair2_fwd_cw … HLK V) -HLK #H
+ elim (lt_refl_false … H)
+| #a #I #L #V #T #H
+ elim (discr_lpair_x_xy … H)
+]
+qed-.
+
+lemma csup_inv_all4_refl: ∀L,T1,T2. ⦃L, T1⦄ > ⦃L, T2⦄ →
+ ∨∨ ∃∃a,I,U. T1 = ⓑ{a,I}T2.U
+ | ∃∃I,W. T1 = ⓕ{I}W.T2
+ | ∃∃I,U. T1 = ⓕ{I}T2.U.
+/2 width=4 by csup_inv_all4_refl_aux/ qed-.
(* SUPCLOSURE ***************************************************************)
-(* Advanced inversion lemmas ************************************************)
-
-lemma csup_inv_ldrop: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
- ∀J,W,j. ⇩[0, j] L1 ≡ L2.ⓑ{J}W → T1 = #j ∧ T2 = W.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #I #L #K #V #i #HLKV #J #W #j #HLKW
- elim (ldrop_conf_div … HLKV … HLKW) -L /2 width=1/
-| #a
-| #a
-]
-#I #L #V #T #J #W #j #H
-lapply (ldrop_pair2_fwd_cw … H W) -H #H
-[2: lapply (transitive_lt (#{L,W}) … H) /2 width=1/ -H #H ]
-elim (lt_refl_false … H)
-qed-.
-
(* Main forward lemmas ******************************************************)
theorem csup_trans_fwd_refl: ∀L,L0,T1,T2. ⦃L, T1⦄ > ⦃L0, 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( ⦃ L1, break T1 ⦄ > + break ⦃ L2 , break T2 ⦄ )"
- non associative with precedence 45
- for @{ 'SupTermPlus $L1 $T1 $L2 $T2 }.
-
-include "basic_2/substitution/csup.ma".
-
-(* PLUS-ITERATED SUPCLOSURE *************************************************)
-
-definition csupp: bi_relation lenv term ≝ bi_TC … csup.
-
-interpretation "plus-iterated structural predecessor (closure)"
- 'SupTermPlus L1 T1 L2 T2 = (csupp L1 T1 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma csupp_ind: ∀L1,T1. ∀R:relation2 lenv term.
- (∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → R L2 T2) →
- (∀L,T,L2,T2. ⦃L1, T1⦄ >+ ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ → R L T → R L2 T2) →
- ∀L2,T2. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → R L2 T2.
-#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
-@(bi_TC_ind … IH1 IH2 ? ? H)
-qed-.
-
-lemma csupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
- (∀L1,T1. ⦃L1, T1⦄ > ⦃L2, T2⦄ → R L1 T1) →
- (∀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.
-#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
-@(bi_TC_ind_dx … IH1 IH2 ? ? H)
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma csup_csupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ⦃L1, T1⦄ >+ ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma csupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >+ ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ →
- ⦃L1, T1⦄ >+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma csupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >+ ⦃L2, T2⦄ →
- ⦃L1, T1⦄ >+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma csupp_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
-#L1 #L2 #T1 #T2 #H @(csupp_ind … H) -L2 -T2
-/3 width=3 by csup_fwd_cw, transitive_lt/
-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/unfold/csupp.ma".
-
-(* PLUS-ITERATED SUPCLOSURE *************************************************)
-
-(* Main propertis ***********************************************************)
-
-theorem csupp_trans: bi_transitive … csupp.
-/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 *)
-(* *)
-(**************************************************************************)
-
-notation "hvbox( ⦃ L1, break T1 ⦄ > * break ⦃ L2 , break T2 ⦄ )"
- non associative with precedence 45
- for @{ 'SupTermStar $L1 $T1 $L2 $T2 }.
-
-include "basic_2/substitution/csup.ma".
-include "basic_2/unfold/csupp.ma".
-
-(* STAR-ITERATED SUPCLOSURE *************************************************)
-
-definition csups: bi_relation lenv term ≝ bi_star … csup.
-
-interpretation "star-iterated structural predecessor (closure)"
- 'SupTermStar L1 T1 L2 T2 = (csups L1 T1 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma csups_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.
-#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
-@(bi_star_ind … IH1 IH2 ? ? H)
-qed-.
-
-lemma csups_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.
-#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
-@(bi_star_ind_dx … IH1 IH2 ? ? H)
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma csups_refl: bi_reflexive … csups.
-/2 width=1/ qed.
-
-lemma csupp_csups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → ⦃L1, T1⦄ >* ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma csup_csups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ⦃L1, T1⦄ >* ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma csups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ →
- ⦃L1, T1⦄ >* ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma csups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >* ⦃L2, T2⦄ →
- ⦃L1, T1⦄ >* ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma csups_csupp_csupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ →
- ⦃L, T⦄ >+ ⦃L2, T2⦄ → ⦃L1, T1⦄ >+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma csupp_csups_csupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >+ ⦃L, T⦄ →
- ⦃L, T⦄ >* ⦃L2, T2⦄ → ⦃L1, T1⦄ >+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma csups_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → #{L2, T2} ≤ #{L1, T1}.
-#L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2 //
-/4 width=3 by csup_fwd_cw, lt_to_le_to_lt, lt_to_le/ (**) (* slow even with trace *)
-qed-.
-
-(* Advanced inversion lemmas for csupp **************************************)
-
-lemma csupp_inv_atom1_csups: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ >+ ⦃L2, T2⦄ →
- ∃∃I,K,V,i. ⇩[0, i] L1 ≡ K.ⓑ{I}V &
- ⦃K, V⦄ >* ⦃L2, T2⦄ & J = LRef i.
-#J #L1 #L2 #T2 #H @(csupp_ind … H) -L2 -T2
-[ #L2 #T2 #H
- elim (csup_inv_atom1 … H) -H * #i #HL12 #H destruct /2 width=7/
-| #L #T #L2 #T2 #_ #HT2 * #I #K #V #i #HLK #HVT #H destruct /3 width=8/
-]
-qed-.
-
-lemma csupp_inv_bind1_csups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ >+ ⦃L2, T2⦄ →
- ⦃L1, W⦄ >* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ >* ⦃L2, T2⦄.
-#b #J #L1 #L2 #W #U #T2 #H @(csupp_ind … H) -L2 -T2
-[ #L2 #T2 #H
- elim (csup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/
-| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
-]
-qed-.
-
-lemma csupp_inv_flat1_csups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ >+ ⦃L2, T2⦄ →
- ⦃L1, W⦄ >* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ >* ⦃L2, T2⦄.
-#J #L1 #L2 #W #U #T2 #H @(csupp_ind … H) -L2 -T2
-[ #L2 #T2 #H
- elim (csup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/
-| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
-]
-qed-.
#L #L2 #U #U2 #HL1 #HL2 #IHL1 #H destruct
* -T1 -U1 -d -e
-
-(* Main propertis ***********************************************************)
-
-theorem csups_trans: bi_transitive … csups.
-/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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'RestSupTerm $L1 $T1 $L2 $T2 }.
+
+include "basic_2/grammar/cl_weight.ma".
+include "basic_2/substitution/lift.ma".
+
+(* RESTRICTED SUPCLOSURE ****************************************************)
+
+inductive frsup: bi_relation lenv term ≝
+| frsup_bind_sn: ∀a,I,L,V,T. frsup L (ⓑ{a,I}V.T) L V
+| frsup_bind_dx: ∀a,I,L,V,T. frsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
+| frsup_flat_sn: ∀I,L,V,T. frsup L (ⓕ{I}V.T) L V
+| frsup_flat_dx: ∀I,L,V,T. frsup L (ⓕ{I}V.T) L T
+.
+
+interpretation
+ "restricted structural predecessor (closure)"
+ 'RestSupTerm L1 T1 L2 T2 = (frsup L1 T1 L2 T2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact frsup_inv_atom1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ →
+ ∀J. T1 = ⓪{J} → ⊥.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #a #I #L #V #T #J #H destruct
+| #a #I #L #V #T #J #H destruct
+| #I #L #V #T #J #H destruct
+| #I #L #V #T #J #H destruct
+]
+qed-.
+
+lemma frsup_inv_atom1: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⧁ ⦃L2, T2⦄ → ⊥.
+/2 width=7 by frsup_inv_atom1_aux/ qed-.
+
+fact frsup_inv_bind1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ →
+ ∀b,J,W,U. T1 = ⓑ{b,J}W.U →
+ (L2 = L1 ∧ T2 = W) ∨
+ (L2 = L1.ⓑ{J}W ∧ T2 = U).
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
+| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
+| #I #L #V #T #b #J #W #U #H destruct
+| #I #L #V #T #b #J #W #U #H destruct
+]
+qed-.
+
+lemma frsup_inv_bind1: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⧁ ⦃L2, T2⦄ →
+ (L2 = L1 ∧ T2 = W) ∨
+ (L2 = L1.ⓑ{J}W ∧ T2 = U).
+/2 width=4 by frsup_inv_bind1_aux/ qed-.
+
+fact frsup_inv_flat1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ →
+ ∀J,W,U. T1 = ⓕ{J}W.U →
+ L2 = L1 ∧ (T2 = W ∨ T2 = U).
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #a #I #L #V #T #J #W #U #H destruct
+| #a #I #L #V #T #J #W #U #H destruct
+| #I #L #V #T #J #W #U #H destruct /3 width=1/
+| #I #L #V #T #J #W #U #H destruct /3 width=1/
+]
+qed-.
+
+lemma frsup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⧁ ⦃L2, T2⦄ →
+ L2 = L1 ∧ (T2 = W ∨ T2 = U).
+/2 width=4 by frsup_inv_flat1_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma frsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/
+qed-.
+
+lemma frsup_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/
+qed-.
+
+lemma frsup_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=1 by le_minus_to_plus/
+qed-.
+
+lemma frsup_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #a
+| #a #I #L #V #_ @(ex_intro … (⋆.ⓑ{I}V)) //
+]
+#I #L #V #T @(ex_intro … (⋆)) //
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lift_frsup_trans: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
+ ∀L,K,U2. ⦃L, U1⦄ ⧁ ⦃L @@ K, U2⦄ →
+ ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
+#T1 #U1 #d #e * -T1 -U1 -d -e
+[5: #a #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HTU1 #L #K #X #H
+ elim (frsup_inv_bind1 … H) -H *
+ [ -HTU1 #H1 #H2 destruct
+ >(append_inv_refl_dx … H1) -L -K normalize /2 width=2/
+ | -HVW1 #H1 #H2 destruct
+ >(append_inv_pair_dx … H1) -L -K normalize /2 width=2/
+ ]
+|6: #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HUT1 #L #K #X #H
+ elim (frsup_inv_flat1 … H) -H #H1 * #H2 destruct
+ >(append_inv_refl_dx … H1) -L -K normalize /2 width=2/
+]
+#i #d #e [2,3: #_ ] #L #K #X #H
+elim (frsup_inv_atom1 … 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( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ + break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'RestSupTermPlus $L1 $T1 $L2 $T2 }.
+
+include "basic_2/substitution/frsup.ma".
+
+(* PLUS-ITERATED RESTRICTED SUPCLOSURE **************************************)
+
+definition frsupp: bi_relation lenv term ≝ bi_TC … frsup.
+
+interpretation "plus-iterated restricted structural predecessor (closure)"
+ 'RestSupTermPlus L1 T1 L2 T2 = (frsupp L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma frsupp_ind: ∀L1,T1. ∀R:relation2 lenv term.
+ (∀L2,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → R L2 T2) →
+ (∀L,T,L2,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ → R L T → R L2 T2) →
+ ∀L2,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → R L2 T2.
+#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
+@(bi_TC_ind … IH1 IH2 ? ? H)
+qed-.
+
+lemma frsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
+ (∀L1,T1. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → R L1 T1) →
+ (∀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.
+#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
+@(bi_TC_ind_dx … IH1 IH2 ? ? H)
+qed-.
+
+(* Baic inversion lemmas ****************************************************)
+
+lemma frsupp_inv_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨
+ ∃∃L,T. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ & ⦃L, T⦄ ⧁ ⦃L2, T2⦄.
+/2 width=1 by bi_TC_decomp_r/ qed-.
+
+lemma frsupp_inv_sn: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨
+ ∃∃L,T. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ & ⦃L, T⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=1 by bi_TC_decomp_l/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma frsup_frsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma frsupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma frsupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ → ⦃L, T⦄ ⧁+ ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma frsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
+#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
+/3 width=3 by frsup_fwd_fw, transitive_lt/
+qed-.
+
+lemma frsupp_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}.
+#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
+/2 width=3 by frsup_fwd_lw/ (**) (* /3 width=5 by frsup_fwd_lw, transitive_le/ is too slow *)
+#L #T #L2 #T2 #_ #HL2 #HL1
+lapply (frsup_fwd_lw … HL2) -HL2 /2 width=3 by transitive_le/
+qed-.
+
+lemma frsupp_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}.
+#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
+/3 width=3 by frsup_fwd_tw, transitive_lt/
+qed-.
+
+lemma frsupp_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L.
+#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 /2 width=3 by frsup_fwd_append/
+#L #T #L2 #T2 #_ #HL2 * #K1 #H destruct
+elim (frsup_fwd_append … HL2) -HL2 #K2 #H destruct /2 width=2/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lift_frsupp_trans: ∀L,U1,K,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ →
+ ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
+ ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
+#L #U1 @(f2_ind … fw … L U1) -L -U1 #n #IH
+#L #U1 #Hn #K #U2 #H #T1 #d #e #HTU1 destruct
+elim (frsupp_inv_sn … H) -H /2 width=5 by lift_frsup_trans/ *
+#L0 #U0 #HL0 #HL
+elim (frsup_fwd_append … HL0) #K0 #H destruct
+elim (frsupp_fwd_append … HL) #L0 >append_assoc #H
+elim (append_inj_dx … H ?) -H // #_ #H destruct
+<append_assoc in HL; #HL
+elim (lift_frsup_trans … HTU1 … HL0) -T1 #T #HTU
+lapply (frsup_fwd_fw … HL0) -HL0 #HL0
+elim (IH … HL … HTU) -IH -HL -T // -L -U1 -U0 /2 width=2/
+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/unfold/frsupp.ma".
+
+(* PLUS-ITERATED RESTRICTED SUPCLOSURE **************************************)
+
+(* Main propertis ***********************************************************)
+
+theorem frsupp_trans: bi_transitive … frsupp.
+/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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'RestSupTermStar $L1 $T1 $L2 $T2 }.
+
+include "basic_2/unfold/frsupp.ma".
+
+(* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************)
+
+definition frsups: bi_relation lenv term ≝ bi_star … frsup.
+
+interpretation "star-iterated restricted structural predecessor (closure)"
+ 'RestSupTermStar L1 T1 L2 T2 = (frsups L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma frsups_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.
+#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
+@(bi_star_ind … IH1 IH2 ? ? H)
+qed-.
+
+lemma frsups_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.
+#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
+@(bi_star_ind_dx … IH1 IH2 ? ? H)
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma frsups_refl: bi_reflexive … frsups.
+/2 width=1/ qed.
+
+lemma frsupp_frsups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma frsup_frsups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma frsups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁* ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma frsups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ → ⦃L, T⦄ ⧁* ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma frsups_frsupp_frsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁* ⦃L, T⦄ →
+ ⦃L, T⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma frsupp_frsups_frsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ →
+ ⦃L, T⦄ ⧁* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma frsups_inv_all: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ →
+ (L1 = L2 ∧ T1 = T2) ∨ ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+#L1 #L2 #T1 #T2 * /2 width=1/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma frsups_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}.
+#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
+/3 width=1 by frsupp_fwd_fw, lt_to_le/
+qed-.
+
+lemma frsups_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}.
+#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
+/2 width=3 by frsupp_fwd_lw/
+qed-.
+
+lemma frsups_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{T2} ≤ ♯{T1}.
+#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
+/3 width=3 by frsupp_fwd_tw, lt_to_le/
+qed-.
+
+lemma frsups_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L.
+#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H
+[ * #H1 #H2 destruct
+ @(ex_intro … (⋆)) //
+| /2 width=3 by frsupp_fwd_append/
+qed-.
+
+(* Advanced forward lemmas ***************************************************)
+
+lemma lift_frsups_trans: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
+ ∀L,K,U2. ⦃L, U1⦄ ⧁* ⦃L @@ K, U2⦄ →
+ ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
+#T1 #U1 #d #e #HTU1 #L #K #U2 #H elim (frsups_inv_all … H) -H
+[ * #H1 #H2 destruct
+ >(append_inv_refl_dx … (sym_eq … H1)) -H1 normalize /2 width=2/
+| /2 width=5 by lift_frsupp_trans/
+]
+qed-.
+
+(* Advanced inversion lemmas for frsupp **************************************)
+
+lemma frsupp_inv_atom1_frsups: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⧁+ ⦃L2, T2⦄ → ⊥.
+#J #L1 #L2 #T2 #H @(frsupp_ind … H) -L2 -T2 //
+#L2 #T2 #H elim (frsup_inv_atom1 … H)
+qed-.
+
+lemma frsupp_inv_bind1_frsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⧁+ ⦃L2, T2⦄ →
+ ⦃L1, W⦄ ⧁* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⧁* ⦃L2, T2⦄.
+#b #J #L1 #L2 #W #U #T2 #H @(frsupp_ind … H) -L2 -T2
+[ #L2 #T2 #H
+ elim (frsup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/
+| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
+]
+qed-.
+
+lemma frsupp_inv_flat1_frsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⧁+ ⦃L2, T2⦄ →
+ ⦃L1, W⦄ ⧁* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ ⧁* ⦃L2, T2⦄.
+#J #L1 #L2 #W #U #T2 #H @(frsupp_ind … H) -L2 -T2
+[ #L2 #T2 #H
+ elim (frsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/
+| #L #T #L2 #T2 #_ #HT2 * /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/unfold/frsups.ma".
+
+(* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************)
+
+(* Main propertis ***********************************************************)
+
+theorem frsups_trans: bi_transitive … frsups.
+/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/unfold/frsups.ma".
+include "basic_2/static/ssta.ma".
+
+(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥.
+#h #g #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #l #_ #H
+ elim (frsupp_inv_atom1_frsups … H)
+| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H
+ elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H
+ elim (lift_inv_lref2_be … H ? ?) -H //
+| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H
+ elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H
+ elim (lift_inv_lref2_be … H ? ?) -H //
+| #a #I #L #V #T #U #l #_ #IHTU #H
+ elim (frsupp_inv_bind1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU
+ lapply (frsups_fwd_fw … H) -H normalize
+ <associative_plus <associative_plus #H
+ elim (le_plus_xySz_x_false … H)
+| #L #V #T #U #l #_ #IHTU #H
+ elim (frsupp_inv_flat1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU
+ lapply (frsups_fwd_fw … H) -H normalize
+ <associative_plus <associative_plus #H
+ elim (le_plus_xySz_x_false … H)
+| /3 width=4/
+]
+qed-.
+
+fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → T = U → ⊥.
+#h #g #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #l #_ #H
+ lapply (next_lt h k) destruct -H -e0 (**) (* destruct: these premises are not erased *)
+ <e1 -e1 #H elim (lt_refl_false … H)
+| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H destruct
+ elim (lift_inv_lref2_be … HWU ? ?) -HWU //
+| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H destruct
+ elim (lift_inv_lref2_be … HWU ? ?) -HWU //
+| #a #I #L #V #T #U #l #_ #IHTU #H destruct /2 width=1/
+| #L #V #T #U #l #_ #IHTU #H destruct /2 width=1/
+| #L #W #T #U #l #HTU #_ #H destruct
+ elim (ssta_inv_frsupp … HTU ?) -HTU /2 width=1/
+]
+qed-.
+
+lemma ssta_inv_refl: ∀h,g,T,L,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, T⦄ → ⊥.
+/2 width=8 by ssta_inv_refl_aux/ qed-.
+
+lemma ssta_inv_frsups: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁* ⦃L, T⦄ → ⊥.
+#h #g #L #T #U #L #HTU #H elim (frsups_inv_all … H) -H
+[ * #_ #H destruct /2 width=6 by ssta_inv_refl/
+| /2 width=8 by ssta_inv_frsupp/
+]
+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/ldrop.ma".
+
+(* SUPCLOSURE ***************************************************************)
+
+(* Basic inversion lemmas ***************************************************)
+
+fact fsup_inv_atom1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀J. T1 = ⓪{J} →
+ (∃∃I,K,V. L1 = K.ⓑ{I}V & J = LRef 0 & L2 = K & T2 = V) ∨
+ ∃∃I,K,V,i. ⦃K, #i⦄ ⊃ ⦃L2, T2⦄ & L1 = K.ⓑ{I}V & J = LRef (i+1).
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #I #L #V #J #H destruct /3 width=6/
+| #I #L #K #V #T #i #HLK #J #H destruct /3 width=7/
+| #a #I #L #V #T #J #H destruct
+| #a #I #L #V #T #J #H destruct
+| #I #L #V #T #J #H destruct
+| #I #L #V #T #J #H destruct
+]
+qed-.
+
+lemma fsup_inv_atom1: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⊃ ⦃L2, T2⦄ →
+ (∃∃I,K,V. L1 = K.ⓑ{I}V & J = LRef 0 & L2 = K & T2 = V) ∨
+ ∃∃I,K,V,i. ⦃K, #i⦄ ⊃ ⦃L2, T2⦄ & L1 = K.ⓑ{I}V & J = LRef (i+1).
+/2 width=3 by fsup_inv_atom1_aux/ qed-.
+
+fact fsup_inv_bind1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+ ∀b,J,W,U. T1 = ⓑ{b,J}W.U →
+ (L2 = L1 ∧ T2 = W) ∨
+ (L2 = L1.ⓑ{J}W ∧ T2 = U).
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #I #L #V #b #J #W #U #H destruct
+| #I #L #K #V #T #i #_ #b #J #W #U #H destruct
+| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
+| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
+| #I #L #V #T #b #J #W #U #H destruct
+| #I #L #V #T #b #J #W #U #H destruct
+]
+qed-.
+
+lemma fsup_inv_bind1: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⊃ ⦃L2, T2⦄ →
+ (L2 = L1 ∧ T2 = W) ∨
+ (L2 = L1.ⓑ{J}W ∧ T2 = U).
+/2 width=4 by fsup_inv_bind1_aux/ qed-.
+
+fact fsup_inv_flat1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+ ∀J,W,U. T1 = ⓕ{J}W.U →
+ L2 = L1 ∧ (T2 = W ∨ T2 = U).
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #I #L #K #J #W #U #H destruct
+| #I #L #K #V #T #i #_ #J #W #U #H destruct
+| #a #I #L #V #T #J #W #U #H destruct
+| #a #I #L #V #T #J #W #U #H destruct
+| #I #L #V #T #J #W #U #H destruct /3 width=1/
+| #I #L #V #T #J #W #U #H destruct /3 width=1/
+]
+qed-.
+
+lemma fsup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⊃ ⦃L2, T2⦄ →
+ L2 = L1 ∧ (T2 = W ∨ T2 = U).
+/2 width=4 by fsup_inv_flat1_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/fsupp.ma".
+
+(* STAR-ITERATED SUPCLOSURE *************************************************)
+
+definition fsups: bi_relation lenv term ≝ bi_star … fsup.
+
+interpretation "star-iterated structural successor (closure)"
+ 'SupTermStar L1 T1 L2 T2 = (fsups L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma fsups_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.
+#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
+@(bi_star_ind … IH1 IH2 ? ? H)
+qed-.
+
+lemma fsups_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.
+#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
+@(bi_star_ind_dx … IH1 IH2 ? ? H)
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fsups_refl: bi_reflexive … fsups.
+/2 width=1/ qed.
+
+lemma fsupp_fsups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma fsup_fsups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma fsups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃* ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fsups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃* ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fsups_fsupp_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃* ⦃L, T⦄ →
+ ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fsupp_fsups_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ →
+ ⦃L, T⦄ ⊃* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fsups_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}.
+#L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 //
+/4 width=3 by fsup_fwd_cw, lt_to_le_to_lt, lt_to_le/ (**) (* slow even with trace *)
+qed-.
+
+(* Advanced inversion lemmas on plus-iterated supclosure ********************)
+
+lemma fsupp_inv_bind1_fsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃L2, T2⦄ →
+ ⦃L1, W⦄ ⊃* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⊃* ⦃L2, T2⦄.
+#b #J #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -L2 -T2
+[ #L2 #T2 #H
+ elim (fsup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/
+| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
+]
+qed-.
+
+lemma fsupp_inv_flat1_fsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⊃+ ⦃L2, T2⦄ →
+ ⦃L1, W⦄ ⊃* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ ⊃* ⦃L2, T2⦄.
+#J #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -L2 -T2
+[ #L2 #T2 #H
+ elim (fsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/
+| #L #T #L2 #T2 #_ #HT2 * /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/grammar/fsups.ma".
+
+(* STAR-ITERATED SUPCLOSURE *************************************************)
+
+(* Main properties **********************************************************)
+
+theorem fsups_trans: bi_transitive … fsups.
+/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/substitution/fsup.ma".
+include "basic_2/substitution/ldrop_ldrop.ma".
+
+(* LOCAL ENVIRONMENT SLICING ************************************************)
+
+(* Inversion lemmas on supclosure *******************************************)
+
+lemma fsup_inv_atom1_ldrop: ∀K,V,L,I. ⦃L, ⓪{I}⦄ ⊃ ⦃K, V⦄ →
+ ∃∃J,i. ⇩[0, i] L ≡ K.ⓑ{J}V & I = LRef i.
+#K #V #L @(f_ind … length … L) -L #n #IH #L #Hn #I #H
+elim (fsup_inv_atom1 … H) -H *
+[ #J #L0 #V0 #H1 #H2 #H3 #H4 destruct /2 width=4/
+| #J #L0 #V0 #i #HLK #H1 #H2 destruct
+ elim (IH … HLK) -IH -HLK [2: normalize // ] #I #j #HLK #H destruct /3 width=4/
+]
+qed-.
+
+(* Advanced eliminators on supclosure ***************************************)
+
+lemma fsup_ind_ldrop: ∀R:bi_relation lenv term.
+ (∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → R L (#i) K V) →
+ (∀a,I,L,V,T. R L (ⓑ{a,I}V.T) L V) →
+ (∀a,I,L,V,T. R L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T) →
+ (∀I,L,V,T. R L (ⓕ{I}V.T) L V) →
+ (∀I,L,V,T. R L (ⓕ{I}V.T) L T) →
+ ∀L1,T1,L2,T2. ⦃L1,T1⦄⊃⦃L2,T2⦄ → R L1 T1 L2 T2.
+#R #H1 #H2 #H3 #H4 #H5 #L1 #T1 #L2 #T2 #H elim H -L1 -T1 -L2 -T2 //
+[ /3 width=2/
+| #I #L #K #V #T #i #H #H1LK
+ elim (fsup_inv_atom1_ldrop … H) -H #J #j #H2LK #H destruct /3 width=2/
+]
+qed-.
+
+(* Advanced inversion lemmas on supclosure **********************************)
+
+lemma fsup_inv_ldrop: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+ ∀J,W,j. ⇩[0, j] L1 ≡ L2.ⓑ{J}W → T1 = #j ∧ T2 = W.
+#L1 #L2 #T1 #T2 #H @(fsup_ind_ldrop … H) -L1 -L2 -T1 -T2
+[ #I #L #K #V #i #HLKV #J #W #j #HLKW
+ elim (ldrop_conf_div … HLKV … HLKW) -L /2 width=1/
+| #a
+| #a
+]
+#I #L #V #T #J #W #j #H
+lapply (ldrop_pair2_fwd_fw … H W) -H #H
+[2: lapply (transitive_lt (♯{L,W}) … H) /2 width=1/ -H #H ]
+elim (lt_refl_false … 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/fsups.ma".
+include "basic_2/substitution/ldrop_fsup.ma".
+
+(* LOCAL ENVIRONMENT SLICING ************************************************)
+
+(* Inversion lemmas on plus-iterated supclosure ****************************)
+
+lemma fsupp_inv_atom1_fsups: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⊃+ ⦃L2, T2⦄ →
+ ∃∃I,K,V,i. ⇩[0, i] L1 ≡ K.ⓑ{I}V &
+ ⦃K, V⦄ ⊃* ⦃L2, T2⦄ & J = LRef i.
+#J #L1 #L2 #T2 #H @(fsupp_ind … H) -L2 -T2
+[ #L2 #T2 #H
+ elim (fsup_inv_atom1_ldrop … H) -H * #i #HL12 #H destruct /2 width=7/
+| #L #T #L2 #T2 #_ #HT2 * #I #K #V #i #HLK #HVT #H destruct /3 width=8/
+]
+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 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ break [ term 46 g ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'XPRed $h $g $L $T1 $T2 }.
-
-include "basic_2/static/ssta.ma".
-include "basic_2/reducibility/cpr.ma".
-
-(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************)
-
-inductive xpr (h) (g) (L) (T1) (T2): Prop ≝
-| xpr_cpr : L ⊢ T1 ➡ T2 → xpr h g L T1 T2
-| xpr_ssta: ∀l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → xpr h g L T1 T2
-.
-
-interpretation
- "extended parallel reduction (term)"
- 'XPRed h g L T1 T2 = (xpr h g L T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma xpr_refl: ∀h,g,L. reflexive … (xpr h g L).
-/2 width=1/ qed.
qed.
lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. ♯{L, V2} < ♯{L, ②{I1}V1.②{I2}V2.T}.
-normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1/
+normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1 by monotonic_le_plus_r/ (**) (* auto too slow without trace *)
qed.
lemma fw_tpair_sn_sn_shift: ∀I,I1,I2,L,V1,V2,T.
lemma fw_tpair_sn_dx_shift: ∀I,I1,I2,L,V1,V2,T.
♯{L.ⓑ{I}V2, T} < ♯{L, ②{I1}V1.②{I2}V2.T}.
-normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1/
+normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1 by monotonic_le_plus_r/ (**) (* auto too slow without trace *)
+qed.
+
+lemma fw_lpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L.ⓑ{I}V, T}.
+normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *)
qed.
(* Basic_1: removed theorems 7:
non associative with precedence 45
for @{ 'RDrop $d $e $L1 $L2 }.
-notation "hvbox( â¦\83 term 46 L1, break term 46 T1 â¦\84 â§\81 break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( â¦\83 term 46 L1, break term 46 T1 â¦\84 â\8a\83 break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
- for @{ 'RestSupTerm $L1 $T1 $L2 $T2 }.
+ for @{ 'SupTerm $L1 $T1 $L2 $T2 }.
notation "hvbox( L ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )"
non associative with precedence 45
for @{ 'ICM $L $T $k }.
-notation "hvbox( L ⊢ break term 46 T1 break ▶ [ term 46 d , break term 46 e ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PSubst $L $T1 $d $e $T2 }.
-
(* Unfold *******************************************************************)
notation "hvbox( @ ⦃ term 46 T1 , break term 46 f ⦄ ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'RDropStar $e $L1 $L2 }.
-notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ + break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'RestSupTermPlus $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'RestSupTermStar $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PSubstStar $T1 $d $e $T2 }.
-
-notation "hvbox( L ⊢ break term 46 T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃ + break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
- for @{ 'PSubstStar $L $T1 $d $e $T2 }.
+ for @{ 'SupTermPlus $L1 $T1 $L2 $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
- for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
+ for @{ 'SupTermStar $L1 $T1 $L2 $T2 }.
-notation "hvbox( T1 break ⊢ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 ▶* break term 46 T2 )"
non associative with precedence 45
- for @{ 'PSubstStarSn $T1 $d $e $T2 }.
+ for @{ 'PSubstStar $L $T1 $T2 }.
-notation "hvbox( T1 break ⊢ ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+notation "hvbox( T1 ⊢ ▶ * break term 46 T2 )"
non associative with precedence 45
- for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }.
+ for @{ 'PSubstStarSn $T1 $T2 }.
notation "hvbox( ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )"
non associative with precedence 45
∃∃T. L ⊢ T1 ➡ T & L ⊢ T2 ➡ T.
#L #U0 #T1 #T2 * #U1 #HU01 #HUT1 * #U2 #HU02 #HUT2
elim (tpr_conf … HU01 HU02) -U0 #U #HU1 #HU2
-elim (tpr_tpss_ltpr ? L … HU1 … HUT1) -U1 // #U1 #HTU1 #HU1
-elim (tpr_tpss_ltpr ? L … HU2 … HUT2) -U2 // #U2 #HTU2 #HU2
+elim (ltpr_tpr_tpss_conf ? L … HU1 … HUT1) -U1 // #U1 #HTU1 #HU1
+elim (ltpr_tpr_tpss_conf ? L … HU2 … HUT2) -U2 // #U2 #HTU2 #HU2
elim (tpss_conf_eq … HU1 … HU2) -U /3 width=5/
qed.
[ #V #T #T0 #HV1 #HT1 #HT0 #H destruct
elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT02 #H destruct
lapply (tps_lsubr_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
- lapply (tps_weak_all … HT0) -HT0 #HT0
+ lapply (tps_weak_full … HT0) -HT0 #HT0
lapply (tpss_lsubr_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02
- lapply (tpss_weak_all … HT02) -HT02 #HT02
+ lapply (tpss_weak_full … HT02) -HT02 #HT02
lapply (tpss_strap2 … HT0 HT02) -T0 /4 width=7/
| #T2 #HT12 #HXT2 #H destruct
elim (lift_total Y 0 1) #Z #HYZ
(* *)
(**************************************************************************)
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
(* Properties concerning parallel unfold on terms ***************************)
-(* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *)
+(* Note: we could invoke tpss_weak_full instead of ltpr_fwd_length *)
(* Basic_1: was only: pr2_subst1 *)
lemma cpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 →
∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 →
∃∃U2. L2 ⊢ U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
#L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1
-elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U #HU1 #HTU
+elim (ltpr_tpr_tpss_conf … HL12 … HT1 … HTU1) -L1 -HT1 #U #HU1 #HTU
elim (tpss_conf_eq … HT2 … HTU) -T /3 width=3/
qed.
∃∃T. L2 ⊢ T1 ➡ T & T2 ➡ T.
#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
>(ltpr_fwd_length … HL12) in HT2; #HT2
-elim (tpr_tpss_ltpr … HL12 … HT2) -L1 /3 width=3/
+elim (ltpr_tpr_tpss_conf … HL12 … HT2) -L1 /3 width=3/
qed.
lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 →
#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1
elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2
elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U2 #HU12 #HTU2
-lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *)
+lapply (tpss_weak_full … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *)
qed.
lemma ltpss_sn_cpr_trans: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 →
∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
#L1 #L2 #d #e #HL12 #T1 #T2 *
-lapply (ltpss_sn_weak_all … HL12)
+lapply (ltpss_sn_weak_full … HL12)
<(ltpss_sn_fwd_length … HL12) -HL12 /3 width=5/
qed.
(* *)
(**************************************************************************)
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
lemma cpr_tpss_trans: ∀L,T1,T. L ⊢ T1 ➡ T →
∀T2,d,e. L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡ T2.
#L #T1 #T * #T0 #HT10 #HT0 #T2 #d #e #HT2
-lapply (tpss_weak_all … HT2) -HT2 #HT2
+lapply (tpss_weak_full … HT2) -HT2 #HT2
lapply (tpss_trans_eq … HT0 HT2) -T /2 width=3/
qed.
[ elim (ldrop_ltpss_sn_trans_ge … HLK … HK2 …)
| elim (ldrop_ltpss_sn_trans_be … HLK … HK2 …)
] // -Hd #L2 #HL2 #HLK2
-lapply (ltpss_sn_weak_all … HL2) -K /3 width=4/
+lapply (ltpss_sn_weak_full … HL2) -K /3 width=4/
qed-.
(* Advanced properties ******************************************************)
(**************************************************************************)
include "basic_2/unfold/ltpss_sn_ltpss_sn.ma".
+include "basic_2/reducibility/ltpr_ldrop.ma".
include "basic_2/reducibility/cpr.ma".
include "basic_2/reducibility/lfpr.ma".
lapply (ltpss_sn_tpss_trans_eq … HV2 … HL2) -HV2 #V2
@(ex2_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *)
qed.
+
+(* Properties on supclosure *************************************************)
+(*
+lamma fsub_cpr_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ➡ U2 →
+ ∃∃L,U1. ⦃L1⦄ ➡ ⦃L⦄ & L ⊢ T1 ➡ U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄.
+#L1 #L2 #T1 #T2 #HT12 #U2 * #T #H1 #H2
+elim (fsub_tpr_trans … HT12 … H1) -T2 #L #U #HL1 #HT1U #HUT
+elim (fsup_tpss_trans_full … HUT … H2) -T -HUT -H2 #L #U #HL1 #HT1U #HUT
+
+
+
+
+
+
+ #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HK2
+elim (lift_total T d e) #U #HTU
+elim (ldrop_ltpr_trans … HLK1 … HK1) -HLK1 -HK1 #L #HL1 #HLK
+lapply (tpr_lift … HT1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+qed-.
+*)
\ No newline at end of file
(**************************************************************************)
include "basic_2/substitution/ldrop_lpx.ma".
+include "basic_2/substitution/fsup.ma".
include "basic_2/reducibility/tpr_lift.ma".
include "basic_2/reducibility/ltpr.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+(* Properies on local environment slicing ***********************************)
+
(* Basic_1: was: wcpr0_drop *)
lemma ltpr_ldrop_conf: dropable_sn ltpr.
/3 width=3 by lpx_deliftable_dropable, tpr_inv_lift1/ qed.
lemma ltpr_ldrop_trans_O1: dropable_dx ltpr.
/2 width=3/ qed.
+
+(* Properties on supclosure *************************************************)
+
+lemma fsub_tpr_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. T2 ➡ U2 →
+ ∃∃L,U1. L1 ➡ L & T1 ➡ U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HK2
+elim (lift_total T d e) #U #HTU
+elim (ldrop_ltpr_trans … HLK1 … HK1) -HLK1 -HK1 #L #HL1 #HLK
+lapply (tpr_lift … HT1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
| #L1 #K1 #I #V1 #W1 #e #_ #HVW1 #IHLK1 #X #H
elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
- elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/
+ elim (ltpr_tpr_tpss_conf … HK12 … HV12 … HVW1) -V1 /3 width=5/
| #L1 #K1 #I #V1 #W1 #d #e #_ #HVW1 #IHLK1 #X #H
elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
- elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/
+ elim (ltpr_tpr_tpss_conf … HK12 … HV12 … HVW1) -V1 /3 width=5/
]
qed.
(* Properties concerning parallel substitution on terms *********************)
-lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 ▶ [d, e] T2 → ∀L1. L1 ➡ L2 →
- ∃∃T. L1 ⊢ T1 ▶ [d, e] T & T ➡ T2.
-#L2 #T1 #T2 #d #e #H elim H -L2 -T1 -T2 -d -e
-[ /2 width=3/
-| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12
- elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
- elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2
- elim (lift_total V1 0 (i+1)) #W1 #HVW1
- lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=4/
-| #L2 #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12
- elim (IHV12 … HL12) -IHV12 #V #HV1 #HV2
- elim (IHT12 (L1.ⓑ{I}V) ?) /2 width=1/ -L2 /3 width=5/
-| #L2 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12
- elim (IHV12 … HL12) -IHV12
- elim (IHT12 … HL12) -L2 /3 width=5/
-]
-qed.
-
+(* Basic_1: was: pr0_subst1_fwd *)
lemma ltpr_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 → ∀L2. L1 ➡ L2 →
∃∃T. L2 ⊢ T1 ▶ [d, e] T & T2 ➡ T.
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
elim (IHV12 … HL12) -IHV12
elim (IHT12 … HL12) -L1 /3 width=5/
]
-qed.
+qed-.
+
+(* Basic_1: was: pr0_subst1_back *)
+lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 ▶ [d, e] T2 → ∀L1. L1 ➡ L2 →
+ ∃∃T. L1 ⊢ T1 ▶ [d, e] T & T ➡ T2.
+#L2 #T1 #T2 #d #e #H elim H -L2 -T1 -T2 -d -e
+[ /2 width=3/
+| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12
+ elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+ elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2
+ elim (lift_total V1 0 (i+1)) #W1 #HVW1
+ lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=4/
+| #L2 #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12
+ elim (IHV12 … HL12) -IHV12 #V #HV1 #HV2
+ elim (IHT12 (L1.ⓑ{I}V) ?) /2 width=1/ -L2 /3 width=5/
+| #L2 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12
+ elim (IHV12 … HL12) -IHV12
+ elim (IHT12 … HL12) -L2 /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/unfold/ltpss_dx_ltpss_dx.ma".
+include "basic_2/reducibility/ltpr_tps.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+(* Properties on partial unfold for terms ***********************************)
+
+(* Basic_1: was: pr0_subst1 *)
+lemma ltpr_tpr_tps_conf: ∀T1,T2. T1 ➡ T2 →
+ ∀L1,d,e,U1. L1 ⊢ T1 ▶ [d, e] U1 →
+ ∀L2. L1 ➡ L2 →
+ ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
+#T1 #T2 #H elim H -T1 -T2
+[ #I #L1 #d #e #U1 #H #L2 #HL12
+ elim (ltpr_tps_conf … H … HL12) -L1 /3 width=3/
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (IHV12 … HVW1 … HL12) -V1
+ elim (IHT12 … HTU1 … HL12) -T1 -HL12 /3 width=5/
+| #a #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
+ elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct
+ elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
+ elim (IHT12 … HTT1 (L2. ⓛWW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
+ lapply (tpss_lsubr_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
+| #a #I #V1 #V2 #T1 #T #T2 #HV12 #_ #HT2 #IHV12 #IHT1 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (IHV12 … HVW1 … HL12) -V1 #W2 #HW12 #HVW2
+ elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
+ elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2
+ lapply (tps_lsubr_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2
+ elim (ltpss_dx_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23
+ lapply (tps_lsubr_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3
+ lapply (tpss_lsubr_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23
+ lapply (tpss_trans_eq … HTU2 … HU23) -U2 /3 width=5/
+| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
+ elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct
+ elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
+ elim (IHW12 … HWW1 … HL12) -W1 #WW2 #HWW12 #HWW2
+ elim (IHT12 … HTT1 (L2. ⓓWW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
+ elim (lift_total VV2 0 1) #VV #H2VV
+ lapply (tpss_lift_ge … HVV2 (L2. ⓓWW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
+ @ex2_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
+| #V #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_bind1 … H) -H #W #U1 #_ #HTU1 #H destruct -V
+ elim (IHT1 … HTU1 (L2.ⓓW) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
+ elim (tpss_inv_lift1_ge … HTU L2 … HT2 ?) -T <minus_plus_m_m /3 width=3/
+| #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
+ elim (IHT12 … HTT1 … HL12) -T1 -HL12 /3 width=3/
+]
+qed-.
+
+lemma tpr_tps_conf_bind: ∀I,V1,V2,T1,T2,U1. V1 ➡ V2 → T1 ➡ T2 →
+ ⋆. ⓑ{I} V1 ⊢ T1 ▶ [0, 1] U1 →
+ ∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] U2.
+#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
+elim (ltpr_tpr_tps_conf … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ -V1 #U2 #HU12 #HTU2
+lapply (tpss_inv_SO2 … HTU2) -HTU2 /2 width=3/
+qed-.
+
+lemma ltpr_tpr_tpss_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 →
+ ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 →
+ ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
+#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
+[ /2 width=3/
+| -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
+ elim (ltpr_tpr_tps_conf … HUT … HU1 … HL12) -U -HL12 #U2 #HU12 #HTU2
+ lapply (tpss_trans_eq … HT2 … HTU2) -T /2 width=3/
+]
+qed-.
+
+lemma tpr_tpss_conf: ∀T1,T2. T1 ➡ T2 →
+ ∀L,U1,d,e. L ⊢ T1 ▶* [d, e] U1 →
+ ∃∃U2. U1 ➡ U2 & L ⊢ T2 ▶* [d, e] U2.
+/2 width=5 by ltpr_tpr_tpss_conf/ qed-.
(**************************************************************************)
include "basic_2/unfold/delift.ma".
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
#U1 #U2 #HU12 #L #T1 #d #e * #W1 #HUW1 #HTW1
elim (tpr_tpss_conf … HU12 … HUW1) -U1 #U1 #HWU1 #HU21
elim (tpr_inv_lift1 … HWU1 … HTW1) -W1 /3 width=5/
-qed.
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
[ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct
elim (IH … HW02 … HWW2) -HW02 -HWW2 /2 width=1/ #W #HW02 #HWW2
elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH /2 width=1/ #U #HU2 #HUUU2
- elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1
+ elim (tpr_tps_conf_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1
@ex2_intro
[2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ]
|1:skip
#a #I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
-elim (tpr_tps_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1
-elim (tpr_tps_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2
+elim (tpr_tps_conf_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1
+elim (tpr_tps_conf_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2
elim (tps_conf_eq … HTU1 … HTU2) -T #U #HU1 #HU2
@ex2_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
qed.
∃∃X. +ⓓV1. TT1 ➡ X & X2 ➡ X.
#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HT02 #HXT2
elim (IH … HT01 … HT02) -IH -HT01 -HT02 // -V0 -T0 #T #HT1 #HT2
-elim (tpr_tps_bind ? ? V1 … HT1 HTT1) -T1 // #TT #HTT1 #HTT
+elim (tpr_tps_conf_bind ? ? V1 … HT1 HTT1) -T1 // #TT #HTT1 #HTT
elim (tpr_inv_lift1 … HT2 … HXT2) -T2 #X #HXT #HX2
lapply (tps_inv_lift1_eq … HTT … HXT) -HTT #H destruct /3 width=3/
qed.
]
]
]
-qed.
+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".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-
-(* Properties on parallel substitution for terms ****************************)
-
-(* Basic_1: was: pr0_subst1_fwd *)
-lemma ltpr_tpr_conf: ∀L1,T,U1,d,e. L1 ⊢ T ▶ [d, e] U1 → ∀L2. L1 ➡ L2 →
- ∃∃U2. U1 ➡ U2 & L2 ⊢ T ▶ [d, e] U2.
-#L1 #T #U1 #d #e #H elim H -L1 -T -U1 -d -e
-[ /2 width=3/
-| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L2 #HL12
- elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
- elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct -K1
- elim (lift_total V2 0 (i+1)) #W2 #HVW2
- lapply (tpr_lift … HV12 … HVW1 … HVW2) -V1 /3 width=6/
-| #L1 #a #I #V #W1 #T #U1 #d #e #_ #_ #IHV #IHT #L2 #HL12
- elim (IHV … HL12) -IHV #W2 #HW12
- elim (IHT (L2.ⓑ{I}W2) ?) -IHT /2 width=1/ -L1 /3 width=5/
-| #L1 #I #V #W1 #T #U1 #d #e #_ #_ #IHV #IHT #L2 #HL12
- elim (IHV … HL12) -IHV
- elim (IHT … HL12) -IHT -HL12 /3 width=5/
-]
-qed.
-
-(* Basic_1: was: pr0_subst1_back *)
-lemma ltpr_tps_trans: ∀L2,T,U2,d,e. L2 ⊢ T ▶ [d, e] U2 → ∀L1. L1 ➡ L2 →
- ∃∃U1. U1 ➡ U2 & L1 ⊢ T ▶ [d, e] U1.
-#L2 #T #U2 #d #e #H elim H -L2 -T -U2 -d -e
-[ /2 width=3/
-| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12
- elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
- elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2
- elim (lift_total V1 0 (i+1)) #W1 #HVW1
- lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=6/
-| #L2 #a #I #V #W2 #T #U2 #d #e #_ #_ #IHV #IHT #L1 #HL12
- elim (IHV … HL12) -IHV #W1 #HW12
- elim (IHT (L1.ⓑ{I}W1) ?) -IHT /2 width=1/ -L2 /3 width=5/
-| #L2 #I #V #W2 #T #U2 #d #e #_ #_ #IHV #IHT #L1 #HL12
- elim (IHV … HL12) -IHV
- elim (IHT … HL12) -IHT -HL12 /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/unfold/ltpss_dx_ltpss_dx.ma".
-include "basic_2/reducibility/tpr_tps.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-
-(* Unfold properties ********************************************************)
-
-(* Basic_1: was: pr0_subst1 *)
-lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
- ∀L1,d,e,U1. L1 ⊢ T1 ▶ [d, e] U1 →
- ∀L2. L1 ➡ L2 →
- ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
-#T1 #T2 #H elim H -T1 -T2
-[ #I #L1 #d #e #U1 #H #L2 #HL12
- elim (ltpr_tpr_conf … H … HL12) -L1 /3 width=3/
-| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
- elim (IHV12 … HVW1 … HL12) -V1
- elim (IHT12 … HTU1 … HL12) -T1 -HL12 /3 width=5/
-| #a #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
- elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct
- elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
- elim (IHT12 … HTT1 (L2. ⓛWW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
- lapply (tpss_lsubr_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
-| #a #I #V1 #V2 #T1 #T #T2 #HV12 #_ #HT2 #IHV12 #IHT1 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
- elim (IHV12 … HVW1 … HL12) -V1 #W2 #HW12 #HVW2
- elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
- elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2
- lapply (tps_lsubr_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2
- elim (ltpss_dx_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23
- lapply (tps_lsubr_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3
- lapply (tpss_lsubr_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23
- lapply (tpss_trans_eq … HTU2 … HU23) -U2 /3 width=5/
-| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
- elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct
- elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
- elim (IHW12 … HWW1 … HL12) -W1 #WW2 #HWW12 #HWW2
- elim (IHT12 … HTT1 (L2. ⓓWW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
- elim (lift_total VV2 0 1) #VV #H2VV
- lapply (tpss_lift_ge … HVV2 (L2. ⓓWW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
- @ex2_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
-| #V #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_bind1 … H) -H #W #U1 #_ #HTU1 #H destruct -V
- elim (IHT1 … HTU1 (L2.ⓓW) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
- elim (tpss_inv_lift1_ge … HTU L2 … HT2 ?) -T <minus_plus_m_m /3 width=3/
-| #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
- elim (IHT12 … HTT1 … HL12) -T1 -HL12 /3 width=3/
-]
-qed.
-
-lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ➡ V2 → T1 ➡ T2 →
- ⋆. ⓑ{I} V1 ⊢ T1 ▶ [0, 1] U1 →
- ∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] U2.
-#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
-elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ -V1 #U2 #HU12 #HTU2
-lapply (tpss_inv_SO2 … HTU2) -HTU2 /2 width=3/
-qed.
-
-lemma tpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 →
- ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 →
- ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
-#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
-[ /2 width=3/
-| -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
- elim (tpr_tps_ltpr … HUT … HU1 … HL12) -U -HL12 #U2 #HU12 #HTU2
- lapply (tpss_trans_eq … HT2 … HTU2) -T /2 width=3/
-]
-qed.
-
-lemma tpr_tpss_conf: ∀T1,T2. T1 ➡ T2 →
- ∀L,U1,d,e. L ⊢ T1 ▶* [d, e] U1 →
- ∃∃U2. U1 ➡ U2 & L ⊢ T2 ▶* [d, e] U2.
-/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/static/ssta.ma".
+include "basic_2/reducibility/cpr.ma".
+
+lemma arith1: ∀x,y,z,w. z < y → x + (y + w) - z = x + y - z + w.
+#x #y #z #w #H <le_plus_minus_comm // /3 width=1 by lt_to_le, le_plus_a/
+qed-.
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+notation "hvbox( ⦃term 46 h, break term 46 L⦄ ⊢ break term 46 T1 ➡ break [ term 46 g ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'XPRed $h $g $L $T1 $T2 }.
+
+inductive xpr (h) (g): lenv → relation term ≝
+| xpr_cpr : ∀I,L,U2. L ⊢ ⓪{I} ➡ U2 → xpr h g L (⓪{I}) U2
+| xpr_ssta: ∀I,L,U2,l. ⦃h, L⦄ ⊢ ⓪{I} •[g] ⦃l+1, U2⦄ → xpr h g L (⓪{I}) U2
+| xpr_bind: ∀a,I,L,V1,V2,T1,T2,U2. xpr h g L V1 V2 → xpr h g (L.ⓑ{I}V2) T1 T2 →
+ L ⊢ ⓑ{a,I}V2.T2 ➡ U2 → xpr h g L (ⓑ{a,I}V1.T1) U2
+| xpr_flat: ∀I,L,V1,V2,T1,T2,U2. xpr h g L V1 V2 → xpr h g L T1 T2 →
+ L ⊢ ⓕ{I}V2.T2 ➡ U2 → xpr h g L (ⓕ{I}V1.T1) U2
+.
+
+interpretation
+ "context-sensitive extended parallel reduction (term)"
+ 'XPRed h g L T1 T2 = (xpr h g L T1 T2).
+
+(* Basic properties *********************************************************)
+
+(* Note: this is "∀h,g,L. reflexive … (xpr h g L)" *)
+lemma xpr_refl: ∀h,g,T,L. ⦃h, L⦄ ⊢ T ➡[g] T.
+#h #g #T elim T -T /2 width=1/ * /2 width=5/
+qed.
+
+lemma cpr_xpr: ∀h,g,T1,L,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+#h #g #T1 elim T1 -T1 /2 width=1/ * /2 width=5/
+qed.
+
+lemma ssta_xpr: ∀h,g,T1,L,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+#h #g #T1 elim T1 -T1 /2 width=2/ * [|*]
+[ #a #I #V1 #T1 #_ #IHT1 #L #X #l #H
+ elim (ssta_inv_bind1 … H) -H #T2 #HT12 #H destruct /3 width=5/
+| #V1 #T1 #_ #IHT1 #L #X #l #H
+ elim (ssta_inv_appl1 … H) -H #T2 #HT12 #H destruct /3 width=5/
+| #V1 #T1 #_ #IHT1 #L #X #l #H
+ lapply (ssta_inv_cast1 … H) -H /3 width=5/
+]
+qed.
+
+include "basic_2/substitution/lift_lift.ma".
+include "basic_2/substitution/fsup.ma".
+include "basic_2/unfold/ltpss_dx_ldrop.ma".
+
(**************************************************************************)
include "basic_2/substitution/ldrop.ma".
-include "basic_2/unfold/frsups.ma".
include "basic_2/static/sd.ma".
(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X •[g] ⦃l, U⦄ →
⦃h, L⦄ ⊢ X •[g] ⦃l, U⦄.
/2 width=4/ qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥.
-#h #g #L #T #U #l #H elim H -L -T -U -l
-[ #L #k #l #_ #H
- elim (frsupp_inv_atom1_frsups … H)
-| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H
- elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H
- elim (lift_inv_lref2_be … H ? ?) -H //
-| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H
- elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H
- elim (lift_inv_lref2_be … H ? ?) -H //
-| #a #I #L #V #T #U #l #_ #IHTU #H
- elim (frsupp_inv_bind1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU
- lapply (frsups_fwd_fw … H) -H normalize
- <associative_plus <associative_plus #H
- elim (le_plus_xySz_x_false … H)
-| #L #V #T #U #l #_ #IHTU #H
- elim (frsupp_inv_flat1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU
- lapply (frsups_fwd_fw … H) -H normalize
- <associative_plus <associative_plus #H
- elim (le_plus_xySz_x_false … H)
-| /3 width=4/
-]
-qed-.
-
-fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → T = U → ⊥.
-#h #g #L #T #U #l #H elim H -L -T -U -l
-[ #L #k #l #_ #H
- lapply (next_lt h k) destruct -H -e0 (**) (* destruct: these premises are not erased *)
- <e1 -e1 #H elim (lt_refl_false … H)
-| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H destruct
- elim (lift_inv_lref2_be … HWU ? ?) -HWU //
-| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H destruct
- elim (lift_inv_lref2_be … HWU ? ?) -HWU //
-| #a #I #L #V #T #U #l #_ #IHTU #H destruct /2 width=1/
-| #L #V #T #U #l #_ #IHTU #H destruct /2 width=1/
-| #L #W #T #U #l #HTU #_ #H destruct
- elim (ssta_inv_frsupp … HTU ?) -HTU /2 width=1/
-]
-qed-.
-
-lemma ssta_inv_refl: ∀h,g,T,L,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, T⦄ → ⊥.
-/2 width=8 by ssta_inv_refl_aux/ qed-.
-
-lemma ssta_inv_frsups: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁* ⦃L, T⦄ → ⊥.
-#h #g #L #T #U #L #HTU #H elim (frsups_inv_all … H) -H
-[ * #_ #H destruct /2 width=6 by ssta_inv_refl/
-| /2 width=8 by ssta_inv_frsupp/
-]
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/substitution/ldrop_ldrop.ma".
-include "basic_2/static/ssta.ma".
+include "basic_2/static/ssta_lift.ma".
(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
elim (IHTU1 … HTU2) -T /2 width=1/
]
qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma ssta_inv_refl_pos: ∀h,g,L,T,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, T⦄ → ⊥.
+#h #g #L #T #l #HTT
+elim (ssta_fwd_correct … HTT) <minus_plus_m_m #U #HTU
+elim (ssta_mono … HTU … HTT) -h -L #H #_ -T -U
+elim (plus_xySz_x_false 0 l 0 ?) //
+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/cl_weight.ma".
-include "basic_2/substitution/lift.ma".
-
-(* RESTRICTED SUPCLOSURE ****************************************************)
-
-inductive frsup: bi_relation lenv term ≝
-| frsup_bind_sn: ∀a,I,L,V,T. frsup L (ⓑ{a,I}V.T) L V
-| frsup_bind_dx: ∀a,I,L,V,T. frsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
-| frsup_flat_sn: ∀I,L,V,T. frsup L (ⓕ{I}V.T) L V
-| frsup_flat_dx: ∀I,L,V,T. frsup L (ⓕ{I}V.T) L T
-.
-
-interpretation
- "restricted structural predecessor (closure)"
- 'RestSupTerm L1 T1 L2 T2 = (frsup L1 T1 L2 T2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact frsup_inv_atom1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ →
- ∀J. T1 = ⓪{J} → ⊥.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #a #I #L #V #T #J #H destruct
-| #a #I #L #V #T #J #H destruct
-| #I #L #V #T #J #H destruct
-| #I #L #V #T #J #H destruct
-]
-qed-.
-
-lemma frsup_inv_atom1: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⧁ ⦃L2, T2⦄ → ⊥.
-/2 width=7 by frsup_inv_atom1_aux/ qed-.
-
-fact frsup_inv_bind1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ →
- ∀b,J,W,U. T1 = ⓑ{b,J}W.U →
- (L2 = L1 ∧ T2 = W) ∨
- (L2 = L1.ⓑ{J}W ∧ T2 = U).
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
-| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
-| #I #L #V #T #b #J #W #U #H destruct
-| #I #L #V #T #b #J #W #U #H destruct
-]
-qed-.
-
-lemma frsup_inv_bind1: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⧁ ⦃L2, T2⦄ →
- (L2 = L1 ∧ T2 = W) ∨
- (L2 = L1.ⓑ{J}W ∧ T2 = U).
-/2 width=4 by frsup_inv_bind1_aux/ qed-.
-
-fact frsup_inv_flat1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ →
- ∀J,W,U. T1 = ⓕ{J}W.U →
- L2 = L1 ∧ (T2 = W ∨ T2 = U).
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #a #I #L #V #T #J #W #U #H destruct
-| #a #I #L #V #T #J #W #U #H destruct
-| #I #L #V #T #J #W #U #H destruct /3 width=1/
-| #I #L #V #T #J #W #U #H destruct /3 width=1/
-]
-qed-.
-
-lemma frsup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⧁ ⦃L2, T2⦄ →
- L2 = L1 ∧ (T2 = W ∨ T2 = U).
-/2 width=4 by frsup_inv_flat1_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma frsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/
-qed-.
-
-lemma frsup_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/
-qed-.
-
-lemma frsup_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=1 by le_minus_to_plus/
-qed-.
-
-lemma frsup_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #a
-| #a #I #L #V #_ @(ex_intro … (⋆.ⓑ{I}V)) //
-]
-#I #L #V #T @(ex_intro … (⋆)) //
-qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma lift_frsup_trans: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
- ∀L,K,U2. ⦃L, U1⦄ ⧁ ⦃L @@ K, U2⦄ →
- ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
-#T1 #U1 #d #e * -T1 -U1 -d -e
-[5: #a #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HTU1 #L #K #X #H
- elim (frsup_inv_bind1 … H) -H *
- [ -HTU1 #H1 #H2 destruct
- >(append_inv_refl_dx … H1) -L -K normalize /2 width=2/
- | -HVW1 #H1 #H2 destruct
- >(append_inv_pair_dx … H1) -L -K normalize /2 width=2/
- ]
-|6: #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HUT1 #L #K #X #H
- elim (frsup_inv_flat1 … H) -H #H1 * #H2 destruct
- >(append_inv_refl_dx … H1) -L -K normalize /2 width=2/
-]
-#i #d #e [2,3: #_ ] #L #K #X #H
-elim (frsup_inv_atom1 … 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/substitution/ldrop.ma".
+
+(* SUPCLOSURE ***************************************************************)
+
+inductive fsup: bi_relation lenv term ≝
+| fsup_lref : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
+| fsup_bind_sn: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) L V
+| fsup_bind_dx: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
+| fsup_flat_sn: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L V
+| fsup_flat_dx: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L T
+| fsup_ldrop : ∀L1,K1,K2,T1,T2,U1,d,e.
+ ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
+ fsup K1 T1 K2 T2 → fsup L1 U1 K2 T2
+.
+
+interpretation
+ "structural successor (closure)"
+ 'SupTerm L1 T1 L2 T2 = (fsup L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fsup_lref_S_lt: ∀I,L,K,V,T,i. 0 < i → ⦃L, #(i-1)⦄ ⊃ ⦃K, T⦄ → ⦃L.ⓑ{I}V, #i⦄ ⊃ ⦃K, T⦄.
+/3 width=7/ qed.
+
+lemma fsup_lref: ∀I,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃L, #i⦄ ⊃ ⦃K, V⦄.
+#I #K #V #i @(nat_elim1 i) -i #i #IH #L #H
+elim (ldrop_inv_O1_pair2 … H) -H *
+[ #H1 #H2 destruct //
+| #I1 #K1 #V1 #HK1 #H #Hi destruct
+ lapply (IH … HK1) /2 width=1/
+]
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fsup_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 //
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12
+lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1
+lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1
+@(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/
+qed-.
+
+fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀i. T1 = #i → |L2| < |L1|.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
+[ 6: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
+ lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+ elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
+ @(lt_to_le_to_lt … HLK1) /2 width=2/
+| normalize // |2,3: #a
+] #I #L #V #T #j #H destruct
+qed-.
+
+lemma fsup_fwd_length_lref1: ∀L1,L2,T2,i. ⦃L1, #i⦄ ⊃ ⦃L2, T2⦄ → |L2| < |L1|.
+/2 width=5 by fsup_fwd_length_lref1_aux/
+qed-.
L2 = K2. ⓑ{I} V2.
/2 width=3/ qed-.
+lemma ldrop_inv_O1_pair2: ∀I,K,V,e,L1. ⇩[0, e] L1 ≡ K. ⓑ{I} V →
+ (e = 0 ∧ L1 = K. ⓑ{I} V) ∨
+ ∃∃I1,K1,V1. ⇩[0, e - 1] K1 ≡ K. ⓑ{I} V & L1 = K1.ⓑ{I1}V1 & 0 < e.
+#I #K #V #e *
+[ #H lapply (ldrop_inv_atom1 … H) -H #H destruct
+| #L1 #I1 #V1 #H
+ elim (ldrop_inv_O1 … H) -H *
+ [ #H1 #H2 destruct /3 width=1/
+ | /3 width=5/
+ ]
+]
+qed-.
+
fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 &
]
qed-.
+lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| ≤ |L1|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1/
+qed-.
+
lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
[ /2 width=3/
| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
- >(tw_lift … HV21) -HV21 /2 width=1/
+ >(lift_fwd_tw … HV21) -HV21 /2 width=1/
]
qed-.
| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
>commutative_plus normalize #H destruct
]
-qed.
+qed-.
-lemma ltpr_dropable: ∀R. dropable_dx (lpx R).
-/2 width=5/ qed.
+lemma ltpx_dropable: ∀R. dropable_dx (lpx R).
+/2 width=5 by lpx_dropable_aux/ qed.
(* Basic forward lemmas *****************************************************)
-lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.
+lemma lift_fwd_tw: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
qed-.
(* *)
(**************************************************************************)
+notation "hvbox( L ⊢ break term 46 T1 break ▶ [ term 46 d , break term 46 e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubst $L $T1 $d $e $T2 }.
+
include "basic_2/substitution/ldrop_append.ma".
(* PARALLEL SUBSTITUTION ON TERMS *******************************************)
]
qed.
-lemma tps_weak_all: ∀L,T1,T2,d,e.
- L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶ [0, |L|] T2.
+lemma tps_weak_full: ∀L,T1,T2,d,e.
+ L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶ [0, |L|] T2.
#L #T1 #T2 #d #e #HT12
lapply (tps_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
lapply (tps_weak_top … HT12) //
--- /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/ldrop_append.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL UNFOLD FOR TERMS ******************************)
+
+inductive cpss: lenv → relation term ≝
+| cpss_atom : ∀L,I. cpss L (⓪{I}) (⓪{I})
+| cpss_subst: ∀L,K,V,V2,W2,i.
+ ⇩[0, i] L ≡ K. ⓓV → cpss K V V2 →
+ ⇧[0, i + 1] V2 ≡ W2 → cpss L (#i) W2
+| cpss_bind : ∀L,a,I,V1,V2,T1,T2.
+ cpss L V1 V2 → cpss (L. ⓑ{I} V1) T1 T2 →
+ cpss L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
+| cpss_flat : ∀L,I,V1,V2,T1,T2.
+ cpss L V1 V2 → cpss L T1 T2 →
+ cpss L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
+.
+
+interpretation "context-sensitive parallel unfold (term)"
+ 'PSubstStar L T1 T2 = (cpss L T1 T2).
+
+(* 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.
+#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/
+| /4 width=1/
+| /3 width=1/
+]
+qed-.
+
+lemma cpss_refl: ∀T,L. L ⊢ T ▶* T.
+#T elim T -T //
+#I elim I -I /2 width=1/
+qed.
+
+lemma cpss_delift: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. ⓓV) →
+ ∃∃T2,T. L ⊢ T1 ▶* T2 & ⇧[d, 1] T ≡ T2.
+#K #V #T1 elim T1 -T1
+[ * #i #L #d #HLK /2 width=4/
+ 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/
+| * [ #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 … HLK) -IHU1 -HLK /3 width=8/
+ ]
+]
+qed-.
+
+lemma cpss_append: ∀K,T1,T2. K ⊢ T1 ▶* T2 → ∀L. L @@ K ⊢ T1 ▶* T2.
+#K #T1 #T2 #H elim H -K -T1 -T2 // /2 width=1/
+#K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
+lapply (ldrop_fwd_ldrop2_length … HK0) #H
+@(cpss_subst … (L@@K0) V1 … HVW2) //
+@(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *)
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact cpss_inv_atom1_aux: ∀L,T1,T2. L ⊢ T1 ▶* T2 → ∀I. T1 = ⓪{I} →
+ T2 = ⓪{I} ∨
+ ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV &
+ K ⊢ V ▶* V2 &
+ ⇧[O, i + 1] V2 ≡ T2 &
+ I = LRef i.
+#L #T1 #T2 * -L -T1 -T2
+[ #L #I #J #H destruct /2 width=1/
+| #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #I #H destruct /3 width=8/
+| #L #a #I #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+]
+qed-.
+
+lemma cpss_inv_atom1: ∀L,T2,I. L ⊢ ⓪{I} ▶* T2 →
+ T2 = ⓪{I} ∨
+ ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV &
+ K ⊢ V ▶* V2 &
+ ⇧[O, i + 1] V2 ≡ T2 &
+ I = LRef i.
+/2 width=3 by cpss_inv_atom1_aux/ qed-.
+
+lemma cpss_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ▶* T2 → T2 = ⋆k.
+#L #T2 #k #H
+elim (cpss_inv_atom1 … H) -H //
+* #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+lemma cpss_inv_lref1: ∀L,T2,i. L ⊢ #i ▶* T2 →
+ T2 = #i ∨
+ ∃∃K,V,V2. ⇩[O, i] L ≡ K. ⓓV &
+ K ⊢ V ▶* V2 &
+ ⇧[O, i + 1] V2 ≡ T2.
+#L #T2 #i #H
+elim (cpss_inv_atom1 … H) -H /2 width=1/
+* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6/
+qed-.
+
+lemma cpss_inv_gref1: ∀L,T2,p. L ⊢ §p ▶* T2 → T2 = §p.
+#L #T2 #p #H
+elim (cpss_inv_atom1 … H) -H //
+* #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+fact cpss_inv_bind1_aux: ∀L,U1,U2. L ⊢ U1 ▶* U2 →
+ ∀a,I,V1,T1. U1 = ⓑ{a,I} V1. T1 →
+ ∃∃V2,T2. L ⊢ V1 ▶* V2 &
+ L. ⓑ{I} V1 ⊢ T1 ▶* T2 &
+ U2 = ⓑ{a,I} V2. T2.
+#L #U1 #U2 * -L -U1 -U2
+[ #L #k #a #I #V1 #T1 #H destruct
+| #L #K #V #V2 #W2 #i #_ #_ #_ #a #I #V1 #T1 #H destruct
+| #L #b #J #V1 #V2 #T1 #T2 #HV12 #HT12 #a #I #V #T #H destruct /2 width=5/
+| #L #J #V1 #V2 #T1 #T2 #_ #_ #a #I #V #T #H destruct
+]
+qed-.
+
+lemma cpss_inv_bind1: ∀L,a,I,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶* U2 →
+ ∃∃V2,T2. L ⊢ V1 ▶* V2 &
+ L. ⓑ{I} V1 ⊢ T1 ▶* T2 &
+ U2 = ⓑ{a,I} V2. T2.
+/2 width=3 by cpss_inv_bind1_aux/ qed-.
+
+fact cpss_inv_flat1_aux: ∀L,U1,U2. L ⊢ U1 ▶* U2 →
+ ∀I,V1,T1. U1 = ⓕ{I} V1. T1 →
+ ∃∃V2,T2. L ⊢ V1 ▶* V2 & L ⊢ T1 ▶* T2 &
+ U2 = ⓕ{I} V2. T2.
+#L #U1 #U2 * -L -U1 -U2
+[ #L #k #I #V1 #T1 #H destruct
+| #L #K #V #V2 #W2 #i #_ #_ #_ #I #V1 #T1 #H destruct
+| #L #a #J #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
+| #L #J #V1 #V2 #T1 #T2 #HV12 #HT12 #I #V #T #H destruct /2 width=5/
+]
+qed-.
+
+lemma cpss_inv_flat1: ∀L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ▶* U2 →
+ ∃∃V2,T2. L ⊢ V1 ▶* V2 & L ⊢ T1 ▶* T2 &
+ U2 = ⓕ{I} V2. T2.
+/2 width=3 by cpss_inv_flat1_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpss_fwd_tw: ∀L,T1,T2. L ⊢ T1 ▶* T2 → ♯{T1} ≤ ♯{T2}.
+#L #T1 #T2 #H elim H -L -T1 -T2 normalize
+/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
+qed-.
+
+lemma cpss_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ▶* T →
+ ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #L #T1 #T #HT1
+ @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #L #T1 #X
+ >shift_append_assoc normalize #H
+ elim (cpss_inv_bind1 … H) -H
+ #V0 #T0 #_ #HT10 #H destruct
+ elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
+ >append_length >HL12 -HL12
+ @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *)
+]
+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/ldrop_ldrop.ma".
+include "basic_2/unfold/cpss.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL UNFOLD FOR TERMS ******************************)
+
+(* Relocation properties ****************************************************)
+
+lemma cpss_lift: l_liftable cpss.
+#K #T1 #T2 #H elim H -K -T1 -T2
+[ #K #I #L #d #e #_ #U1 #H1 #U2 #H2
+ >(lift_mono … H1 … H2) -H1 -H2 //
+| #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HVW2 … HWU2 ?) -W2 // <minus_plus #W2 #HVW2 #HWU2
+ elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=2/ #X #HLK #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K #Y #HKV #HVY #H destruct /3 width=8/
+ | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 // /2 width=1/ >plus_plus_comm_23 #HVU2
+ lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6/
+ ]
+| #K #a #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+ elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+ elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/
+| #K #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+ elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+ elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/
+]
+qed.
+
+lemma cpss_inv_lift1: l_deliftable_sn cpss.
+#L #U1 #U2 #H elim H -L -U1 -U2
+[ #L * #i #K #d #e #_ #T1 #H
+ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
+ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/
+ | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/
+ ]
+| #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
+ elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+ [ elim (ldrop_conf_lt … HLK … HLV ?) -L // #L #U #HKL #HLV #HUV
+ elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
+ elim (lift_trans_le … HUV2 … HVW2 ?) -V2 // >minus_plus <plus_minus_m_m // -Hid /3 width=8/
+ | elim (le_inv_plus_l … Hid) #Hdie #Hei
+ lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
+ elim (lift_split … HVW2 d (i - e + 1) ? ? ?) -HVW2 [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie
+ #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O /3 width=8/
+ ]
+| #L #a #I #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+ elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
+ elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=5/
+| #L #I #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+ elim (IHV12 … HLK … HWV1) -V1
+ elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5/
+]
+qed-.
lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → ♯{T1} ≤ ♯{T2}.
#L #T1 #T2 #d #e * #T #HT1 #HT2
->(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw/
+>(lift_fwd_tw … HT2) -T2 /2 width=4 by tpss_fwd_tw/
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/frsup.ma".
-
-(* PLUS-ITERATED RESTRICTED SUPCLOSURE **************************************)
-
-definition frsupp: bi_relation lenv term ≝ bi_TC … frsup.
-
-interpretation "plus-iterated restricted structural predecessor (closure)"
- 'RestSupTermPlus L1 T1 L2 T2 = (frsupp L1 T1 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma frsupp_ind: ∀L1,T1. ∀R:relation2 lenv term.
- (∀L2,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → R L2 T2) →
- (∀L,T,L2,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ → R L T → R L2 T2) →
- ∀L2,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → R L2 T2.
-#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
-@(bi_TC_ind … IH1 IH2 ? ? H)
-qed-.
-
-lemma frsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
- (∀L1,T1. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → R L1 T1) →
- (∀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.
-#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
-@(bi_TC_ind_dx … IH1 IH2 ? ? H)
-qed-.
-
-(* Baic inversion lemmas ****************************************************)
-
-lemma frsupp_inv_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨
- ∃∃L,T. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ & ⦃L, T⦄ ⧁ ⦃L2, T2⦄.
-/2 width=1 by bi_TC_decomp_r/ qed-.
-
-lemma frsupp_inv_sn: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨
- ∃∃L,T. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ & ⦃L, T⦄ ⧁+ ⦃L2, T2⦄.
-/2 width=1 by bi_TC_decomp_l/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma frsup_frsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma frsupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ →
- ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma frsupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ → ⦃L, T⦄ ⧁+ ⦃L2, T2⦄ →
- ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma frsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
-#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
-/3 width=3 by frsup_fwd_fw, transitive_lt/
-qed-.
-
-lemma frsupp_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}.
-#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
-/2 width=3 by frsup_fwd_lw/ (**) (* /3 width=5 by frsup_fwd_lw, transitive_le/ is too slow *)
-#L #T #L2 #T2 #_ #HL2 #HL1
-lapply (frsup_fwd_lw … HL2) -HL2 /2 width=3 by transitive_le/
-qed-.
-
-lemma frsupp_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}.
-#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
-/3 width=3 by frsup_fwd_tw, transitive_lt/
-qed-.
-
-lemma frsupp_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L.
-#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 /2 width=3 by frsup_fwd_append/
-#L #T #L2 #T2 #_ #HL2 * #K1 #H destruct
-elim (frsup_fwd_append … HL2) -HL2 #K2 #H destruct /2 width=2/
-qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma lift_frsupp_trans: ∀L,U1,K,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ →
- ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
- ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
-#L #U1 @(f2_ind … fw … L U1) -L -U1 #n #IH
-#L #U1 #Hn #K #U2 #H #T1 #d #e #HTU1 destruct
-elim (frsupp_inv_sn … H) -H /2 width=5 by lift_frsup_trans/ *
-#L0 #U0 #HL0 #HL
-elim (frsup_fwd_append … HL0) #K0 #H destruct
-elim (frsupp_fwd_append … HL) #L0 >append_assoc #H
-elim (append_inj_dx … H ?) -H // #_ #H destruct
-<append_assoc in HL; #HL
-elim (lift_frsup_trans … HTU1 … HL0) -T1 #T #HTU
-lapply (frsup_fwd_fw … HL0) -HL0 #HL0
-elim (IH … HL … HTU) -IH -HL -T // -L -U1 -U0 /2 width=2/
-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/unfold/frsupp.ma".
-
-(* PLUS-ITERATED RESTRICTED SUPCLOSURE **************************************)
-
-(* Main propertis ***********************************************************)
-
-theorem frsupp_trans: bi_transitive … frsupp.
-/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/unfold/frsupp.ma".
-
-(* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************)
-
-definition frsups: bi_relation lenv term ≝ bi_star … frsup.
-
-interpretation "star-iterated restricted structural predecessor (closure)"
- 'RestSupTermStar L1 T1 L2 T2 = (frsups L1 T1 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma frsups_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.
-#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
-@(bi_star_ind … IH1 IH2 ? ? H)
-qed-.
-
-lemma frsups_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.
-#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
-@(bi_star_ind_dx … IH1 IH2 ? ? H)
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma frsups_refl: bi_reflexive … frsups.
-/2 width=1/ qed.
-
-lemma frsupp_frsups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma frsup_frsups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma frsups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁* ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ →
- ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma frsups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ → ⦃L, T⦄ ⧁* ⦃L2, T2⦄ →
- ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma frsups_frsupp_frsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁* ⦃L, T⦄ →
- ⦃L, T⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma frsupp_frsups_frsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ →
- ⦃L, T⦄ ⧁* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma frsups_inv_all: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ →
- (L1 = L2 ∧ T1 = T2) ∨ ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
-#L1 #L2 #T1 #T2 * /2 width=1/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma frsups_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}.
-#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
-/3 width=1 by frsupp_fwd_fw, lt_to_le/
-qed-.
-
-lemma frsups_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}.
-#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
-/2 width=3 by frsupp_fwd_lw/
-qed-.
-
-lemma frsups_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{T2} ≤ ♯{T1}.
-#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
-/3 width=3 by frsupp_fwd_tw, lt_to_le/
-qed-.
-
-lemma frsups_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L.
-#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H
-[ * #H1 #H2 destruct
- @(ex_intro … (⋆)) //
-| /2 width=3 by frsupp_fwd_append/
-qed-.
-
-(* Advanced forward lemmas ***************************************************)
-
-lemma lift_frsups_trans: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
- ∀L,K,U2. ⦃L, U1⦄ ⧁* ⦃L @@ K, U2⦄ →
- ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
-#T1 #U1 #d #e #HTU1 #L #K #U2 #H elim (frsups_inv_all … H) -H
-[ * #H1 #H2 destruct
- >(append_inv_refl_dx … (sym_eq … H1)) -H1 normalize /2 width=2/
-| /2 width=5 by lift_frsupp_trans/
-]
-qed-.
-
-(* Advanced inversion lemmas for frsupp **************************************)
-
-lemma frsupp_inv_atom1_frsups: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⧁+ ⦃L2, T2⦄ → ⊥.
-#J #L1 #L2 #T2 #H @(frsupp_ind … H) -L2 -T2 //
-#L2 #T2 #H elim (frsup_inv_atom1 … H)
-qed-.
-
-lemma frsupp_inv_bind1_frsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⧁+ ⦃L2, T2⦄ →
- ⦃L1, W⦄ ⧁* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⧁* ⦃L2, T2⦄.
-#b #J #L1 #L2 #W #U #T2 #H @(frsupp_ind … H) -L2 -T2
-[ #L2 #T2 #H
- elim (frsup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/
-| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
-]
-qed-.
-
-lemma frsupp_inv_flat1_frsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⧁+ ⦃L2, T2⦄ →
- ⦃L1, W⦄ ⧁* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ ⧁* ⦃L2, T2⦄.
-#J #L1 #L2 #W #U #T2 #H @(frsupp_ind … H) -L2 -T2
-[ #L2 #T2 #H
- elim (frsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/
-| #L #T #L2 #T2 #_ #HT2 * /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/unfold/frsups.ma".
-
-(* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************)
-
-(* Main propertis ***********************************************************)
-
-theorem frsups_trans: bi_transitive … frsups.
-/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/substitution/fsup.ma".
+
+(* PLUS-ITERATED SUPCLOSURE *************************************************)
+
+definition fsupp: bi_relation lenv term ≝ bi_TC … fsup.
+
+interpretation "plus-iterated structural successor (closure)"
+ 'SupTermPlus L1 T1 L2 T2 = (fsupp L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma fsupp_ind: ∀L1,T1. ∀R:relation2 lenv term.
+ (∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L2 T2) →
+ (∀L,T,L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ → R L T → R L2 T2) →
+ ∀L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L2 T2.
+#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
+@(bi_TC_ind … IH1 IH2 ? ? H)
+qed-.
+
+lemma fsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
+ (∀L1,T1. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L1 T1) →
+ (∀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.
+#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
+@(bi_TC_ind_dx … IH1 IH2 ? ? H)
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fsup_fsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma fsupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fsupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fsupp_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
+#L1 #L2 #T1 #T2 #H @(fsupp_ind … H) -L2 -T2
+/3 width=3 by fsup_fwd_cw, transitive_lt/
+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/unfold/fsupp.ma".
+
+(* PLUS-ITERATED SUPCLOSURE *************************************************)
+
+(* Main propertis ***********************************************************)
+
+theorem fsupp_trans: bi_transitive … fsupp.
+/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/unfold/cpss.ma".
+
+(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+
+inductive lcpss: relation lenv ≝
+| lcpss_atom: lcpss (⋆) (⋆)
+| lcpss_pair: ∀I,L1,L2,V1,V2. lcpss L1 L2 → L1 ⊢ V1 ▶* V2 →
+ lcpss (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
+.
+
+interpretation "parallel unfold (local environment, sn variant)"
+ 'PSubstStarSn L1 L2 = (lcpss L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lcpss_inv_atom1_aux: ∀L1,L2. L1 ⊢ ▶* L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lcpss_inv_atom1: ∀L2. ⋆ ⊢ ▶* L2 → L2 = ⋆.
+/2 width=5 by lcpss_inv_atom1_aux/ qed-.
+
+fact lcpss_inv_pair1_aux: ∀L1,L2. L1 ⊢ ▶* L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2.
+#L1 #L2 * -L1 -L2
+[ #I #K1 #V1 #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #J #K1 #W1 #H destruct /2 width=5/
+]
+qed-.
+
+lemma lcpss_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* L2 →
+ ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2.
+/2 width=5 by lcpss_inv_pair1_aux/ qed-.
+
+fact lcpss_inv_atom2_aux: ∀L1,L2. L1 ⊢ ▶* L2 → L2 = ⋆ → L1 = ⋆.
+#L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lcpss_inv_atom2: ∀L1. L1 ⊢ ▶* ⋆ → L1 = ⋆.
+/2 width=5 by lcpss_inv_atom2_aux/ qed-.
+
+fact lcpss_inv_pair2_aux: ∀L1,L2. L1 ⊢ ▶* L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1.
+#L1 #L2 * -L1 -L2
+[ #I #K1 #V1 #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #J #K2 #W2 #H destruct /2 width=5/
+]
+qed-.
+
+lemma lcpss_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ▶* K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1.
+/2 width=5 by lcpss_inv_pair2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lcpss_refl: ∀L. L ⊢ ▶* L.
+#L elim L -L // /2 width=1/
+qed.
+
+lemma lcpss_append: ∀K1,K2. K1 ⊢ ▶* K2 → ∀L1,L2. L1 ⊢ ▶* L2 →
+ L1 @@ K1 ⊢ ▶* L2 @@ K2.
+#K1 #K2 #H elim H -K1 -K2 // /3 width=1/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lcpss_fwd_length: ∀L1,L2. L1 ⊢ ▶* L2 → |L1| = |L2|.
+#L1 #L2 #H elim H -L1 -L2 normalize //
+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/fsup.ma".
+include "basic_2/unfold/lcpss_ldrop.ma".
+
+(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+
+(* Main properties on context-sensitive parallel unfold for terms ***********)
+
+fact cpss_conf_lcpss_aux: ∀L0,i. (
+ ∀L,T0.♯{L, T0} < ♯{L0, #i} →
+ ∀T1. L ⊢ T0 ▶* T1 → ∀T2. L ⊢ T0 ▶* T2 →
+ ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
+ ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ▶* T
+ ) →
+ ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+ ∀V2. K0 ⊢ V0 ▶* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
+ ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 →
+ ∃∃T. L1 ⊢ #i ▶* T & L2 ⊢ T2 ▶* T.
+#L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
+elim (lcpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
+elim (lcpss_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
+elim (lcpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
+elim (lcpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
+elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
+elim (lift_total V 0 (i+1)) #T #HVT
+lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
+qed-.
+
+theorem cpss_conf_lcpss: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀T2. L0 ⊢ T0 ▶* T2 →
+ ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 →
+ ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ▶* T.
+#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*]
+[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
+ elim (cpss_inv_atom1 … H1) -H1
+ elim (cpss_inv_atom1 … H2) -H2
+ [ #H2 #H1 destruct /2 width=3/
+ | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct
+ /3 width=10 by cpss_conf_lcpss_aux/
+ | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct
+ /4 width=10 by ex2_commute, cpss_conf_lcpss_aux/
+ | * #X #Y #V2 #z #H #HV02 #HVT2 #H2
+ * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
+ lapply (ldrop_mono … H … HLK0) -H #H destruct
+ elim (lcpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
+ elim (lcpss_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
+ elim (lcpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
+ elim (lcpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+ lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
+ elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
+ elim (lift_total V 0 (i+1)) #T #HVT
+ lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
+ lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/
+ ]
+| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+ elim (cpss_inv_bind1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
+ elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
+ elim (IH … HV01 … HV02 … HL01 … HL02) //
+ elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/
+| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+ elim (cpss_inv_flat1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
+ elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
+ elim (IH … HV01 … HV02 … HL01 … HL02) //
+ elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/
+]
+qed-.
+
+theorem cpss_conf: ∀L. confluent … (cpss L).
+/2 width=6 by cpss_conf_lcpss/ qed-.
+
+theorem cpss_trans_lcpss: ∀L1,T1,T. L1 ⊢ T1 ▶* T → ∀L2. L1 ⊢ ▶* L2 →
+ ∀T2. L2 ⊢ T ▶* T2 → L1 ⊢ T1 ▶* T2.
+#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*]
+[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct
+ elim (cpss_inv_atom1 … H1) -H1
+ [ #H destruct
+ elim (cpss_inv_atom1 … HT2) -HT2
+ [ #H destruct //
+ | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
+ elim (lcpss_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+ elim (lcpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct
+ lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+ ]
+ | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
+ elim (lcpss_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+ elim (lcpss_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+ elim (cpss_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T
+ lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+ ]
+| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+ elim (cpss_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+ elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
+| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+ elim (cpss_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+ elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+]
+qed-.
+
+theorem cpss_trans: ∀L. Transitive … (cpss L).
+/2 width=5 by cpss_trans_lcpss/ qed-.
+
+(* Properties on context-sensitive parallel unfold for terms ****************)
+
+lemma lcpss_cpss_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 →
+ ∃∃T. L1 ⊢ T0 ▶* T & L1 ⊢ T1 ▶* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (cpss_conf_lcpss … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/
+qed-.
+
+lemma lcpss_cpss_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 →
+ ∃∃T. L1 ⊢ T0 ▶* T & L0 ⊢ T1 ▶* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (cpss_conf_lcpss … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/
+qed-.
+
+lemma lcpss_cpss_trans: ∀L1,L2. L1 ⊢ ▶* L2 →
+ ∀T1,T2. L2 ⊢ T1 ▶* T2 → L1 ⊢ T1 ▶* T2.
+/2 width=5 by cpss_trans_lcpss/ qed-.
+
+lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 →
+ ∃∃L,U1. L1 ⊢ ▶* L & L ⊢ T1 ▶* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
+elim (lift_total T d e) #U #HTU
+elim (ldrop_lcpss_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K
+lapply (cpss_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+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/unfold/lcpss_cpss.ma".
+
+(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+(* Main properties **********************************************************)
+
+theorem lcpss_conf: confluent … lcpss.
+#L0 @(f_ind … length … L0) -L0 #n #IH *
+[ #_ #X1 #H1 #X2 #H2 -n
+ >(lcpss_inv_atom1 … H1) -X1
+ >(lcpss_inv_atom1 … H2) -X2 /2 width=3/
+| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
+ elim (lcpss_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
+ elim (lcpss_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
+ elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
+ elim (cpss_conf_lcpss … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/
+]
+qed-.
+
+theorem lcpss_trans: Transitive … lcpss.
+#L1 #L #H elim H -L1 -L //
+#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H
+elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct
+lapply (cpss_trans_lcpss … HV1 … HL1 … HV2) -V -HL1 /3 width=1/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpss_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ▶* T →
+ ∃∃L2,T2. L @@ L1 ⊢ ▶* L @@ L2 & L @@ L1 ⊢ T1 ▶* T2 &
+ T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1
+[ #L #T1 #T #HT1
+ @ex3_2_intro [3: // |4,5: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H <append_assoc
+ elim (cpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
+ lapply (lcpss_trans … HL12 (L.ⓑ{I}V2@@L2) ?) -HL12 /3 width=1/ #HL12
+ @(ex3_2_intro … (⋆.ⓑ{I}V2@@L2)) [4: /2 width=3/ | skip ] <append_assoc // (**) (* explicit constructor *)
+]
+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/unfold/cpss_lift.ma".
+include "basic_2/unfold/lcpss.ma".
+
+(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lcpss_ldrop_conf: dropable_sn lcpss.
+#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H
+ lapply (lcpss_inv_atom1 … H) -H #H destruct /2 width=3/
+| #L1 #I #V1 #X #H
+ elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=3/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
+ elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (IHLK1 … HL12) -IHLK1 -HL12 /3 width=3/
+| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+ elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (cpss_inv_lift1 … HV12 … HLK1 … HWV1) -HLK1 -V1
+ elim (IHLK1 … HL12) -IHLK1 -HL12 /3 width=5/
+]
+qed-.
+
+lemma ldrop_lcpss_trans: dedropable_sn lcpss.
+#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H
+ lapply (lcpss_inv_atom1 … H) -H #H destruct /2 width=3/
+| #L1 #I #V1 #X #H
+ elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=3/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
+ elim (IHLK1 … HK12) -IHLK1 -HK12 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+ elim (lcpss_inv_pair1 … H) -H #L2 #W2 #HL12 #HW12 #H destruct
+ elim (lift_total W2 d e) #V2 #HWV2
+ lapply (cpss_lift … HW12 … HLK1 … HWV1 … HWV2) -W1 -HLK1
+ elim (IHLK1 … HL12) -IHLK1 -HL12 /3 width=5/
+]
+qed-.
+
+fact lcpss_ldrop_trans_O1_aux: ∀L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. L1 ⊢ ▶* L2 →
+ d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ⊢ ▶* K2.
+#L2 #K2 #d #e #H elim H -L2 -K2 -d -e
+[ #d #e #X #H >(lcpss_inv_atom2 … H) -H /2 width=3/
+| #K2 #I #V2 #X #H
+ elim (lcpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/
+| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_
+ elim (lcpss_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 lcpss_ldrop_trans_O1: dropable_dx lcpss.
+/2 width=5 by lcpss_ldrop_trans_O1_aux/ qed-.
(* *)
(**************************************************************************)
+notation "hvbox( T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStar $T1 $d $e $T2 }.
+
include "basic_2/unfold/tpss.ma".
(* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
]
qed.
-lemma ltpss_dx_weak_all: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ▶* [0, |L2|] L2.
+lemma ltpss_dx_weak_full: ∀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.
(* *)
(**************************************************************************)
+include "basic_2/substitution/fsup.ma".
+include "basic_2/unfold/tpss_lift.ma".
include "basic_2/unfold/ltpss_dx.ma".
(* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+(* Properies on local environment slicing ***********************************)
+
lemma ltpss_dx_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
]
]
qed.
+
+lemma ldrop_ltpss_dx_trans_le: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+ ∀K2,d2,e2. K1 ▶* [d2, e2] K2 → d1 ≤ d2 →
+ ∃∃L2. L1 ▶* [d2 + e1, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_
+ >(ltpss_dx_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #Hd
+ elim (IHLK1 … HK12 Hd) -K1 -Hd /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #_ #HWV1 #IHLK1 #X #d2 #e2 #H #Hd12
+ elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hd2
+ elim (ltpss_dx_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHLK1 … HK12 … Hd12) -IHLK1 -HK12 <le_plus_minus_comm // #L2 #HL12 #HLK2
+ elim (lift_total W2 d1 e1) #V2 #HWV2
+ lapply (tpss_lift_ge … HW12 … HLK2 HWV1 … HWV2) -W1 // -Hd12
+ <le_plus_minus_comm // /4 width=5/
+]
+qed-.
+
+lemma ldrop_ltpss_dx_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+ ∀K2,d2,e2. K1 ▶* [d2, e2] K2 →
+ d2 ≤ d1 → d1 ≤ d2 + e2 →
+ ∃∃L2. L1 ▶* [d2, e1 + e2] L2 &
+ ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_ #_
+ >(ltpss_dx_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H #_
+ lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H1 #H2
+ elim (IHLK1 … HK12 H1 H2) -K1 -H2
+ lapply (le_n_O_to_eq … H1) -H1 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #_ #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 #Hd12
+ elim (eq_or_gt d2) #Hd2 [ -Hd21 elim (eq_or_gt e2) #He2 ] destruct
+ [ lapply (le_n_O_to_eq … Hd12) -Hd12 <plus_n_Sm #H destruct
+ | elim (ltpss_dx_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHLK1 … HK12 …) -IHLK1 // /2 width=1/ >plus_minus_commutative // #L2 #HL12 #HLK2
+ elim (lift_total W2 d1 e1) #V2 #HWV2
+ lapply (tpss_lift_be … HW12 … HLK2 HWV1 … HWV2) -W1 // /2 width=1/
+ >plus_minus // >commutative_plus /4 width=5/
+ | elim (ltpss_dx_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // ] /2 width=1/ #L2 #HL12 #HLK2
+ elim (lift_total W2 d1 e1) #V2 #HWV2
+ lapply (tpss_lift_be … HW12 … HLK2 HWV1 … HWV2) -W1 [ >plus_minus // ] /2 width=1/
+ >commutative_plus /3 width=5/
+ ]
+]
+qed-.
+
+lemma ldrop_ltpss_dx_trans_ge: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+ ∀K2,d2,e2. K1 ▶* [d2, e2] K2 → d2 + e2 ≤ d1 →
+ ∃∃L2. L1 ▶* [d2, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_
+ >(ltpss_dx_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H
+ elim (plus_le_0 … H) -H #H1 #H2 destruct /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H
+ elim (IHLK1 … HK12 H) -K1
+ elim (plus_le_0 … H) -H #H1 #H2 destruct #L2 #HL12
+ >(ltpss_dx_inv_refl_O2 … HL12) -L1 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21
+ elim (eq_or_gt d2) #Hd2 [ elim (eq_or_gt e2) #He2 ] destruct
+ [ -IHLK1 -Hd21 <(ltpss_dx_inv_refl_O2 … H) -X /3 width=5/
+ | elim (ltpss_dx_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHLK1 … HK12 …) -IHLK1 /2 width=1/ #L2 #HL12 #HLK2
+ elim (lift_total W2 d1 e1) #V2 #HWV2
+ lapply (tpss_lift_le … HW12 … HLK2 HWV1 … HWV2) -W1 /2 width=1/ /3 width=5/
+ | elim (ltpss_dx_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // /2 width=1/ ] #L2 #HL12 #HLK2
+ elim (lift_total W2 d1 e1) #V2 #HWV2
+ lapply (tpss_lift_le … HW12 … HLK2 HWV1 … HWV2) -W1 [ >plus_minus // /2 width=1/ ] /3 width=5/
+ ]
+]
+qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fsup_tps_trans_full: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶[0,|L2|] U2 →
+ ∃∃L,U1. L1 ▶*[0,|L|] L & L ⊢ T1 ▶[0,|L|] U1 & ⦃L, U1⦄ ⊃ ⦃L2, T2⦄.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
+elim (lift_total T d e) #U #HTU
+elim (le_or_ge d (|K|)) #Hd
+[ elim (ldrop_ltpss_dx_trans_be … HLK1 … HK1 … Hd) // -HLK1 -HK1 #L2 #HL12 #HL2K
+ lapply (tps_lift_be … HT1 … HL2K … HTU1 HTU … Hd) // -HT1 -HTU1 #HU1
+| elim (ldrop_ltpss_dx_trans_ge … HLK1 … HK1 Hd) -HLK1 -HK1 #L2 #HL12 #HL2K
+ lapply (tps_lift_le … HT1 … HL2K … HTU1 HTU Hd) -HT1 -HTU1 #HU1
+]
+lapply (ltpss_dx_weak_full … HL12) -HL12 #HL12
+lapply (tps_weak_full … HU1) -HU1 #HU1
+@(ex3_2_intro … L2 U) // /2 width=7/ (**) (* explicit constructor: auto /3 width=14/ too slow *)
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/unfold/tpss_lift.ma".
include "basic_2/unfold/ltpss_dx_tps.ma".
(* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
(* *)
(**************************************************************************)
+notation "hvbox( T1 break ⊢ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStarSn $T1 $d $e $T2 }.
+
include "basic_2/unfold/tpss.ma".
(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
]
qed.
-lemma ltpss_sn_weak_all: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ▶* [0, |L1|] L2.
+lemma ltpss_sn_weak_full: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ▶* [0, |L1|] L2.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
// /3 width=2/ /3 width=3/
qed.
(* *)
(**************************************************************************)
+notation "hvbox( T1 break ⊢ ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }.
+
include "basic_2/unfold/ltpss_dx_ltpss_dx.ma".
include "basic_2/unfold/ltpss_sn_ltpss_sn.ma".
(* *)
(**************************************************************************)
+include "basic_2/substitution/fsup.ma".
include "basic_2/unfold/tpss_lift.ma".
include "basic_2/unfold/ltpss_sn.ma".
(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+(* Properies on local environment slicing ***********************************)
+
lemma ltpss_sn_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
]
qed.
+lemma ldrop_ltpss_sn_trans_le: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+ ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d1 ≤ d2 →
+ ∃∃L2. L1 ⊢ ▶* [d2 + e1, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_
+ >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #Hd
+ elim (IHLK1 … HK12 Hd) -K1 -Hd /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd12
+ elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hd2
+ elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHLK1 … HK12 … Hd12) -IHLK1 -HK12 <le_plus_minus_comm // #L2 #HL12 #HLK2
+ elim (lift_total W2 d1 e1) #V2 #HWV2
+ lapply (tpss_lift_ge … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 // -Hd12
+ <le_plus_minus_comm // /4 width=5/
+]
+qed-.
+
lemma ldrop_ltpss_sn_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 →
d2 ≤ d1 → d1 ≤ d2 + e2 →
]
]
qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fsup_tpss_trans_full: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶*[0,|L2|] U2 →
+ ∃∃L,U1. L1 ⊢ ▶*[0,|L1|] L & L ⊢ T1 ▶*[0,|L|] U1 & ⦃L, U1⦄ ⊃ ⦃L2, T2⦄.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
+elim (lift_total T d e) #U #HTU
+lapply (ltpss_sn_fwd_length … HK1) #H >H in HK1; -H #HK1
+elim (le_or_ge d (|K|)) #Hd
+[ elim (ldrop_ltpss_sn_trans_be … HLK1 … HK1 … Hd) // -HLK1 -HK1 #L2 #HL12 #HL2K
+ lapply (tpss_lift_be … HT1 … Hd HL2K HTU1 … HTU) // -HT1 -HTU1 #HU1
+| elim (ldrop_ltpss_sn_trans_ge … HLK1 … HK1 Hd) -HLK1 -HK1 #L2 #HL12 #HL2K
+ lapply (tpss_lift_le … HT1 … Hd HL2K HTU1 … HTU) -HT1 -HTU1 #HU1
+]
+lapply (ltpss_sn_weak_full … HL12) -HL12 #HL12
+lapply (tpss_weak_full … HU1) -HU1 #HU1
+@(ex3_2_intro … L2 U) // /2 width=7/ (**) (* explicit constructor: auto /3 width=14/ too slow *)
+qed-.
(* *)
(**************************************************************************)
+notation "hvbox( L ⊢ break term 46 T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStar $L $T1 $d $e $T2 }.
+
include "basic_2/substitution/tps.ma".
(* PARTIAL UNFOLD ON TERMS **************************************************)
]
qed.
-lemma tpss_weak_all: ∀L,T1,T2,d,e.
- L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [0, |L|] T2.
+lemma tpss_weak_full: ∀L,T1,T2,d,e.
+ L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [0, |L|] T2.
#L #T1 #T2 #d #e #HT12
lapply (tpss_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
lapply (tpss_weak_top … HT12) //
(* *)
(**************************************************************************)
+notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
+
include "basic_2/unfold/tpss_lift.ma".
(* PARALLEL UNFOLD ON TERMS *************************************************)
}
]
[ { "context-free reduction" * } {
- [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ]
- [ "tpr ( ? ➡ ? )" "tpr_lift" + "tpr_tps" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ]
+ [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_tpss" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ]
+ [ "tpr ( ? ➡ ? )" "tpr_lift" + "tpr_delift" + "tpr_tpr" * ]
}
]
}
[ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ]
}
]
- [ { "partial unfold" * } {
+ [ { "revised parallel substitution" * } {
+ [ "lcpss ( ? ⊢ ▶* ? )" "lcpss_ldrop" + "lcpss_cpss" + "lcpss_lcpss" * ]
+ [ "cpss ( ? ⊢ ? ▶* ? )" "cpss_lift" * ]
+ }
+ ]
+ [ { "partial unfold" * } {
[ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" "ltpss_sn_ldrop" + "ltpss_sn_tps" + "ltpss_sn_tpss" + "ltpss_sn_ltpss_sn" * ]
[ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" + "ltpss_dx_tps" + "ltpss_dx_tpss" + "ltpss_dx_ltpss_dx" * ]
[ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
}
]
- [ { "generic local env. slicing" * } {
- [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
+ [ { "iterated structural successor for closures" * } {
+ [ "fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )" "fsupp_fsupp" * ]
}
]
- [ { "iterated restricted structural predecessor for closures" * } {
- [ "frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )" "frsups_frsups" * ]
- [ "frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )" "frsupp_frsupp" * ]
+ [ { "generic local env. slicing" * } {
+ [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
}
]
[ { "generic term relocation" * } {
[ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" + "tps_tps" * ]
}
]
+ [ { "structural successor for closures" * } {
+ [ "fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )" * ]
+ }
+ ]
[ { "global env. slicing" * } {
[ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
}
[ "lsubr ( ? ⊑[?,?] ? )" "(lsubr_lsubr)" "lsubr_lbotr ( ⊒[?,?] ? )" * ]
}
]
- [ { "restricted structural predecessor for closures" * } {
- [ "frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )" * ]
- }
- ]
[ { "basic term relocation" * } {
[ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
[ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]
projects / helm.git / commitdiff