(* Properties on sn extended parallel reduction for local environments ******)
-lemma lpx_cpx_trans: ∀h,G. b_c_transitive … (cpx h G) (λ_.lpx h G).
-#h #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
-[ /2 width=3 by/
-| /3 width=2 by cpx_cpxs, cpx_st/
-| #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
- elim (lpx_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
- elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
- /4 width=7 by cpxs_delta, cpxs_strap2/
-|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/
-|5,7,8: /3 width=1 by cpxs_flat, cpxs_ct, cpxs_eps/
-| /4 width=3 by cpxs_zeta, lpx_pair/
-| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/
-]
-qed-.
-
lemma cpx_bind2: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 →
∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈[h, o] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2.
(* Advanced properties ******************************************************)
-lemma lpx_cpxs_trans: ∀h,o,G. b_rs_transitive … (cpx h o G) (λ_.lpx h o G).
-#h #o #G @b_c_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *)
-qed-.
-
lemma cpxs_bind2_dx: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 →
∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h, o] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2.
⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄.
/4 width=1 by SN_intro/ qed.
-lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃⋆s⦄.
-#h #o #G #L #s elim (deg_total h o s)
-#d generalize in match s; -s elim d -d
-[ #s1 #Hs1 @csx_intro #X #H #HX elim HX -HX
- elim (cpx_inv_sort1 … H) -H #H destruct //
- /3 width=3 by tdeq_sort, deg_next/
-| #d #IH #s #Hsd lapply (deg_next_SO … Hsd) -Hsd
- #Hsd @csx_intro #X #H #HX
- elim (cpx_inv_sort1 … H) -H #H destruct /2 width=1 by/
- elim HX //
-]
-qed.
-
(* Basic forward lemmas *****************************************************)
fact csx_fwd_pair_sn_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ →
(* Basic_1: was just: sn3_nf2 *)
lemma cnx_csx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
/2 width=1 by NF_to_SN/ qed.
+
+(* Advanced properties ******************************************************)
+
+lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃⋆s⦄.
+#h #o #G #L #s elim (deg_total h o s)
+#d generalize in match s; -s elim d -d
+[ /3 width=3 by cnx_csx, cnx_sort/
+| #d #IH #s #Hsd lapply (deg_next_SO … Hsd) -Hsd
+ #Hsd @csx_intro #X #H #HX
+ elim (cpx_inv_sort1 … H) -H #H destruct /2 width=1 by/
+ elim HX -HX //
+]
+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 *)
+(* *)
+(**************************************************************************)
+
+(* STRONGLY NORMALIZING TERM VECTORS FOR UNCOUNTED PARALLEL RT-TRANSITION ***)
+
+include "basic_2/rt_computation/cpxs_theq_vector.ma".
+include "basic_2/rt_computation/csx_simple_theq.ma".
+include "basic_2/rt_computation/csx_cnx.ma".
+include "basic_2/rt_computation/csx_cpxs.ma".
+include "basic_2/rt_computation/csx_vector.ma".
+
+(* Properties with normal terms for uncounted parallel rt-transition ********)
+
+(* Basic_1: was just: sn3_appls_lref *)
+lemma csx_applv_cnx: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ →
+ ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Vs⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.T⦄.
+#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs
+[ #_ normalize in ⊢ (?????%); /2 width=1/
+| #V #Vs #IHV #H
+ elim (csxv_inv_cons … H) -H #HV #HVs
+ @csx_appl_simple_theq /2 width=1 by applv_simple/ -IHV -HV -HVs
+ #X #H #H0
+ lapply (cpxs_fwd_cnx_vector … o … H) -H // -H1T -H2T #H
+ elim (H0) -H0 //
+]
+qed.
+
+(* Advanced properties ******************************************************)
+
+lemma csx_applv_sort: ∀h,o,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Vs⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.⋆s⦄.
+#h #o #G #L #s elim (deg_total h o s)
+#d generalize in match s; -s elim d -d
+[ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/
+| #d #IHd #s #Hd #Vs elim Vs -Vs /2 width=1 by/
+ #V #Vs #IHVs #HVVs
+ elim (csxv_inv_cons … HVVs) #HV #HVs
+ @csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/
+ #X #H #H0
+ elim (cpxs_fwd_sort_vector … o … H) -H #H
+ [ elim H0 -H0 //
+ | -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h s)))
+ /3 width=1 by cpxs_flat_dx, deg_next_SO/
+ ]
+]
+qed.
(**************************************************************************)
include "basic_2/rt_computation/cpxs_lfpx.ma".
-include "basic_2/rt_computation/csx_drops.ma".
include "basic_2/rt_computation/csx_cpxs.ma".
(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
-(* Advanced properties ******************************************************)
+(* Properties with uncounted parallel rt-transition on referred entries *****)
(* Basic_2A1: was just: csx_lpx_conf *)
lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
/5 width=3 by csx_intro, lfpx_cpx_trans, lfpx_cpxs_conf/
qed-.
+(* Advanced properties ******************************************************)
+
lemma csx_abst: ∀h,o,p,G,L,W. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃W⦄ →
∀T. ⦃G, L.ⓛW⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓛ{p}W.T⦄.
#h #o #p #G #L #W #HW @(csx_ind … HW) -W
--- /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/syntax/theq_simple.ma".
+include "basic_2/syntax/theq_theq.ma".
+include "basic_2/rt_transition/cpx_simple.ma".
+include "basic_2/rt_computation/cpxs.ma".
+include "basic_2/rt_computation/csx_csx.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+
+(* Properties with head equivalence for terms *******************************)
+
+(* Basic_1: was just: sn3_appl_appl *)
+(* Basic_2A1: was: csx_appl_simple_tsts *)
+lemma csx_appl_simple_theq: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) →
+ 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T1⦄.
+#h #o #G #L #V #H @(csx_ind … H) -V
+#V #_ #IHV #T1 #H @(csx_ind … H) -T1
+#T1 #H1T1 #IHT1 #H2T1 #H3T1
+@csx_intro #X #HL #H
+elim (cpx_inv_appl1_simple … HL) -HL //
+#V0 #T0 #HLV0 #HLT10 #H0 destruct
+elim (tdneq_inv_pair … H) -H
+[ #H elim H -H //
+| -IHT1 #HV0
+ @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
+ @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
+| -IHV -H1T1 #H1T10
+ @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0
+ elim (theq_dec h o T1 T0) #H2T10
+ [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, theq_canc_sn, simple_theq_repl_dx/
+ | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_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/syntax/theq_simple.ma".
-include "basic_2/syntax/theq_theq.ma".
-include "basic_2/rt_transition/cpx_simple.ma".
-include "basic_2/rt_computation/cpxs.ma".
-include "basic_2/rt_computation/csx_csx.ma".
-
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
-
-(* Properties with head equivalence for terms *******************************)
-
-(* Basic_1: was just: sn3_appl_appl *)
-(* Basic_2A1: was: csx_appl_simple_tsts *)
-lemma csx_appl_simple_theq: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) →
- 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T1⦄.
-#h #o #G #L #V #H @(csx_ind … H) -V
-#V #_ #IHV #T1 #H @(csx_ind … H) -T1
-#T1 #H1T1 #IHT1 #H2T1 #H3T1
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1_simple … HL) -HL //
-#V0 #T0 #HLV0 #HLT10 #H0 destruct
-elim (tdneq_inv_pair … H) -H
-[ #H elim H -H //
-| -IHT1 #HV0
- @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
- @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
-| -IHV -H1T1 #H1T10
- @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0
- elim (theq_dec h o T1 T0) #H2T10
- [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, theq_canc_sn, simple_theq_repl_dx/
- | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/
- ]
-]
-qed.
(* v GNU General Public License Version 2 *)
(* *)
(**************************************************************************)
-
+(*
include "basic_2/computation/gcp_cr.ma".
-include "basic_2/computation/cpxs_theq_vector.ma".
-include "basic_2/computation/csx_lpx.ma".
-include "basic_2/computation/csx_vector.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************)
+*)
+include "basic_2/rt_computation/cpxs_theq_vector.ma".
+include "basic_2/rt_computation/csx_vector.ma".
+include "basic_2/rt_computation/csx_theq.ma".
+include "basic_2/rt_computation/csx_lfpx.ma".
-(* Advanced properties ******************************************************)
-
-(* Basic_1: was just: sn3_appls_lref *)
-lemma csx_applv_cnx: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ →
- ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.T.
-#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *)
-#V #Vs #IHV #H
-elim (csxv_inv_cons … H) -H #HV #HVs
-@csx_appl_simple_theq /2 width=1 by applv_simple/ -IHV -HV -HVs
-#X #H #H0
-lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H
-elim (H0) -H0 //
-qed.
+(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
-lemma csx_applv_sort: ∀h,o,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.⋆s.
-#h #o #G #L #s elim (deg_total h o s)
-#d generalize in match s; -s @(nat_ind_plus … d) -d [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ]
-#d #IHd #s #Hkd lapply (deg_next_SO … Hkd) -Hkd
-#Hkd #Vs elim Vs -Vs /2 width=1 by/
-#V #Vs #IHVs #HVVs
-elim (csxv_inv_cons … HVVs) #HV #HVs
-@csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs
-#X #H #H0
-elim (cpxs_fwd_sort_vector … H) -H #H
-[ elim H0 -H0 //
-| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h s))) /2 width=1 by cpxs_flat_dx/
-]
-qed.
+(* Vector form of properties with head equivalence for terms ****************)
+(*
+*)
+(*
+*)
(* Basic_1: was just: sn3_appls_beta *)
-lemma csx_applv_beta: ∀h,o,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.ⓓ{a}ⓝW.V.T →
- â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] â\92¶Vs. â\93\90V.â\93\9b{a}W.T.
+lemma csx_applv_beta: ∀h,o,p,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs.ⓓ{p}ⓝW.V.T →
+ â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] â\92¶Vs. â\93\90V.â\93\9b{p}W.T.
#h #o #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
#V0 #Vs #IHV #V #W #T #H1T
lapply (csx_fwd_pair_sn … H1T) #HV0
lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 →
∀V2. ⬆[0, i + 1] V1 ≡ V2 →
- â\88\80Vs. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] (â\92¶Vs.V2) â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] (ⒶVs.#i).
+ â\88\80Vs. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] (â\92¶Vs.V2) â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] (ⒶVs.#i).
#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
[ /4 width=12 by csx_inv_lift, csx_lref_bind, drop_fwd_drop2/
| #V #Vs #IHV #H1T
(* Basic_1: was just: sn3_appls_abbr *)
lemma csx_applv_theta: ∀h,o,a,G,L,V1b,V2b. ⬆[0, 1] V1b ≡ V2b →
- â\88\80V,T. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] ⓓ{a}V.ⒶV2b.T →
- â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] ⒶV1b.ⓓ{a}V.T.
+ â\88\80V,T. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ⓓ{a}V.ⒶV2b.T →
+ â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ⒶV1b.ⓓ{a}V.T.
#h #o #a #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/
#V1b #V2b #V1 #V2 #HV12 #H
generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
qed.
(* Basic_1: was just: sn3_appls_cast *)
-lemma csx_applv_cast: â\88\80h,o,G,L,Vs,W,T. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] â\92¶Vs.W â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] ⒶVs.T →
- â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] ⒶVs.ⓝW.T.
+lemma csx_applv_cast: â\88\80h,o,G,L,Vs,W,T. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] â\92¶Vs.W â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ⒶVs.T →
+ â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ⒶVs.ⓝW.T.
#h #o #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/
#V #Vs #IHV #W #T #H1W #H1T
lapply (csx_fwd_pair_sn … H1W) #HV
cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma
-csx.ma csx_simple.ma csx_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
-csx_vector.ma
+csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
+csx_vector.ma csx_cnx_vector.ma
[ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
[ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ]
*)
- [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ]
- [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
+ [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" * ]
+ [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
[ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ]
[ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
projects / helm.git / commitdiff