+++ /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( L1 ⨵ [ break term 46 f ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'Clear $f $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 o , break term 46 f ] break term 46 L )"
- non associative with precedence 45
- for @{ 'CoSN $h $o $f $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( G ⊢ break term 46 L1 ⊆ⓧ [ break term 46 h, break term 46 o, break term 46 f ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LSubEqX $h $o $f $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/cosn_5.ma".
-include "basic_2/computation/lsx.ma".
-
-(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
-
-inductive lcosx (h) (o) (G): relation2 ynat lenv ≝
-| lcosx_sort: ∀l. lcosx h o G l (⋆)
-| lcosx_skip: ∀I,L,T. lcosx h o G 0 L → lcosx h o G 0 (L.ⓑ{I}T)
-| lcosx_pair: ∀I,L,T,l. G ⊢ ⬊*[h, o, T, l] L →
- lcosx h o G l L → lcosx h o G (⫯l) (L.ⓑ{I}T)
-.
-
-interpretation
- "sn extended strong conormalization (local environment)"
- 'CoSN h o l G L = (lcosx h o G l L).
-
-(* Basic properties *********************************************************)
-
-lemma lcosx_O: ∀h,o,G,L. G ⊢ ~⬊*[h, o, 0] L.
-#h #o #G #L elim L /2 width=1 by lcosx_skip/
-qed.
-
-lemma lcosx_drop_trans_lt: ∀h,o,G,L,l. G ⊢ ~⬊*[h, o, l] L →
- ∀I,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → i < l →
- G ⊢ ~⬊*[h, o, ⫰(l-i)] K ∧ G ⊢ ⬊*[h, o, V, ⫰(l-i)] K.
-#h #o #G #L #l #H elim H -L -l
-[ #l #J #K #V #i #H elim (drop_inv_atom1 … H) -H #H destruct
-| #I #L #T #_ #_ #J #K #V #i #_ #H elim (ylt_yle_false … H) -H //
-| #I #L #T #l #HT #HL #IHL #J #K #V #i #H #Hil
- elim (drop_inv_O1_pair1 … H) -H * #Hi #HLK destruct
- [ >ypred_succ /2 width=1 by conj/
- | lapply (ylt_pred … Hil ?) -Hil /2 width=1 by ylt_inj/ >ypred_succ #Hil
- elim (IHL … HLK ?) -IHL -HLK <yminus_inj >yminus_SO2 //
- <(ypred_succ l) in ⊢ (%→%→?); >yminus_pred /2 width=1 by ylt_inj, conj/
- ]
-]
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lcosx_inv_succ_aux: ∀h,o,G,L,x. G ⊢ ~⬊*[h, o, x] L → ∀l. x = ⫯l →
- L = ⋆ ∨
- ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ~⬊*[h, o, l] K &
- G ⊢ ⬊*[h, o, V, l] K.
-#h #o #G #L #l * -L -l /2 width=1 by or_introl/
-[ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H)
-| #I #L #T #l #HT #HL #x #H <(ysucc_inv_inj … H) -x
- /3 width=6 by ex3_3_intro, or_intror/
-]
-qed-.
-
-lemma lcosx_inv_succ: ∀h,o,G,L,l. G ⊢ ~⬊*[h, o, ⫯l] L → L = ⋆ ∨
- ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ~⬊*[h, o, l] K &
- G ⊢ ⬊*[h, o, V, l] K.
-/2 width=3 by lcosx_inv_succ_aux/ qed-.
-
-lemma lcosx_inv_pair: ∀h,o,I,G,L,T,l. G ⊢ ~⬊*[h, o, ⫯l] L.ⓑ{I}T →
- G ⊢ ~⬊*[h, o, l] L ∧ G ⊢ ⬊*[h, o, T, l] L.
-#h #o #I #G #L #T #l #H elim (lcosx_inv_succ … H) -H
-[ #H destruct
-| * #Z #Y #X #H destruct /2 width=1 by conj/
-]
-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/lsx_drop.ma".
-include "basic_2/computation/lsx_lpx.ma".
-include "basic_2/computation/lsx_lpxs.ma".
-include "basic_2/computation/lcosx.ma".
-
-(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
-
-(* Properties on extended context-sensitive parallel reduction for term *****)
-
-lemma lsx_cpx_trans_lcosx: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 →
- ∀l. G ⊢ ~⬊*[h, o, l] L →
- G ⊢ ⬊*[h, o, T1, l] L → G ⊢ ⬊*[h, o, T2, l] L.
-#h #o #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
-[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #l #HL #H
- elim (ylt_split i l) #Hli [ -H | -HL ]
- [ <(ymax_pre_sn l (⫯i)) /2 width=1 by ylt_fwd_le_succ1/
- elim (lcosx_drop_trans_lt … HL … HLK) // -HL -Hli
- lapply (drop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
- | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hli
- lapply (drop_fwd_drop2 … HLK) -HLK
- /4 width=10 by lsx_ge, lsx_lift_le/
- ]
-| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
- elim (lsx_inv_bind … H) -H #HV1 #HT1
- @lsx_bind /2 width=2 by/ (**) (* explicit constructor *)
- @(lsx_lreq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, lreq_succ/
-| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
- elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/
-| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #l #HL #H
- elim (lsx_inv_bind … H) -H #HV #HU1
- <(ypred_succ l) <yminus_SO2
- /4 width=7 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
-| #G #L #V #T1 #T2 #_ #IHT12 #l #HL #H
- elim (lsx_inv_flat … H) -H /2 width=1 by/
-| #G #L #V1 #V2 #T #_ #IHV12 #l #HL #H
- elim (lsx_inv_flat … H) -H /2 width=1 by/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #l #HL #H
- elim (lsx_inv_flat … H) -H #HV1 #H
- elim (lsx_inv_bind … H) -H #HW1 #HT1
- @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *)
- @(lsx_lreq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, lreq_succ/
-| #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #l #HL #H
- elim (lsx_inv_flat … H) -H #HV1 #H
- elim (lsx_inv_bind … H) -H #HW1 #HT1
- @lsx_bind /2 width=1 by/ (**) (* explicit constructor *)
- @lsx_flat [ <yplus_SO2 /3 width=7 by lsx_lift_ge, drop_drop/ ]
- @(lsx_lreq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, lreq_succ/
-]
-qed-.
-
-lemma lsx_cpx_trans_O: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 →
- G ⊢ ⬊*[h, o, T1, 0] L → G ⊢ ⬊*[h, o, T2, 0] L.
-/2 width=3 by lsx_cpx_trans_lcosx/ qed-.
--- /dev/null
+
+include "basic_2/static/lfxs_lfxs.ma".
+include "basic_2/rt_transition/lfpx_frees.ma".
+include "basic_2/rt_computation/lfpxs_fqup.ma".
+
+axiom cpx_frees_conf_lfpxs: ∀h,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
+ ∀f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T1] L2 →
+ ∀g1. L2 ⊢ 𝐅*⦃T1⦄ ≡ g1 →
+ ∃∃g2. L2 ⊢ 𝐅*⦃T2⦄ ≡ g2 & g2 ⊆ g1 & g1 ⊆ f1.
+
+lemma lfpxs_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G).
+#h #G #L1 #T1 #T2 #HT12 #L2 #H
+lapply (cpx_frees_conf_lfpxs … HT12) -HT12 #HT12
+@(lfpxs_ind_sn … H) -L2 //
+#L #L2 #HL1 * #g1 #Hg1 #HL2 #IH
+elim (frees_total L1 T1) #f1 #Hf1
+elim (HT12 … Hf1 … HL1 … Hg1) -T1 #g2 #Hg2 #Hg21 #_ -f1
+/4 width=7 by lfpxs_step_dx, sle_lexs_trans, ex2_intro/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/lfpxs.ma".
include "basic_2/rt_computation/csx_cpxs.ma".
include "basic_2/rt_computation/csx_lsubr.ma".
-include "basic_2/rt_computation/lfsx_drops.ma".
-include "basic_2/rt_computation/lfsx_lfpxs.ma".
+include "basic_2/rt_computation/lsubsx_lfsx.ma".
(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
| @lfsx_lfpx_trans
[2: @(IHV0 … HnV02 K0 … I) -IHV0 -HnV02
[ /2 width=3 by lfpxs_cpx_trans/
- |
+ | /2 width=3 by lfsx_cpx_trans/
|
]
|1: skip
|3: @lfpx_pair /2 width=3 by lfpx_cpx_conf/
- ]
- /3 width=4 by lsx_cpx_trans_O, lsx_lpx_trans, lpxs_cpx_trans, lpxs_strap1/ (**) (* full auto too slow *)
+ ]
]
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/lsubeqx_6.ma".
+include "basic_2/rt_computation/lfsx.ma".
+
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+
+(* Note: this should be an instance of a more general lexs *)
+(* Basic_2A1: uses: lcosx *)
+inductive lsubsx (h) (o) (G): rtmap → relation lenv ≝
+| lsubsx_atom: ∀f. lsubsx h o G f (⋆) (⋆)
+| lsubsx_push: ∀f,I,K1,K2. lsubsx h o G f K1 K2 →
+ lsubsx h o G (↑f) (K1.ⓘ{I}) (K2.ⓘ{I})
+| lsubsx_unit: ∀f,I,K1,K2. lsubsx h o G f K1 K2 →
+ lsubsx h o G (⫯f) (K1.ⓤ{I}) (K2.ⓧ)
+| lsubsx_pair: ∀f,I,K1,K2,V. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ →
+ lsubsx h o G f K1 K2 → lsubsx h o G (⫯f) (K1.ⓑ{I}V) (K2.ⓧ)
+.
+
+interpretation
+ "local environment refinement (clear)"
+ 'LSubEqX h o f G L1 L2 = (lsubsx h o G f L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubsx_inv_atom_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
+ L1 = ⋆ → L2 = ⋆.
+#h #o #g #G #L1 #L2 * -g -L1 -L2 //
+[ #f #I #K1 #K2 #_ #H destruct
+| #f #I #K1 #K2 #_ #H destruct
+| #f #I #K1 #K2 #V #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubsx_inv_atom_sn: ∀h,o,g,G,L2. G ⊢ ⋆ ⊆ⓧ[h, o, g] L2 → L2 = ⋆.
+/2 width=7 by lsubsx_inv_atom_sn_aux/ qed-.
+
+fact lsubsx_inv_push_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
+ ∀f,I,K1. g = ↑f → L1 = K1.ⓘ{I} →
+ ∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓘ{I}.
+#h #o #g #G #L1 #L2 * -g -L1 -L2
+[ #f #g #J #L1 #_ #H destruct
+| #f #I #K1 #K2 #HK12 #g #J #L1 #H1 #H2 destruct
+ <(injective_push … H1) -g /2 width=3 by ex2_intro/
+| #f #I #K1 #K2 #_ #g #J #L1 #H
+ elim (discr_next_push … H)
+| #f #I #K1 #K2 #V #_ #_ #g #J #L1 #H
+ elim (discr_next_push … H)
+]
+qed-.
+
+lemma lsubsx_inv_push_sn: ∀h,o,f,I,G,K1,L2. G ⊢ K1.ⓘ{I} ⊆ⓧ[h, o, ↑f] L2 →
+ ∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓘ{I}.
+/2 width=5 by lsubsx_inv_push_sn_aux/ qed-.
+
+fact lsubsx_inv_unit_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
+ ∀f,I,K1. g = ⫯f → L1 = K1.ⓤ{I} →
+ ∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
+#h #o #g #G #L1 #L2 * -g -L1 -L2
+[ #f #g #J #L1 #_ #H destruct
+| #f #I #K1 #K2 #_ #g #J #L1 #H
+ elim (discr_push_next … H)
+| #f #I #K1 #K2 #HK12 #g #J #L1 #H1 #H2 destruct
+ <(injective_next … H1) -g /2 width=3 by ex2_intro/
+| #f #I #K1 #K2 #V #_ #_ #g #J #L1 #_ #H destruct
+]
+qed-.
+
+lemma lsubsx_inv_unit_sn: ∀h,o,f,I,G,K1,L2. G ⊢ K1.ⓤ{I} ⊆ⓧ[h, o, ⫯f] L2 →
+ ∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
+/2 width=6 by lsubsx_inv_unit_sn_aux/ qed-.
+
+fact lsubsx_inv_pair_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
+ ∀f,I,K1,V. g = ⫯f → L1 = K1.ⓑ{I}V →
+ ∃∃K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ &
+ G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
+#h #o #g #G #L1 #L2 * -g -L1 -L2
+[ #f #g #J #L1 #W #_ #H destruct
+| #f #I #K1 #K2 #_ #g #J #L1 #W #H
+ elim (discr_push_next … H)
+| #f #I #K1 #K2 #_ #g #J #L1 #W #_ #H destruct
+| #f #I #K1 #K2 #V #HV #HK12 #g #J #L1 #W #H1 #H2 destruct
+ <(injective_next … H1) -g /2 width=4 by ex3_intro/
+]
+qed-.
+
+(* Basic_2A1: uses: lcosx_inv_pair *)
+lemma lsubsx_inv_pair_sn: ∀h,o,f,I,G,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊆ⓧ[h, o, ⫯f] L2 →
+ ∃∃K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ &
+ G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
+/2 width=6 by lsubsx_inv_pair_sn_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lsubsx_inv_pair_sn_gen: ∀h,o,g,I,G,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊆ⓧ[h, o, g] L2 →
+ ∨∨ ∃∃f,K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & g = ↑f & L2 = K2.ⓑ{I}V
+ | ∃∃f,K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ &
+ G ⊢ K1 ⊆ⓧ[h, o, f] K2 & g = ⫯f & L2 = K2.ⓧ.
+#h #o #g #I #G #K1 #L2 #V #H
+elim (pn_split g) * #f #Hf destruct
+[ elim (lsubsx_inv_push_sn … H) -H /3 width=5 by ex3_2_intro, or_introl/
+| elim (lsubsx_inv_pair_sn … H) -H /3 width=6 by ex4_2_intro, or_intror/
+]
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lsubsx_fwd_bind_sn: ∀h,o,g,I1,G,K1,L2. G ⊢ K1.ⓘ{I1} ⊆ⓧ[h, o, g] L2 →
+ ∃∃I2,K2. G ⊢ K1 ⊆ⓧ[h, o, ⫱g] K2 & L2 = K2.ⓘ{I2}.
+#h #o #g #I1 #G #K1 #L2
+elim (pn_split g) * #f #Hf destruct
+[ #H elim (lsubsx_inv_push_sn … H) -H
+| cases I1 -I1 #I1
+ [ #H elim (lsubsx_inv_unit_sn … H) -H
+ | #V #H elim (lsubsx_inv_pair_sn … H) -H
+ ]
+]
+/2 width=4 by ex2_2_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsubsx_eq_repl_back: ∀h,o,G,L1,L2. eq_repl_back … (λf. G ⊢ L1 ⊆ⓧ[h, o, f] L2).
+#h #o #G #L1 #L2 #f1 #H elim H -L1 -L2 -f1 //
+[ #f #I #L1 #L2 #_ #IH #x #H
+ elim (eq_inv_px … H) -H /3 width=3 by lsubsx_push/
+| #f #I #L1 #L2 #_ #IH #x #H
+ elim (eq_inv_nx … H) -H /3 width=3 by lsubsx_unit/
+| #f #I #L1 #L2 #V #HV #_ #IH #x #H
+ elim (eq_inv_nx … H) -H /3 width=3 by lsubsx_pair/
+]
+qed-.
+
+lemma lsubsx_eq_repl_fwd: ∀h,o,G,L1,L2. eq_repl_fwd … (λf. G ⊢ L1 ⊆ⓧ[h, o, f] L2).
+#h #o #G #L1 #L2 @eq_repl_sym /2 width=3 by lsubsx_eq_repl_back/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lcosx_O *)
+lemma lsubsx_refl: ∀h,o,f,G. 𝐈⦃f⦄ → reflexive … (lsubsx h o G f).
+#h #o #f #G #Hf #L elim L -L
+/3 width=3 by lsubsx_eq_repl_back, lsubsx_push, eq_push_inv_isid/
+qed.
+
+(* Basic_2A1: removed theorems 2:
+ lcosx_drop_trans_lt lcosx_inv_succ
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/lfsx_drops.ma".
+include "basic_2/rt_computation/lfsx_lfpxs.ma".
+include "basic_2/rt_computation/lsubsx.ma".
+
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+
+(* Properties with strong normalizing env's for uncounted rt-transition *****)
+
+(* Basic_2A1: uses: lsx_cpx_trans_lcosx *)
+lemma lfsx_cpx_trans_lsubsx: ∀h,o,G,L0,T1,T2. ⦃G, L0⦄ ⊢ T1 ⬈[h] T2 →
+ ∀f,L. G ⊢ L0 ⊆ⓧ[h, o, f] L →
+ G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
+#h #o #G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2 //
+[ #I0 #G #K0 #V1 #V2 #W2 #_ #IH #HVW2 #g #L #HK0 #HL
+ elim (lsubsx_inv_pair_sn_gen … HK0) -HK0 *
+ [ #f #K #HK0 #H1 #H2 destruct
+ /4 width=8 by lfsx_lifts, lfsx_fwd_pair, drops_refl, drops_drop/
+ | #f #K #HV1 #HK0 #H1 #H2 destruct
+ /4 width=8 by lfsx_lifts, drops_refl, drops_drop/
+ ]
+| #I0 #G #K0 #T #U #i #_ #IH #HTU #g #L #HK0 #HL
+ elim (lsubsx_fwd_bind_sn … HK0) -HK0 #I #K #HK0 #H destruct
+ /6 width=8 by lfsx_inv_lifts, lfsx_lifts, drops_refl, drops_drop/
+| #p #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
+ elim (lfsx_inv_bind … HL) -HL
+ /4 width=2 by lsubsx_pair, lfsx_bind_void/
+| #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
+ elim (lfsx_inv_flat … HL) -HL /3 width=2 by lfsx_flat/
+| #G #L0 #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #f #L #HL0 #HL
+ elim (lfsx_inv_bind … HL) -HL #HV #HU1
+ /4 width=8 by lsubsx_pair, lfsx_inv_lifts, drops_refl, drops_drop/
+| #G #L0 #V #T1 #T2 #_ #IHT12 #f #L #HL0 #HL
+ elim (lfsx_inv_flat … HL) -HL /2 width=2 by/
+| #G #L0 #V1 #V2 #T #_ #IHV12 #f #L #HL0 #HL
+ elim (lfsx_inv_flat … HL) -HL /2 width=2 by/
+| #p #G #L0 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #f #L #HL0 #HL
+ elim (lfsx_inv_flat … HL) -HL #HV1 #HL
+ elim (lfsx_inv_bind … HL) -HL #HW1 #HT1
+ /4 width=2 by lsubsx_pair, lfsx_bind_void, lfsx_flat/
+| #p #G #L0 #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #HVU2 #f #L #HL0 #HL
+ elim (lfsx_inv_flat … HL) -HL #HV1 #HL
+ elim (lfsx_inv_bind … HL) -HL #HW1 #HT1
+ /6 width=8 by lsubsx_pair, lfsx_lifts, lfsx_bind_void, lfsx_flat, drops_refl, drops_drop/
+]
+qed-.
+
+(* Basic_2A1: uses: lsx_cpx_trans_O *)
+lemma lfsx_cpx_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
+ G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
+/3 width=6 by lfsx_cpx_trans_lsubsx, lsubsx_refl/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/lsubsx.ma".
+
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+
+(* Main properties **********************************************************)
+
+theorem lsubsx_fix: ∀h,o,f,G,L1,L. G ⊢ L1 ⊆ⓧ[h, o, f] L →
+ ∀L2. G ⊢ L ⊆ⓧ[h, o, f] L2 → L = L2.
+#h #o #f #G #L1 #L #H elim H -f -L1 -L
+[ #f #L2 #H
+ >(lsubsx_inv_atom_sn … H) -L2 //
+| #f #I #K1 #K2 #_ #IH #L2 #H
+ elim (lsubsx_inv_push_sn … H) -H /3 width=1 by eq_f2/
+| #f #I #K1 #K2 #_ #IH #L2 #H
+ elim (lsubsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/
+| #f #I #K1 #K2 #V #_ #_ #IH #L2 #H
+ elim (lsubsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/
+]
+qed-.
+
+theorem lsubsx_trans: ∀h,o,f,G. Transitive … (lsubsx h o G f).
+#h #o #f #G #L1 #L #H1 #L2 #H2
+<(lsubsx_fix … H1 … H2) -L2 //
+qed-.
csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma
csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma
lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma
+lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma
}
]
[ { "strongly normalizing rt-computation" * } {
- [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ]
[ "llsx_csx" * ]
[ "csx_fpbs" * ]
}
[ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
}
]
-*)
+*)
[ { "uncounted context-sensitive rt-computation" * } {
+ [ "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
[ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
projects / helm.git / commitdiff