CONTRIB := lambdadelta_2
-TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib clean
+WWW := ../../../../helm/www/lambdadelta
+
+TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib clean \
+ www up-html
PACKAGES := ground_2 basic_2 apps_2 alpha_1
XPACKAGES := ground_2 basic_2
# clean ######################################################################
clean:
- @$(RM) `find -name "*~" -type f -print`
+ $(H)$(RM) `find -name "*~" -type f -print`
+
+# www ######################################################################
+
+www:
+ $(H)$(MAKE) --no-print-directory -C $(WWW) www
+
+# www ######################################################################
+
+up-html:
+ $(H)$(MAKE) --no-print-directory -C $(WWW) up-html
##############################################################################
#h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1,
cpr_cpx/
qed.
-
-lemma cpxs_neq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 = T2 → ⊥) →
- ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T2.
-#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
-[ #H elim H -H //
-| #T1 #T #H1 #H2 #IH2 #H12 elim (eq_term_dec T1 T) #H destruct
- [ -H1 -H2 /3 width=1 by/
- | -IH2 /3 width=4 by ex3_intro/ (**) (* auto fails without clear *)
- ]
-]
-qed-.
lemma sta_fpbg: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 →
⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄.
/4 width=2 by fpb_fpbg, sta_fpb/ qed.
+
+lemma lstas_fpbg: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → (T1 = T2 → ⊥) →
+ ∀d1. d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄.
+/3 width=5 by lstas_cpxs, cpxs_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 *)
-(* *)
-(**************************************************************************)
-
-(* 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 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'LazyBTPRedStarProper $h $o $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 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedSubTyStarProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
lapply (cpxs_strap1 … HW1 … HW2) -W
lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/
qed-.
-
-(* Basic_2A1: removed theorems 1: cpxs_neq_inv_step_sn *)
qed-.
(* Note: this requires tdeq to be symmetric *)
-lemma cpxs_tdneq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) →
+(* Nasic_2A1: uses: cpxs_neq_inv_step_sn *)
+lemma cpxs_tdneq_fwd_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) →
∃∃T,T0. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 ≛[h, o] T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T0 & T0 ≛[h, o] T2.
#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
[ #H elim H -H //
-| #T1 #T #H1 #H2 #IH #Hn12 elim (tdeq_dec h o T1 T) #H destruct
- [ -H1 -H2 elim IH -IH /3 width=3 by tdeq_trans/ -Hn12
- #X #X2 #HTX #HnTX #HX2 #HXT2 elim (tdeq_cpx_trans … H … HTX) -HTX
- #X1 #HTX1 #HX1 elim (tdeq_cpxs_trans … HX1 … HX2) -HX2
- /5 width=8 by tdeq_canc_sn, tdeq_trans, ex4_2_intro/ (* Note: 2 tdeq_trans *)
- | -IH -Hn12 /3 width=6 by ex4_2_intro/
+| #T1 #T0 #HT10 #HT02 #IH #Hn12
+ elim (tdeq_dec h o T1 T0) [ -HT10 -HT02 #H10 | -IH #Hn10 ]
+ [ elim IH -IH /3 width=3 by tdeq_trans/ -Hn12
+ #T3 #T4 #HT03 #Hn03 #HT34 #H42
+ elim (tdeq_cpx_trans … H10 … HT03) -HT03 #T5 #HT15 #H53
+ elim (tdeq_cpxs_trans … H53 … HT34) -HT34 #T6 #HT56 #H64
+ /5 width=8 by tdeq_canc_sn, (* 2x *) tdeq_trans, ex4_2_intro/
+ | /3 width=6 by ex4_2_intro/
]
]
qed-.
elim (tdeq_dec h o T1 T0) #H
[ lapply (tdeq_tdneq_trans … H … HnTV0) -H -HnTV0 #Hn10
lapply (cpxs_trans … HT10 … HTV0) -T0 #H10
- elim (cpxs_tdneq_inv_step_sn … H10 … Hn10) -H10 -Hn10
+ elim (cpxs_tdneq_fwd_step_sn … H10 … Hn10) -H10 -Hn10
/3 width=8 by tdeq_trans/
-| elim (cpxs_tdneq_inv_step_sn … HT10 … H) -HT10 -H #T #V #HT1 #HnT1 #HTV #HVT0
+| elim (cpxs_tdneq_fwd_step_sn … HT10 … H) -HT10 -H #T #V #HT1 #HnT1 #HTV #HVT0
elim (tdeq_cpxs_trans … HVT0 … HTV0) -T0
/3 width=8 by cpxs_trans, tdeq_trans/
]
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazybtpredstarproper_8.ma".
-include "basic_2/reduction/fpb.ma".
-include "basic_2/computation/fpbs.ma".
+include "basic_2/notation/relations/predsubtystarproper_8.ma".
+include "basic_2/rt_transition/fpb.ma".
+include "basic_2/rt_computation/fpbs.ma".
-(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************)
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
definition fpbg: ∀h. sd h → tri_relation genv lenv term ≝
λh,o,G1,L1,T1,G2,L2,T2.
∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-interpretation "'qrst' proper parallel computation (closure)"
- 'LazyBTPRedStarProper h o G1 L1 T1 G2 L2 T2 = (fpbg h o G1 L1 T1 G2 L2 T2).
+interpretation "proper parallel rst-computation (closure)"
+ 'PRedSubTyStarProper h o G1 L1 T1 G2 L2 T2 = (fpbg h o G1 L1 T1 G2 L2 T2).
(* Basic properties *********************************************************)
lemma fpb_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄.
+ ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
/2 width=5 by ex2_3_intro/ qed.
lemma fpbg_fpbq_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2.
- ⦃G1, L1, T1⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄.
+ ⦃G1, L1, T1⦄ >[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
#h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 *
/3 width=9 by fpbs_strap1, ex2_3_intro/
qed-.
+
+(* Note: this is used in the closure proof *)
+lemma fpbg_fpbs_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ >[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
+#h #o #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpbq_trans/
+qed-.
+
+(* Basic_2A1: uses: fpbg_fleq_trans *)
+lemma fpbg_ffdeq_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >[h, o] ⦃G, L, T⦄ →
+ ∀G2,L2,T2. ⦃G, L, T⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
+/3 width=5 by fpbg_fpbq_trans, fpbq_ffdeq/ 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_computation/cpxs_tdeq.ma".
+include "basic_2/rt_computation/fpbs_cpxs.ma".
+include "basic_2/rt_computation/fpbg.ma".
+
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES **************************)
+
+(* Properties with uncounted context-sensitive parallel rt-computation ******)
+
+(* Basic_2A1: was: cpxs_fpbg *)
+lemma cpxs_tdneq_fpbg: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
+ (T1 ≛[h, o] T2 → ⊥) → ⦃G, L, T1⦄ >[h, o] ⦃G, L, T2⦄.
+#h #o #G #L #T1 #T2 #H #H0
+elim (cpxs_tdneq_fwd_step_sn … H … H0) -H -H0
+/4 width=5 by cpxs_tdeq_fpbs, fpb_cpx, ex2_3_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 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/multiple/fleq_fleq.ma".
-include "basic_2/reduction/fpbq_alt.ma".
-include "basic_2/computation/fpbg.ma".
-
-(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************)
-
-(* Properties on lazy equivalence for closures ******************************)
-
-lemma fpbg_fleq_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G, L, T⦄ →
- ∀G2,L2,T2. ⦃G, L, T⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄.
-/3 width=5 by fpbg_fpbq_trans, fleq_fpbq/ qed-.
-
-lemma fleq_fpbg_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ →
- ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≡[0] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄.
-#h #o #G #G2 #L #L2 #T #T2 * #G0 #L0 #T0 #H0 #H02 #G1 #L1 #T1 #H1
-elim (fleq_fpb_trans … H1 … H0) -G -L -T
-/4 width=9 by fpbs_strap2, fleq_fpbq, ex2_3_intro/
-qed-.
-
-(* alternative definition of fpbs *******************************************)
-
-lemma fleq_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2.
- ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=1 by lleq_fpbs/
-qed.
-
-lemma fpbg_fwd_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2.
- ⦃G1, L1, T1⦄ >≛[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 *
-/3 width=5 by fpbs_strap2, fpb_fpbq/
-qed-.
-
-lemma fpbs_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨
- ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄.
-#h #o #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 @(fpbq_ind_alt … H2) -H2 #H2
- [ /3 width=5 by fleq_trans, or_introl/
- | elim (fleq_fpb_trans … H1 … H2) -G -L -T
- /4 width=5 by ex2_3_intro, or_intror, fleq_fpbs/
- | /3 width=5 by fpbg_fleq_trans, or_intror/
- | /4 width=5 by fpbg_fpbq_trans, fpb_fpbq, or_intror/
- ]
-]
-qed-.
-
-(* Advanced properties of "qrst" parallel computation on closures ***********)
-
-lemma fpbs_fpb_trans: ∀h,o,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, o] ⦃F2, K2, T2⦄ →
- ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, o] ⦃G2, L2, U2⦄ →
- ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, o] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, o] ⦃G2, L2, U2⦄.
-#h #o #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_fpbg … H) -H
-[ #H12 #G2 #L2 #U2 #H2 elim (fleq_fpb_trans … H12 … H2) -F2 -K2 -T2
- /3 width=5 by fleq_fpbs, ex2_3_intro/
-| * #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
- @(ex2_3_intro … H4) -H4 /3 width=5 by fpbs_strap1, fpb_fpbq/
-]
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/fpbg_fpbs.ma".
+include "basic_2/rt_computation/fpbg_fpbs.ma".
-(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************)
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
(* Main properties **********************************************************)
(* *)
(**************************************************************************)
-include "basic_2/computation/lpxs_lleq.ma".
-include "basic_2/computation/fpbs_lift.ma".
-include "basic_2/computation/fpbg_fleq.ma".
+include "basic_2/static/ffdeq_fqup.ma".
+include "basic_2/static/ffdeq_ffdeq.ma".
+include "basic_2/rt_transition/fpbq_fpb.ma".
+include "basic_2/rt_computation/fpbg.ma".
-(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************)
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
-(* Properties on "qrst" parallel reduction on closures **********************)
+(* Advanced forward lemmas **************************************************)
+
+lemma fpbg_fwd_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2.
+ ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 *
+/3 width=5 by fpbs_strap2, fpb_fpbq/
+qed-.
+
+(* Advanced properties with degree-based equivalence on closures ************)
+
+(* Basic_2A1: uses: fleq_fpbg_trans *)
+lemma ffdeq_fpbg_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >[h, o] ⦃G2, L2, T2⦄ →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
+#h #o #G #G2 #L #L2 #T #T2 * #G0 #L0 #T0 #H0 #H02 #G1 #L1 #T1 #H1
+elim (ffdeq_fpb_trans … H1 … H0) -G -L -T
+/4 width=9 by fpbs_strap2, fpbq_ffdeq, ex2_3_intro/
+qed-.
+
+(* Properties with parallel proper rst-reduction on closures ****************)
lemma fpb_fpbg_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2.
- ⦃G1, L1, T1⦄ ≻[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄.
+ ⦃G1, L1, T1⦄ ≻[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >[h, o] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
/3 width=5 by fpbg_fwd_fpbs, ex2_3_intro/ qed-.
+(* Properties with parallel rst-reduction on closures ***********************)
+
lemma fpbq_fpbg_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2.
- ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 @(fpbq_ind_alt … H1) -H1
-/2 width=5 by fleq_fpbg_trans, fpb_fpbg_trans/
+ ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >[h, o] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
+elim (fpbq_inv_fpb … H1) -H1
+/2 width=5 by ffdeq_fpbg_trans, fpb_fpbg_trans/
qed-.
-(* Properties on "qrst" parallel compuutation on closures *******************)
+(* Properties with parallel rst-compuutation on closures ********************)
lemma fpbs_fpbg_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ →
- ∀G2,L2,T2. ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄.
+ ∀G2,L2,T2. ⦃G, L, T⦄ >[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
#h #o #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpbq_fpbg_trans/
qed-.
-(* Note: this is used in the closure proof *)
-lemma fpbg_fpbs_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
- ∀G1,L1,T1. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄.
-#h #o #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpbq_trans/
+(* Advanced inversion lemmas of parallel rst-computation on closures ********)
+
+(* Basic_2A1: was: fpbs_fpbg *)
+lemma fpbs_inv_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
+ ∨∨ ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄
+ | ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
+#h #o #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 (fpbq_inv_fpb … H2) -H2 #H2
+ [ /3 width=5 by ffdeq_trans, or_introl/
+ | elim (ffdeq_fpb_trans … H1 … H2) -G -L -T
+ /4 width=5 by ex2_3_intro, or_intror, ffdeq_fpbs/
+ | /3 width=5 by fpbg_ffdeq_trans, or_intror/
+ | /4 width=5 by fpbg_fpbq_trans, fpb_fpbq, or_intror/
+ ]
+]
qed-.
-(* Note: this is used in the closure proof *)
-lemma fqup_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
-/3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/
-qed.
-
-lemma cpxs_fpbg: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 →
- (T1 = T2 → ⊥) → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄.
-#h #o #G #L #T1 #T2 #H #H0 elim (cpxs_neq_inv_step_sn … H … H0) -H -H0
-/4 width=5 by cpxs_fpbs, fpb_cpx, ex2_3_intro/
-qed.
-
-lemma lstas_fpbg: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → (T1 = T2 → ⊥) →
- ∀d1. d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄.
-/3 width=5 by lstas_cpxs, cpxs_fpbg/ qed.
-
-lemma lpxs_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 →
- (L1 ≡[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ >≛[h, o] ⦃G, L2, T⦄.
-#h #o #G #L1 #L2 #T #H #H0 elim (lpxs_nlleq_inv_step_sn … H … H0) -H -H0
-/4 width=5 by fpb_lpx, lpxs_lleq_fpbs, ex2_3_intro/
-qed.
+(* Advanced properties of parallel rst-computation on closures **************)
+
+lemma fpbs_fpb_trans: ∀h,o,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, o] ⦃F2, K2, T2⦄ →
+ ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, o] ⦃G2, L2, U2⦄ →
+ ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, o] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, o] ⦃G2, L2, U2⦄.
+#h #o #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H
+[ #H12 #G2 #L2 #U2 #H2 elim (ffdeq_fpb_trans … H12 … H2) -F2 -K2 -T2
+ /3 width=5 by ffdeq_fpbs, ex2_3_intro/
+| * #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
+ @(ex2_3_intro … H4) -H4 /3 width=5 by fpbs_strap1, fpb_fpbq/
+]
+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_computation/fpbs_fqup.ma".
+include "basic_2/rt_computation/fpbg.ma".
+
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
+
+(* Properties with plus-iterated structural successor for closures **********)
+
+(* Note: this is used in the closure proof *)
+lemma fqup_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
+/3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_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 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/lpxs_ffdeq.ma".
+include "basic_2/computation/fpbg_ffdeq.ma".
+
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES **************************)
+
+lemma lpxs_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 →
+ (L1 ≡[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ >≛[h, o] ⦃G, L2, T⦄.
+#h #o #G #L1 #L2 #T #H #H0 elim (lpxs_nlleq_inv_step_sn … H … H0) -H -H0
+/4 width=5 by fpb_lpx, lpxs_lleq_fpbs, ex2_3_intro/
+qed.
⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
/2 width=5 by tri_TC_strap/ qed-.
-(* Basic_2A1: uses: lleq_fpbs *)
+(* Basic_2A1: uses: lleq_fpbs fleq_fpbs *)
lemma ffdeq_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
/3 width=1 by fpbq_fpbs, fpbq_ffdeq/ qed.
(* *)
(**************************************************************************)
+include "basic_2/static/ffdeq_fqup.ma".
include "basic_2/rt_computation/cpxs.ma".
include "basic_2/rt_computation/fpbs_fqup.ma".
/3 width=5 by fpbs_strap2, fpbq_cpx/
qed-.
+lemma cpxs_tdeq_fpbs: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈*[h] T →
+ ∀T2. T ≛[h, o] T2 → ⦃G, L, T1⦄ ≥[h, o] ⦃G, L, T2⦄.
+/4 width=3 by cpxs_fpbs_trans, ffdeq_fpbs, tdeq_ffdeq/ qed.
+
(* Properties with star-iterated structural successor for closures **********)
lemma cpxs_fqus_fpbs: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_csx.ma lfsx_lfsx.ma
lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma
fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma
+fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma
(* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************)
+(* Properties with degree-based equivalence for terms ***********************)
+
+lemma tdeq_ffdeq: ∀h,o,T1,T2. T1 ≛[h, o] T2 →
+ ∀G,L. ⦃G, L, T1⦄ ≛[h, o] ⦃G, L, T2⦄.
+/2 width=1 by ffdeq_intro_sn/ qed.
+
(* Advanced properties ******************************************************)
lemma ffdeq_refl: ∀h,o. tri_reflexive … (ffdeq h o).
}
]
[ { "parallel qrst-computation" * } {
- [ [ "" ] "fpbg ( ⦃?,?,?⦄ >≛[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
+
}
]
[ { "decomposed rt-computation" * } {
]
*)
[ { "uncounted context-sensitive parallel rst-computation" * } {
+ [ [ "proper for closures" ] "fpbg" + "( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ]
[ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ]
}
]
projects / helm.git / commitdiff