--- /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/lreq_lreq.ma".
+include "basic_2/static/lfxs_drops.ma".
+include "basic_2/i_static/tc_lfxs.ma".
+
+(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
+
+definition tc_dedropable_sn: predicate (relation3 lenv term term) ≝
+ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 →
+ ∀K2,T. K1 ⦻**[R, T] K2 → ∀U. ⬆*[f] T ≡ U →
+ ∃∃L2. L1 ⦻**[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2.
+
+definition tc_dropable_sn: predicate (relation3 lenv term term) ≝
+ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ →
+ ∀L2,U. L1 ⦻**[R, U] L2 → ∀T. ⬆*[f] T ≡ U →
+ ∃∃K2. K1 ⦻**[R, T] K2 & ⬇*[b, f] L2 ≡ K2.
+
+definition tc_dropable_dx: predicate (relation3 lenv term term) ≝
+ λR. ∀L1,L2,U. L1 ⦻**[R, U] L2 →
+ ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U →
+ ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻**[R, T] K2.
+
+(* Properties with generic slicing for local environments *******************)
+
+lemma dedropable_sn_LTC: ∀R. dedropable_sn R → tc_dedropable_sn R.
+#R #HR #b #f #L1 #K1 #HLK1 #K2 #T #H elim H -K2
+[ #K2 #HK12 #U #HTU elim (HR … HLK1 … HK12 … HTU) -K1 -T -HR
+ /3 width=4 by ex3_intro, inj/
+| #K #K2 #_ #HK2 #IH #U #HTU -HLK1
+ elim (IH … HTU) -IH #L #HL1 #HLK
+ elim (HR … HLK … HK2 … HTU) -K -T -HR
+ /3 width=6 by lreq_trans, tc_lfxs_step_dx, ex3_intro/
+]
+qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+lemma dropable_sn_LTC: ∀R. dropable_sn R → tc_dropable_sn R.
+#R #HR #b #f #L1 #K1 #HLK1 #Hf #L2 #U #H elim H -L2
+[ #L2 #HL12 #T #HTU elim (HR … HLK1 … HL12 … HTU) -L1 -U -HR
+ /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IH #T #HTU -HLK1
+ elim (IH … HTU) -IH #K #HK1 #HLK
+ elim (HR … HLK … HL2 … HTU) -L -U -HR
+ /3 width=3 by tc_lfxs_step_dx, ex2_intro/
+]
+qed-.
+
+lemma dropable_dx_LTC: ∀R. dropable_dx R → tc_dropable_dx R.
+#R #HR #L1 #L2 #U #H elim H -L2
+[ #L2 #HL12 #b #f #K2 #HLK2 #Hf #T #HTU
+ elim (HR … HL12 … HLK2 … HTU) -L2 -U -HR
+ /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IH #b #f #K2 #HLK2 #Hf #T #HTU
+ elim (HR … HL2 … HLK2 … HTU) -L2 -HR // #K #HLK #HK2
+ elim (IH … HLK … HTU) -IH -L -U
+ /3 width=5 by tc_lfxs_step_dx, ex2_intro/
+]
+qed-.
(* Properties with atomic arity assignment on terms *************************)
-lemma cpxs_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
- ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-#h #G #L #T1 #A #HT1 #T2 #HT12
-@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by cpx_aaa_conf/
+lemma cpxs_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpxs h G L).
+#h #G #L @TC_Conf3 @cpx_aaa_conf (**) (* auto fails *)
qed-.
--- /dev/null
+lemma lprs_aaa_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/3 width=5 by lprs_lpxs, lpxs_aaa_conf/ qed-.
--- /dev/null
+(* Basic_2A1: was just: lprs_lpxs *)
+lemma lprs_lfpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2.
+/3 width=3 by lpr_lpx, monotonic_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/rt_transition/lfpx_aaa.ma".
+include "basic_2/rt_computation/lfpxs.ma".
+
+(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+
+(* Properties with atomic arity assignment on terms **************************)
+
+(* Basic_2A1: uses: lpxs_aaa_conf *)
+lemma lfpxs_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpxs h G T).
+#h #G #T @TC_Conf3 @lfpx_aaa_conf (**) (* auto fails *)
+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/i_static/tc_lfxs_drops.ma".
+include "basic_2/rt_transition/lfpx_drops.ma".
+
+(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_2A1: uses: drop_lpxs_trans *)
+lemma drops_lfpxs_trans: ∀h,G. tc_dedropable_sn (cpx h G).
+/3 width=5 by drops_lfpx_trans, dedropable_sn_LTC/ qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_2A1: uses: lpxs_drop_conf *)
+lemma lfpxs_drops_conf: ∀h,G. tc_dropable_sn (cpx h G).
+/3 width=5 by lfpx_drops_conf, dropable_sn_LTC/ qed-.
+
+(* Basic_2A1: uses: lpxs_drop_trans_O1 *)
+lemma lfpxs_drops_trans: ∀h,G. tc_dropable_dx (cpx h G).
+/3 width=5 by lfpx_drops_trans, dropable_dx_LTC/ qed-.
+++ /dev/null
-(* Basic_2A1: was just: lprs_lpxs *)
-lemma lprs_lfpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2.
-/3 width=3 by lpr_lpx, monotonic_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/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 lpxs_aaa_conf: ∀h,o,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
- ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-#h #o #G #L1 #T #A #HT #L2 #HL12
-@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by lpx_aaa_conf/
-qed-.
-
-lemma lprs_aaa_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
- ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-/3 width=5 by lprs_lpxs, lpxs_aaa_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/reduction/lpx_drop.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* Properties on local environment slicing ***********************************)
-
-lemma lpxs_drop_conf: ∀h,o,G. dropable_sn (lpxs h o G).
-/3 width=3 by dropable_sn_TC, lpx_drop_conf/ qed-.
-
-lemma drop_lpxs_trans: ∀h,o,G. dedropable_sn (lpxs h o G).
-/3 width=3 by dedropable_sn_TC, drop_lpx_trans/ qed-.
-
-lemma lpxs_drop_trans_O1: ∀h,o,G. dropable_dx (lpxs h o G).
-/3 width=3 by dropable_dx_TC, lpx_drop_trans_O1/ qed-.
cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
-lfpxs.ma lfpxs_length.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma
+lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma
csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma
lfsx.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma
(* Properties with atomic arity assignment for terms ************************)
-lemma cpr_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
- ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+lemma cpr_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpm 0 h G L).
/3 width=5 by cpx_aaa_conf, cpm_fwd_cpx/ qed-.
-lemma lfpr_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+(* Basic_2A1: uses: lpr_aaa_conf *)
+lemma lfpr_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpr h G T).
/3 width=4 by lfpx_aaa_conf, lfpr_fwd_lfpx/ qed-.
]
qed-.
-lemma cpx_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
- ∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+lemma cpx_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpx h G L).
/2 width=6 by cpx_aaa_conf_lfpx/ qed-.
-lemma lfpx_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
- ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+(* Basic_2A1: uses: lpx_aaa_conf *)
+lemma lfpx_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpx h G T).
/2 width=6 by cpx_aaa_conf_lfpx/ qed-.
[ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "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_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
- [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
+ [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
[ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
]
class "water"
[ { "iterated static typing" * } {
[ { "iterated extension on referred entries" * } {
- [ "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
+ [ "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
}
]
}
projects / helm.git / commitdiff