--- /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/notation/relations/predsn_5.ma".
+include "basic_2/static/lfxs.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
+
+definition lfpr: sh → genv → relation3 term lenv lenv ≝
+ λh,G. lfxs (cpm 0 h G).
+
+interpretation
+ "parallel r-transition on referred entries (local environment)"
+ 'PRedSn h T G L1 L2 = (lfpr h G T L1 L2).
+
+(* Basic properties ***********************************************************)
+
+lemma lfpr_atom: ∀h,I,G. ⦃G, ⋆⦄ ⊢ ➡[h, ⓪{I}] ⋆.
+/2 width=1 by lfxs_atom/ qed.
+
+lemma lfpr_sort: ∀h,I,G,L1,L2,V1,V2,s.
+ ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, ⋆s] L2.ⓑ{I}V2.
+/2 width=1 by lfxs_sort/ qed.
+
+lemma lfpr_zero: ∀h,I,G,L1,L2,V.
+ ⦃G, L1⦄ ⊢ ➡[h, V] L2 → ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, #0] L2.ⓑ{I}V.
+/2 width=1 by lfxs_zero/ qed.
+
+lemma lfpr_lref: ∀h,I,G,L1,L2,V1,V2,i.
+ ⦃G, L1⦄ ⊢ ➡[h, #i] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #⫯i] L2.ⓑ{I}V2.
+/2 width=1 by lfxs_lref/ qed.
+
+lemma lfpr_gref: ∀h,I,G,L1,L2,V1,V2,l.
+ ⦃G, L1⦄ ⊢ ➡[h, §l] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, §l] L2.ⓑ{I}V2.
+/2 width=1 by lfxs_gref/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfpr_inv_atom_sn: ∀h,I,G,Y2. ⦃G, ⋆⦄ ⊢ ➡[h, ⓪{I}] Y2 → Y2 = ⋆.
+/2 width=3 by lfxs_inv_atom_sn/ qed-.
+
+lemma lfpr_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ➡[h, ⓪{I}] ⋆ → Y1 = ⋆.
+/2 width=3 by lfxs_inv_atom_dx/ qed-.
+
+lemma lfpr_inv_zero: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ➡[h, #0] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 &
+ ⦃G, L1⦄ ⊢ V1 ➡[h] V2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+/2 width=1 by lfxs_inv_zero/ qed-.
+
+lemma lfpr_inv_lref: ∀h,G,Y1,Y2,i. ⦃G, Y1⦄ ⊢ ➡[h, #⫯i] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+/2 width=1 by lfxs_inv_lref/ qed-.
+
+lemma lfpr_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V.T] L2 →
+ ⦃G, L1⦄ ⊢ ➡[h, V] L2 ∧ ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, T] L2.ⓑ{I}V.
+/2 width=2 by lfxs_inv_bind/ qed-.
+
+lemma lfpr_inv_flat: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, ⓕ{I}V.T] L2 →
+ ⦃G, L1⦄ ⊢ ➡[h, V] L2 ∧ ⦃G, L1⦄ ⊢ ➡[h, T] L2.
+/2 width=2 by lfxs_inv_flat/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lfpr_inv_zero_pair_sn: ∀h,I,G,Y2,L1,V1. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #0] Y2 →
+ ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h] V2 &
+ Y2 = L2.ⓑ{I}V2.
+/2 width=1 by lfxs_inv_zero_pair_sn/ qed-.
+
+lemma lfpr_inv_zero_pair_dx: ∀h,I,G,Y1,L2,V2. ⦃G, Y1⦄ ⊢ ➡[h, #0] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h] V2 &
+ Y1 = L1.ⓑ{I}V1.
+/2 width=1 by lfxs_inv_zero_pair_dx/ qed-.
+
+lemma lfpr_inv_lref_pair_sn: ∀h,I,G,Y2,L1,V1,i. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #⫯i] Y2 →
+ ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 & Y2 = L2.ⓑ{I}V2.
+/2 width=2 by lfxs_inv_lref_pair_sn/ qed-.
+
+lemma lfpr_inv_lref_pair_dx: ∀h,I,G,Y1,L2,V2,i. ⦃G, Y1⦄ ⊢ ➡[h, #⫯i] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 & Y1 = L1.ⓑ{I}V1.
+/2 width=2 by lfxs_inv_lref_pair_dx/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lfpr_fwd_bind_sn: ∀h,p,I,G,L1,L2,V,T.
+ ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, V] L2.
+/2 width=4 by lfxs_fwd_bind_sn/ qed-.
+
+lemma lfpr_fwd_bind_dx: ∀h,p,I,G,L1,L2,V,T.
+ ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V.T] L2 → ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, T] L2.ⓑ{I}V.
+/2 width=2 by lfxs_fwd_bind_dx/ qed-.
+
+lemma lfpr_fwd_flat_sn: ∀h,I,G,L1,L2,V,T.
+ ⦃G, L1⦄ ⊢ ➡[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, V] L2.
+/2 width=3 by lfxs_fwd_flat_sn/ qed-.
+
+lemma lfpr_fwd_flat_dx: ∀h,I,G,L1,L2,V,T.
+ ⦃G, L1⦄ ⊢ ➡[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, T] L2.
+/2 width=3 by lfxs_fwd_flat_dx/ qed-.
+
+lemma lfpr_fwd_pair_sn: ∀h,I,G,L1,L2,V,T.
+ ⦃G, L1⦄ ⊢ ➡[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, V] L2.
+/2 width=3 by lfxs_fwd_pair_sn/ qed-.
+
+(* Basic_2A1: removed theorems 11:
+ lpr_inv_atom1 lpr_inv_pair1 lpr_inv_atom2 lpr_inv_pair2
+ lpr_refl lpr_pair
+ lpr_fwd_length lpr_lpx
+ lpr_drop_conf drop_lpr_trans lpr_drop_trans_O1
+*)
+(* Basic_1: removed theorems 7: wcpr0_gen_sort wcpr0_gen_head
+ wcpr0_getl wcpr0_getl_back
+ pr0_subst1_back
+ wcpr0_drop wcpr0_drop_back
+*)
--- /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/lfxs_drops.ma".
+include "basic_2/rt_transition/cpm_drops.ma".
+include "basic_2/rt_transition/lfpr.ma".
+
+(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
+
+(* Properties with generic slicing for local environments *******************)
+
+lemma drops_lfpr_trans: ∀h,G. dedropable_sn (cpm 0 h G).
+/3 width=6 by lfxs_liftable_dedropable, cpm_lifts/ qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+lemma lfpr_drops_conf: ∀h,G. dropable_sn (cpm 0 h G).
+/2 width=5 by lfxs_dropable_sn/ qed-.
+
+lemma lfpr_drops_trans: ∀h,G. dropable_dx (cpm 0 h G).
+/2 width=5 by lfxs_dropable_dx/ 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/lfxs_fqup.ma".
+include "basic_2/rt_transition/lfpr.ma".
+
+(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
+
+(* Advanced properties ******************************************************)
+
+(* Note: lemma 250 *)
+lemma lfpr_refl: ∀h,G,T. reflexive … (lfpr h G T).
+/2 width=1 by lfxs_refl/ 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/lfxs_length.ma".
+include "basic_2/rt_transition/lfpr.ma".
+
+(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
+
+(* Forward lemmas with length for local environments ************************)
+
+lemma lfpr_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → |L1| = |L2|.
+/2 width=3 by lfxs_fwd_length/ 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/rt_transition/lfpx.ma".
+include "basic_2/rt_transition/cpm_cpx.ma".
+include "basic_2/rt_transition/lfpr.ma".
+
+(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
+
+(* Fwd. lemmas with unc. rt-transition for local env.s on referred entries **)
+
+lemma lfpr_fwd_lfpx: ∀h,T,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2.
+/3 width=3 by cpm_fwd_cpx, lfxs_co/ qed-.
/2 width=3 by lfxs_inv_atom_dx/ qed-.
lemma lfpx_inv_zero: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ⬈[h, #0] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 &
⦃G, L1⦄ ⊢ V1 ⬈[h] V2 &
Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
/2 width=1 by lfxs_inv_zero/ qed-.
lemma lfpx_inv_lref: ∀h,G,Y1,Y2,i. ⦃G, Y1⦄ ⊢ ⬈[h, #⫯i] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 &
Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
/2 width=1 by lfxs_inv_lref/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma lfpx_fwd_bind_sn: ∀h,p,I,G,L1,L2,V,T.
+lemma lfpx_fwd_bind_sn: ∀h,p,I,G,L1,L2,V,T.
⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, V] L2.
/2 width=4 by lfxs_fwd_bind_sn/ 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/notation/relations/predsn_3.ma".
-include "basic_2/substitution/lpx_sn.ma".
-include "basic_2/reduction/cpr.ma".
-
-(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
-
-definition lpr: relation3 genv lenv lenv ≝ λG. lpx_sn (cpr G).
-
-interpretation "parallel reduction (local environment, sn variant)"
- 'PRedSn G L1 L2 = (lpr G L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-(* Basic_1: includes: wcpr0_gen_sort *)
-lemma lpr_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ➡ L2 → L2 = ⋆.
-/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
-
-(* Basic_1: includes: wcpr0_gen_head *)
-lemma lpr_inv_pair1: ∀I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ L2 →
- ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡ K2 & ⦃G, K1⦄ ⊢ V1 ➡ V2 & L2 = K2.ⓑ{I}V2.
-/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
-
-lemma lpr_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ➡ ⋆ → L1 = ⋆.
-/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
-
-lemma lpr_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡ K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡ K2 & ⦃G, K1⦄ ⊢ V1 ➡ V2 & L1 = K1. ⓑ{I} V1.
-/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
-
-(* Basic properties *********************************************************)
-
-(* Note: lemma 250 *)
-lemma lpr_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡ L.
-/2 width=1 by lpx_sn_refl/ qed.
-
-lemma lpr_pair: ∀I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡ K2 → ⦃G, K1⦄ ⊢ V1 ➡ V2 →
- ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ K2.ⓑ{I}V2.
-/2 width=1 by lpx_sn_pair/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lpr_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → |L1| = |L2|.
-/2 width=2 by lpx_sn_fwd_length/ qed-.
-
-lemma lpr_lpx: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, o] L2.
-#h #o #G #L1 #L2 #H elim H -L1 -L2 /3 width=1 by lpx_pair, cpr_cpx/
-qed.
-
-(* Basic_1: removed theorems 3: wcpr0_getl wcpr0_getl_back
- pr0_subst1_back
-*)
+++ /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/lpx_sn_drop.ma".
-include "basic_2/substitution/fquq_alt.ma".
-include "basic_2/reduction/cpr_lift.ma".
-include "basic_2/reduction/lpr.ma".
-
-(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
-
-(* Properties on local environment slicing ***********************************)
-
-(* Basic_1: includes: wcpr0_drop *)
-lemma lpr_drop_conf: ∀G. dropable_sn (lpr G).
-/3 width=6 by lpx_sn_deliftable_dropable, cpr_inv_lift1/ qed-.
-
-(* Basic_1: includes: wcpr0_drop_back *)
-lemma drop_lpr_trans: ∀G. dedropable_sn (lpr G).
-/3 width=10 by lpx_sn_liftable_dedropable, cpr_lift/ qed-.
-
-lemma lpr_drop_trans_O1: ∀G. dropable_dx (lpr G).
-/2 width=3 by lpx_sn_dropable/ qed-.
-
-(* Properties on context-sensitive parallel reduction for terms *************)
-
-lemma fqu_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
- ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/
-#G #L #K #U #T #k #HLK #HUT #U2 #HU2
-elim (lift_total U2 0 (k+1)) #T2 #HUT2
-lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/
-qed-.
-
-lemma fquq_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
- ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (fqu_cpr_trans_dx … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma fqu_cpr_trans_sn: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
- ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L1⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/
-#G #L #K #U #T #k #HLK #HUT #U2 #HU2
-elim (lift_total U2 0 (k+1)) #T2 #HUT2
-lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/
-qed-.
-
-lemma fquq_cpr_trans_sn: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
- ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L1⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (fqu_cpr_trans_sn … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma fqu_lpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ➡ K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡ K1 & ⦃G1, L1⦄ ⊢ T1 ➡ T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpr_pair, ex3_2_intro/
-[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpr_inv_pair1 … H) -H
- #K2 #W2 #HLK2 #HVW2 #H destruct
- /3 width=5 by fqu_fquq, cpr_pair_sn, fqu_bind_dx, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #k #HLK1 #HTU1 #K2 #HK12
- elim (drop_lpr_trans … HLK1 … HK12) -HK12
- /3 width=7 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma fquq_lpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ➡ K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡ K1 & ⦃G1, L1⦄ ⊢ T1 ➡ T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (fqu_lpr_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
--- /dev/null
+(* Properties on context-sensitive parallel reduction for terms *************)
+
+lemma fqu_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
+ ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/
+#G #L #K #U #T #k #HLK #HUT #U2 #HU2
+elim (lift_total U2 0 (k+1)) #T2 #HUT2
+lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/
+qed-.
+
+lemma fquq_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
+ ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_cpr_trans_dx … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma fqu_cpr_trans_sn: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
+ ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L1⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/
+#G #L #K #U #T #k #HLK #HUT #U2 #HU2
+elim (lift_total U2 0 (k+1)) #T2 #HUT2
+lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/
+qed-.
+
+lemma fquq_cpr_trans_sn: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
+ ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L1⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_cpr_trans_sn … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma fqu_lpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∀K2. ⦃G2, L2⦄ ⊢ ➡ K2 →
+ ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡ K1 & ⦃G1, L1⦄ ⊢ T1 ➡ T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpr_pair, ex3_2_intro/
+[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpr_inv_pair1 … H) -H
+ #K2 #W2 #HLK2 #HVW2 #H destruct
+ /3 width=5 by fqu_fquq, cpr_pair_sn, fqu_bind_dx, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #k #HLK1 #HTU1 #K2 #HK12
+ elim (drop_lpr_trans … HLK1 … HK12) -HK12
+ /3 width=7 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma fquq_lpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ∀K2. ⦃G2, L2⦄ ⊢ ➡ K2 →
+ ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡ K1 & ⦃G1, L1⦄ ⊢ T1 ➡ T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_lpr_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma
cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_cpx.ma
cpr.ma cpr_drops.ma
+lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_lfpx.ma
]
*)
[ { "t-bound context-sensitive rt-transition" * } {
-(* [ "lpr ( ⦃?,?⦄ ⊢ ➡ ? )" "lpr_drop" + "lpr_lpr" * ] *)
+ [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_lfpx" * ]
[ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" (* + "cpr_llpx_sn" + "cpr_cir" *) * ]
[ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_cpx" * ]
}
projects / helm.git / commitdiff