R T1
) →
∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R T.
-#h #g #G #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
-@H0 -H0 /3 width=1/ -IHT1 /4 width=1/
+#h #g #G #L #R #H0 #T1 #H elim H -T1
+/5 width=1 by SN_intro/
qed-.
(* Basic properties *********************************************************)
lemma csx_intro: ∀h,g,G,L,T1.
(∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] T2) →
⦃G, L⦄ ⊢ ⬊*[h, g] T1.
-/4 width=1/ qed.
+/4 width=1 by SN_intro/ qed.
lemma csx_cpx_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ ⬊*[h, g] T2.
-#h #g #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
-@csx_intro #T #HLT2 #HT2
-elim (eq_term_dec T1 T2) #HT12
-[ -IHT1 -HLT12 destruct /3 width=1/
-| -HT1 -HT2 /3 width=4/
+#h #g #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12
+elim (eq_term_dec T1 T2) #HT12 destruct /3 width=4 by/
qed-.
(* Basic_1: was just: sn3_nf2 *)
lemma cnx_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-/2 width=1/ qed.
+/2 width=1 by NF_to_SN/ qed.
-lemma cnx_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ⬊*[h, g] ⋆k.
+lemma csx_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ⬊*[h, g] ⋆k.
#h #g #G #L #k elim (deg_total h g k)
-#l generalize in match k; -k @(nat_ind_plus … l) -l /3 width=1/
+#l generalize in match k; -k @(nat_ind_plus … l) -l /3 width=6 by cnx_csx, cnx_sort/
#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
#Hkl @csx_intro #X #H #HX elim (cpx_inv_sort1 … H) -H
[ #H destruct elim HX //
-| -HX * #l0 #_ #H destruct -l0 /2 width=1/
+| -HX * #l0 #_ #H destruct -l0 /2 width=1 by/
]
qed.
[ * #W0 #T0 #HLW0 #HLT0 #H destruct
elim (eq_false_inv_tpair_sn … H2) -H2
[ /3 width=3 by csx_cpx_trans/
- | -HLW0 * #H destruct /3 width=1/
+ | -HLW0 * #H destruct /3 width=1 by/
]
|2,3: /3 width=3 by csx_cpx_trans/
]
∀I,V,T. U = ②{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] V.
#h #g #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csx_intro #V2 #HLV2 #HV2
-@(IH (②{I}V2.T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/
+@(IH (②{I}V2.T)) -IH /2 width=3 by cpx_pair_sn/ -HLV2
+#H destruct /2 width=1 by/
qed-.
(* Basic_1: was just: sn3_gen_head *)
∀a,I,V,T. U = ⓑ{a,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬊*[h, g] T.
#h #g #G #L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct
@csx_intro #T2 #HLT2 #HT2
-@(IH (ⓑ{a,I}V.T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
+@(IH (ⓑ{a,I}V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2
+#H destruct /2 width=1 by/
qed-.
(* Basic_1: was just: sn3_gen_bind *)
∀I,V,T. U = ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
#h #g #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csx_intro #T2 #HLT2 #HT2
-@(IH (ⓕ{I}V.T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
+@(IH (ⓕ{I}V.T2)) -IH /2 width=3 by cpx_flat/ -HLT2
+#H destruct /2 width=1 by/
qed-.
(* Basic_1: was just: sn3_gen_flat *)
+++ /dev/null
-include "basic_2/computation/fpbc.ma".
-
-(* Advanced eliminators *****************************************************)
-
-fact csx_ind_fpbc_aux: ∀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⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#h #g #R #IH1 #G1 #L1 #T1 #H @(csx_ind … H) -T1
-#T1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1
-#G1 #L1 #T1 #IH2 #H1 #IH3 #G2 #L2 #T2 #H12 @IH1 -IH1 /2 width=5 by csx_fqus_conf/
-#G #L #T *
-[ #G0 #L0 #T0 #H20 lapply (fqus_fqup_trans … H12 H20) -G2 -L2 -T2
- #H10 @(IH2 … H10) -IH2 /2 width=5 by csx_fqup_conf/
- #T2 #HT02 #H #G3 #L3 #T3 #HT23 elim (fqup_cpx_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/
-]
-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-.
--- /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.ma".
+include "basic_2/computation/csx_lpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
+
+(* Advanced properties ******************************************************)
+
+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/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/lpxs_lleq.ma".
+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".
#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 elim (fqup_inv_step_sn … HT2) -HT2
- #H6 #H7 #H8 #H9 #H10 @or_intror @(ex2_3_intro … H6 H7 H8)
- /5 width=9 by fpbsa_inv_fpbs, fpbc_fqup, fqu_fqup, ex3_2_intro, ex2_3_intro, or_intror/
+ [ #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/
- | elim (lpxs_nlleq_inv_step_sn … HL2 H) -HL2 -H
- /5 width=5 by fpbc_lpxs, lpxs_fpbs, ex2_3_intro, or_intror/
+ | /5 width=5 by fpbc_lpxs, ex2_3_intro, or_intror/
]
]
| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H
(* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************)
-(* Inversion lemmas on lazy equivalence for local environments **************)
+(* Advanced properties ******************************************************)
-lemma lpxs_nlleq_inv_step_sn: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[d, T] L2 → ⊥) →
- ∃∃L. ⦃G, L1⦄ ⊢ ➡*[h, g] L & L1 ⋕[d, T] L → ⊥ & ⦃G, L⦄ ⊢ ➡*[h, g] L2.
-#h #g #G #L1 #L2 #T #d #H @(lpxs_ind_dx … H) -L1
-[ #H elim H -H //
-| #L1 #L #H1 #H2 #IH2 #H12 elim (lleq_dec T L1 L d) #H
- [ -H2 elim IH2 -IH2
- /4 width=4 by lpxs_strap2, lleq_canc_sn, lleq_trans, ex3_intro/
- | -IH2 -H12 /3 width=4 by lpx_lpxs, ex3_intro/ (**) (* auto fails without clear *)
- ]
-]
-qed-.
+axiom lleq_lpxs_trans_nlleq: ∀h,g,G,L1s,L1d,T,d. L1s ⋕[d, T] L1d →
+ ∀L2d. ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → (L1d ⋕[d, T] L2d → ⊥) →
+ ∃∃L2s. ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s & L2s ⋕[d, T] L2d & L1s ⋕[d, T] L2s → ⊥.
+
+(* Advanced inversion lemmas ************************************************)
+
+axiom lpxs_inv_cpxs_nlleq: ∀h,g,G,L1,L2,T1. ⦃G, L1⦄ ⊢ ➡*[h,g] L2 → (L1 ⋕[O, T1] L2 → ⊥) →
+ ∃∃T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & T1 = T2 → ⊥ & ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2.
(* Properties on lazy equivalence for local environments ********************)
--- /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/lazysn_5.ma".
+include "basic_2/relocation/lleq.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+definition lsx: ∀h. sd h → relation3 term genv lenv ≝
+ λh,g,T,G. SN … (lpxs h g G) (lleq 0 T).
+
+interpretation
+ "extended strong normalization (local environment)"
+ 'LazySN h g T G L = (lsx h g T G L).
+
+(* Basic eliminators ********************************************************)
+
+lemma lsx_ind: ∀h,g,T,G. ∀R:predicate lenv.
+ (∀L1. G ⊢ ⋕⬊*[h, g, T] L1 →
+ (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T] L2 → ⊥) → R L2) →
+ R L1
+ ) →
+ ∀L. G ⊢ ⋕⬊*[h, g, T] L → R L.
+#h #g #T #G #R #H0 #L1 #H elim H -L1
+/5 width=1 by lleq_sym, SN_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsx_intro: ∀h,g,T,G,L1.
+ (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) →
+ G ⊢ ⋕⬊*[h, g, T] L1.
+/5 width=1 by lleq_sym, SN_intro/ qed.
+
+lemma lsx_atom: ∀h,g,T,G. G ⊢ ⋕⬊*[h, g, T] ⋆.
+#h #g #T #G @lsx_intro
+#X #H #HT lapply (lpxs_inv_atom1 … H) -H
+#H destruct elim HT -HT //
+qed.
+
+lemma lsx_sort: ∀h,g,G,L,k. G ⊢ ⋕⬊*[h, g, ⋆k] L.
+#h #g #G #L1 #k @lsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=4 by lpxs_fwd_length, lleq_sort/
+qed.
+
+lemma lsx_gref: ∀h,g,G,L,p. G ⊢ ⋕⬊*[h, g, §p] L.
+#h #g #G #L1 #p @lsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=4 by lpxs_fwd_length, lleq_gref/
+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_lleq.ma".
+include "basic_2/computation/lsx.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* Advanced properties ******************************************************)
+
+lemma lsx_lleq_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 →
+ ∀L2. L1 ⋕[0, T] L2 → G ⊢ ⋕⬊*[h, g, T] L2.
+#h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
+@lsx_intro #L #HL2 #HnT elim (lleq_lpxs_trans_nlleq … HL12 … HL2 HnT) -L2 /3 width=4 by/
+qed-.
+
+lemma lsx_lpxs_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → G ⊢ ⋕⬊*[h, g, T] L2.
+#h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
+elim (lleq_dec T L1 L2 0) /3 width=4 by lsx_lleq_trans/
+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_lleq.ma".
+include "basic_2/computation/csx_alt.ma".
+include "basic_2/computation/lsx.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* Main properties **********************************************************)
+
+axiom csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → G ⊢ ⋕⬊*[h, g, T] L.
+
+axiom lsx_inv_csx: ∀h,g,G,L,T. G ⊢ ⋕⬊*[h, g, T] L → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+
+(*
+#h #g #G #L1 #T1 #H @(csx_ind_alt … H) -T1
+#T1 #_ #IHT1 @lsx_intro
+#L2 #HL12 #HnT1 elim (lpxs_inv_cpxs_nlleq … HL12 HnT1) -HL12 -HnT1
+#T2 #H1T12 #HnT12 #H2T12 lapply (IHT1 … H1T12 HnT12) -IHT1 -H1T12 -HnT12
+#HT2
+*)
--- /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-.
--- /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( G ⊢ ⋕ ⬊ * break [ term 46 h , break term 46 g , break term 46 T ] break term 46 L )"
+ non associative with precedence 45
+ for @{ 'LazySN $h $g $T $G $L }.
}
]
[ { "strongly normalizing extended computation" * } {
- [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
- [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" * ]
+ [ "lsx ()" "lsx_cpxs" + "lsx_fpbc" + "lsx_csx" * ]
+ [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
+ [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ]
}
]
[ { "\"big tree\" parallel computation" * } {
projects / helm.git / commitdiff