+++ /dev/null
-(* Properties on extended context-sensitive parallel computation for terms **)
-
-lemma fpbs_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, o] U2 → (T2 = U2 → ⊥) →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ≥[h, o] ⦃G2, L2, U2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 elim (fpbs_inv_alt … H) -H
-#L00 #L0 #T0 #HT10 #H10 #HL00 #HL02 lapply (lleq_cpx_trans … HTU2 … HL02) -HTU2
-#HTU2 lapply (cpx_lleq_conf_sn … HTU2 … HL02) -HL02
-#HL02 lapply (lpxs_cpx_trans … HTU2 … HL00) -HTU2
-#HTU2 elim (fqus_cpxs_trans_neq … H10 … HTU2 HnTU2) -H10 -HTU2 -HnTU2
-#U0 #HTU0 #HnTU0 #HU02 elim (eq_term_dec T1 T0) #HnT10 destruct
-[ -HT10 elim (cpxs_neq_inv_step_sn … HTU0 HnTU0) -HTU0 -HnTU0
-| -HnTU0 elim (cpxs_neq_inv_step_sn … HT10 HnT10) -HT10 -HnT10
-]
-/4 width=10 by fpbs_intro_alt, cpxs_trans, ex3_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 h, break term 46 o ] ⦃ break term 46 G, break term 46 L, break term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'BTSN $h $o $G $L $T }.
+++ /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 h, break term 46 o ] ⦃ break term 46 G, break term 46 L, break term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'BTSNAlt $h $o $G $L $T }.
--- /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 h, break term 46 o ] 𝐒 ⦃ break term 46 G, break term 46 L, break term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedSubTyStrong $h $o $G $L $T }.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/btsn_5.ma".
-include "basic_2/reduction/fpb.ma".
-include "basic_2/computation/csx.ma".
+include "basic_2/notation/relations/predsubtystrong_5.ma".
+include "basic_2/rt_transition/fpb.ma".
-(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************)
+(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
inductive fsb (h) (o): relation3 genv lenv term ≝
| fsb_intro: ∀G1,L1,T1. (
.
interpretation
- "'qrst' strong normalization (closure)"
- 'BTSN h o G L T = (fsb h o G L T).
+ "strong normalization for parallel rst-transition (closure)"
+ 'PRedSubTyStrong h o G L T = (fsb h o G L T).
(* Basic eliminators ********************************************************)
+(* Note: eliminator with shorter ground hypothesis *)
+(* Note: to be named fsb_ind when fsb becomes a definition like csx, lfsx ***)
lemma fsb_ind_alt: ∀h,o. ∀R: relation3 …. (
- â\88\80G1,L1,T1. ⦥[h,o] ⦃G1, L1, T1⦄ → (
+ â\88\80G1,L1,T1. â\89¥[h,o] ð\9d\90\92⦃G1, L1, T1⦄ → (
∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2
) → R G1 L1 T1
) →
- â\88\80G,L,T. ⦥[h, o] ⦃G, L, T⦄ → R G L T.
+ â\88\80G,L,T. â\89¥[h, o] ð\9d\90\92⦃G, L, T⦄ → R G L T.
#h #o #R #IH #G #L #T #H elim H -G -L -T
/4 width=1 by fsb_intro/
qed-.
-(* Basic inversion lemmas ***************************************************)
-
-lemma fsb_inv_csx: ∀h,o,G,L,T. ⦥[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, o] T.
-#h #o #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpb_cpx/
-qed-.
+(* Basic_2A1: removed theorems 5:
+ fsba_intro fsba_ind_alt fsba_fpbs_trans fsb_fsba fsba_inv_fsb
+*)
+++ /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/btsnalt_5.ma".
-include "basic_2/computation/fpbg_fpbs.ma".
-include "basic_2/computation/fsb.ma".
-
-(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************)
-
-(* Note: alternative definition of fsb *)
-inductive fsba (h) (o): relation3 genv lenv term ≝
-| fsba_intro: ∀G1,L1,T1. (
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → fsba h o G2 L2 T2
- ) → fsba h o G1 L1 T1.
-
-interpretation
- "'big tree' strong normalization (closure) alternative"
- 'BTSNAlt h o G L T = (fsba h o G L T).
-
-(* Basic eliminators ********************************************************)
-
-lemma fsba_ind_alt: ∀h,o. ∀R: relation3 …. (
- ∀G1,L1,T1. ⦥⦥[h,o] ⦃G1, L1, T1⦄ → (
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2
- ) → R G1 L1 T1
- ) →
- ∀G,L,T. ⦥⦥[h, o] ⦃G, L, T⦄ → R G L T.
-#h #o #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,o,G1,L1,T1. ⦥⦥[h, o] ⦃G1, L1, T1⦄ →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦥⦥[h, o] ⦃G2, L2, T2⦄.
-#h #o #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,o,G,L,T. ⦥[h, o] ⦃G, L, T⦄ → ⦥⦥[h, o] ⦃G, L, T⦄.
-#h #o #G #L #T #H @(fsb_ind_alt … H) -G -L -T
-#G1 #L1 #T1 #_ #IH @fsba_intro
-#G2 #L2 #T2 * /3 width=5 by fsba_fpbs_trans/
-qed.
-
-(* Main inversion lemmas ****************************************************)
-
-theorem fsba_inv_fsb: ∀h,o,G,L,T. ⦥⦥[h, o] ⦃G, L, T⦄ → ⦥[h, o] ⦃G, L, T⦄.
-#h #o #G #L #T #H @(fsba_ind_alt … H) -G -L -T
-/4 width=1 by fsb_intro, fpb_fpbg/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma fsb_fpbs_trans: ∀h,o,G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦥[h, o] ⦃G2, L2, T2⦄.
-/4 width=5 by fsba_inv_fsb, fsb_fsba, fsba_fpbs_trans/ qed-.
-
-(* Advanced eliminators *****************************************************)
-
-lemma fsb_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term.
- (∀G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
- ) →
- ∀G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ → R G1 L1 T1.
-#h #o #R #IH #G1 #L1 #T1 #H @(fsba_ind_alt h o … G1 L1 T1)
-/3 width=1 by fsba_inv_fsb, fsb_fsba/
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_transition/fpb_ffdeq.ma".
+include "basic_2/rt_computation/fsb.ma".
+
+(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
+
+(* Properties with degree-based equivalence for closures ********************)
+
+lemma fsb_ffdeq_trans: ∀h,o,G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ≥[h, o] 𝐒⦃G2, L2, T2⦄.
+#h #o #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+#G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12
+@fsb_intro #G #L #T #H2
+elim (ffdeq_fpb_trans … H12 … H2) -G2 -L2 -T2
+/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/rt_computation/fpbg_fpbs.ma".
+include "basic_2/rt_computation/fsb_ffdeq.ma".
+
+(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
+
+(* Properties with parallel rst-computation for closures ********************)
+
+lemma fsb_fpbs_trans: ∀h,o,G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ≥[h, o] 𝐒⦃G2, L2, T2⦄.
+#h #o #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
+elim (fpbs_inv_fpbg … H12) -H12
+[ -IH /2 width=5 by fsb_ffdeq_trans/
+| -H1 * /2 width=5 by/
+]
+qed-.
+
+(* Properties with proper parallel rst-computation for closures *************)
+
+lemma fsb_intro_fpbg: ∀h,o,G1,L1,T1. (
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → ≥[h, o] 𝐒⦃G2, L2, T2⦄
+ ) → ≥[h, o] 𝐒⦃G1, L1, T1⦄.
+/4 width=1 by fsb_intro, fpb_fpbg/ qed.
+
+(* Eliminators with proper parallel rst-computation for closures ************)
+
+lemma fsb_ind_fpbg_fpbs: ∀h,o. ∀R:relation3 genv lenv term.
+ (∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ R G1 L1 T1
+ ) →
+ ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2.
+#h #o #R #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
+@IH1 -IH1
+[ -IH /2 width=5 by fsb_fpbs_trans/
+| -H1 #G0 #L0 #T0 #H10
+ elim (fpbs_fpbg_trans … H12 … H10) -G2 -L2 -T2
+ /2 width=5 by/
+]
+qed-.
+
+lemma fsb_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term.
+ (∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ R G1 L1 T1
+ ) →
+ ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → R G1 L1 T1.
+#h #o #R #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
+/3 width=1 by/
+qed-.
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_lfpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma
+fsb.ma fsb_ffdeq.ma fsb_fpbg.ma
class "sky"
[ { "rt-computation" * } {
(*
- [ { "evaluation for context-sensitive rt-reduction" * } {
- [ [ "" ] "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ]
- }
- ]
- [ { "evaluation for context-sensitive reduction" * } {
- [ [ "" ] "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
- }
- ]
- [ { "strongly normalizing qrst-computation" * } {
- [ [ "" ] "fsb ( ⦥[?,?] ⦃?,?,?⦄ )" "fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )" "fsb_aaa" + "fsb_csx" * ]
- }
- ]
- [ { "parallel qrst-computation" * } {
-
- }
- ]
[ { "decomposed rt-computation" * } {
[ [ "" ] "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ]
}
]
*)
[ { "uncounted context-sensitive parallel rst-computation" * } {
+ [ [ "strongly normalizing for closures" ] "fsb" + "( ≥[?,?] 𝐒⦃?,?,?⦄ )" "fsb_ffdeq" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ]
[ [ "proper for closures" ] "fpbg" + "( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lfpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ]
[ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ]
}
class "italic" { 2 }
(*
+ [ { "evaluation for context-sensitive rt-reduction" * } {
+ [ [ "" ] "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ]
+ }
+ ]
+ [ { "evaluation for context-sensitive reduction" * } {
+ [ [ "" ] "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
+ }
+ ]
[ { "normal forms for context-sensitive rt-reduction" * } {
[ [ "" ] "cnx_crx" + "cnx_cix" * ]
}
[ [ "" ] "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
}
]
- [ { "pointwise union for local environments" * } {
- [ [ "" ] "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ]
- }
- ]
- [ { "lazy pointwise extension of a relation" * } {
- [ [ "" ] "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_lreq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ]
- }
- ]
[ { "global env. slicing" * } {
[ [ "" ] "gget ( ⬇[?] ? ≡ ? )" "gget_gget" * ]
}
[ [ "" ] "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ]
}
]
- [ { "pointwise extension of a relation" * } {
- [ [ "" ] "lpx_sn" "lpx_sn_alt" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
- }
- ]
- [ [ "" ] "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ]
- [ [ "" ] "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
*)
projects / helm.git / commitdiff