(∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
/5 width=1 by lfdeq_sym, SN_intro/ qed.
-(*
+
+(* Basic_2A1: was: lsx_sort *)
lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄.
#h #o #G #L1 #s @lfsx_intro
#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H *
[ #H1 #H2 destruct //
-| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
- @lfdeq_sort
+| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
+ /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort_gen, frees_inv_sort/
+]
qed.
-lemma lfsx_gref: ∀h,o,G,L,l,p. G ⊢ ⬈*[h, o, §p, l] L.
-#h #o #G #L1 #l #p @lfsx_intro
-#L2 #HL12 #H elim H -H
-/3 width=4 by lfpx_fwd_length, lfdeq_gref/
+(* Basic_2A1: was: lsx_gref *)
+lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄.
+#h #o #G #L1 #s @lfsx_intro
+#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_gref … H) -H *
+[ #H1 #H2 destruct //
+| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
+ /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref_gen, frees_inv_gref/
+]
qed.
-(* Basic forward lemmas *****************************************************)
-
-lemma lfsx_fwd_bind_sn: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L →
- G ⊢ ⬈*[h, o, V, l] L.
-#h #o #a #I #G #L #V #T #l #H @(lfsx_ind … H) -L
-#L1 #_ #IHL1 @lfsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=4 by lfdeq_fwd_bind_sn/
-qed-.
-
-lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
- G ⊢ ⬈*[h, o, V, l] L.
-#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
-#L1 #_ #IHL1 @lfsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/
-qed-.
-
-lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
- G ⊢ ⬈*[h, o, T, l] L.
-#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
-#L1 #_ #IHL1 @lfsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/
-qed-.
-
-lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L →
- G ⊢ ⬈*[h, o, V, l] L.
-#h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
- G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L.
-/3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-.
-
-(* Basic_2A1: removed theorems 5:
- lsx_atom lsx_sort lsx_gref lsx_ge_up lsx_ge
-*)
+(* Basic_2A1: removed theorems 2:
+ lsx_ge_up lsx_ge
*)
--- /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/lfdeq_lfdeq.ma".
+include "basic_2/rt_transition/lfpx_lfdeq.ma".
+include "basic_2/rt_computation/lfsx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+
+axiom pippo: ∀h,o,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 →
+ ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L & L ≡[h, o, V] L2.
+
+(* Advanced properties ******************************************************)
+
+lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L2. L1 ≡[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
+#h #o #G #L1 #T #H @(lfsx_ind … H) -L1
+#L1 #_ #IHL1 #L2 #HL12 @lfsx_intro
+#L #HL2 #HnL2 elim (lfdeq_lfpx_trans … HL2 … HL12) -HL2
+/4 width=5 by lfdeq_repl/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+(* Basic_2A1: was: lsx_fwd_bind_sn *)
+lemma lfsx_fwd_bind_sn: ∀h,o,p,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ →
+ G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄.
+#h #o #p #I #G #L #V #T #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #H #HnL12 elim (pippo … o p I … T H) -H
+/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_bind_sn/
+qed-.
+(*
+lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+ G ⊢ ⬈*[h, o, V, l] L.
+#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/
+qed-.
+
+lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+ G ⊢ ⬈*[h, o, T, l] L.
+#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/
+qed-.
+
+lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L →
+ G ⊢ ⬈*[h, o, V, l] L.
+#h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+ G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L.
+/3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-.
+*)
\ No newline at end of file
theorem lfdeq_canc_dx: ∀h,o,T. right_cancellable … (lfdeq h o T).
/3 width=3 by lfdeq_trans, lfdeq_sym/ qed-.
+theorem lfdeq_repl: ∀h,o,L1,L2. ∀T:term. L1 ≡[h, o, T] L2 →
+ ∀K1. L1 ≡[h, o, T] K1 → ∀K2. L2 ≡[h, o, T] K2 → K1 ≡[h, o, T] K2.
+/3 width=3 by lfdeq_canc_sn, lfdeq_trans/ qed-.
+
(* Advanced properies on negated lazy equivalence *****************************)
(* Note: auto works with /4 width=8/ so lfdeq_canc_sn is preferred ************)
#R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/
qed-.
+lemma lfxs_isid: ∀R1,R2,L1,L2,T1,T2.
+ (∀f. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → 𝐈⦃f⦄) →
+ (∀f. 𝐈⦃f⦄ → L1 ⊢ 𝐅*⦃T2⦄ ≡ f) →
+ L1 ⦻*[R1, T1] L2 → L1 ⦻*[R2, T2] L2.
+#R1 #R2 #L1 #L2 #T1 #T2 #H1 #H2 *
+/4 width=7 by lexs_co_isid, ex2_intro/
+qed-.
+
(* Basic inversion lemmas ***************************************************)
lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⦻*[R, T] Y2 → Y2 = ⋆.
[ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
[ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ]
*)
+ [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfsx" * ]
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
[ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ]
projects / helm.git / commitdiff