From 93768d9ebc0e3c8e3bcd69571d7a635cb1a16b29 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 27 Jul 2018 20:50:11 +0200
Subject: [PATCH] update in basic_2
+ refinement for native validity (lsubv)
allows to prove cnv_cpm_trans_lpr_aux (rt-confluence implies validity)
---
.../dynamic/{cnv_lpr.ma => cnv_cpm_trans.ma} | 65 +++++------
.../lambdadelta/basic_2/dynamic/cnv_etc.ma | 17 ++-
.../lambdadelta/basic_2/dynamic/lsubv.ma | 103 ++++++++++++++++++
.../lambdadelta/basic_2/dynamic/lsubv_cnv.ma | 37 +++++++
.../lambdadelta/basic_2/dynamic/lsubv_cpcs.ma | 25 +++++
.../lambdadelta/basic_2/dynamic/lsubv_cpms.ma | 25 +++++
.../basic_2/dynamic/lsubv_drops.ma | 70 ++++++++++++
.../basic_2/dynamic/lsubv_lsuba.ma | 33 ++++++
.../basic_2/dynamic/lsubv_lsubr.ma | 25 +++++
.../lambdadelta/basic_2/dynamic/partial.txt | 3 +-
.../lsubsv.ma => etc/lsubsv/lsubsv.etc} | 0
.../lsubsv/lsubsv_cpcs.etc} | 0
.../lsubsv/lsubsv_lstas.etc} | 0
.../lsubsv/lsubsv_lsuba.etc} | 0
.../lsubsv/lsubsv_lsubd.etc} | 0
.../lsubsv/lsubsv_scpds.etc} | 0
.../lsubsv/lsubsv_snv.etc} | 0
.../shnv/nativevalid_6.etc} | 0
.../{dynamic/shnv.ma => etc/shnv/shnv.etc} | 0
.../basic_2/notation/relations/lrsubeqv_5.ma | 4 +-
.../lambdadelta/basic_2/web/basic_2_src.tbl | 13 +--
21 files changed, 364 insertions(+), 56 deletions(-)
rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{cnv_lpr.ma => cnv_cpm_trans.ma} (75%)
create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma
create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma
create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma
create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma
create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma
rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv.ma => etc/lsubsv/lsubsv.etc} (100%)
rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_cpcs.ma => etc/lsubsv/lsubsv_cpcs.etc} (100%)
rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_lstas.ma => etc/lsubsv/lsubsv_lstas.etc} (100%)
rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_lsuba.ma => etc/lsubsv/lsubsv_lsuba.etc} (100%)
rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_lsubd.ma => etc/lsubsv/lsubsv_lsubd.etc} (100%)
rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_scpds.ma => etc/lsubsv/lsubsv_scpds.etc} (100%)
rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_snv.ma => etc/lsubsv/lsubsv_snv.etc} (100%)
rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/nativevalid_6.ma => etc/shnv/nativevalid_6.etc} (100%)
rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/shnv.ma => etc/shnv/shnv.etc} (100%)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
similarity index 75%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
index 4a87a4c3d..2d9f53b9c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
@@ -16,13 +16,9 @@ include "basic_2/rt_computation/cpms_fpbg.ma".
include "basic_2/rt_computation/cprs_cprs.ma".
include "basic_2/rt_computation/lprs_cpms.ma".
include "basic_2/dynamic/cnv_drops.ma".
-(*
-include "basic_2/dynamic/snv_aaa.ma".
-*)
include "basic_2/dynamic/cnv_etc.ma".
-(*
-include "basic_2/dynamic/lsubsv_snv.ma".
-*)
+include "basic_2/dynamic/lsubv_cnv.ma".
+
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
(* Properties with context-free parallel reduction for local environments *****)
@@ -32,10 +28,10 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = â» â
(âG1,L1,T1. â¦G0, L0, T0⦠>[h, o] â¦G1, L1, T1⦠â IH_cnv_cpms_conf_lpr a h G1 L1 T1) â
(âG1,L1,T1. â¦G0, L0, T0⦠>[h, o] â¦G1, L1, T1⦠â IH_cnv_cpm_trans_lpr a h G1 L1 T1) â
âG1,L1,T1. G0 = G1 â L0 = L1 â T0 = T1 â IH_cnv_cpm_trans_lpr a h G1 L1 T1.
-#a #h #o #Ha #G0 #L0 #T0 (* #IH4 #IH3 *) #IH2 #IH1 #G1 #L1 * * [|||| * ]
-[ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct (* -IH4 -IH3 *) -IH2 -IH1 -H1
+#a #h #o #Ha #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+[ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct -IH2 -IH1 -H1
elim (cpm_inv_sort1 ⦠H2) -H2 * #H1 #H2 destruct //
-| #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2
+| #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2
elim (cnv_inv_lref_drops ⦠H1) -H1 #I #K1 #V1 #HLK1 #HV1
elim (lpr_drops_conf ⦠HLK1 ⦠HL12) -HL12 // #Y #H #HLK2
elim (lpr_inv_pair_sn ⦠H) -H #K2 #V2 #HK12 #HV12 #H destruct
@@ -49,9 +45,9 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = â» â
lapply (drops_mono ⦠H ⦠HLK1) -HLK1 -H #H destruct
lapply (drops_isuni_fwd_drop2 ⦠HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/
]
-| #l #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2 -IH1
+| #l #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 -IH1
elim (cnv_inv_gref ⦠H1)
-| #p #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2
+| #p #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2
elim (cnv_inv_bind ⦠H1) -H1 #HV1 #HT1
elim (cpm_inv_bind1 ⦠H2) -H2 *
[ #V2 #T2 #HV12 #HT12 #H destruct /4 width=9 by fqup_fpbg, cnv_bind, lpr_pair/
@@ -61,13 +57,13 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = â» â
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
elim (cnv_inv_appl ⦠H1) -H1 #n #p #W1 #U1 #Hn #HV1 #HT1 #HVW1 #HTU1
elim (cpm_inv_appl1 ⦠H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct (* -IH4 *)
+ [ #V2 #T2 #HV12 #HT12 #H destruct
lapply (IH1 ⦠HV12 ⦠HL12) /2 width=1 by fqup_fpbg/ #HV2
lapply (IH1 ⦠HT12 ⦠HL12) /2 width=1 by fqup_fpbg/ #HT2
- elim (IH2 ⦠HVW1 ⦠V2 ⦠L2 ⦠L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV12
+ elim (cnv_cpms_strip_lpr_far ⦠IH2 ⦠HVW1 ⦠HV12 ⦠HL12 ⦠HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
<minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
- elim (IH2 ⦠HTU1 ⦠T2 ⦠L2 ⦠L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HTU1 -HT12
- #X #H #HTU2 (* -IH3 *) -IH2 -IH1 -L1 -V1 -T1
+ elim (cnv_cpms_strip_lpr_far ⦠IH2 ⦠HTU1 ⦠HT12 ⦠HL12 ⦠HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
+ #X #H #HTU2 -IH2 -IH1 -L1 -V1 -T1
elim (cpms_inv_abst_sn ⦠H) -H #W2 #U2 #HW12 #_ #H destruct
elim (cprs_conf ⦠HXW1 ⦠HW12) -W1 #W1 #HXW1 #HW21
lapply (cpms_trans ⦠HXV2 ⦠HXW1) -XW1 <plus_n_O #HV2W1
@@ -80,32 +76,25 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = â» â
lapply (IH1 ⦠HV12 ⦠HL12) /2 width=1 by fqup_fpbg/ #HV2
lapply (IH1 ⦠HW120 ⦠HL12) /2 width=1 by fqup_fpbg/ #HW20
lapply (IH1 ⦠HT10 ⦠HT120 ⦠(L2.âW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 -HT120 #HT20
- elim (IH2 ⦠HVW1 ⦠V2 ⦠L2 ⦠L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV12
+ elim (cnv_cpms_strip_lpr_far ⦠IH2 ⦠HVW1 ⦠HV12 ⦠HL12 ⦠HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
<minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
- elim (IH2 ⦠HW130 ⦠W20 ⦠L2 ⦠L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HW130 -HW120
- <minus_n_O #XW30 #HXW30 #HW230
+ elim (cnv_cpms_strip_lpr_far ⦠IH2 ⦠HW130 ⦠HW120 ⦠HL12 ⦠HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HW130 -HW120
+ <minus_n_O #XW30 #HXW30 #HW230 -IH2 -IH1 -L1 -V1 -W10 -T10
elim (cprs_conf ⦠HXW1 ⦠HXW30) -W30 #W30 #HXW1 #HXW30
lapply (cpms_trans ⦠HXV2 ⦠HXW1) -XW1 <plus_n_O #HV2W30
lapply (cprs_trans ⦠HW230 ⦠HXW30) -XW30 #HW230
- @cnv_bind [ /2 width=3 by cnv_cast/ ]
-(*
- @(lsubsv_snv_trans ⦠HT20) -HT20
- @(lsubsv_beta ⦠(d-1)) //
- @shnv_cast [1,2: // ] #d0 #Hd0
- lapply (scpes_le_aux ⦠IH4 IH1 IH2 IH3 ⦠HW20d ⦠HV2d ⦠d0 ⦠HVW20) -IH4 -IH3 -IH2 -IH1 -HW20d -HV2d -HVW20
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
-*)
- | #q #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct (* -IH4 *)
+ /5 width=4 by lsubv_cnv_trans, lsubv_beta, cnv_cast, cnv_bind/
+ | #q #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct
elim (cnv_inv_bind ⦠HT1) -HT1 #HW0 #HT0
elim (cpms_inv_abbr_abst ⦠HTU1) -HTU1 #X #HTU0 #HX #H destruct
elim (lifts_inv_bind1 ⦠HX) -HX #W3 #U3 #HW13 #_ #H destruct
lapply (IH1 ⦠HW02 ⦠HL12) /2 width=1 by fqup_fpbg/ #HW2
lapply (IH1 ⦠HV10 ⦠HL12) /2 width=1 by fqup_fpbg/ #HV0
lapply (IH1 ⦠HT02 (L2.âW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ #HT2
- elim (IH2 ⦠HVW1 ⦠V0 ⦠L2 ⦠L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV10
+ elim (cnv_cpms_strip_lpr_far ⦠IH2 ⦠HVW1 ⦠HV10 ⦠HL12 ⦠HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV10
<minus_n_O <minus_O_n #XW1 #HXW1 #HXV0
- elim (IH2 ⦠HTU0 ⦠T2 ⦠(L2.âW2) ⦠(L2.âW2)) [|*: /2 width=2 by fqup_fpbg, cpm_cpms, lpr_pair/ ] -HT02 -HTU0 -HW02
- #X #H #HTU2 -IH2 -IH1
+ elim (cnv_cpms_strip_lpr_far ⦠IH2 ⦠HTU0 ⦠HT02 ⦠(L2.âW2) ⦠(L2.âW2)) [|*: /2 width=2 by fqup_fpbg, lpr_pair/ ] -HTU0 -HT02 -HW02
+ #X #H #HTU2 -IH2 -IH1 -L1 -W0 -T0 -U1
elim (cpms_inv_abst_sn ⦠H) -H #W #U2 #HW3 #_ #H destruct -U3
lapply (cnv_lifts ⦠HV0 (â) ⦠(L2.âW2) ⦠HV02) /3 width=1 by drops_refl, drops_drop/ -HV0 #HV2
elim (cpms_lifts_sn ⦠HXV0 (â) ⦠(L2.âW2) ⦠HV02) /3 width=1 by drops_refl, drops_drop/ -V0 #XW2 #HXW12 #HXVW2
@@ -113,30 +102,28 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = â» â
elim (cprs_conf ⦠HXW32 ⦠HW3) -W3 #W3 #HXW23 #HW3
lapply (cpms_trans ⦠HXVW2 ⦠HXW23) -XW2 <plus_n_O #H1
lapply (cpms_trans ⦠HTU2 ? (â{p}W3.U2) ?) [3:|*:/2 width=2 by cpms_bind/ ] -W #H2
- @cnv_bind // @(cnv_appl ⦠H1 H2) // #H destruct
+ @cnv_bind // @(cnv_appl ⦠H1 H2) // #H destruct
]
-| #W1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 *)
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
elim (cnv_inv_cast ⦠H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
elim (cpm_inv_cast1 ⦠H2) -H2
[ * #W2 #T2 #HW12 #HT12 #H destruct
lapply (IH1 ⦠HW12 ⦠HL12) /2 width=1 by fqup_fpbg/ #HW2
lapply (IH1 ⦠HT12 ⦠HL12) /2 width=1 by fqup_fpbg/ #HT2
- lapply (cnv_cpms_trans_lpr_aux ⦠IH1 ⦠HTU1 L1 ?) /2 width=1 by fqup_fpbg/ #HU1
- elim (IH2 ⦠HWU1 ⦠W2 ⦠L1 ⦠HL12) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HW12
+ lapply (cnv_cpms_trans_lpr_far ⦠IH1 ⦠HTU1 L1 ?) /2 width=1 by fqup_fpbg/ #HU1
+ elim (cnv_cpms_strip_lpr_far ⦠IH2 ⦠HWU1 ⦠HW12 ⦠L1 ⦠HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HW12
<minus_n_O <minus_O_n #XW1 #HXUW1 #HXW21
- elim (IH2 ⦠HTU1 ⦠T2 ⦠L1 ⦠HL12) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HTU1 -HT12
+ elim (cnv_cpms_strip_lpr_far ⦠IH2 ⦠HTU1 ⦠HT12 ⦠L1 ⦠HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
#XT1 #HXUT1 #HXT21
elim (IH2 ⦠HXUW1 ⦠HXUT1 ⦠HL12 ⦠HL12) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ] -HXUW1 -HXUT1 -HWU1
- >eq_minus_O // #W0 #H1 #H2
+ >eq_minus_O // #W0 #H1 #H2 -IH2 -IH1 -L1 -W1 -T1 -U1
lapply (cprs_trans ⦠HXW21 ⦠H1) -XW1 #H1
lapply (cpms_trans ⦠HXT21 ⦠H2) -XT1 <arith_l #H2
/2 width=3 by cnv_cast/
- | #HX (* -IH3 *) -IH2 -HW1 -U1
+ | #HX -IH2 -HW1 -U1
lapply (IH1 ⦠HX ⦠HL12) /2 width=1 by fqup_fpbg/
| * #n #HX #H destruct -IH2 -HT1 -U1
lapply (IH1 ⦠HX ⦠HL12) /2 width=1 by fqup_fpbg/
]
]
-(*
qed-.
-*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma
index c2e0809f8..d7ac516cd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma
@@ -48,16 +48,23 @@ definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term â
âL1. â¦G, L0⦠⢠â¡[h] L1 â âL2. â¦G, L0⦠⢠â¡[h] L2 â
ââT. â¦G, L1⦠⢠T1 â¡*[n2-n1,h] T & â¦G, L2⦠⢠T2 â¡*[n1-n2,h] T.
-(* Auxiliary properties for preservation ************************************)
+(* Properties for preservation **********************************************)
-fact cnv_cpms_trans_lpr_aux (a) (h) (o):
- âG0,L0,T0.
- (âG1,L1,T1. â¦G0, L0, T0⦠>[h, o] â¦G1, L1, T1⦠â IH_cnv_cpm_trans_lpr a h G1 L1 T1) â
- âG1,L1,T1. â¦G0, L0, T0⦠>[h, o] â¦G1, L1, T1⦠â IH_cnv_cpms_trans_lpr a h G1 L1 T1.
+lemma cnv_cpms_trans_lpr_far (a) (h) (o):
+ âG0,L0,T0.
+ (âG1,L1,T1. â¦G0, L0, T0⦠>[h, o] â¦G1, L1, T1⦠â IH_cnv_cpm_trans_lpr a h G1 L1 T1) â
+ âG1,L1,T1. â¦G0, L0, T0⦠>[h, o] â¦G1, L1, T1⦠â IH_cnv_cpms_trans_lpr a h G1 L1 T1.
#a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
@(cpms_ind_dx ⦠H) -n -T2
/4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/
qed-.
+
+lemma cnv_cpms_strip_lpr_far (a) (h) (o):
+ âG0,L0,T0.
+ (âG1,L1,T1. â¦G0, L0, T0⦠>[h, o] â¦G1, L1, T1⦠â IH_cnv_cpms_conf_lpr a h G1 L1 T1) â
+ âG1,L1,T1. â¦G0, L0, T0⦠>[h, o] â¦G1, L1, T1⦠â IH_cnv_cpms_strip_lpr a h G1 L1 T1.
+/3 width=8 by cpm_cpms/ qed-.
+
(*
fact cnv_cpms_strip_lpr_aux (a) (h) (o):
âG0,L0,T0.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
new file mode 100644
index 000000000..bba857ac8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
@@ -0,0 +1,103 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/lrsubeqv_5.ma".
+include "basic_2/dynamic/cnv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Note: this is not transitive *)
+inductive lsubv (a) (h) (G): relation lenv â
+| lsubv_atom: lsubv a h G (â) (â)
+| lsubv_bind: âI,L1,L2. lsubv a h G L1 L2 â lsubv a h G (L1.â{I}) (L2.â{I})
+| lsubv_beta: âL1,L2,W,V. â¦G, L1⦠⢠âW.V ![a,h] â â¦G, L2⦠⢠W ![a,h] â
+ lsubv a h G L1 L2 â lsubv a h G (L1.ââW.V) (L2.âW)
+.
+
+interpretation
+ "local environment refinement (native validity)"
+ 'LRSubEqV a h G L1 L2 = (lsubv a h G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubv_inv_atom_sn_aux (a) (h) (G): âL1,L2. G ⢠L1 â«![a,h] L2 â L1 = â â L2 = â.
+#a #h #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #_ #H destruct
+| #L1 #L2 #W #V #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_atom1 *)
+lemma lsubv_inv_atom_sn (a) (h) (G): âL2. G ⢠â â«![a,h] L2 â L2 = â.
+/2 width=6 by lsubv_inv_atom_sn_aux/ qed-.
+
+fact lsubv_inv_bind_sn_aux (a) (h) (G): âL1,L2. G ⢠L1 â«![a,h] L2 â
+ âI,K1. L1 = K1.â{I} â
+ â¨â¨ ââK2. G ⢠K1 â«![a,h] K2 & L2 = K2.â{I}
+ | ââK2,W,V. â¦G, K1⦠⢠âW.V ![a,h] & â¦G, K2⦠⢠W ![a,h] &
+ G ⢠K1 â«![a,h] K2 &
+ I = BPair Abbr (âW.V) & L2 = K2.âW.
+#a #h #G #L1 #L2 * -L1 -L2
+[ #J #K1 #H destruct
+| #I #L1 #L2 #HL12 #J #K1 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #HWV #HW #HL12 #J #K1 #H destruct /3 width=8 by ex5_3_intro, or_intror/
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_pair1 *)
+lemma lsubv_inv_bind_sn (a) (h) (G): âI,K1,L2. G ⢠K1.â{I} â«![a,h] L2 â
+ â¨â¨ ââK2. G ⢠K1 â«![a,h] K2 & L2 = K2.â{I}
+ | ââK2,W,V. â¦G, K1⦠⢠âW.V ![a,h] & â¦G, K2⦠⢠W ![a,h] &
+ G ⢠K1 â«![a,h] K2 &
+ I = BPair Abbr (âW.V) & L2 = K2.âW.
+/2 width=3 by lsubv_inv_bind_sn_aux/ qed-.
+
+fact lsubv_inv_atom_dx_aux (a) (h) (G): âL1,L2. G ⢠L1 â«![a,h] L2 â L2 = â â L1 = â.
+#a #h #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #_ #H destruct
+| #L1 #L2 #W #V #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_atom2 *)
+lemma lsubv_inv_atom2 (a) (h) (G): âL1. G ⢠L1 â«![a,h] â â L1 = â.
+/2 width=6 by lsubv_inv_atom_dx_aux/ qed-.
+
+fact lsubv_inv_bind_dx_aux (a) (h) (G): âL1,L2. G ⢠L1 â«![a,h] L2 â
+ âI,K2. L2 = K2.â{I} â
+ â¨â¨ ââK1. G ⢠K1 â«![a,h] K2 & L1 = K1.â{I}
+ | ââK1,W,V. â¦G, K1⦠⢠âW.V ![a,h] & â¦G, K2⦠⢠W ![a,h] &
+ G ⢠K1 â«![a,h] K2 & I = BPair Abst W & L1 = K1.ââW.V.
+#a #h #G #L1 #L2 * -L1 -L2
+[ #J #K2 #H destruct
+| #I #L1 #L2 #HL12 #J #K2 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #HWV #HW #HL12 #J #K2 #H destruct /3 width=8 by ex5_3_intro, or_intror/
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_pair2 *)
+lemma lsubv_inv_bind_dx (a) (h) (G): âI,L1,K2. G ⢠L1 â«![a,h] K2.â{I} â
+ â¨â¨ ââK1. G ⢠K1 â«![a,h] K2 & L1 = K1.â{I}
+ | ââK1,W,V. â¦G, K1⦠⢠âW.V ![a,h] & â¦G, K2⦠⢠W ![a,h] &
+ G ⢠K1 â«![a,h] K2 & I = BPair Abst W & L1 = K1.ââW.V.
+/2 width=3 by lsubv_inv_bind_dx_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: uses: lsubsv_refl *)
+lemma lsubv_refl (a) (h) (G): reflexive ⦠(lsubv a h G).
+#a #h #G #L elim L -L /2 width=1 by lsubv_atom, lsubv_bind/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma
new file mode 100644
index 000000000..b1782a021
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/dynamic/lsubv_cpms.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with native validity **************************************)
+
+(* Basic_2A1: uses: lsubsv_snv_trans *)
+lemma lsubv_cnv_trans (a) (h) (G):
+ âL2,T. â¦G, L2⦠⢠T ![a,h] â
+ âL1. G ⢠L1 â«![a,h] L2 â â¦G, L1⦠⢠T ![a,h].
+#a #h #G #L2 #T #H elim H -G -L2 -T //
+[ #I #G #K2 #V #HV #IH #L1 #H
+ elim (lsubv_inv_bind_dx ⦠H) -H * /3 width=1 by cnv_zero/
+| #I #G #K2 #i #_ #IH #L1 #H
+ elim (lsubv_inv_bind_dx ⦠H) -H * /3 width=1 by cnv_lref/
+| #p #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12
+ /4 width=1 by cnv_bind, lsubv_bind/
+| #n #p #G #L2 #V #W #T #U #Ha #_ #_ #HVW #HTU #IHV #IHT #L1 #HL
+ /4 width=10 by lsubv_cpms_trans, cnv_appl/
+| #G #L2 #U #T #U0 #_ #_ #HU0 #HTU0 #IHU #IHT #L1 #HL12
+ /4 width=6 by lsubv_cpms_trans, cnv_cast/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma
new file mode 100644
index 000000000..c02ec80b0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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_equivalence/cpcs_lsubr.ma".
+include "basic_2/dynamic/lsubv_lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with context-sensitive r-equivalence for terms ************)
+
+(* Basic_2A1: uses: lsubsv_cprs_trans *)
+lemma lsubv_cpcs_trans (a) (h) (G): lsub_trans ⦠(cpcs h G) (lsubv a h G).
+/3 width=6 by lsubv_fwd_lsubr, lsubr_cpcs_trans/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma
new file mode 100644
index 000000000..81d385add
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/cpms_lsubr.ma".
+include "basic_2/dynamic/lsubv_lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with t-bound contex-sensitive rt-computation for terms ****)
+
+(* Basic_2A1: uses: lsubsv_cprs_trans lsubsv_scpds_trans *)
+lemma lsubv_cpms_trans (a) (n) (h) (G): lsub_trans ⦠(λL. cpms h G L n) (lsubv a h G).
+/3 width=6 by lsubv_fwd_lsubr, lsubr_cpms_trans/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
new file mode 100644
index 000000000..90b59cba0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
@@ -0,0 +1,70 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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 "static_2/relocation/drops.ma".
+include "basic_2/dynamic/lsubv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Note: the premise ðâ¦f⦠cannot be removed *)
+(* Basic_2A1: includes: lsubsv_drop_O1_conf *)
+lemma lsubv_drops_conf_isuni (a) (h) (G):
+ âL1,L2. G ⢠L1 â«![a,h] L2 â
+ âb,f,K1. ðâ¦f⦠â â¬*[b,f] L1 â K1 â
+ ââK2. G ⢠K1 â«![a,h] K2 & â¬*[b,f] L2 â K2.
+#a #h #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #HL12 #IH #b #f #K1 #Hf #H
+ elim (drops_inv_bind1_isuni ⦠Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by lsubv_bind, drops_refl, ex2_intro/
+ | #g #Hg #HLK1 #H destruct -HL12
+ elim (IH ⦠Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
+ ]
+| #L1 #L2 #W #V #HVW #HW #HL12 #IH #b #f #K1 #Hf #H
+ elim (drops_inv_bind1_isuni ⦠Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
+ | #g #Hg #HLK1 #H destruct -HL12
+ elim (IH ⦠Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
+ ]
+]
+qed-.
+
+(* Note: the premise ðâ¦f⦠cannot be removed *)
+(* Basic_2A1: includes: lsubsv_drop_O1_trans *)
+lemma lsubv_drops_trans_isuni (a) (h) (G):
+ âL1,L2. G ⢠L1 â«![a,h] L2 â
+ âb,f,K2. ðâ¦f⦠â â¬*[b,f] L2 â K2 â
+ ââK1. G ⢠K1 â«![a,h] K2 & â¬*[b,f] L1 â K1.
+#a #h #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #HL12 #IH #b #f #K2 #Hf #H
+ elim (drops_inv_bind1_isuni ⦠Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by lsubv_bind, drops_refl, ex2_intro/
+ | #g #Hg #HLK2 #H destruct -HL12
+ elim (IH ⦠Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
+ ]
+| #L1 #L2 #W #V #HWV #HW #HL12 #IH #b #f #K2 #Hf #H
+ elim (drops_inv_bind1_isuni ⦠Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
+ | #g #Hg #HLK2 #H destruct -HL12
+ elim (IH ⦠Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
+ ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma
new file mode 100644
index 000000000..ac03aa297
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/dynamic/cnv_aaa.ma".
+include "basic_2/dynamic/lsubv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with lenv refinement for atomic arity assignment **********)
+
+(* Basic_2A1: uses: lsubsv_fwd_lsuba *)
+lemma lsubsv_fwd_lsuba (a) (h) (G): âL1,L2. G ⢠L1 â«![a,h] L2 â G ⢠L1 â«â L2.
+#a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_bind/
+#L1 #L2 #W #V #H #_ #_ #IH
+elim (cnv_inv_cast ⦠H) -H #W0 #HW #HV #HW0 #HVW0
+elim (cnv_fwd_aaa ⦠HW) -HW #B #HW
+elim (cnv_fwd_aaa ⦠HV) -HV #A #HV
+lapply (cpms_aaa_conf ⦠HW ⦠HW0) -HW0 #H
+lapply (cpms_aaa_conf ⦠HV ⦠HVW0) -HVW0 #HW0
+lapply (aaa_mono ⦠H ⦠HW0) -W0 #H destruct
+/4 width=5 by lsuba_aaa_conf, lsuba_beta, aaa_cast/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma
new file mode 100644
index 000000000..938c116c5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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 "static_2/static/lsubr.ma".
+include "basic_2/dynamic/lsubv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with restricted refinement for local environments *********)
+
+(* Basic_2A1: uses: lsubsv_fwd_lsubr *)
+lemma lsubv_fwd_lsubr (a) (h) (G): âL1,L2. G ⢠L1 â«![a,h] L2 â L1 â« L2.
+#a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_beta/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt
index 87d2cd592..ad9b95be0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt
@@ -1,2 +1,3 @@
cnv.ma cnv_drops.ma cnv_fqus.ma cnv_aaa.ma cnv_fsb.ma
-cnv_etc.ma cnv_lpr.ma
+cnv_etc.ma cnv_cpm_trans.ma
+lsubv.ma lsubv_drops.ma lsubv_lsubr.ma lsubv_lsuba.ma lsubv_cpms.ma lsubv_cpcs.ma lsubv_cnv.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_cpcs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_cpcs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lstas.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lstas.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsuba.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsuba.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsubd.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsubd.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_scpds.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_scpds.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_scpds.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/shnv/nativevalid_6.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/shnv/nativevalid_6.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/shnv/shnv.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/shnv/shnv.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
index 78eeb36a2..ff9313322 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
@@ -14,6 +14,6 @@
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⢠break term 46 L1 ⫠¡ [ break term 46 h, break term 46 o ] break term 46 L2 )"
+notation "hvbox( G ⢠break term 46 L1 â«![ break term 46 a, break term 46 h ] break term 46 L2 )"
non associative with precedence 45
- for @{ 'LRSubEqV $h $o $G $L1 $L2 }.
+ for @{ 'LRSubEqV $a $h $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index e6a1ea5d3..1c19f4e3a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -28,16 +28,10 @@ table {
[ [ "" ] "nta ( �,?⦠⢠? : ? )" "nta_alt ( �,?⦠⢠? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
}
]
- [ { "local env. ref. for stratified native validity" * } {
- [ [ "" ] "lsubsv ( ? ⢠? â«Â¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
- }
- ]
-*)
- [ { "context-sensitive native validity" * } {
-(*
- [ [ "" ] "shnv ( �,?⦠⢠? ¡[?,?,?] )" * ]
*)
- [ [ "for terms" ] "cnv" + "( �,?⦠⢠? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" (* + "snv_lpr" + "snv_scpes" + "snv_preserve" *) * ]
+ [ { "context-sensitive native validity" * } {
+ [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⢠? â«![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" * ]
+ [ [ "for terms" ] "cnv" + "( �,?⦠⢠? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "snv_cpm_trans" (* + "snv_scpes" + "snv_preserve" *) * ]
}
]
}
@@ -127,6 +121,7 @@ class "capitalize italic" { 0 1 }
class "italic" { 2 }
(*
+ [ [ "" ] "shnv ( �,?⦠⢠? ¡[?,?,?] )" * ]
[ { "decomposed rt-equivalence" * } {
[ [ "" ] "scpes ( â¦?,?⦠⢠? â¢*â¬*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
}
--
2.39.2