the alternative definition of lpx_sn and llpx_sn is useless since it is recursive
llor seems to contain a bug in the referred components
- some work pointwise extended reduction:
we restore the "full" version and use it for the normaliztion of extended reduction
we still use "lazy" version for the "big-tree" theorem
(* *)
(**************************************************************************)
+include "basic_2/reduction/lpx_ldrop.ma".
include "basic_2/computation/cpxs_lift.ma".
(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
(* Properties on sn extended parallel reduction for local environments ******)
-lemma llpx_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (llpx h g G 0).
+lemma lpx_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (λ_.lpx h g G).
#h #g #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
[ /2 width=3 by/
| /3 width=2 by cpx_cpxs, cpx_sort/
| #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
- elim (llpx_inv_lref_ge_dx … HL12 … HLK2) -L2
- /5 width=8 by cpxs_delta, cpxs_strap2, llpx_cpx_conf/
-| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
- elim (llpx_inv_bind_O … HL12) -HL12 /4 width=1 by cpxs_bind/
-| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
- elim (llpx_inv_flat … HL12) -HL12 /3 width=1 by cpxs_flat/
-| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
- elim (llpx_inv_bind_O … HL12) /3 width=3 by cpxs_zeta/
-| #G #L2 #V2 #T1 #T2 #HT12 #IHT12 #L1 #HL12
- elim (llpx_inv_flat … HL12) /3 width=1 by cpxs_tau/
-| #G #L2 #V1 #V2 #T2 #HV12 #IHV12 #L1 #HL12
- elim (llpx_inv_flat … HL12) /3 width=1 by cpxs_ti/
-| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12
- elim (llpx_inv_flat … HL12) -HL12 #HV1 #HL12
- elim (llpx_inv_bind_O … HL12) /3 width=3 by cpxs_beta/
-| #a #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12
- elim (llpx_inv_flat … HL12) -HL12 #HV1 #HL12
- elim (llpx_inv_bind_O … HL12) /3 width=3 by cpxs_theta/
+ elim (lpx_ldrop_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_ti, cpxs_tau/
+| /4 width=3 by cpxs_zeta, lpx_pair/
+| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/
]
qed-.
lemma cpx_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡[h, g] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-/4 width=9 by llpx_cpx_trans, cpxs_bind_dx, llpx_bind_repl_O/ qed.
+/4 width=5 by lpx_cpx_trans, cpxs_bind_dx, lpx_pair/ qed.
(* Advanced properties ******************************************************)
-lemma cpxs_llpx_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (llpx h g G 0).
-#h #g #G @s_r_trans_LTC1 /2 width=3 by llpx_cpx_trans, llpx_cpx_conf/ (**) (* full auto fails here but works in cprs_cprs *)
+lemma lpx_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (λ_.lpx h g G).
+#h #g #G @s_r_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *)
qed-.
lemma cpxs_bind2_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-/4 width=9 by cpxs_llpx_trans, cpxs_bind_dx, llpx_bind_repl_O/ qed.
+/4 width=5 by lpx_cpxs_trans, cpxs_bind_dx, lpx_pair/ qed.
(* Properties on supclosure *************************************************)
include "basic_2/substitution/fqus_fqus.ma".
include "basic_2/unfold/lsstas_lift.ma".
-include "basic_2/reduction/llpx_ldrop.ma".
+include "basic_2/reduction/cpx_lift.ma".
include "basic_2/computation/cpxs.ma".
(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
]
qed.
-lemma cpxs_llpx_conf: ∀h,g,G. s_r_confluent1 … (cpxs h g G) (llpx h g G 0).
-/3 width=5 by llpx_cpx_conf, s_r_conf1_LTC1/ qed-.
-
(* Advanced inversion lemmas ************************************************)
lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 →
(**************************************************************************)
include "basic_2/computation/fpbs.ma".
+include "basic_2/computation/csx_lift.ma". (* added *)
include "basic_2/computation/csx_llpx.ma".
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
(* *)
(**************************************************************************)
-include "basic_2/grammar/tstc_tstc.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/cpxs_llpx.ma".
include "basic_2/computation/csx_alt.ma".
-include "basic_2/computation/csx_lift.ma".
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-(* Advanced properties ******************************************************)
+(* Properties on lazy sn extended reduction for local environments **********)
lemma csx_llpx_conf: ∀h,g,G,L1,T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T →
∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T, 0] L2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
#h #g #G #L1 #T #H @(csx_ind_alt … H) -T
-/5 width=3 by csx_intro_cpxs, cpxs_llpx_trans, cpxs_llpx_conf/ (* 2 cpxs_llpx_trans *)
+/5 width=3 by csx_intro_cpxs, llpx_cpxs_trans, cpxs_llpx_conf/ (* 2 cpxs_llpx_trans *)
qed-.
-
-lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
- ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T.
-#h #g #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abst1 … H1) -H1
-#W0 #T0 #HLW0 #HLT0 #H destruct
-elim (eq_false_inv_tpair_sn … H2) -H2
-[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT
- #HT0 lapply (csx_llpx_conf … HT0 (L.ⓛW0)) -HT0
- /4 width=4 by llpx_bind_repl_O/
-| -IHW -HLW0 -HT * #H destruct /3 width=1 by/
-]
-qed.
-
-lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V →
- ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T.
-#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abbr1 … H1) -H1 *
-[ #V1 #T1 #HLV1 #HLT1 #H destruct
- elim (eq_false_inv_tpair_sn … H2) -H2
- [ /4 width=9 by csx_cpx_trans, csx_llpx_conf, llpx_bind_repl_O/
- | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/
- ]
-| -IHV -IHT -H2
- /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/
-]
-qed.
-
-fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 →
- ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1.
-#h #g #a #G #L #X #H @(csx_ind … H) -X
-#X #HT1 #IHT1 #V #W #T1 #H1 destruct
-@csx_intro #X #H1 #H2
-elim (cpx_inv_appl1 … H1) -H1 *
-[ -HT1 #V0 #Y #HLV0 #H #H0 destruct
- elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
- @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2
- lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/
-| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
- lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02
- /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/
-| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-(* Basic_1: was just: sn3_beta *)
-lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T.
-/2 width=3 by csx_appl_beta_aux/ qed.
-
-fact csx_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
-#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
-lapply (csx_fwd_pair_sn … HVT) #HV
-lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1 … HL) -HL *
-[ -HV #V0 #Y #HLV10 #HL #H0 destruct
- elim (cpx_inv_abbr1 … HL) -HL *
- [ #V3 #T3 #HV3 #HLT3 #H0 destruct
- elim (lift_total V0 0 1) #V4 #HV04
- elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
- [ -IHVT #H0 destruct
- elim (eq_false_inv_tpair_sn … H) -H
- [ -HLV10 -HV3 -HLT3 -HVT
- >(lift_inj … HV12 … HV04) -V4
- #H elim H //
- | * #_ #H elim H //
- ]
- | -H -HVT #H
- lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_drop/ #HV24
- @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/
- ]
- | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
- lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0
- lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0
- /3 width=5 by csx_cpx_trans, cpx_pair_sn, ldrop_drop, lift_flat/
- ]
-| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
-| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
- lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23
- @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
- @(csx_llpx_conf … (L.ⓓW0)) /2 width=4 by llpx_bind_repl_O/ -W1
- /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
-]
-qed-.
-
-lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
-/2 width=5 by csx_appl_theta_aux/ qed.
-
-(* Basic_1: was just: sn3_appl_appl *)
-lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
- (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
- 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.
-#h #g #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 (eq_false_inv_tpair_sn … 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 -HLV0 * #H #H1T10 destruct
- elim (tstc_dec T1 T0) #H2T10
- [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_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/grammar/tstc_tstc.ma".
+include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/csx_alt.ma".
+include "basic_2/computation/csx_lift.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
+
+(* Advanced properties ******************************************************)
+
+lemma csx_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+ ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T
+/4 width=3 by csx_intro, lpx_cpx_trans/
+qed-.
+
+lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
+ ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T.
+#h #g #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT
+@csx_intro #X #H1 #H2
+elim (cpx_inv_abst1 … H1) -H1
+#W0 #T0 #HLW0 #HLT0 #H destruct
+elim (eq_false_inv_tpair_sn … H2) -H2
+[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT
+ #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /3 width=1 by lpx_pair/
+| -IHW -HLW0 -HT * #H destruct /3 width=1 by/
+]
+qed.
+
+lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V →
+ ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T.
+#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT
+@csx_intro #X #H1 #H2
+elim (cpx_inv_abbr1 … H1) -H1 *
+[ #V1 #T1 #HLV1 #HLT1 #H destruct
+ elim (eq_false_inv_tpair_sn … H2) -H2
+ [ /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/
+ | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/
+ ]
+| -IHV -IHT -H2
+ /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/
+]
+qed.
+
+fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 →
+ ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1.
+#h #g #a #G #L #X #H @(csx_ind … H) -X
+#X #HT1 #IHT1 #V #W #T1 #H1 destruct
+@csx_intro #X #H1 #H2
+elim (cpx_inv_appl1 … H1) -H1 *
+[ -HT1 #V0 #Y #HLV0 #H #H0 destruct
+ elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
+ @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2
+ lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/
+| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
+ lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02
+ /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/
+| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_1: was just: sn3_beta *)
+lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T.
+/2 width=3 by csx_appl_beta_aux/ qed.
+
+fact csx_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
+ ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
+#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
+lapply (csx_fwd_pair_sn … HVT) #HV
+lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
+@csx_intro #X #HL #H
+elim (cpx_inv_appl1 … HL) -HL *
+[ -HV #V0 #Y #HLV10 #HL #H0 destruct
+ elim (cpx_inv_abbr1 … HL) -HL *
+ [ #V3 #T3 #HV3 #HLT3 #H0 destruct
+ elim (lift_total V0 0 1) #V4 #HV04
+ elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
+ [ -IHVT #H0 destruct
+ elim (eq_false_inv_tpair_sn … H) -H
+ [ -HLV10 -HV3 -HLT3 -HVT
+ >(lift_inj … HV12 … HV04) -V4
+ #H elim H //
+ | * #_ #H elim H //
+ ]
+ | -H -HVT #H
+ lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_drop/ #HV24
+ @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/
+ ]
+ | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
+ lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0
+ lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0
+ /3 width=5 by csx_cpx_trans, cpx_pair_sn, ldrop_drop, lift_flat/
+ ]
+| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
+| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
+ lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23
+ @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
+ @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1
+ /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
+]
+qed-.
+
+lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
+ ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
+/2 width=5 by csx_appl_theta_aux/ qed.
+
+(* Basic_1: was just: sn3_appl_appl *)
+lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
+ (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
+ 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.
+#h #g #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 (eq_false_inv_tpair_sn … 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 -HLV0 * #H #H1T10 destruct
+ elim (tstc_dec T1 T0) #H2T10
+ [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_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/computation/csx_lpx.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
+
+(* Properties on sn extended parallel computation for local environments ****)
+
+lemma csx_lpxs_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L1 #L2 #H @(lpxs_ind … H) -L2 /3 by lpxs_strap1, csx_lpx_conf/
+qed-.
include "basic_2/computation/acp_cr.ma".
include "basic_2/computation/cpxs_tstc_vector.ma".
-include "basic_2/computation/csx_llpx.ma".
+include "basic_2/computation/csx_lpx.ma".
include "basic_2/computation/csx_vector.ma".
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************)
[ elim (fquq_cpxs_trans … HT0 … HG1) -T
/3 width=7 by fqus_strap2, ex3_2_intro/
| /3 width=5 by cpxs_strap2, ex3_2_intro/
-| lapply (cpxs_llpx_trans … HT0 … HL1) -HT0 #HT10
+| lapply (llpx_cpxs_trans … HT0 … HL1) -HT0 #HT10
lapply (cpxs_llpx_conf … HT10 … HL1) -HL1 #HL1
elim (llpx_fqus_trans … HG2 … HL1) -L
/3 width=7 by llpxs_strap2, cpxs_trans, ex3_2_intro/
(* *)
(**************************************************************************)
+include "basic_2/reduction/fpb_lift.ma".
include "basic_2/computation/cpxs_lift.ma".
include "basic_2/computation/fpbs.ma".
∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
/3 width=5 by cpxs_fpbs, lsstas_cpxs/ qed.
-(* Note: this should be moved *)
lemma ssta_fpbs: ∀h,g,G,L,T,U,l.
⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U →
⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄.
-/3 width=5 by lsstas_fpbs, ssta_lsstas/ qed.
+/4 width=2 by fpb_fpbs, ssta_fpb/ qed.
(**************************************************************************)
include "basic_2/relocation/llpx_sn_tc.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/cpxs_llpx.ma".
include "basic_2/computation/llpxs.ma".
(* LAZY SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS **************)
(* Properties on context-sensitive extended parallel computation for terms **)
lemma llpxs_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (llpxs h g G 0).
-/3 width=5 by s_r_trans_LTC2, cpxs_llpx_trans/ qed-.
+/3 width=5 by s_r_trans_LTC2, llpx_cpxs_trans/ qed-.
lemma llpxs_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (llpxs h g G 0).
#h #g #G @s_r_to_s_rs_trans @s_r_trans_LTC2
-/3 width=5 by cpxs_llpx_trans, s_rs_trans_TC1/ (**) (* full auto too slow *)
+/3 width=5 by llpx_cpxs_trans, s_rs_trans_TC1/ (**) (* full auto too slow *)
qed-.
(* Note: this is an instance of a general theorem *)
#h #g #G2 #L2 #T2 #U2 #HTU2 #L0 #H @(llpxs_ind_dx … H) -L0 //
#L0 #L #HL0 #HL2 #IHL2 @(llpxs_strap2 … IHL2) -IHL2
lapply (llpxs_cpxs_trans … HTU2 … HL2) -L2 #HTU2
-/3 width=3 by cpxs_llpx_trans, cpxs_llpx_conf/
+/3 width=3 by llpx_cpxs_trans, cpxs_llpx_conf/
qed-.
(* Note: this is an instance of a general theorem *)
#h #g #G2 #L2 #T2 #U2 #HTU2 #L0 #H @(llpxs_ind_dx … H) -L0 //
#L0 #L #HL0 #HL2 #IHL2 @(llpxs_strap2 … IHL2) -IHL2
lapply (llpxs_cpx_trans … HTU2 … HL2) -L2 #HTU2
-/3 width=3 by cpxs_llpx_trans, cpxs_llpx_conf/
+/3 width=3 by llpx_cpxs_trans, cpxs_llpx_conf/
qed-.
lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(llpxs_ind_dx … H) -K1
[ /2 width=5 by ex3_2_intro/
| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
- lapply (cpxs_llpx_trans … HT1 … HK1) -HT1 #HT1
+ lapply (llpx_cpxs_trans … HT1 … HK1) -HT1 #HT1
lapply (cpxs_llpx_conf … HT1 … HK1) -HK1 #HK1
elim (llpx_fquq_trans … HT2 … HK1) -K
/3 width=7 by llpxs_strap2, cpxs_strap1, ex3_2_intro/
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(llpxs_ind_dx … H) -K1
[ /2 width=5 by ex3_2_intro/
| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
- lapply (cpxs_llpx_trans … HT1 … HK1) -HT1 #HT1
+ lapply (llpx_cpxs_trans … HT1 … HK1) -HT1 #HT1
lapply (cpxs_llpx_conf … HT1 … HK1) -HK1 #HK1
elim (llpx_fqup_trans … HT2 … HK1) -K
/3 width=7 by llpxs_strap2, cpxs_trans, ex3_2_intro/
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(llpxs_ind_dx … H) -K1
[ /2 width=5 by ex3_2_intro/
| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
- lapply (cpxs_llpx_trans … HT1 … HK1) -HT1 #HT1
+ lapply (llpx_cpxs_trans … HT1 … HK1) -HT1 #HT1
lapply (cpxs_llpx_conf … HT1 … HK1) -HK1 #HK1
elim (llpx_fqus_trans … HT2 … HK1) -K
/3 width=7 by llpxs_strap2, cpxs_trans, ex3_2_intro/
(* *)
(**************************************************************************)
+include "basic_2/computation/csx_lift.ma". (* added *)
include "basic_2/computation/csx_llpxs.ma".
include "basic_2/computation/llsx_ldrop.ma".
include "basic_2/computation/llsx_llpx.ma".
--- /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/predsnstar_5.ma".
+include "basic_2/reduction/lpx.ma".
+include "basic_2/computation/lprs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+definition lpxs: ∀h. sd h → relation3 genv lenv lenv ≝
+ λh,g,G. TC … (lpx h g G).
+
+interpretation "extended parallel computation (local environment, sn variant)"
+ 'PRedSnStar h g G L1 L2 = (lpxs h g G L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma lpxs_ind: ∀h,g,G,L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → R L → R L2) →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L2.
+#h #g #G #L1 #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma lpxs_ind_dx: ∀h,g,G,L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → R L → R L1) →
+ ∀L1. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1.
+#h #g #G #L2 #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/3 width=3 by lpr_lpx, monotonic_TC/ qed.
+
+lemma lpx_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/2 width=1 by inj/ qed.
+
+lemma lpxs_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡*[h, g] L.
+/2 width=1 by lprs_lpxs/ qed.
+
+lemma lpxs_strap1: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/2 width=3 by step/ qed.
+
+lemma lpxs_strap2: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/2 width=3 by TC_strap/ qed.
+
+lemma lpxs_pair_refl: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V.
+/2 width=1 by TC_lpx_sn_pair_refl/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpxs_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡*[h, g] L2 → L2 = ⋆.
+/2 width=2 by TC_lpx_sn_inv_atom1/ qed-.
+
+lemma lpxs_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡*[h, g] ⋆ → L1 = ⋆.
+/2 width=2 by TC_lpx_sn_inv_atom2/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpxs_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → |L1| = |L2|.
+/2 width=2 by TC_lpx_sn_fwd_length/ 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/reduction/lpx_aaa.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_lpxs_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+#h #g #G #L1 #T #A #HT #L2 #HL12
+@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/
+qed-.
+
+lemma aaa_lprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/3 width=5 by lprs_lpxs, aaa_lpxs_conf/ 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/predsnstaralt_5.ma".
+include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* alternative definition *)
+definition lpxsa: ∀h. sd h → relation3 genv lenv lenv ≝
+ λh,g,G. lpx_sn … (cpxs h g G).
+
+interpretation "extended parallel computation (local environment, sn variant) alternative"
+ 'PRedSnStarAlt h g G L1 L2 = (lpxsa h g G L1 L2).
+
+(* Main properties on the alternative definition ****************************)
+
+theorem lpxsa_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
+
+(* Main inversion lemmas on the alternative definition **********************)
+
+theorem lpxs_inv_lpxsa: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2.
+/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpx_cpxs_trans/ qed-.
+
+(* Alternative eliminators **************************************************)
+
+lemma lpxs_ind_alt: ∀h,g,G. ∀R:relation lenv.
+ R (⋆) (⋆) → (
+ ∀I,K1,K2,V1,V2.
+ ⦃G, K1⦄ ⊢ ➡*[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 →
+ R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ ) →
+ ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1 L2.
+/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_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/cpxs_cpxs.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Advanced properties ******************************************************)
+
+lemma lpxs_pair: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡*[h, g] V2 →
+ ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
+/2 width=1 by TC_lpx_sn_pair/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lpxs_inv_pair1: ∀h,g,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L2 = K2.ⓑ{I}V2.
+/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-.
+
+lemma lpxs_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, g] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L1 = K1.ⓑ{I}V1.
+/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-.
+
+(* Properties on context-sensitive extended parallel computation for terms **)
+
+lemma lpxs_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (λ_.lpxs h g G).
+/3 width=5 by s_r_trans_LTC2, lpx_cpxs_trans/ qed-.
+
+(* Note: alternative proof: /3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ *)
+lemma lpxs_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (λ_.lpxs h g G).
+#h #g #G @s_r_to_s_rs_trans @s_r_trans_LTC2
+@s_rs_trans_TC1 /2 width=3 by lpx_cpxs_trans/ (**) (* full auto too slow *)
+qed-.
+
+lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
+ ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
+/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed.
+
+(* Inversion lemmas on context-sensitive ext parallel computation for terms *)
+
+lemma cpxs_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, g] U2 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[h, g] T2 &
+ U2 = ⓛ{a}V2.T2.
+#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/
+#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
+elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
+lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?)
+/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/
+qed-.
+
+lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, g] U2 → (
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 &
+ U2 = ⓓ{a}V2.T2
+ ) ∨
+ ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
+#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
+#U0 #U2 #_ #HU02 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpx_inv_abbr1 … HU02) -HU02 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct
+ lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?)
+ /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/
+ | #T2 #HT02 #HUT2
+ lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02
+ /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/
+ ]
+| #U1 #HTU1 #HU01
+ elim (lift_total U2 0 1) #U #HU2
+ /6 width=12 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/
+]
+qed-.
+
+(* More advanced properties *************************************************)
+
+lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
+/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.
+
+(* Properties on supclosure *************************************************)
+
+lemma lpx_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1
+ /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+ #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L
+ #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
+ /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T
+/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/
+qed-.
+
+lemma lpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
+[ /2 width=5 by ex3_2_intro/
+| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
+ lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
+ elim (lpx_fquq_trans … HT2 … HK1) -K
+ /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/
+]
+qed-.
+
+lemma lpxs_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
+[ /2 width=5 by ex3_2_intro/
+| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
+ lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
+ elim (lpx_fqup_trans … HT2 … HK1) -K
+ /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
+]
+qed-.
+
+lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T
+/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_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/reduction/lpx_ldrop.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpxs_ldrop_conf: ∀h,g,G. dropable_sn (lpxs h g G).
+/3 width=3 by dropable_sn_TC, lpx_ldrop_conf/ qed-.
+
+lemma ldrop_lpxs_trans: ∀h,g,G. dedropable_sn (lpxs h g G).
+/3 width=3 by dedropable_sn_TC, ldrop_lpx_trans/ qed-.
+
+lemma lpxs_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpxs h g G).
+/3 width=3 by dropable_dx_TC, lpx_ldrop_trans_O1/ 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/substitution/lleq_leq.ma".
+include "basic_2/reduction/lpx_lleq.ma".
+include "basic_2/computation/cpxs_leq.ma".
+include "basic_2/computation/lpxs_ldrop.ma".
+include "basic_2/computation/lpxs_cpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 →
+ ∀L1,T,d. L1 ⋕[T, d] L2 →
+ ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2.
+#h #g #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/
+#K #K2 #_ #HK2 #IH #L1 #T #d #HT elim (IH … HT) -L2
+#L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K
+/3 width=3 by lpxs_strap1, ex2_intro/
+qed-.
+
+lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1
+ #K0 #V0 #H1KL1 #_ #H destruct
+ elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
+ #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
+ /2 width=4 by fqu_lref_O, ex3_intro/
+| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
+ [ elim (lleq_inv_bind … H)
+ | elim (lleq_inv_flat … H)
+ ] -H /2 width=4 by fqu_pair_sn, ex3_intro/
+| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H
+ /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/
+| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
+ /2 width=4 by fqu_flat_dx, ex3_intro/
+| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
+ elim (ldrop_O1_le (e+1) K1)
+ [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
+ #H2KL elim (lpxs_ldrop_trans_O1 … H1KL1 … HL1) -L1
+ #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct
+ /3 width=4 by fqu_drop, ex3_intro/
+ | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g
+ lapply (lleq_fwd_length … H2KL1) //
+ ]
+]
+qed-.
+
+lemma lpxs_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
+elim (fquq_inv_gen … H) -H
+[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
+ /3 width=4 by fqu_fquq, ex3_intro/
+| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
+]
+qed-.
+
+lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
+ /3 width=4 by fqu_fqup, ex3_intro/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1
+ #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L
+ /3 width=5 by fqup_strap1, ex3_intro/
+]
+qed-.
+
+lemma lpxs_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
+elim (fqus_inv_gen … H) -H
+[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
+ /3 width=4 by fqup_fqus, ex3_intro/
+| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
+]
+qed-.
+
+fact leq_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ≃[d, e] L0 → e = ∞ →
+ ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 →
+ ∃∃L. L ≃[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L &
+ (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
+#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e
+[ #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H
+ /3 width=5 by ex3_intro, conj/
+| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct
+| #I #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H
+ elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
+ lapply (ysucc_inv_Y_dx … He) -He #He
+ elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
+ @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, leq_cpxs_trans, leq_pair/
+ #T elim (IH T) #HL0dx #HL0sn
+ @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_pair_O_Y/
+| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H
+ elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
+ elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
+ @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, leq_succ/
+ #T elim (IH T) #HL0dx #HL0sn
+ @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_succ/
+]
+qed-.
+
+lemma leq_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ≃[d, ∞] L0 →
+ ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 →
+ ∃∃L. L ≃[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L &
+ (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
+/2 width=1 by leq_lpxs_trans_lleq_aux/ 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".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Main properties **********************************************************)
+
+theorem lpxs_trans: ∀h,g,G. Transitive … (lpxs h g G).
+/2 width=3 by trans_TC/ 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/grammar/tstc_tstc.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
-include "basic_2/computation/csx_alt.ma".
-include "basic_2/computation/csx_lift.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-
-(* Advanced properties ******************************************************)
-
-lemma csx_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
- ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T
-/4 width=3 by csx_intro, lpx_cpx_trans/
-qed-.
-
-lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
- ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T.
-#h #g #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abst1 … H1) -H1
-#W0 #T0 #HLW0 #HLT0 #H destruct
-elim (eq_false_inv_tpair_sn … H2) -H2
-[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT
- #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /3 width=1 by lpx_pair/
-| -IHW -HLW0 -HT * #H destruct /3 width=1 by/
-]
-qed.
-
-lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V →
- ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T.
-#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abbr1 … H1) -H1 *
-[ #V1 #T1 #HLV1 #HLT1 #H destruct
- elim (eq_false_inv_tpair_sn … H2) -H2
- [ /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/
- | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/
- ]
-| -IHV -IHT -H2
- /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/
-]
-qed.
-
-fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 →
- ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1.
-#h #g #a #G #L #X #H @(csx_ind … H) -X
-#X #HT1 #IHT1 #V #W #T1 #H1 destruct
-@csx_intro #X #H1 #H2
-elim (cpx_inv_appl1 … H1) -H1 *
-[ -HT1 #V0 #Y #HLV0 #H #H0 destruct
- elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
- @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2
- lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/
-| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
- lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02
- /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/
-| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-(* Basic_1: was just: sn3_beta *)
-lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T.
-/2 width=3 by csx_appl_beta_aux/ qed.
-
-fact csx_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
-#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
-lapply (csx_fwd_pair_sn … HVT) #HV
-lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1 … HL) -HL *
-[ -HV #V0 #Y #HLV10 #HL #H0 destruct
- elim (cpx_inv_abbr1 … HL) -HL *
- [ #V3 #T3 #HV3 #HLT3 #H0 destruct
- elim (lift_total V0 0 1) #V4 #HV04
- elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
- [ -IHVT #H0 destruct
- elim (eq_false_inv_tpair_sn … H) -H
- [ -HLV10 -HV3 -HLT3 -HVT
- >(lift_inj … HV12 … HV04) -V4
- #H elim H //
- | * #_ #H elim H //
- ]
- | -H -HVT #H
- lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_drop/ #HV24
- @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/
- ]
- | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
- lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0
- lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0
- /3 width=5 by csx_cpx_trans, cpx_pair_sn, ldrop_drop, lift_flat/
- ]
-| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
-| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
- lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23
- @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
- @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1
- /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
-]
-qed-.
-
-lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
-/2 width=5 by csx_appl_theta_aux/ qed.
-
-(* Basic_1: was just: sn3_appl_appl *)
-lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
- (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
- 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.
-#h #g #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 (eq_false_inv_tpair_sn … 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 -HLV0 * #H #H1T10 destruct
- elim (tstc_dec T1 T0) #H2T10
- [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_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/computation/csx_lpx.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-
-(* Properties on sn extended parallel computation for local environments ****)
-
-lemma csx_lpxs_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
- ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L1 #L2 #H @(lpxs_ind … H) -L2 /3 by lpxs_strap1, csx_lpx_conf/
-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 d ] break term 46 L )"
- non associative with precedence 45
- for @{ 'LazyCoSN $h $g $d $G $L }.
+++ /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/predsn_5.ma".
-include "basic_2/reduction/lpr.ma".
-include "basic_2/reduction/cpx.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝
- λh,g,G. lpx_sn (cpx h g G).
-
-interpretation "extended parallel reduction (local environment, sn variant)"
- 'PRedSn h g G L1 L2 = (lpx h g G L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lpx_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡[h, g] L2 → L2 = ⋆.
-/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
-
-lemma lpx_inv_pair1: ∀h,g,I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] L2 →
- ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 &
- L2 = K2. ⓑ{I} V2.
-/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
-
-lemma lpx_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡[h, g] ⋆ → L1 = ⋆.
-/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
-
-lemma lpx_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 &
- L1 = K1. ⓑ{I} V1.
-/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
-
-lemma lpx_inv_pair: ∀h,g,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ➡[h, g] L2.ⓑ{I2}V2 →
- ∧∧ ⦃G, L1⦄ ⊢ ➡[h, g] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h, g] V2 & I1 = I2.
-/2 width=1 by lpx_sn_inv_pair/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lpx_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡[h, g] L.
-/2 width=1 by lpx_sn_refl/ qed.
-
-lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 →
- ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2.
-/2 width=1 by lpx_sn_pair/ qed.
-
-lemma lpr_lpx: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g] L2.
-#h #g #G #L1 #L2 #H elim H -L1 -L2 /3 width=1 by lpx_pair, cpr_cpx/
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lpx_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|.
-/2 width=2 by lpx_sn_fwd_length/ 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/aaa_lift.ma".
-include "basic_2/static/lsuba_aaa.ma".
-include "basic_2/reduction/lpx_ldrop.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties on atomic arity assignment for terms **************************)
-
-(* Note: lemma 500 *)
-lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
-#h #g #G #L1 #T1 #A #H elim H -G -L1 -T1 -A
-[ #g #L1 #k #X #H
- elim (cpx_inv_sort1 … H) -H // * //
-| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12
- elim (cpx_inv_lref1 … H) -H
- [ #H destruct
- elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
- elim (lpx_inv_pair1 … H) -H
- #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/
- | * #J #Y #Z #V2 #H #HV12 #HV2
- lapply (ldrop_mono … H … HLK1) -H #H destruct
- elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
- elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
- /3 width=8 by aaa_lift, ldrop_fwd_drop2/
- ]
-| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpx_inv_abbr1 … H) -H *
- [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/
- | #T2 #HT12 #HT2 #H destruct -IHV1
- /4 width=8 by lpx_pair, aaa_inv_lift, ldrop_drop/
- ]
-| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=1 by lpx_pair, aaa_abst/
-| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpx_inv_appl1 … H) -H *
- [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/
- | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
- lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
- lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
- elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
- /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/
- | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
- lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2
- lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
- elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/
- ]
-| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpx_inv_cast1 … H) -H
- [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/
- | -IHV1 /2 width=1 by/
- | -IHT1 /2 width=1 by/
- ]
-]
-qed-.
-
-lemma aaa_cpx_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-/2 width=7 by aaa_cpx_lpx_conf/ qed-.
-
-lemma aaa_lpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-/2 width=7 by aaa_cpx_lpx_conf/ qed-.
-
-lemma aaa_cpr_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-.
-
-lemma aaa_lpr_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-/3 width=5 by aaa_lpx_conf, lpr_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/relocation/ldrop_lpx_sn.ma".
-include "basic_2/reduction/cpx_lift.ma".
-include "basic_2/reduction/lpx.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properies on local environment slicing ***********************************)
-
-lemma lpx_ldrop_conf: ∀h,g,G. dropable_sn (lpx h g G).
-/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
-
-lemma ldrop_lpx_trans: ∀h,g,G. dedropable_sn (lpx h g G).
-/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
-
-lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G).
-/2 width=3 by lpx_sn_dropable/ qed-.
-
-(* Properties on supclosure *************************************************)
-
-lemma fqu_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/
-[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H
- #K2 #W2 #HLK2 #HVW2 #H destruct
- /3 width=5 by fqu_fquq, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
- elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
- /3 width=7 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma fquq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/
-[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
- #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
- /4 width=7 by cpx_delta, fqu_drop, ldrop_drop, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
- elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1
- /3 width=5 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_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/relocation/lleq_ldrop.ma".
-include "basic_2/reduction/lpx_ldrop.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties on lazy equivalence for local environments ********************)
-(*
-lamma pippo: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → ∀L1. |L1| = |L2| →
- ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & |K1| = |K2| &
- (∀T,d. L1 ⋕[T, d] L2 ↔ K1 ⋕[T, d] K2).
-#h #g #G #L2 #K2 #H elim H -L2 -K2
-[ #L1 #H >(length_inv_zero_dx … H) -L1 /3 width=5 by ex3_intro, conj/
-| #I2 #L2 #K2 #V2 #W2 #_ #HVW2 #IHLK2 #Y #H
- elim (length_inv_pos_dx … H) -H #I #L1 #V1 #HL12 #H destruct
- elim (IHLK2 … HL12) -IHLK2 #K1 #HLK1 #HK12 #IH
- elim (eq_term_dec V1 V2) #H destruct
- [ @(ex3_intro … (K1.ⓑ{I}W2)) normalize /2 width=1 by /
-*)
-axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 →
- ∀L1,T,d. L1 ⋕[T, d] L2 →
- ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2.
-(*
-#h #g #G #L2 #K2 #H elim H -L2 -K2
-[ #L1 #T #d #H lapply (lleq_fwd_length … H) -H
- #H >(length_inv_zero_dx … H) -L1 /2 width=3 by ex2_intro/
-| #I2 #L2 #K2 #V2 #W2 #HLK2 #HVW2 #IHLK2 #Y #T #d #HT
- lapply (lleq_fwd_length … HT) #H
- elim (length_inv_pos_dx … H) -H #I1 #L1 #V1 #HL12 #H destruct
- elim (eq_term_dec V1 V2) #H destruct
- [ @ex2_intro …
-*)
-
-lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1
- #K0 #V0 #H1KL1 #_ #H destruct
- elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
- #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
- /2 width=4 by fqu_lref_O, ex3_intro/
-| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
- [ elim (lleq_inv_bind … H)
- | elim (lleq_inv_flat … H)
- ] -H /2 width=4 by fqu_pair_sn, ex3_intro/
-| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H
- /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/
-| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
- /2 width=4 by fqu_flat_dx, ex3_intro/
-| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
- elim (ldrop_O1_le (e+1) K1)
- [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
- #H2KL elim (lpx_ldrop_trans_O1 … H1KL1 … HL1) -L1
- #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct
- /3 width=4 by fqu_drop, ex3_intro/
- | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g
- lapply (lleq_fwd_length … H2KL1) //
- ]
-]
-qed-.
-
-lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
-elim (fquq_inv_gen … H) -H
-[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
- /3 width=4 by fqu_fquq, ex3_intro/
-| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
-]
-qed-.
-
-lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
- /3 width=4 by fqu_fqup, ex3_intro/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1
- #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L
- /3 width=5 by fqup_strap1, ex3_intro/
-]
-qed-.
-
-lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
-elim (fqus_inv_gen … H) -H
-[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
- /3 width=4 by fqup_fqus, ex3_intro/
-| * #HG #HL #HT destruct /2 width=4 by 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 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/predsnstar_5.ma".
-include "basic_2/reduction/lpx.ma".
-include "basic_2/computation/lprs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-definition lpxs: ∀h. sd h → relation3 genv lenv lenv ≝
- λh,g,G. TC … (lpx h g G).
-
-interpretation "extended parallel computation (local environment, sn variant)"
- 'PRedSnStar h g G L1 L2 = (lpxs h g G L1 L2).
-
-(* Basic eliminators ********************************************************)
-
-lemma lpxs_ind: ∀h,g,G,L1. ∀R:predicate lenv. R L1 →
- (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → R L → R L2) →
- ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L2.
-#h #g #G #L1 #R #HL1 #IHL1 #L2 #HL12
-@(TC_star_ind … HL1 IHL1 … HL12) //
-qed-.
-
-lemma lpxs_ind_dx: ∀h,g,G,L2. ∀R:predicate lenv. R L2 →
- (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → R L → R L1) →
- ∀L1. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1.
-#h #g #G #L2 #R #HL2 #IHL2 #L1 #HL12
-@(TC_star_ind_dx … HL2 IHL2 … HL12) //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/3 width=3/ qed.
-
-lemma lpx_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/2 width=1/ qed.
-
-lemma lpxs_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡*[h, g] L.
-/2 width=1/ qed.
-
-lemma lpxs_strap1: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/2 width=3/ qed.
-
-lemma lpxs_strap2: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/2 width=3/ qed.
-
-lemma lpxs_pair_refl: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V.
-/2 width=1 by TC_lpx_sn_pair_refl/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lpxs_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡*[h, g] L2 → L2 = ⋆.
-/2 width=2 by TC_lpx_sn_inv_atom1/ qed-.
-
-lemma lpxs_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡*[h, g] ⋆ → L1 = ⋆.
-/2 width=2 by TC_lpx_sn_inv_atom2/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lpxs_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → |L1| = |L2|.
-/2 width=2 by TC_lpx_sn_fwd_length/ 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/reduction/lpx_aaa.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* Properties about atomic arity assignment on terms ************************)
-
-lemma aaa_lpxs_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
- ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-#h #g #G #L1 #T #A #HT #L2 #HL12
-@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/
-qed-.
-
-lemma aaa_lprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
- ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-#G #L1 #T #A #HT #L2 #HL12
-@(aaa_lpxs_conf … HT) -A -T /2 width=3/
-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/predsnstaralt_5.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* alternative definition *)
-definition lpxsa: ∀h. sd h → relation3 genv lenv lenv ≝
- λh,g,G. lpx_sn … (cpxs h g G).
-
-interpretation "extended parallel computation (local environment, sn variant) alternative"
- 'PRedSnStarAlt h g G L1 L2 = (lpxsa h g G L1 L2).
-
-(* Main properties on the alternative definition ****************************)
-
-theorem lpxsa_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
-
-(* Main inversion lemmas on the alternative definition **********************)
-
-theorem lpxs_inv_lpxsa: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2.
-/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpx_cpxs_trans/ qed-.
-
-(* Alternative eliminators **************************************************)
-
-lemma lpxs_ind_alt: ∀h,g,G. ∀R:relation lenv.
- R (⋆) (⋆) → (
- ∀I,K1,K2,V1,V2.
- ⦃G, K1⦄ ⊢ ➡*[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 →
- R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
- ) →
- ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1 L2.
-/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_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/cpxs_cpxs.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* Advanced properties ******************************************************)
-
-lemma lpxs_pair: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
- ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡*[h, g] V2 →
- ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
-/2 width=1 by TC_lpx_sn_pair/ qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma lpxs_inv_pair1: ∀h,g,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2 →
- ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L2 = K2.ⓑ{I}V2.
-/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-.
-
-lemma lpxs_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, g] K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L1 = K1.ⓑ{I}V1.
-/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-.
-
-(* Properties on context-sensitive extended parallel computation for terms **)
-
-lemma lpxs_cpx_trans: ∀h,g,G. s_r_trans … (cpx h g G) (lpxs h g G).
-/3 width=5 by s_r_trans_TC2, lpx_cpxs_trans/ qed-.
-
-lemma lpxs_cpxs_trans: ∀h,g,G. s_rs_trans … (cpx h g G) (lpxs h g G).
-/3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ qed-.
-
-lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
- ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
- ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed.
-
-(* Inversion lemmas on context-sensitive ext parallel computation for terms *)
-
-lemma cpxs_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, g] U2 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[h, g] T2 &
- U2 = ⓛ{a}V2.T2.
-#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/
-#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
-elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
-lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?)
-/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/
-qed-.
-
-lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, g] U2 → (
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 &
- U2 = ⓓ{a}V2.T2
- ) ∨
- ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
-#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
-#U0 #U2 #_ #HU02 * *
-[ #V0 #T0 #HV10 #HT10 #H destruct
- elim (cpx_inv_abbr1 … HU02) -HU02 *
- [ #V2 #T2 #HV02 #HT02 #H destruct
- lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?)
- /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/
- | #T2 #HT02 #HUT2
- lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02
- /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/
- ]
-| #U1 #HTU1 #HU01
- elim (lift_total U2 0 1) #U #HU2
- /6 width=12 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/
-]
-qed-.
-
-(* More advanced properties *************************************************)
-
-lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
- ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
-/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.
-
-(* Properties on supclosure *************************************************)
-
-lemma lpx_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1
- /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
-| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
- #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L
- #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
- /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
-#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
-#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T
-/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/
-qed-.
-
-lemma lpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
-[ /2 width=5 by ex3_2_intro/
-| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
- lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
- elim (lpx_fquq_trans … HT2 … HK1) -K
- /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/
-]
-qed-.
-
-lemma lpxs_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
-[ /2 width=5 by ex3_2_intro/
-| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
- lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
- elim (lpx_fqup_trans … HT2 … HK1) -K
- /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
-]
-qed-.
-
-lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
-#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
-#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T
-/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_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/reduction/lpx_ldrop.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* Properies on local environment slicing ***********************************)
-
-lemma lpxs_ldrop_conf: ∀h,g,G. dropable_sn (lpxs h g G).
-/3 width=3 by dropable_sn_TC, lpx_ldrop_conf/ qed-.
-
-lemma ldrop_lpxs_trans: ∀h,g,G. dedropable_sn (lpxs h g G).
-/3 width=3 by dedropable_sn_TC, ldrop_lpx_trans/ qed-.
-
-lemma lpxs_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpxs h g G).
-/3 width=3 by dropable_dx_TC, lpx_ldrop_trans_O1/ 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_leq.ma".
-include "basic_2/reduction/lpx_lleq.ma".
-include "basic_2/computation/cpxs_leq.ma".
-include "basic_2/computation/lpxs_ldrop.ma".
-include "basic_2/computation/lpxs_cpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 →
- ∀L1,T,d. L1 ⋕[T, d] L2 →
- ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2.
-#h #g #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/
-#K #K2 #_ #HK2 #IH #L1 #T #d #HT elim (IH … HT) -L2
-#L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K
-/3 width=3 by lpxs_strap1, ex2_intro/
-qed-.
-
-lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1
- #K0 #V0 #H1KL1 #_ #H destruct
- elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
- #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
- /2 width=4 by fqu_lref_O, ex3_intro/
-| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
- [ elim (lleq_inv_bind … H)
- | elim (lleq_inv_flat … H)
- ] -H /2 width=4 by fqu_pair_sn, ex3_intro/
-| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H
- /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/
-| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
- /2 width=4 by fqu_flat_dx, ex3_intro/
-| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
- elim (ldrop_O1_le (e+1) K1)
- [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
- #H2KL elim (lpxs_ldrop_trans_O1 … H1KL1 … HL1) -L1
- #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct
- /3 width=4 by fqu_drop, ex3_intro/
- | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g
- lapply (lleq_fwd_length … H2KL1) //
- ]
-]
-qed-.
-
-lemma lpxs_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
-elim (fquq_inv_gen … H) -H
-[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
- /3 width=4 by fqu_fquq, ex3_intro/
-| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
-]
-qed-.
-
-lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
- /3 width=4 by fqu_fqup, ex3_intro/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1
- #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L
- /3 width=5 by fqup_strap1, ex3_intro/
-]
-qed-.
-
-lemma lpxs_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
-elim (fqus_inv_gen … H) -H
-[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
- /3 width=4 by fqup_fqus, ex3_intro/
-| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
-]
-qed-.
-
-fact leq_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ≃[d, e] L0 → e = ∞ →
- ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 →
- ∃∃L. L ≃[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L &
- (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
-#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e
-[ #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H
- /3 width=5 by ex3_intro, conj/
-| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct
-| #I #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H
- elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
- lapply (ysucc_inv_Y_dx … He) -He #He
- elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
- @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, leq_cpxs_trans, leq_pair/
- #T elim (IH T) #HL0dx #HL0sn
- @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_pair_O_Y/
-| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H
- elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
- elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
- @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, leq_succ/
- #T elim (IH T) #HL0dx #HL0sn
- @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_succ/
-]
-qed-.
-
-lemma leq_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ≃[d, ∞] L0 →
- ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 →
- ∃∃L. L ≃[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L &
- (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
-/2 width=1 by leq_lpxs_trans_lleq_aux/ 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".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* Main properties **********************************************************)
-
-theorem lpxs_trans: ∀h,g,G. Transitive … (lpxs h g G).
-/2 width=3/ 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 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PRedSn $h $g $G $L1 $L2 }.
+++ /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 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PRedSnStar $h $g $G $L1 $L2 }.
+++ /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 G, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PRedSnStarAlt $h $g $G $L1 $L2 }.
--- /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 d ] break term 46 L )"
+ non associative with precedence 45
+ for @{ 'LazyCoSN $h $g $d $G $L }.
--- /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 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedSn $h $g $G $L1 $L2 }.
--- /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 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedSnStar $h $g $G $L1 $L2 }.
--- /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 G, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedSnStarAlt $h $g $G $L1 $L2 }.
--- /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/predsn_5.ma".
+include "basic_2/reduction/lpr.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝
+ λh,g,G. lpx_sn (cpx h g G).
+
+interpretation "extended parallel reduction (local environment, sn variant)"
+ 'PRedSn h g G L1 L2 = (lpx h g G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpx_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡[h, g] L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+lemma lpx_inv_pair1: ∀h,g,I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 &
+ L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+lemma lpx_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡[h, g] ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpx_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 &
+ L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+lemma lpx_inv_pair: ∀h,g,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ➡[h, g] L2.ⓑ{I2}V2 →
+ ∧∧ ⦃G, L1⦄ ⊢ ➡[h, g] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h, g] V2 & I1 = I2.
+/2 width=1 by lpx_sn_inv_pair/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡[h, g] L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 →
+ ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2.
+/2 width=1 by lpx_sn_pair/ qed.
+
+lemma lpr_lpx: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g] L2.
+#h #g #G #L1 #L2 #H elim H -L1 -L2 /3 width=1 by lpx_pair, cpr_cpx/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ 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/aaa_lift.ma".
+include "basic_2/static/lsuba_aaa.ma".
+include "basic_2/reduction/lpx_ldrop.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+(* Properties on atomic arity assignment for terms **************************)
+
+(* Note: lemma 500 *)
+lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+#h #g #G #L1 #T1 #A #H elim H -G -L1 -T1 -A
+[ #g #L1 #k #X #H
+ elim (cpx_inv_sort1 … H) -H // * //
+| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12
+ elim (cpx_inv_lref1 … H) -H
+ [ #H destruct
+ elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
+ elim (lpx_inv_pair1 … H) -H
+ #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/
+ | * #J #Y #Z #V2 #H #HV12 #HV2
+ lapply (ldrop_mono … H … HLK1) -H #H destruct
+ elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
+ elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
+ /3 width=8 by aaa_lift, ldrop_fwd_drop2/
+ ]
+| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+ elim (cpx_inv_abbr1 … H) -H *
+ [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/
+ | #T2 #HT12 #HT2 #H destruct -IHV1
+ /4 width=8 by lpx_pair, aaa_inv_lift, ldrop_drop/
+ ]
+| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+ elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ /4 width=1 by lpx_pair, aaa_abst/
+| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+ elim (cpx_inv_appl1 … H) -H *
+ [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/
+ | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
+ lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
+ lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
+ elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
+ /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/
+ | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
+ lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2
+ lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
+ elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/
+ ]
+| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+ elim (cpx_inv_cast1 … H) -H
+ [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/
+ | -IHV1 /2 width=1 by/
+ | -IHT1 /2 width=1 by/
+ ]
+]
+qed-.
+
+lemma aaa_cpx_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+/2 width=7 by aaa_cpx_lpx_conf/ qed-.
+
+lemma aaa_lpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/2 width=7 by aaa_cpx_lpx_conf/ qed-.
+
+lemma aaa_cpr_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-.
+
+lemma aaa_lpr_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/3 width=5 by aaa_lpx_conf, lpr_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/relocation/lpx_sn_ldrop.ma".
+include "basic_2/reduction/cpx_lift.ma".
+include "basic_2/reduction/lpx.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpx_ldrop_conf: ∀h,g,G. dropable_sn (lpx h g G).
+/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
+
+lemma ldrop_lpx_trans: ∀h,g,G. dedropable_sn (lpx h g G).
+/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
+
+lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G).
+/2 width=3 by lpx_sn_dropable/ qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fqu_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
+ ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/
+[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H
+ #K2 #W2 #HLK2 #HVW2 #H destruct
+ /3 width=5 by fqu_fquq, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
+ elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
+ /3 width=7 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma fquq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
+ ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/
+[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
+ #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
+ /4 width=7 by cpx_delta, fqu_drop, ldrop_drop, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
+ elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1
+ /3 width=5 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_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/substitution/lleq_ldrop.ma".
+include "basic_2/reduction/lpx_ldrop.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 →
+ ∀L1,T,d. L1 ⋕[T, d] L2 →
+ ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2.
+
+lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1
+ #K0 #V0 #H1KL1 #_ #H destruct
+ elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
+ #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
+ /2 width=4 by fqu_lref_O, ex3_intro/
+| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
+ [ elim (lleq_inv_bind … H)
+ | elim (lleq_inv_flat … H)
+ ] -H /2 width=4 by fqu_pair_sn, ex3_intro/
+| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H
+ /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/
+| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
+ /2 width=4 by fqu_flat_dx, ex3_intro/
+| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
+ elim (ldrop_O1_le (e+1) K1)
+ [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
+ #H2KL elim (lpx_ldrop_trans_O1 … H1KL1 … HL1) -L1
+ #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct
+ /3 width=4 by fqu_drop, ex3_intro/
+ | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g
+ lapply (lleq_fwd_length … H2KL1) //
+ ]
+]
+qed-.
+
+lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
+elim (fquq_inv_gen … H) -H
+[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
+ /3 width=4 by fqu_fquq, ex3_intro/
+| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
+]
+qed-.
+
+lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
+ /3 width=4 by fqu_fqup, ex3_intro/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1
+ #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L
+ /3 width=5 by fqup_strap1, ex3_intro/
+]
+qed-.
+
+lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
+elim (fqus_inv_gen … H) -H
+[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
+ /3 width=4 by fqup_fqus, ex3_intro/
+| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
+]
+qed-.
(* *)
(**************************************************************************)
+include "ground_2/xoa/xoa2.ma".
include "basic_2/notation/relations/lazyor_4.ma".
include "basic_2/relocation/lpx_sn_alt.ma".
(* Alternative definition ***************************************************)
-lemma llor_intro_alt_eq: ∀T,L2,L1,L. |L1| = |L2| → |L1| = |L| →
- (∀I1,I,K1,K,V1,V,U,i. ⇧[i, 1] U ≡ T →
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
- ∧∧ I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K
- ) →
- (∀I1,I2,I,K1,K2,K,V1,V2,V,i. (∀U. ⇧[i, 1] U ≡ T → ⊥) →
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ⇩[i] L ≡ K.ⓑ{I}V → ∧∧ I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K
- ) → L1 ⩖[T] L2 ≡ L.
-#T #L2 #L1 #L #HL12 #HL1 #IH1 #IH2 @lpx_sn_intro_alt // -HL1
+(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
+lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
+#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
+qed-.
+
+fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
+/2 width=1 by plus_minus_minus_be/ qed-.
+
+lemma llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| →
+ (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
+ (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T →
+ ∧∧ I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K
+ ) ∧
+ (∀I2,K2,V2. (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T → ⊥) →
+ ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K
+ )
+ ) → L1 ⩖[T] L2 ≡ L.
+#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1
#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
lapply (ldrop_fwd_length_minus4 … HLK1)
lapply (ldrop_fwd_length_le4 … HLK1)
-normalize >HL12 <minus_plus #HKL1 #Hi elim (is_lift_dec T i 1) -HL12
-[ * #U #HUT elim (IH1 … HUT HLK1 HLK) -IH1 -HLK1 -HLK #H1 #H2 #HT destruct
+normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) // #H2i
+lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 #HKL1
+elim (IH … HLK1 HLK) -IH -HLK1 -HLK #IH1 #IH2
+elim (is_lift_dec T (|L2|-|L1|+i) 1)
+[ -IH2 * #U #HUT elim (IH1 … HUT) -IH1
/3 width=2 by clor_sn, and3_intro/
-| #H elim (ldrop_O1_lt L2 i) destruct /2 width=1 by monotonic_lt_minus_l/
- #I2 #K2 #V2 #HLK2 elim (IH2 … HLK1 HLK2 HLK) -HLK1 -HLK
+| -IH1 #H elim (ldrop_O1_lt L2 (|L2|-|L1|+i)) /2 width=1 by monotonic_lt_minus_l/
+ #I2 #K2 #V2 #HLK2 elim (IH2 … HLK2) -IH2
/5 width=3 by clor_dx, ex_intro, and3_intro/
]
qed.
-lemma llor_inv_gen_eq: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| = |L2| →
- |L1| = |L| ∧
- (∀I1,I,K1,K,V1,V,i.
+lemma llor_ind_alt: ∀T,L2. ∀S:relation lenv. (
+ ∀L1,L. |L1| = |L| → (
+ ∀I1,I,K1,K,V1,V,i.
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
- (∃∃U. ⇧[i, 1] U ≡ T &
- I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K
+ (∃∃U. ⇧[|L2|-|L1|+i, 1] U ≡ T &
+ I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K & S K1 K
) ∨
- (∃∃I2,K2,V2. (∀U. ⇧[i, 1] U ≡ T → ⊥) &
- ⇩[i] L2 ≡ K2.ⓑ{I2}V2 &
- I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K
+ (∃∃I2,K2,V2. (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T → ⊥) &
+ ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 &
+ I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K & S K1 K
)
- ).
-#T #L2 #L1 #L #H #HL12 elim (lpx_sn_inv_gen … H) -H
-#HL1 #IH @conj //
+ ) → |L1| ≤ |L2| → S L1 L
+ ) →
+ ∀L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → S L1 L.
+#T #L2 #S #IH1 #L1 #L #H @(lpx_sn_ind_alt … H) -L1 -L
+#L1 #L #HL1 #IH2 #HL12 @IH1 // -IH1 -HL1
+#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
+lapply (ldrop_fwd_length_minus4 … HLK1)
+lapply (ldrop_fwd_length_le4 … HLK1)
+normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) //
+lapply (transitive_le … HKL1 HL12) -HKL1 -HL12
+elim (IH2 … HLK1 HLK) -IH2 #H *
+/5 width=5 by lt_to_le, ex6_3_intro, ex5_intro, or_intror, or_introl/
+qed-.
+
+lemma llor_inv_alt: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| →
+ |L1| = |L| ∧
+ (∀I1,I,K1,K,V1,V,i.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
+ (∃∃U. ⇧[|L2|-|L1|+i, 1] U ≡ T &
+ I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K
+ ) ∨
+ (∃∃I2,K2,V2. (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T → ⊥) &
+ ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 &
+ I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K
+ )
+ ).
+#T #L2 #L1 #L #H #HL12 elim (lpx_sn_inv_alt … H) -H
+#HL1 #IH @conj // -HL1
#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
lapply (ldrop_fwd_length_minus4 … HLK1)
lapply (ldrop_fwd_length_le4 … HLK1)
-normalize >HL12 <minus_plus #HKL1 #Hi elim (IH … HLK1 HLK) -IH #H *
+normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) //
+lapply (transitive_le … HKL1 HL12) -HKL1 -HL12
+elim (IH … HLK1 HLK) -IH #H *
/4 width=5 by ex5_3_intro, ex4_intro, or_intror, or_introl/
qed-.
(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
-(* alternative definition of llpx_sn_alt *)
+(* alternative definition of llpx_sn *)
inductive llpx_sn_alt (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝
| llpx_sn_alt_intro: ∀L1,L2,T,d.
(∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
) → |L1| = |L2| → llpx_sn_alt R d T L1 L2
.
-(* Basic inversion lemmas ****************************************************)
+(* Compact definition of llpx_sn_alt ****************************************)
-lemma llpx_sn_alt_inv_gen: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 →
+lemma llpx_sn_alt_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
+ (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2
+ ) → llpx_sn_alt R d T L1 L2.
+#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_intro // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by conj/
+qed.
+
+lemma llpx_sn_alt_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv.
+ (∀L1,L2,T,d. |L1| = |L2| → (
+ ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2 & S 0 V1 K1 K2
+ ) → S d T L1 L2) →
+ ∀L1,L2,T,d. llpx_sn_alt R d T L1 L2 → S d T L1 L2.
+#R #S #IH #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
+#L1 #L2 #T #d #H1 #H2 #HL12 #IH2 @IH -IH // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (H1 … HnT HLK1 HLK2) -H1 /4 width=8 by and4_intro/
+qed-.
+
+lemma llpx_sn_alt_inv_alt: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 →
|L1| = |L2| ∧
∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2.
-#R #L1 #L2 #T #d * -L1 -L2 -T -d
-#L1 #L2 #T #d #IH1 #IH2 #HL12 @conj //
-#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
-elim (IH1 … HnT HLK1 HLK2) -IH1 /4 width=8 by and3_intro/
+#R #L1 #L2 #T #d #H @(llpx_sn_alt_ind_alt … H) -L1 -L2 -T -d
+#L1 #L2 #T #d #HL12 #IH @conj // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
qed-.
+(* Basic inversion lemmas ***************************************************)
+
lemma llpx_sn_alt_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓕ{I}V.T) L1 L2 →
llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R d T L1 L2.
-#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_inv_gen … H) -H
-#HL12 #IH @conj @llpx_sn_alt_intro // -HL12
+#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_inv_alt … H) -H
+#HL12 #IH @conj @llpx_sn_alt_intro_alt // -HL12
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2
-elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
-/3 width=8 by nlift_flat_sn, nlift_flat_dx, conj/
+elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 //
+/3 width=8 by nlift_flat_sn, nlift_flat_dx, and3_intro/
qed-.
lemma llpx_sn_alt_inv_bind: ∀R,a,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2 →
llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
-#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_inv_gen … H) -H
-#HL12 #IH @conj @llpx_sn_alt_intro [3,6: normalize // ] -HL12
+#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_inv_alt … H) -H
+#HL12 #IH @conj @llpx_sn_alt_intro_alt [1,3: normalize // ] -HL12
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2
-[1,2: elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
- /3 width=9 by nlift_bind_sn, conj/
-|3,4: lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi
+[ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
+ /3 width=9 by nlift_bind_sn, and3_intro/
+| lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi
lapply (ldrop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1
lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2
- elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
- [1,3,4,6: /2 width=1 by conj/ ]
+ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by and3_intro/
@nlift_bind_dx <plus_minus_m_m /2 width=2 by ylt_O/
]
qed-.
(* Basic forward lemmas ******************************************************)
lemma llpx_sn_alt_fwd_length: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 → |L1| = |L2|.
-#R #L1 #L2 #T #d * -L1 -L2 -T -d //
+#R #L1 #L2 #T #d #H elim (llpx_sn_alt_inv_alt … H) -H //
qed-.
lemma llpx_sn_alt_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt R d (#i) L1 L2 →
⇩[i] L2 ≡ K2.ⓑ{I}V2 &
llpx_sn_alt R (yinj 0) V1 K1 K2 &
R K1 V1 V2 & d ≤ yinj i.
-#R #L1 #L2 #d #i #H elim (llpx_sn_alt_inv_gen … H) -H
+#R #L1 #L2 #d #i #H elim (llpx_sn_alt_inv_alt … H) -H
#HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/
elim (ylt_split i d) /3 width=1 by or3_intro1/
#Hdi #HL1 elim (ldrop_O1_lt … HL1)
(* Basic properties **********************************************************)
-lemma llpx_sn_alt_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
- (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2
- ) → llpx_sn_alt R d T L1 L2.
-#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_intro // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
-elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by conj/
-qed.
-
lemma llpx_sn_alt_sort: ∀R,L1,L2,d,k. |L1| = |L2| → llpx_sn_alt R d (⋆k) L1 L2.
#R #L1 #L2 #d #k #HL12 @llpx_sn_alt_intro_alt // -HL12
#I1 #I2 #K1 #K2 #V1 #V2 #i #_ #H elim (H (⋆k)) //
llpx_sn_alt R d V L1 L2 → llpx_sn_alt R d T L1 L2 →
llpx_sn_alt R d (ⓕ{I}V.T) L1 L2.
#R #I #L1 #L2 #V #T #d #HV #HT
-elim (llpx_sn_alt_inv_gen … HV) -HV #HL12 #IHV
-elim (llpx_sn_alt_inv_gen … HT) -HT #_ #IHT
+elim (llpx_sn_alt_inv_alt … HV) -HV #HL12 #IHV
+elim (llpx_sn_alt_inv_alt … HT) -HT #_ #IHT
@llpx_sn_alt_intro_alt // -HL12
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnVT #HLK1 #HLK2
elim (nlift_inv_flat … HnVT) -HnVT #H
llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2.
#R #a #I #L1 #L2 #V #T #d #HV #HT
-elim (llpx_sn_alt_inv_gen … HV) -HV #HL12 #IHV
-elim (llpx_sn_alt_inv_gen … HT) -HT #_ #IHT
+elim (llpx_sn_alt_inv_alt … HV) -HV #HL12 #IHV
+elim (llpx_sn_alt_inv_alt … HT) -HT #_ #IHT
@llpx_sn_alt_intro_alt // -HL12
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnVT #HLK1 #HLK2
elim (nlift_inv_bind … HnVT) -HnVT #H
]
qed-.
-(* Advanced properties ******************************************************)
+(* Alternative definition of llpx_sn ****************************************)
lemma llpx_sn_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
(∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_lpx_sn_alt, and3_intro/
qed.
-(* Advanced inversion lemmas ************************************************)
+lemma llpx_sn_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv.
+ (∀L1,L2,T,d. |L1| = |L2| → (
+ ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2 & S 0 V1 K1 K2
+ ) → S d T L1 L2) →
+ ∀L1,L2,T,d. llpx_sn R d T L1 L2 → S d T L1 L2.
+#R #S #IH1 #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt … H) -H
+#H @(llpx_sn_alt_ind_alt … H) -L1 -L2 -T -d
+#L1 #L2 #T #d #HL12 #IH2 @IH1 -IH1 // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH2 … HnT HLK1 HLK2) -IH2 -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_alt_inv_lpx_sn, and4_intro/
+qed-.
-lemma llpx_sn_inv_gen: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
+lemma llpx_sn_inv_alt: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
|L1| = |L2| ∧
∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2.
#R #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt … H) -H
-#H elim (llpx_sn_alt_inv_gen … H) -H
+#H elim (llpx_sn_alt_inv_alt … H) -H
#HL12 #IH @conj //
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_alt_inv_lpx_sn, and3_intro/
(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
-(* alternative definition of lpx_sn_alt *)
+(* alternative definition of lpx_sn *)
inductive lpx_sn_alt (R:relation3 lenv term term): relation lenv ≝
| lpx_sn_alt_intro: ∀L1,L2.
(∀I1,I2,K1,K2,V1,V2,i.
) → |L1| = |L2| → lpx_sn_alt R L1 L2
.
-(* Basic forward lemmas ******************************************************)
-
-lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|.
-#R #L1 #L2 * -L1 -L2 //
+(* compact definition of lpx_sn_alt *****************************************)
+
+lemma lpx_sn_alt_ind_alt: ∀R. ∀S:relation lenv.
+ (∀L1,L2. |L1| = |L2| → (
+ ∀I1,I2,K1,K2,V1,V2,i.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn_alt R K1 K2 & S K1 K2
+ ) → S L1 L2) →
+ ∀L1,L2. lpx_sn_alt R L1 L2 → S L1 L2.
+#R #S #IH #L1 #L2 #H elim H -L1 -L2
+#L1 #L2 #H1 #H2 #HL12 #IH2 @IH -IH // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2 elim (H1 … HLK1 HLK2) -H1
+/3 width=7 by and4_intro/
qed-.
-(* Basic inversion lemmas ***************************************************)
-
-lemma lpx_sn_alt_inv_gen: ∀R,L1,L2. lpx_sn_alt R L1 L2 →
+lemma lpx_sn_alt_inv_alt: ∀R,L1,L2. lpx_sn_alt R L1 L2 →
|L1| = |L2| ∧
∀I1,I2,K1,K2,V1,V2,i.
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn_alt R K1 K2.
-#R #L1 #L2 * -L1 -L2
-#L1 #L2 #IH1 #IH2 #HL12 @conj //
-#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #HLK1 #HLK2
-elim (IH1 … HLK1 HLK2) -IH1 /3 width=7 by and3_intro/
+#R #L1 #L2 #H @(lpx_sn_alt_ind_alt … H) -L1 -L2
+#L1 #L2 #HL12 #IH @conj // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2 elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
+/2 width=1 by and3_intro/
qed-.
+lemma lpx_sn_alt_intro_alt: ∀R,L1,L2. |L1| = |L2| →
+ (∀I1,I2,K1,K2,V1,V2,i.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn_alt R K1 K2
+ ) → lpx_sn_alt R L1 L2.
+#R #L1 #L2 #HL12 #IH @lpx_sn_alt_intro // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2
+elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by conj/
+qed.
+
+(* Basic forward lemmas ******************************************************)
+
+lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim (lpx_sn_alt_inv_alt … H) //
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
lemma lpx_sn_alt_inv_atom1: ∀R,L2. lpx_sn_alt R (⋆) L2 → L2 = ⋆.
#R #L2 #H lapply (lpx_sn_alt_fwd_length … H) -H
normalize /2 width=1 by length_inv_zero_sn/
lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 →
∃∃K2,V2. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2.
-#R #I1 #L2 #K1 #V1 #H elim (lpx_sn_alt_inv_gen … H) -H
+#R #I1 #L2 #K1 #V1 #H elim (lpx_sn_alt_inv_alt … H) -H
#H #IH elim (length_inv_pos_sn … H) -H
#I2 #K2 #V2 #HK12 #H destruct
elim (IH I1 I2 K1 K2 V1 V2 0) -IH /2 width=5 by ex3_2_intro/
lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) →
∃∃K1,V1. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1.
-#R #I2 #L1 #K2 #V2 #H elim (lpx_sn_alt_inv_gen … H) -H
+#R #I2 #L1 #K2 #V2 #H elim (lpx_sn_alt_inv_alt … H) -H
#H #IH elim (length_inv_pos_dx … H) -H
#I1 #K1 #V1 #HK12 #H destruct
elim (IH I1 I2 K1 K2 V1 V2 0) -IH /2 width=5 by ex3_2_intro/
(* Basic properties *********************************************************)
-lemma lpx_sn_alt_intro_alt: ∀R,L1,L2. |L1| = |L2| →
- (∀I1,I2,K1,K2,V1,V2,i.
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn_alt R K1 K2
- ) → lpx_sn_alt R L1 L2.
-#R #L1 #L2 #HL12 #IH @lpx_sn_alt_intro // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2
-elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by conj/
-qed.
-
lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆).
#R @lpx_sn_alt_intro_alt //
#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 elim (ldrop_inv_atom1 … HLK1) -HLK1
lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2.
lpx_sn_alt R L1 L2 → R L1 V1 V2 →
lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2).
-#R #I #L1 #L2 #V1 #V2 #H #HV12 elim (lpx_sn_alt_inv_gen … H) -H
+#R #I #L1 #L2 #V1 #V2 #H #HV12 elim (lpx_sn_alt_inv_alt … H) -H
#HL12 #IH @lpx_sn_alt_intro_alt normalize //
#I1 #I2 #K1 #K2 #W1 #W2 #i @(nat_ind_plus … i) -i
[ #HLK1 #HLK2
]
qed-.
-(* Advanced properties ******************************************************)
+(* alternative definition of lpx_sn *****************************************)
lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| →
(∀I1,I2,K1,K2,V1,V2,i.
elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /3 width=1 by lpx_sn_lpx_sn_alt, and3_intro/
qed.
-(* Advanced inversion lemmas ************************************************)
+lemma lpx_sn_ind_alt: ∀R. ∀S:relation lenv.
+ (∀L1,L2. |L1| = |L2| → (
+ ∀I1,I2,K1,K2,V1,V2,i.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn R K1 K2 & S K1 K2
+ ) → S L1 L2) →
+ ∀L1,L2. lpx_sn R L1 L2 → S L1 L2.
+#R #S #IH1 #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H
+#H @(lpx_sn_alt_ind_alt … H) -L1 -L2
+#L1 #L2 #HL12 #IH2 @IH1 -IH1 // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2 elim (IH2 … HLK1 HLK2) -IH2 -HLK1 -HLK2
+/3 width=1 by lpx_sn_alt_inv_lpx_sn, and4_intro/
+qed-.
-lemma lpx_sn_inv_gen: ∀R,L1,L2. lpx_sn R L1 L2 →
+lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 →
|L1| = |L2| ∧
∀I1,I2,K1,K2,V1,V2,i.
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn R K1 K2.
#R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H
-#H elim (lpx_sn_alt_inv_gen … H) -H
+#H elim (lpx_sn_alt_inv_alt … H) -H
#HL12 #IH @conj //
#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2
elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /3 width=1 by lpx_sn_alt_inv_lpx_sn, and3_intro/
elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
qed.
-theorem lleq_inv_gen: ∀L1,L2,T,d. L1 ⋕[T, d] L2 →
+theorem lleq_ind_alt: ∀S:relation4 ynat term lenv lenv.
+ (∀L1,L2,T,d. |L1| = |L2| → (
+ ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2 & S 0 V1 K1 K2
+ ) → S d T L1 L2) →
+ ∀L1,L2,T,d. L1 ⋕[T, d] L2 → S d T L1 L2.
+#S #IH1 #L1 #L2 #T #d #H @(llpx_sn_ind_alt … H) -L1 -L2 -T -d
+#L1 #L2 #T #d #HL12 #IH2 @IH1 -IH1 // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH2 … HnT HLK1 HLK2) -IH2 -HnT -HLK1 -HLK2 /2 width=1 by and4_intro/
+qed-.
+
+theorem lleq_inv_alt: ∀L1,L2,T,d. L1 ⋕[T, d] L2 →
|L1| = |L2| ∧
∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2.
-#L1 #L2 #T #d #H elim (llpx_sn_inv_gen … H) -H
+#L1 #L2 #T #d #H elim (llpx_sn_inv_alt … H) -H
#HL12 #IH @conj //
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
(* [ "lcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )" "lcosx_cpxs" * ] *)
[ "llsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )" "llsx_alt ( ? ⊢ ⋕⬊⬊*[?,?,?,?] ? )" "llsx_ldrop" + "llsx_llpx" + "llsx_llpxs" + "llsx_csx" * ]
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
- [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ]
+ [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_llpx" + "csx_lpxs" + "csx_llpxs" + "csx_fpbs" * ]
}
]
[ { "\"big tree\" parallel computation" * } {
]
[ { "context-sensitive extended computation" * } {
[ "llpxs ( ⦃?,?⦄ ⊢ ➡*[?,?,?,?] ? )" "llpxs_lleq" + "llpxs_aaa" + "llpxs_lprs" "llpxs_cpxs" + "llpxs_llpxs" * ]
-(* [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] *)
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
+ [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_llpx" + "cpxs_cpxs" * ]
}
]
[ { "context-sensitive computation" * } {
]
[ { "context-sensitive extended reduction" * } {
[ "llpx ( ⦃?,?⦄ ⊢ ➡[?,?,?,?] ? )" "llpx_ldrop" + "llpx_lleq" + "llpx_aaa" + "llpx_lpr" * ]
-(* [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ] *)
+ [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
[ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
}
]
projects / helm.git / commitdiff