#h #g #G #L2 #T1 #T2 #H @(cpxs_ind_dx … H) -T1
/4 width=6 by lleq_cpx_conf_dx, lleq_cpx_trans, cpxs_strap2/
qed-.
+
+lemma lleq_cpxs_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 →
+ ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2.
+#h #g #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by lleq_cpx_conf_dx/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/lpxs.ma".
+include "basic_2/computation/fpbs.ma".
include "basic_2/computation/csx_lpx.ma".
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
(* Advanced properties ******************************************************)
+lemma csx_fpb_conf: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, g] T2.
+#h #g #G1 #L1 #T1 #HT1 #G2 #L2 #T2 *
+/2 width=5 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf/
+qed-.
+
+lemma csx_fpbs_conf: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, g] T2.
+#h #g #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
+/2 width=5 by csx_fpb_conf/
+qed-.
+
lemma csx_lpxs_conf: ∀h,g,G,L1. ∀T:term. ⦃G, L1⦄ ⊢ ⬊*[h, g] T →
∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L1 #T #HT #L2 #H @(lpxs_ind … H) -L2 /2 width=3 by csx_lpx_conf/
+/3 width=5 by csx_fpbs_conf, lpxs_fpbs/
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/btpredproper_8.ma".
-include "basic_2/relocation/lleq.ma".
-include "basic_2/computation/fpbs.ma".
-
-(* ATOMIC "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************)
-
-inductive fpbc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpbc_fqup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbc h g G1 L1 T1 G2 L2 T2
-| fpbc_cpxs: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbc h g G1 L1 T1 G1 L1 T2
-| fpbc_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T1] L2 → ⊥) → fpbc h g G1 L1 T1 G1 L2 T1
-.
-
-interpretation
- "'big tree' proper parallel reduction (closure)"
- 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpbc h g G1 L1 T1 G2 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma cprs_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
- ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
-/3 width=1 by fpbc_cpxs, cprs_cpxs/ qed.
-
-lemma lprs_fpbc: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[0, T] L2 → ⊥) →
- ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄.
-/3 width=1 by fpbc_lpxs, lprs_lpxs/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fpbc_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=1 by lpxs_fpbs, cpxs_fpbs, fqup_fpbs/
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/fpbs_fpns.ma".
+include "basic_2/computation/fpbs_fpbs.ma".
+include "basic_2/computation/fpbc.ma".
+
+(* SINGLE-STEP "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********)
+
+(* Forward lemmas on "big tree" parallel computation for closures ***********)
+
+lemma fpbc_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 *
+/3 width=5 by fpbu_fwd_fpbs, fpbs_trans, fpns_fpbs/
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/lleq_lleq.ma".
-include "basic_2/computation/fpns.ma".
-include "basic_2/computation/fpbs_alt.ma".
-include "basic_2/computation/fpbc.ma".
-
-(* ATOMIC "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************)
-
-(* Forward lemmas on parallel computation for "big tree" normal forms *******)
-
-lemma fpbs_fwd_fpbc_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ ∨
- ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_fpbsa … H) -H
-#L #T #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct
-[ -HT1 elim (fqus_inv_gen … HT2) -HT2
- [ #HT2 @or_intror
- /5 width=9 by fpbsa_inv_fpbs, fpbc_fqup, ex3_2_intro, ex2_3_intro, or_intror/
- | * #HG #HL #HT destruct elim (lleq_dec T2 L L2 0) #H
- [ /3 width=1 by fpns_intro, or_introl/
- | /5 width=5 by fpbc_lpxs, ex2_3_intro, or_intror/
- ]
- ]
-| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H
- /5 width=9 by fpbsa_inv_fpbs, fpbc_cpxs, cpx_cpxs, ex3_2_intro, ex2_3_intro, or_intror/
-]
-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_ssta.ma".
-include "basic_2/computation/cpxs_lift.ma".
-include "basic_2/computation/fpbc.ma".
-
-(* ATOMIC "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************)
-
-(* Advanced properties ******************************************************)
-
-lemma lsstas_fpbc: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) →
- ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
-/4 width=5 by fpbc_cpxs, lsstas_cpxs/ qed.
-
-lemma ssta_fpbc: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 →
- ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2)
-/3 width=5 by ssta_lsstas, lsstas_fpbc/ #H destruct
-elim (ssta_inv_refl_pos … HT1 … HT12)
-qed.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/btpredstarproper_8.ma".
+include "basic_2/notation/relations/lazybtpredstarproper_8.ma".
include "basic_2/computation/fpbc.ma".
(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************)
-(* Note: this is not transitive *)
-inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpbg_cpxs: ∀L2,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 →
- fpbg h g G1 L1 T1 G1 L2 T2
-| fpbg_fqup: ∀G2,L,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃+ ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 →
- fpbg h g G1 L1 T1 G2 L2 T2
-| fpbg_lpxs: ∀G2,L,L0,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L0 →
- (L ⋕[0, T2] L0 → ⊥) → ⦃G2, L0⦄ ⊢ ➡*[h, g] L2 → L0 ⋕[0, T2] L2 →
- fpbg h g G1 L1 T1 G2 L2 T2
-.
+definition fpbg: ∀h. sd h → tri_relation genv lenv term ≝
+ λh,g. tri_TC … (fpbc h g).
-interpretation "'big tree' proper parallel computation (closure)"
- 'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2).
+interpretation "general 'big tree' proper parallel computation (closure)"
+ 'LazyBTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2).
(* Basic properties *********************************************************)
-lemma fpbc_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=9 by fpbg_fqup, fpbg_cpxs, fpbg_lpxs/
-qed.
+lemma fpbc_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+/2 width=1 by tri_inj/ qed.
+
+lemma fpbg_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2.
+ ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+/2 width=5 by tri_step/ qed.
+
+lemma fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2.
+ ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+/2 width=5 by tri_TC_strap/ qed.
+
+(* Note: this is used in the closure proof *)
+lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+/4 width=1 by fpbc_fpbg, fpbu_fpbc, fpbu_fqup/ qed.
+
+(* Basic eliminators ********************************************************)
+
+lemma fpbg_ind: ∀h,g,G1,L1,T1. ∀R:relation3 ….
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2.
+#h #g #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
+@(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
+qed-.
+
+lemma fpbg_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 ….
+ (∀G1,L1,T1. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1) →
+ (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1.
+#h #g #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
+@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/lpxs_lpxs.ma".
-include "basic_2/computation/fpbs_alt.ma".
-include "basic_2/computation/fpbg.ma".
+include "basic_2/computation/fpbc_fpbs.ma".
+include "basic_2/computation/fpbg_fpns.ma".
(* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
-(* Advanced forward lemmas **************************************************)
-
-lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
-/3 width=5 by cpxs_fqus_lpxs_fpbs, cpxs_fqup_fpbs, fpbs_trans, lpxs_fpbs, cpxs_fpbs/
-qed-.
+(* Advanced inversion lemmas ************************************************)
-lemma fpbg_fwd_fpbc_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ →
+lemma fpbg_inv_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ →
∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
-[ /4 width=5 by fpbc_cpxs, lpxs_fpbs, ex2_3_intro/
-| #G2 #L #L2 #T #T2 #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct
- [ -HT1 /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/
- | /5 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, fqup_fqus, ex3_2_intro, ex2_3_intro/
- ]
-| #G2 #L #L0 #L2 #T #T2 #HT1 #HT2 #HL0 #H0 #HL02 #H02
- lapply (lpxs_trans … HL0 … HL02) #HL2
- elim (eq_term_dec T1 T) #H destruct
- [ -HT1 elim (fqus_inv_gen … HT2) -HT2
- [ /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/
- | * #H1 #H2 #H3 destruct
- /4 width=5 by fpbc_lpxs, lpxs_fpbs, ex2_3_intro/
- ]
- | /4 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, ex3_2_intro, ex2_3_intro/
- ]
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbg_ind_dx … H) -G1 -L1 -T1
+[ #G1 #L1 #T1 * /3 width=5 by fpns_fpbs, ex2_3_intro/
+| #G1 #G #L1 #L #T1 #T *
+ #G0 #L0 #T0 #H10 #H0 #_ *
+ /5 width=9 by fpbu_fwd_fpbs, fpbs_trans, fpns_fpbs, ex2_3_intro/
]
qed-.
+(* Advanced forward lemmas **************************************************)
+
+lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbg_ind … H) -G2 -L2 -T2
+[2: #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 @(fpbs_trans … IH1) -IH1 ] (**) (* full auto fails *)
+/2 width=1 by fpbc_fwd_fpbs/
+qed-.
+
(* Advanced properties ******************************************************)
-lemma fqu_fpbs_fpbg: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H elim(fpbs_fpbsa … H) -H
-#L0 #T0 #HT0 #HT02 #HL02 elim (fqu_cpxs_trans … HT0 … H1) -T
-/3 width=7 by fpbg_fqup, fqus_strap2_fqu/
-qed.
+lemma fpbs_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F2, K2, T2⦄ →
+ ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ →
+ ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄.
+/5 width=5 by fpbg_inv_fpbu_sn, fpbs_fpbg_trans, fpbc_fpbg, fpbu_fpbc/ qed-.
+
+(* Man properties ***********************************************************)
+
+theorem fpbg_trans: ∀h,g. tri_transitive … (fpbg h g).
+/2 width=5 by tri_TC_transitive/ qed-.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/fpbc_fpns.ma".
+include "basic_2/computation/fpbg.ma".
+
+(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************)
+
+(* Properties on parallel computation for "big tree" normal forms ***********)
+
+lemma fpbg_fpns_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ →
+ ∀G2,L2,T2. ⦃G, L, T⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #L1 #L #T1 #T #H @(fpbg_ind … H) -G -L -T
+[ /3 width=5 by fpbc_fpbg, fpbc_fpns_trans/
+| /4 width=9 by fpbg_strap1, fpbc_fpns_trans/
+]
+qed-.
+
+lemma fpns_fpbg_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G #G2 #L #L2 #T #T2 #H @(fpbg_ind_dx … H) -G -L -T
+[ /3 width=5 by fpbc_fpbg, fpns_fpbc_trans/
+| /4 width=9 by fpbg_strap2, fpns_fpbc_trans/
+]
+qed-.
+
+lemma fpbs_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ ∨
+ ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
+[ /2 width=1 by or_introl/
+| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 elim (fpb_fpbu … H2) -H2 #H2
+ [ /3 width=5 by fpns_trans, or_introl/
+ | /5 width=5 by fpbc_fpbg, fpns_fpbc_trans, fpbu_fpbc, or_intror/
+ | /3 width=5 by fpbg_fpns_trans, or_intror/
+ | /4 width=5 by fpbg_strap1, fpbu_fpbc, or_intror/
+ ]
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma fpbg_fpb_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2.
+ ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim (fpb_fpbu … H2) -H2
+/3 width=5 by fpbg_fpns_trans, fpbg_strap1, fpbu_fpbc/
+qed-.
+
+
+lemma fpb_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2.
+ ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 elim (fpb_fpbu … H1) -H1
+/3 width=5 by fpns_fpbg_trans, fpbg_strap2, fpbu_fpbc/
+qed-.
+
+lemma fpbs_fpbg_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+ ∀G2,L2,T2. ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpb_fpbg_trans/
+qed-.
+
+(* Note: this is used in the closure proof *)
+lemma fpbg_fpbs_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpb_trans/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/fpbc_lift.ma".
+include "basic_2/computation/fpbu_lift.ma".
include "basic_2/computation/fpbg.ma".
(* GENERAL "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *********************)
(* Advanced properties ******************************************************)
lemma lsstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) →
- ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
-/4 width=5 by fpbc_fpbg, lsstas_fpbc/ qed.
+ ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >⋕[h, g] ⦃G, L, T2⦄.
+/5 width=5 by fpbc_fpbg, fpbu_fpbc, lsstas_fpbu/ qed.
lemma ssta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 →
- ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
-/3 width=2 by fpbc_fpbg, ssta_fpbc/ qed.
+ ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ >⋕[h, g] ⦃G, L, T2⦄.
+/4 width=2 by fpbc_fpbg, fpbu_fpbc, ssta_fpbu/ 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/btpredstarrestricted_8.ma".
-include "basic_2/computation/fpbs.ma".
-
-(* RESTRICTED "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***********)
-
-inductive fpbr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpbr_inj : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpbr h g G1 L1 T1 G2 L2 T2
-| fpbr_step: ∀G,G2,L,L2,T,T2. fpbr h g G1 L1 T1 G L T → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
- fpbr h g G1 L1 T1 G2 L2 T2
-.
-
-interpretation "restricted 'big tree' proper parallel computation (closure)"
- 'BTPRedStarRestricted h g G1 L1 T1 G2 L2 T2 = (fpbr h g G1 L1 T1 G2 L2 T2).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma fpbr_inv_fqu_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ →
- ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 [ /2 width=5 by ex2_3_intro/ ] (**) (* auto fails without brackets *)
-#G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=9 by fpbs_strap1, ex2_3_intro/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fpbr_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
-/3 width=5 by fpbs_strap1, fqup_fpbs, fqu_fqup/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma fqu_fpbs_fpbr: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fpbs_ind … H) -G2 -L2 -T2
-/2 width=5 by fpbr_inj, fpbr_step/
-qed.
-
-lemma fpbr_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄.
-/3 width=5 by fqu_fpbs_fpbr, fpbr_fwd_fpbs/ qed-.
-
-(* Note: this is used in the closure proof *)
-lemma fpbr_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(fpbs_ind … HT2) -G2 -L2 -T2
-/2 width=5 by fpbr_step/
-qed-.
-
-lemma fqup_fpbr_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 @(fqup_ind … HT1) -G -L -T
-/3 width=5 by fpbr_strap2/
-qed-.
-
-(* Note: this is used in the closure proof *)
-lemma fqup_fpbr: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
-/3 width=5 by fqu_fpbs_fpbr, fqus_fpbs/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/computation/fpbg_fpbg.ma".
-include "basic_2/computation/fpbr.ma".
-
-(* RESTRICTED "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***********)
-
-(* Advanced forward lemmas **************************************************)
-
-lemma fpbr_fwd_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fpbr_inv_fqu_fpbs … H) -H
-/2 width=5 by fqu_fpbs_fpbg/
-qed-.
-
-lemma fpbr_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-/3 width=5 by fpbr_fwd_fpbg, fpbg_fwd_fpbs/
-qed-.
-
-(* Main properties **********************************************************)
-
-theorem fpbr_trans: ∀h,g. tri_transitive … (fpbr h g).
-/3 width=5 by fpbr_fwd_fpbs, fpbr_fpbs_trans/ qed-.
lemma cpr_lpr_fpbs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄.
/4 width=5 by fpbs_strap1, lpr_fpb, cpr_fpb/ qed.
+
+lemma fpbs_fqus_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind … H) -G2 -L2 -T2
+/3 width=5 by fpbs_strap1, fpb_fquq/
+qed-.
+
+lemma fpbs_cpxs_trans: ∀h,g,G1,G,L1,L,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+ ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
+#h #g #G1 #G #L1 #L #T1 #T #T2 #H1 #H @(cpxs_ind … H) -T2
+/3 width=5 by fpbs_strap1, fpb_cpx/
+qed-.
+
+lemma fpbs_lpxs_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+ ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄.
+#h #g #G1 #G #L1 #L #L2 #T1 #T #H1 #H @(lpxs_ind … H) -L2
+/3 width=5 by fpbs_strap1, fpb_lpx/
+qed-.
+
+lemma fqus_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind_dx … H) -G1 -L1 -T1
+/3 width=5 by fpbs_strap2, fpb_fquq/
+qed-.
+
+lemma cpxs_fpbs_trans: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T #T2 #H1 #H @(cpxs_ind_dx … H) -T1
+/3 width=5 by fpbs_strap2, fpb_cpx/
+qed-.
+
+lemma lpxs_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ ➡*[h, g] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L #L2 #T1 #T2 #H1 #H @(lpxs_ind_dx … H) -L1
+/3 width=5 by fpbs_strap2, fpb_lpx/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/fpns.ma".
+include "basic_2/computation/fpbs.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+(* Properties on parallel computation for "big tree" normal forms ***********)
+
+lemma fpns_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2.
+ ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=1 by lpxs_fpbs/
+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/btpredproper_8.ma".
+include "basic_2/relocation/lleq.ma".
+include "basic_2/computation/fpbs.ma".
+
+(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
+
+inductive fpbu (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
+| fpbu_fqup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2
+| fpbu_cpxs: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2
+| fpbu_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T1] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1
+.
+
+interpretation
+ "unitary 'big tree' proper parallel reduction (closure)"
+ 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpbu h g G1 L1 T1 G2 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma cprs_fpbu: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
+ ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
+/3 width=1 by fpbu_cpxs, cprs_cpxs/ qed.
+
+lemma lprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[0, T] L2 → ⊥) →
+ ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄.
+/3 width=1 by fpbu_lpxs, lprs_lpxs/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fpbu_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
+/3 width=1 by lpxs_fpbs, cpxs_fpbs, fqup_fpbs/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/cpxs_lleq.ma".
+include "basic_2/computation/lpxs_lleq.ma".
+include "basic_2/computation/lpxs_lpxs.ma".
+include "basic_2/computation/fpns.ma".
+include "basic_2/computation/fpbs_alt.ma".
+include "basic_2/computation/fpbu.ma".
+
+(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
+
+(* Properties on parallel computation for "big tree" normal forms ***********)
+
+lemma fpns_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ⊢ ⋕➡*[h, g] ⦃F2, K2, T2⦄ →
+ ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ →
+ ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, U2⦄.
+#h #g #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2
+#K2 #HK12 #HT1 #G2 #L2 #U2 * -G2 -L2 -U2
+[ #G2 #L2 #U2 #H12 elim (lpxs_lleq_fqup_trans … H12 … HK12 HT1) -K2
+ /3 width=5 by fpbu_fqup, fpns_intro, ex2_3_intro/
+| /4 width=9 by fpbu_cpxs, fpns_intro, lpxs_cpxs_trans, lleq_cpxs_conf_dx, ex2_3_intro/
+| /5 width=5 by fpbu_lpxs, lpxs_trans, lleq_canc_sn, ex2_3_intro/
+]
+qed-.
+
+lemma fpb_fpbu: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ ∨
+ ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
+[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H
+ [ /4 width=1 by fpbu_fqup, fqu_fqup, or_intror/
+ | * #H1 #H2 #H3 destruct /2 width=1 by or_introl/
+ ]
+| #T2 #HT12 elim (eq_term_dec T1 T2)
+ #HnT12 destruct /4 width=1 by fpbu_cpxs, cpx_cpxs, or_intror, or_introl/
+| #L2 #HL12 elim (lleq_dec … T1 L1 L2 0)
+ /4 width=3 by fpbu_lpxs, fpns_intro, lpx_lpxs, or_intror, or_introl/
+]
+qed-.
+
+lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ ∨
+ ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+(* ALTERNATIVE PROOF
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1
+[ /2 width=1 by or_introl/
+| #G1 #G #L1 #L #T1 #T #H1 #_ * [ #H2 | * #G0 #L0 #T0 #H0 #H02 ]
+ elim (fpb_fpbu … H1) -H1 #H1
+ [ /3 width=1 by
+*)
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_fpbsa … H) -H
+#L #T #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct
+[ -HT1 elim (fqus_inv_gen … HT2) -HT2
+ [ #HT2 @or_intror
+ /5 width=9 by fpbsa_inv_fpbs, fpbu_fqup, ex3_2_intro, ex2_3_intro, or_intror/
+ | * #HG #HL #HT destruct elim (lleq_dec T2 L L2 0) #H
+ [ /3 width=1 by fpns_intro, or_introl/
+ | /5 width=5 by fpbu_lpxs, ex2_3_intro, or_intror/
+ ]
+ ]
+| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H
+ /5 width=9 by fpbsa_inv_fpbs, fpbu_cpxs, cpx_cpxs, ex3_2_intro, ex2_3_intro, or_intror/
+]
+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_ssta.ma".
+include "basic_2/computation/cpxs_lift.ma".
+include "basic_2/computation/fpbu.ma".
+
+(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
+
+(* Advanced properties ******************************************************)
+
+lemma lsstas_fpbu: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) →
+ ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
+/4 width=5 by fpbu_cpxs, lsstas_cpxs/ qed.
+
+lemma ssta_fpbu: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 →
+ ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
+#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2)
+/3 width=5 by ssta_lsstas, lsstas_fpbu/ #H destruct
+elim (ssta_inv_refl_pos … HT1 … HT12)
+qed.
(**************************************************************************)
include "basic_2/notation/relations/btsn_5.ma".
-include "basic_2/computation/fpbc.ma".
+include "basic_2/computation/fpbu.ma".
include "basic_2/computation/csx_alt.ma".
(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
(* Basic inversion lemmas ***************************************************)
lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro_cprs, fpbc_cpxs/
+#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro_cprs, fpbu_cpxs/
qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/csx_aaa.ma".
+include "basic_2/computation/fsb_csx.ma".
+
+(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
+
+(* Main properties **********************************************************)
+
+(* Note: this is the "big tree" theorem ("small step" version) *)
+theorem aaa_fsb: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥[h, g] T.
+/3 width=2 by aaa_csx, csx_fsb/ qed.
+
+(* Note: this is the "big tree" theorem ("big step" version) *)
+theorem aaa_fsba: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥⦥[h, g] T.
+/3 width=2 by fsb_fsba, aaa_fsb/ qed.
+
+(* Advanced eliminators on atomica arity assignment for terms ***************)
+
+fact aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
+ (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ R G1 L1 T1
+ ) →
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+#h #g #R #IH #G #L #T #H @(csx_ind_fpbu … H) -G -L -T
+#G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
+#G2 #L2 #T2 #H12 @IH1 //
\ No newline at end of file
(**************************************************************************)
include "basic_2/notation/relations/btsnalt_5.ma".
-include "basic_2/computation/fpbg.ma".
+include "basic_2/computation/fpbg_fpbg.ma".
include "basic_2/computation/fsb.ma".
(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
(* Note: alternative definition of fsb *)
inductive fsba (h) (g): relation3 genv lenv term ≝
| fsba_intro: ∀G1,L1,T1. (
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → fsba h g G2 L2 T2
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → fsba h g G2 L2 T2
) → fsba h g G1 L1 T1.
interpretation
(* Basic eliminators ********************************************************)
-theorem fsba_ind_alt: ∀h,g. ∀R: relation3 …. (
- ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥⦥[h,g] T1 → (
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2
- ) → R G1 L1 T1
- ) →
- ∀G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → R G L T.
+lemma fsba_ind_alt: ∀h,g. ∀R: relation3 …. (
+ ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥⦥[h,g] T1 → (
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2
+ ) → R G1 L1 T1
+ ) →
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → R G L T.
#h #g #R #IH #G #L #T #H elim H -G -L -T
/4 width=1 by fsba_intro/
qed-.
+(* Basic properties *********************************************************)
+
+lemma fsba_fpbs_trans: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥⦥[h, g] T1 →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥⦥[h, g] T2.
+#h #g #G1 #L1 #T1 #H @(fsba_ind_alt … H) -G1 -L1 -T1
+/4 width=5 by fsba_intro, fpbs_fpbg_trans/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem fsb_fsba: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥⦥[h, g] T.
+#h #g #G #L #T #H @(fsb_ind_alt … H) -G -L -T
+#G1 #L1 #T1 #_ #IH @fsba_intro
+#G2 #L2 #T2 #H elim (fpbg_inv_fpbu_sn … H) -H
+/3 width=5 by fsba_fpbs_trans/
+qed.
+
(* Main inversion lemmas ****************************************************)
theorem fsba_inv_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T.
#h #g #G #L #T #H @(fsba_ind_alt … H) -G -L -T
-/4 width=1 by fsb_intro, fpbc_fpbg/
+/5 width=1 by fsb_intro, fpbc_fpbg, fpbu_fpbc/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma fsb_fpbs_trans: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥[h, g] T2.
+/4 width=5 by fsba_inv_fsb, fsb_fsba, fsba_fpbs_trans/ qed-.
+
+(* Advanced eliminators *****************************************************)
+
+lemma fsb_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term.
+ (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 →
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ R G1 L1 T1
+ ) →
+ ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 → R G1 L1 T1.
+#h #g #R #IH #G1 #L1 #T1 #H @(fsba_ind_alt h g … G1 L1 T1)
+/3 width=1 by fsba_inv_fsb, fsb_fsba/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/csx_aaa.ma".
-include "basic_2/computation/fsb.ma".
+include "basic_2/computation/lsx_csx.ma".
+include "basic_2/computation/fsb_alt.ma".
+
+axiom lsx_fqup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ G1 ⊢ ⋕⬊*[h, g, T1] L1 → G2 ⊢ ⋕⬊*[h, g, T2] L2.
+
+axiom fqup_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ →
+ ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) →
+ ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 &
+ K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
-(* Advanced propreties ******************************************************)
+(* Advanced propreties on context-senstive extended bormalizing terms *******)
lemma csx_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T.
-#h #g #G #L #T #H @(csx_ind_fpbc … H) -T /3 width=1 by fsb_intro/
+#h #g #G1 #L1 #T1 #H @(csx_ind_alt … H) -T1
+#T1 #HT1 @(lsx_ind h g T1 G1 … L1) /2 width=1 by csx_lsx/ -L1
+#L1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1
+#G1 #L1 #T1 #IHu #H1 #IHl #IHc @fsb_intro
+#G2 #L2 #T2 * -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 @IHu -IHu /2 width=5 by lsx_fqup_conf/ -H1 [| -IHl ]
+ [ #L0 #HL20 #HnL20 #_ elim (fqup_lpxs_trans_nlleq … H12 … HL20 HnL20) -L2
+ /6 width=5 by fsb_fpbs_trans, lpxs_fpbs, fqup_fpbs, lpxs_cpxs_trans/
+ | #T0 #HT20 #HnT20 elim (fqup_cpxs_trans_neq … H12 … HT20 HnT20) -T2
+ /4 width=5 by fsb_fpbs_trans, fqup_fpbs/
+ ]
+| -H1 -IHu -IHl /3 width=1 by/
+| -H1 -IHu /5 width=5 by fsb_fpbs_trans, lpxs_fpbs, lpxs_cpxs_trans/
+]
qed.
-(* Main properties **********************************************************)
+(* Advanced eliminators *****************************************************)
+
+lemma csx_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
+ (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ R G1 L1 T1
+ ) →
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T.
+/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
-(* Note: this is the "big tree" theorem ("small step" version) *)
-theorem aaa_fsb: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥[h, g] T.
-/3 width=2 by aaa_csx, csx_fsb/ qed.
+lemma csx_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term.
+ (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ R G1 L1 T1
+ ) →
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T.
+/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/computation/fpbs_fleq.ma".
-include "basic_2/computation/fpbg_fpbg.ma".
-include "basic_2/computation/fsb.ma".
-
-(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
-
-axiom fleq_fpbc_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ≻[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄.
-
-axiom fleq_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G, L, T⦄ →
- ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-
-(* Properties ******************************************************)
-
-lemma fsb_fleq_trans: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥[h, g] T2.
-#h #g #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
-/4 width=5 by fsb_intro, fleq_fpbc_trans/
-qed-.
-
-(* Advanced eliminators *****************************************************)
-
-lemma fsb_ind_fpbg_fpbs: ∀h,g. ∀R:relation3 genv lenv term.
- (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
- ) →
- ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#h #g #R #IH #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
-#G1 #L1 #T1 #H1 #IH1 #G2 #L2 #T2 #H12 elim (fpbs_fwd_fpb_sn … H12) -H12
-[ #H12 @IH -IH /2 width=5 by fsb_fleq_trans/
- -H1 #G0 #L0 #T0 #H20 lapply (fleq_fpbg_trans … H12 H20) -G2 -L2 -T2
- #H10 elim (fpbg_fwd_fpb_sn … H10) -H10 /2 width=5 by/
-| -H1 -IH * /2 width=5 by/
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/computation/lpxs_lpxs.ma".
-include "basic_2/computation/fpbs.ma".
-include "basic_2/computation/fpbc.ma".
-include "basic_2/computation/csx_lift.ma".
-include "basic_2/computation/csx_lpxs.ma".
-include "basic_2/computation/lsx_csx.ma".
-
-(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
-
-(* Advanced eliminators for context-sensitive ext. strongly norm. terms *****)
-
-lemma tollens: ∀R1,R2,R3:Prop. (R1 → R2) → (R2 → R3) → R1 → R3.
-/3 width=1/ qed-.
-
-axiom fqus_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ →
- ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) →
- ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 &
- K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-
-axiom fpbs_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ≥[h, g] ⦃G2, K2, T2⦄ →
- ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) →
- ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 &
- K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-
-
-lemma csx_ind_fpbc_fpbs: ∀h,g. ∀R:relation3 genv lenv term.
- (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
- ) →
- ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
- R G2 L2 T2.
-#h #g #R #IH1 #G1 #L1 #T1 #H @(csx_ind_alt … H) -T1
-#T1 #HT1 @(lsx_ind h g T1 G1 … L1) /2 width=1 by csx_lsx/ -L1
-#L1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1
-#G1 #L1 #T1 #IH2 #H1 #IH3 #IH4 #G2 #L2 #T2 #H12
-@IH1 -IH1 (* /4 width=5 by lsx_inv_csx, csx_lpxs_conf, csx_fqus_conf/ *)
-[2: #G #L #T *
- [
- |
- | #L0 #HL20 #HnT2 elim (fpbs_lpxs_trans_nlleq … H12 … HL20 HnT2) -L2
- #L2 #HL12 #HnT1 #H12 @(IH3 … HL12 HnT1 … H12) -IH3
- #H26 #H27 #H28 #H29 #H30 #H31 #H32
- @(IH4) … H27 H28)
-
- [ #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
- lapply (fqup_fqus_trans … H15 … H21) -H15 -H21 #H
- @(IH3 … H23 H24)
-
- #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10
- @(IH4 … H3 … H10) -IH4 -H10 -H3 //
-
-
-
- [ -IH4 | -H1 -IH2 -IH4 | -H1 -H2 -IH2 -IH3 ]
-[ #G0 #L0 #T0 #H20 elim (lpxs_lleq_fqup_trans … H20 … HYL2 HT2) -L2
- #L2 #H20 #HL20 lapply (fqus_fqup_trans … H12 H20) -G2 -Y -T2
- #H10 @(IH2 … H10) -IH2 /2 width=5 by csx_fqup_conf/
-(*
- #T2 #HT02 #H #G3 #L3 #T3 #HT23 elim (fqup_cpxs_trans_neq … H10 … HT02 H) -T0
- /4 width=8 by fqup_fqus_trans, fqup_fqus/
-*)
-| (* #T0 #HT20 #H elim (fqus_cpxs_trans_neq … H12 … HT20 H) -T2 /3 width=4 by/ *)
-| #L0 #HL20 #HnT2 @(IH4 L0) /3 width=3 by lpxs_trans, lleq_canc_sn/
-
-
-
-
-
- | /3 width=3 by /
- [ /2 width=3
-
- lapply (lpxs_trans … HYL2 … HL20)
- #HYL0 lapply (tollens ???? HnT2) [ @(lleq_canc_sn … HT2) | skip ] -L2
- #HnT2 elim (fqus_lpxs_trans_nlleq … H12 … HYL0 HnT2) -
-
-
- lapply (lleq_canc_sn … L0 … HT2)
-
-
-
- |
-
-elim (lpxs_lleq_fqup_trans … H12 … HYL2 HT2) -L2
-
-
-]
-qed-.
-
-lemma csx_ind_fpbc: ∀h,g. ∀R:relation3 genv lenv term.
- (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
- ) →
- ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T.
-/4 width=8 by csx_ind_fpbc_fqus/ qed-.
qed-.
lemma snv_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T ¡[h, g] →
- ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g].
+ ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g].
/2 width=4 by snv_inv_bind_aux/ qed-.
fact snv_inv_appl_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T →
∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
- ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 &
- ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U.
+ ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 &
+ ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U.
#h #g #G #L #X * -L -X
[ #G #L #k #V #T #H destruct
| #I #G #L #K #V0 #i #_ #_ #V #T #H destruct
lemma snv_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] →
∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
- ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 &
- ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U.
+ ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 &
+ ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U.
/2 width=3 by snv_inv_appl_aux/ qed-.
fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = ⓝW.T →
include "basic_2/unfold/lsstas_lsstas.ma".
include "basic_2/computation/fpbs_lift.ma".
-include "basic_2/computation/fpbr.ma".
+include "basic_2/computation/fpbg_fpns.ma".
include "basic_2/equivalence/cpes_cpds.ma".
include "basic_2/dynamic/snv.ma".
(* Properties for the preservation results **********************************)
fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
-@(cprs_ind … H) -T2 /4 width=6 by fpbr_fpbs_trans, cprs_fpbs/
+@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/
qed-.
fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H
-@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbr_fpbs_trans, cprs_fpbs/
+@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/
qed-.
fact da_cpcs_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- ∀G,L,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
- ∀T2. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ ∀G,L,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+ ∀T2. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 →
⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2.
#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l1 #Hl1 #l2 #Hl2 #H
qed-.
fact ssta_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 →
∀U1. ⦃G, L1⦄ ⊢ T1 •[h, g] U1 →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
qed-.
fact lsstas_cprs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g, l2] U1 →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, g, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=10/ ]
+@(cprs_ind … H) -T2 [ /2 width=10 by/ ]
#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
elim (IHT1 L1) // -IHT1 #U #HTU #HU1
elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
[2: /3 width=12 by da_cprs_lpr_aux/
|3: /3 width=10 by snv_cprs_lpr_aux/
-|4: /3 width=5 by fpbr_fpbs_trans, cprs_fpbs/
+|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/
] -G0 -L0 -T0 -T1 -T -l1 #U2 #HTU2 #HU2
/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
qed-.
fact lsstas_cpcs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g, l] U1 →
- ∀T2. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+ ∀T2. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, g, l] U2 →
⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #H02 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12
elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (lsstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1/ #W1 #H1 #HUW1
-elim (lsstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1/ #W2 #H2 #HUW2 -L0 -T0
+elim (lsstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1 by/ #W1 #H1 #HUW1
+elim (lsstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1 by/ #W2 #H2 #HUW2 -L0 -T0
lapply (lsstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/
qed-.
fact snv_ssta_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
- ∀G,L,T. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ ∀G,L,T. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 →
∀U. ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ U ¡[h, g].
/3 width=8 by lsstas_inv_SO, ssta_lsstas/ qed-.
fact lsstas_cpds_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
∀U1. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 →
∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, g, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2.
| lapply (lsstas_da_conf … HT1T … Hl1) #Hl1l
lapply (lsstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1
elim (lsstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L)
- /3 width=8 by fpbr_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12
+ /3 width=8 by fpbg_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12
/3 width=5 by cpcs_cpes, ex3_2_intro/
]
qed-.
fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
(* Properties on degree assignment for terms ********************************)
fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h g G1 L1 T1.
#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #k #_ #_ #_ #_ #l #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1
lapply (fqup_lref … G1 … HLK1)
elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
- /4 width=10 by da_ldef, da_ldec, fqup_fpbr/
+ /4 width=10 by da_ldef, da_ldec, fqup_fpbg/
|2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
lapply (ldrop_mono … H … HLK1) -H #H destruct
lapply (fqup_lref … G1 … HLK1)
elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -V2
- /4 width=7 by da_lift, fqup_fpbr/
+ /4 width=7 by da_lift, fqup_fpbg/
]
| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
lapply (da_inv_bind … H2) -H2
elim (cpr_inv_bind1 … H3) -H3 *
[ #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=9 by da_bind, fqup_fpbr, lpr_pair/
+ /4 width=9 by da_bind, fqup_fpbg, lpr_pair/
| #T2 #HT12 #HT2 #H1 #H2 destruct
- /4 width=11 by da_inv_lift, fqup_fpbr, lpr_pair, ldrop_ldrop/
+ /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_ldrop/
]
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct
elim (snv_inv_appl … H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10
lapply (da_inv_flat … H2) -H2 #Hl
elim (cpr_inv_appl1 … H3) -H3 *
- [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbr/
+ [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbg/
| #b #V2 #W #W2 #U1 #U2 #HV12 #HW2 #HU12 #H1 #H2 destruct
elim (snv_inv_bind … HT1) -HT1 #HW #HU1
lapply (da_inv_bind … Hl) -Hl #Hl
lapply (cprs_div … HW3 … HW10) -W3 #HWW1
lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #H
elim (snv_fwd_da … HW) #l1 #Hl1
- lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fqup_fpbr, ssta_lsstas/ #HW1
+ lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fqup_fpbg, ssta_lsstas/ #HW1
lapply (da_cpcs_aux … IH2 IH1 … Hl1 … H … HWW1) -H
- /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, ssta_fpbs/ #H destruct
- lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fqup_fpbr/ ] #Hl0
- lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fqup_fpbr/ -HW
- lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fqup_fpbr, lpr_pair/ ] -HL12 -HW2
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, ssta_fpbs/ #H destruct
+ lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fqup_fpbg/ ] #Hl0
+ lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fqup_fpbg/ -HW
+ lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2
/4 width=6 by da_bind, lsubd_da_trans, lsubd_abbr/
| #b #V #V2 #W #W2 #U1 #U2 #HV1 #HV2 #HW2 #HU12 #H1 #H2 destruct -IH3 -IH2 -V -W0 -T0 -l0 -HV1 -HVW1
elim (snv_inv_bind … HT1) -HT1 #_
lapply (da_inv_bind … Hl) -Hl
- /5 width=9 by da_bind, da_flat, fqup_fpbr, lpr_pair/
+ /5 width=9 by da_bind, da_flat, fqup_fpbg, lpr_pair/
]
| #W1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1
lapply (da_inv_flat … H2) -H2 #Hl
elim (cpr_inv_cast1 … H3) -H3
- [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbr/
- | /3 width=7 by fqup_fpbr/
+ [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/
+ | /3 width=7 by fqup_fpbg/
]
]
qed-.
(* Properties on context-free parallel reduction for local environments *****)
fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g G1 L1 T1.
#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #k #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
lapply (fqup_lref … G1 … HLK1) #HKL
elim (cpr_inv_lref1 … H2) -H2
- [ #H destruct -HLK1 /4 width=10 by fqup_fpbr, snv_lref/
+ [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/
| * #K0 #V0 #W0 #H #HVW0 #W0 -HV12
lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbr, snv_lift/
+ lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/
]
| #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
elim (snv_inv_bind … H1) -H1 #HV1 #HT1
elim (cpr_inv_bind1 … H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbr, snv_bind, lpr_pair/
+ [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/
| #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
- /4 width=10 by fqup_fpbr, snv_inv_lift, lpr_pair, ldrop_ldrop/
+ /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_ldrop/
]
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1
elim (cpr_inv_appl1 … H2) -H2 *
[ #V2 #T2 #HV12 #HT12 #H destruct -IH4
- lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #HV2
- lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbr/ #HT2
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #H2l0
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbr/ -HV1 #W2 #HVW2 #HW12
- elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbr/ -HT12 -HTU1 #X #HTU2 #H
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
+ lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0
+ elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12
+ elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HT12 -HTU1 #X #HTU2 #H
elim (cprs_inv_abst1 … H) -H #W20 #U2 #HW120 #_ #H destruct
lapply (lpr_cprs_conf … HL12 … HW10) -L1 #HW10
lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120
elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
lapply (cprs_div … HW10 … HW230) -W30 #HW120
- lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbr/ #HW10
+ lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #HW10
lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #HlW10
elim (snv_fwd_da … HW20) #l #Hl
lapply (da_cpcs_aux … IH1 IH2 … HlW10 … Hl … HW120) // -HlW10
- /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, ssta_fpbs/ #H destruct
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #HlV2
- lapply (IH2 … Hl … HW202 … HL12) /2 width=1 by fqup_fpbr/ #HlW2
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #W3 #HV2W3 #HW103
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, ssta_fpbs/ #H destruct
+ lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HlV2
+ lapply (IH2 … Hl … HW202 … HL12) /2 width=1 by fqup_fpbg/ #HlW2
+ elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #W3 #HV2W3 #HW103
lapply (ssta_da_conf … HV2W3 … HlV2) <minus_plus_m_m #HlW3
lapply (cpcs_cpr_strap1 … HW120 … HW202) -HW120 #HW102
lapply (lpr_cpcs_conf … HL12 … HW102) -HW102 #HW102
lapply (cpcs_canc_sn … HW103 … HW102) -W10 #HW32
- lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbr/ -HV1 #HV2
- lapply (IH1 … HW202 … HL12) /2 width=1 by fqup_fpbr/ -HW20 #HW2
- lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fqup_fpbr, lpr_pair/ -HT20 #HT2
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1 #HV2
+ lapply (IH1 … HW202 … HL12) /2 width=1 by fqup_fpbg/ -HW20 #HW2
+ lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT20 #HT2
lapply (snv_ssta_aux … IH4 … HlV2 … HV2W3)
- /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_fpbs/ #HW3
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW3
lapply (lsubsv_snv_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /3 width=3 by snv_bind, snv_cast/
- @(lsubsv_abbr … l) /3 width=7 by fqup_fpbr/ #W #W0 #l0 #Hl0 #HV2W #HW20
+ @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
lapply (lsstas_ssta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W
@(lsstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) //
- [ /3 width=9 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_ssta_fpbs/
- | /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_fpbs/
+ [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_ssta_fpbs/
+ | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/
]
| #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4
elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
elim (cpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
lapply (lpr_cprs_conf … HL12 … HW10) -HW10 #HW10
- elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbr, lpr_pair/ -HTU0 #X #HTU2 #H
+ elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HTU2 #H
elim (cprs_inv_abst1 … H) -H #W #U2 #HW1 #_ #H destruct -U3
- elim (ssta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbr/ -IH3 -HVW1 #X #H1 #H2
+ elim (ssta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HVW1 #X #H1 #H2
lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
elim (lift_total X 0 1) #W20 #H3
lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1 by ldrop_ldrop/ -H1 #HVW20
lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) /2 width=1 by cprs_bind/ -HW3 -HTU2 #HTU2
- lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbr/ -IH2 -Hl0 #Hl0
+ lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -Hl0 #Hl0
lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=1 by ldrop_ldrop/ -Hl0 #Hl0
- lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbr/ -HW0 #HW2
- lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbr/ -HV1 -HV10 #HV0
- lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbr, lpr_pair/ -L1 #HT2
+ lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ -HW0 #HW2
+ lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV10 #HV0
+ lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2
lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /3 width=7 by snv_bind, snv_appl, ldrop_ldrop/
]
| #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4
elim (cpr_inv_cast1 … H2) -H2
[ * #W2 #T2 #HW12 #HT12 #H destruct
lapply (cpcs_cprs_strap1 … HUW1 W2 ?) /2 width=1 by cpr_cprs/ -HUW1 #H1
- lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbr/ -HW1 -HW12 #HW2
- lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbr/ -IH1 #HT2
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HTU1 … HT12 … HL12) /2 width=2 by fqup_fpbr/ -IH3 -HTU1 #U2 #HTU2 #HU12
- lapply (IH2 … Hl0 … HT12 … HL12) /2 width=1 by fqup_fpbr/ -IH2 -HT1 -HT12 -Hl0 #Hl0
+ lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ -HW1 -HW12 #HW2
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH1 #HT2
+ elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HTU1 … HT12 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HTU1 #U2 #HTU2 #HU12
+ lapply (IH2 … Hl0 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -HT1 -HT12 -Hl0 #Hl0
/4 width=7 by snv_cast, lpr_cpcs_conf, cpcs_canc_sn/
| #H -IH3 -IH2 -HW1 -HTU1 -HUW1
- lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbr/
+ lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbg/
]
]
qed-.
(* Properties on nat-iterated stratified static type assignment for terms ***)
fact snv_lsstas_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lsstas h g G1 L1 T1.
#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #k #HG0 #HL0 #HT0 #_ #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H destruct
[ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ]
lapply (fqup_lref … G1 … HLK1) #H
- lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbr, snv_lift/
+ lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/
| #p #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2
elim (snv_inv_bind … H1) -H1 #HV1 #HT1
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
- elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbr, snv_bind/
+ elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, snv_bind/
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct
elim (snv_inv_appl … H1) -H1 #a #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10
lapply (da_inv_flat … Hl1) -Hl1 #Hl1
elim (lsstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
- lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbr/ #HU1
- elim (lsstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbr/ -T1 -l1 #X #l #_ #H #HU10 -l2
+ lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbg/ #HU1
+ elim (lsstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #X #l #_ #H #HU10 -l2
elim (lsstas_inv_bind1 … H) -H #U0 #_ #H destruct -T0 -l
elim (cpes_inv_abst2 … HU10) -HU10 #W2 #U2 #HU12 #HU02
elim (cprs_inv_abst … HU02) -HU02 #HW02 #_
[ lapply (lsstas_inv_O … H2) -H2 #H destruct // ]
elim (snv_inv_cast … H1) -H1
lapply (da_inv_flat … Hl1) -Hl1
- lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbr/
+ lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/
]
qed-.
(* Properties on sn parallel reduction for local environments ***************)
fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lsstas_cpr_lpr h g G1 L1 T1.
#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #k #_ #_ #_ #_ #l1 #l2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH4 -IH3 -IH2 -IH1
|2,4: * #K0 #V0 #X0 #H #HVX0 #HX0
lapply (ldrop_mono … H … HLK1) -H -HLK1 #H destruct
]
- [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbr/ #V2 #HWV2 #HV2
+ [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2
elim (lift_total V2 0 (i+1))
- /6 width=11 by fqup_fpbr, cpcs_lift, lsstas_ldec, ex2_intro/
- | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbr/ #W2 #HVW2 #HW02
+ /6 width=11 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/
+ | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02
elim (lift_total W2 0 (i+1))
/4 width=11 by cpcs_lift, lsstas_ldef, ex2_intro/
- | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbr/ -l1 #W2 #HXW2 #HW02
+ | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02
elim (lift_total W2 0 (i+1))
/3 width=11 by cpcs_lift, lsstas_lift, ex2_intro/
]
elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
elim (cpr_inv_bind1 … H3) -H3 *
[ #V2 #T2 #HV12 #HT12 #H destruct
- elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbr, lpr_pair/ -T1
+ elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, lpr_pair/ -T1
/4 width=5 by cpcs_bind2, lpr_cpr_conf, lsstas_bind, ex2_intro/
| #T3 #HT13 #HXT3 #H1 #H2 destruct
- elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbr, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
+ elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
elim (lsstas_inv_lift1 … HTU3 L2 … HXT3) -T3
/5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_ldrop, ex2_intro/
]
elim (cpr_inv_appl1 … H3) -H3 *
[ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH4 -IH3 -IH2
elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1
- /4 width=5 by fqup_fpbr, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/
+ /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/
| #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct
elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
lapply (cprs_div … HW10 … HW20) -W0 #HW12
lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #H
elim (snv_fwd_da … HW2) #l #Hl
- lapply (IH4 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fqup_fpbr, ssta_lsstas/ #HW1
+ lapply (IH4 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fqup_fpbg, ssta_lsstas/ #HW1
lapply (da_cpcs_aux … IH3 IH2 … H … Hl … HW12) // -H
- /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, ssta_fpbs/ #H destruct
- lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #HV2
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #HV2l
- elim (IH1 … 1 … Hl0 … W1 … HV12 … HL12) /2 width=1 by fqup_fpbr, ssta_lsstas/ -HVW1 #W4 #H #HW14
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, ssta_fpbs/ #H destruct
+ lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2l
+ elim (IH1 … 1 … Hl0 … W1 … HV12 … HL12) /2 width=1 by fqup_fpbg, ssta_lsstas/ -HVW1 #W4 #H #HW14
lapply (lsstas_inv_SO … H) #HV2W4
lapply (ssta_da_conf … HV2W4 … HV2l) <minus_plus_m_m #HW4l
- lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_fpbs/ #HW4
- lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbr/ #HW3
- lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fqup_fpbr/ #HW3l
- elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fqup_fpbr, lpr_pair/ #U3 #HTU3 #HU23
+ lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW4
+ lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
+ lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3l
+ elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23
lapply (cpcs_cpr_strap1 … HW12 … HW23) #H
lapply (lpr_cpcs_conf … HL12 … H) -H #H
lapply (cpcs_canc_sn … HW14 H) -H #HW43
@(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W3.U3)) /2 width=1 by cpr_beta/
/4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
| -U3
- @(lsubsv_abbr … l) /3 width=7 by fqup_fpbr/
+ @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/
#W #W0 #l0 #Hl0 #HV2W #HW30
lapply (lsstas_ssta_conf_pos … HV2W4 … HV2W) -HV2W #HW4W
@(lsstas_cpcs_lpr_aux … IH3 IH2 IH1 … Hl0 … HW4W … Hl0 … HW30 … HW43) //
- [ /3 width=9 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_ssta_fpbs/
- | /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_fpbs/
+ [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_ssta_fpbs/
+ | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/
]
- | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbr, lpr_pair/
+ | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/
]
| #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -l0 -W1 -W10 -HV1 -IH4 -IH3 -IH2
elim (snv_inv_bind … HT1) -HT1 #_ #HT0
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
elim (lsstas_inv_bind1 … HTU1) -HTU1 #U0 #HTU0 #H destruct
- elim (IH1 … Hl1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hl1 -HTU0 /2 width=1 by fqup_fpbr, lpr_pair/ -T0 #U2 #HTU2 #HU02
+ elim (IH1 … Hl1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hl1 -HTU0 /2 width=1 by fqup_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02
lapply (lpr_cpr_conf … HL12 … HV10) -HV10 #HV10
lapply (lpr_cpr_conf … HL12 … HW02) -L1 #HW02
lapply (cpcs_bind2 b … HW02 … HU02) -HW02 -HU02 #HU02
elim (cpr_inv_cast1 … H3) -H3
[ * #U2 #T2 #_ #HT12 #H destruct
elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 -HL12
- /3 width=3 by fqup_fpbr, lsstas_cast, ex2_intro/
+ /3 width=3 by fqup_fpbg, lsstas_cast, ex2_intro/
| #HT1X3
elim (IH1 … Hl1 … HTU1 … HT1X3 … HL12) -IH1 -Hl1 -HTU1 -HL12
- /2 width=3 by fqup_fpbr, ex2_intro/
+ /2 width=3 by fqup_fpbg, ex2_intro/
]
]
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 FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ > break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'BTPRedStarProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/btpredstarproper_8.ma".
+include "basic_2/computation/fpbc.ma".
+
+(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************)
+
+(* Note: this is not transitive *)
+inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
+| fpbg_cpxs: ∀L2,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 →
+ fpbg h g G1 L1 T1 G1 L2 T2
+| fpbg_fqup: ∀G2,L,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃+ ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 →
+ fpbg h g G1 L1 T1 G2 L2 T2
+| fpbg_lpxs: ∀G2,L,L0,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L0 →
+ (L ⋕[0, T2] L0 → ⊥) → ⦃G2, L0⦄ ⊢ ➡*[h, g] L2 → L0 ⋕[0, T2] L2 →
+ fpbg h g G1 L1 T1 G2 L2 T2
+.
+
+interpretation "'big tree' proper parallel computation (closure)"
+ 'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fpbc_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
+/3 width=9 by fpbg_fqup, fpbg_cpxs, fpbg_lpxs/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/lpxs_lpxs.ma".
+include "basic_2/computation/fpbs_alt.ma".
+include "basic_2/computation/fpbg.ma".
+
+(* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
+
+(* Advanced forward lemmas **************************************************)
+
+lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
+/3 width=5 by cpxs_fqus_lpxs_fpbs, cpxs_fqup_fpbs, fpbs_trans, lpxs_fpbs, cpxs_fpbs/
+qed-.
+
+lemma fpbg_fwd_fpbc_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ →
+ ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
+[ /4 width=5 by fpbc_cpxs, lpxs_fpbs, ex2_3_intro/
+| #G2 #L #L2 #T #T2 #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct
+ [ -HT1 /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/
+ | /5 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, fqup_fqus, ex3_2_intro, ex2_3_intro/
+ ]
+| #G2 #L #L0 #L2 #T #T2 #HT1 #HT2 #HL0 #H0 #HL02 #H02
+ lapply (lpxs_trans … HL0 … HL02) #HL2
+ elim (eq_term_dec T1 T) #H destruct
+ [ -HT1 elim (fqus_inv_gen … HT2) -HT2
+ [ /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/
+ | * #H1 #H2 #H3 destruct
+ /4 width=5 by fpbc_lpxs, lpxs_fpbs, ex2_3_intro/
+ ]
+ | /4 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, ex3_2_intro, ex2_3_intro/
+ ]
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma fqu_fpbs_fpbg: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H elim(fpbs_fpbsa … H) -H
+#L0 #T0 #HT0 #HT02 #HL02 elim (fqu_cpxs_trans … HT0 … H1) -T
+/3 width=7 by fpbg_fqup, fqus_strap2_fqu/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/fpns.ma".
+include "basic_2/computation/fpbg.ma".
+
+(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************)
+
+(* Properties on parallel computation for "big tree" normal forms ***********)
+
+axiom fpns_fpbg_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ⊢ ⋕➡*[h, g] ⦃F2, K2, T2⦄ →
+ ∀G2,L2,U2. ⦃F2, K2, T2⦄ >[h, g] ⦃G2, L2, U2⦄ →
+ ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ >[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, U2⦄.
+(*
+#h #g #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2
+#K2 #HK12 #HT1 #G2 #L2 #U2 * -G2 -L2 -U2
+[ /4 width=9 by fpbc_cpxs, fpns_intro, lpxs_cpxs_trans, lleq_cpxs_conf_dx, ex2_3_intro/
+| #G2 #L2 #U2 #H12 elim (lpxs_lleq_fqup_trans … H12 … HK12 HT1) -K2
+ /3 width=5 by fpbc_fqup, fpns_intro, ex2_3_intro/
+| /5 width=5 by fpbc_lpxs, lpxs_trans, lleq_canc_sn, ex2_3_intro/
+]
+qed-.
+*)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/fpbc_lift.ma".
+include "basic_2/computation/fpbg.ma".
+
+(* GENERAL "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *********************)
+
+(* Advanced properties ******************************************************)
+
+lemma lsstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) →
+ ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
+/4 width=5 by fpbc_fpbg, lsstas_fpbc/ qed.
+
+lemma ssta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 →
+ ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
+/3 width=2 by fpbc_fpbg, ssta_fpbc/ qed.
- forth letter (if present)
-c: proper single step (successor)
+c: proper single step (general) (successor)
e: reflexive transitive closure to normal form (evaluation)
g: proper multiple step (general) (greater)
p: non-reflexive transitive closure (plus)
q: reflexive closure (question)
r: proper multiple step (restricted) (restricted)
s: reflexive transitive closure (star)
+u: proper single step (restricted) (unit)
+++ /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 FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ > break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'BTPRedStarProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊃≥ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'BTPRedStarRestricted $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻⋕ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'LazyBTPRedProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >⋕ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'LazyBTPRedStarProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
}
]
[ { "strongly normalizing \"big tree\" computation" * } {
- [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_fleq" + "fsb_csx" * ]
+ [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_aaa" + "fsb_csx" * ]
}
]
[ { "strongly normalizing extended computation" * } {
- [ "lsx ()" "lsx_cpxs" + "lsx_fpbc" + "lsx_csx" * ]
- [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
+ [ "lsx ( ? ⊢ ⬊*[?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ]
+ [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ]
}
]
[ { "\"big tree\" parallel computation" * } {
- [ "fpbr ( ⦃?,?,?⦄ ⊃≥[?,?] ⦃?,?,?⦄ )" "fpbr_fpbr" * ]
- [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ]
- [ "fpbc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbc_lift" + "fpbc_fpns" * ]
- [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ]
+ [ "fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpns" + "fpbg_fpbg" * ]
+ [ "fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )" "fpbc_fpns" + "fpbc_fpbs" * ]
+ [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_fpns" * ]
+ [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpns" + "fpbs_fpbs" * ]
}
]
[ { "parallel computation for \"big tree\" normal forms" * } {
projects / helm.git / commitdiff