From 947126ce0618ffdfc39cdc7e198c1edbf3b1a926 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 16 May 2013 14:35:06 +0000
Subject: [PATCH] - some renaming - finally we issue the "dynamic" component
---
.../lambdadelta/apps_2/functional/notation.ma | 4 +
.../basic_2/dynamic/lsubsv_dxprs.ma | 16 +-
.../lambdadelta/basic_2/dynamic/lsubsv_snv.ma | 8 +-
.../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 119 +++++++------
.../lambdadelta/basic_2/dynamic/snv_lpr.ma | 140 +++++++++++++++
.../lambdadelta/basic_2/dynamic/snv_ssta.ma | 7 +-
.../basic_2/dynamic/snv_ssta_lpr.ma | 126 ++++++++++++++
.../lambdadelta/basic_2/dynamic/yprs.ma | 4 +-
.../basic_2/equivalence/cpcs_cpcs.ma | 6 +-
.../lambdadelta/basic_2/etc/fpr/fpc.etc | 8 +
.../lambdadelta/basic_2/etc/fpr/fpcs.etc | 8 +
.../lambdadelta/basic_2/etc/lpc/lfpc.etc | 4 +
.../lambdadelta/basic_2/etc/lpc/lfpcs.etc | 4 +
.../basic_2/etc/preservation/snv_cpcs.etc | 161 ++++++++++++++++++
.../preservation/snv_ltpr.etc} | 0
.../preservation/snv_ssta_ltpr.etc} | 0
.../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +-
17 files changed, 544 insertions(+), 73 deletions(-)
create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc
rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/snv_ltpr.ma => etc/preservation/snv_ltpr.etc} (100%)
rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/snv_ssta_ltpr.ma => etc/preservation/snv_ssta_ltpr.etc} (100%)
diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma
index 1c60d6c18..f830afff1 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma
@@ -14,6 +14,10 @@
(* NOTATION FOR THE "functional" COMPONENT ********************************)
+notation "hvbox( T . break ⣠{ term 46 I } break { term 46 T1 , break term 46 T2 , break term 46 T3 } )"
+ non associative with precedence 50
+ for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
+
notation "hvbox( â [ term 46 d , break term 46 e ] break term 46 T )"
non associative with precedence 46
for @{ 'Lift $d $e $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma
index 9666bffdd..04af871fe 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma
@@ -19,9 +19,9 @@ include "basic_2/dynamic/lsubsv_ssta.ma".
(* Properties for the preservation results **********************************)
-fact sstas_lsubsv_aux: âh,g,L0,T0.
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
+fact lsubsv_sstas_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_lsubsv h g L1 T1) â
âL2,T. h ⢠â¦L0, T0⦠>[g] â¦L2, T⦠â â¦h, L2⦠⢠T ¡[g] â
@@ -35,14 +35,14 @@ lapply (snv_sstas_aux ⦠IH2 ⦠HTU2) // #H
lapply (IH1 ⦠H ⦠HL12) [ /3 width=4 by ygt_yprs_trans, sstas_yprs/ ] -H #HU2
elim (snv_fwd_ssta ⦠HU1) #l1 #W1 #HUW1
elim (lsubsv_ssta_trans ⦠HU2W ⦠HL12) -HU2W #W2 #HUW2 #HW2
-elim (ssta_ltpr_cpcs_aux ⦠IH4 IH3 ⦠HU1 HU2 ⦠HUW1 ⦠HUW2 ⦠HU12) -HU1 -HU2 -HUW2 -HU12 //
+elim (ssta_cpcs_lpr_aux ⦠IH4 IH3 ⦠HU1 HU2 ⦠HUW1 ⦠HUW2 ⦠HU12 L1) -HU1 -HU2 -HUW2 -HU12 //
[2,3: /4 width=4 by ygt_yprs_trans, sstas_yprs, lsubsv_yprs/ ] -L2 -L0 -T0 -U2 #H #HW12 destruct
lapply (cpcs_trans ⦠HW12 ⦠HW2) -W2 /3 width=4/
qed-.
-fact dxprs_lsubsv_aux: âh,g,L0,T0.
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
+fact lsubsv_dxprs_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_lsubsv h g L1 T1) â
âL2,T1. h ⢠â¦L0, T0⦠>[g] â¦L2, T1⦠â â¦h, L2⦠⢠T1 ¡[g] â
@@ -50,7 +50,7 @@ fact dxprs_lsubsv_aux: âh,g,L0,T0.
ââT. â¦h, L1⦠⢠T1 â¢*â¡*[g] T & L1 ⢠T2 â¡* T.
#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2
lapply (lsubsv_cprs_trans ⦠HL12 ⦠HTT2) -HTT2 #HTT2
-elim (sstas_lsubsv_aux ⦠IH4 IH3 IH2 IH1 ⦠HLT0 ⦠HL12 ⦠HT1T) // -L2 -L0 -T0 #T0 #HT10 #HT0
+elim (lsubsv_sstas_aux ⦠IH4 IH3 IH2 IH1 ⦠HLT0 ⦠HL12 ⦠HT1T) // -L2 -L0 -T0 #T0 #HT10 #HT0
lapply (cpcs_cprs_strap1 ⦠HT0 ⦠HTT2) -T #HT02
elim (cpcs_inv_cprs ⦠HT02) -HT02 /3 width=3/
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
index 1482dd986..896875371 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
@@ -22,8 +22,8 @@ include "basic_2/dynamic/lsubsv_cpcs.ma".
(* Properties concerning stratified native validity *************************)
fact snv_lsubsv_aux: âh,g,L0,T0.
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_lsubsv h g L1 T1) â
âL1,T1. L0 = L1 â T0 = T1 â IH_snv_lsubsv h g L1 T1.
@@ -45,8 +45,8 @@ fact snv_lsubsv_aux: âh,g,L0,T0.
lapply (lsubsv_cprs_trans ⦠HL12 ⦠HW0) -HW0 #HW0
elim (lsubsv_ssta_trans ⦠HVW ⦠HL12) -HVW #W1 #HVW1 #HW1
lapply (cpcs_cprs_strap1 ⦠HW1 ⦠HW0) -W #HW10
- elim (dxprs_lsubsv_aux ⦠IH4 IH3 IH2 IH1 ⦠HL12 ⦠HTU) -IH4 -IH3 -IH2 -HTU // /2 width=1/ #X #HTU #H
- elim (cprs_inv_abst1 Abst W0 ⦠H) -H #W #U2 #HW0 #HU2 #H destruct
+ elim (lsubsv_dxprs_aux ⦠IH4 IH3 IH2 IH1 ⦠HL12 ⦠HTU) -IH4 -IH3 -IH2 -HTU // /2 width=1/ #X #HTU #H
+ elim (cprs_fwd_abst1 ⦠H Abst W0) -H #W #U2 #HW0 #HU2 #H destruct
lapply (cpcs_cprs_strap1 ⦠HW10 ⦠HW0) -W0 #H
elim (cpcs_inv_cprs ⦠H) -H #W0 #HW10 #HW0
lapply (dxprs_cprs_trans ⦠(â{a}W0.U2) HTU ?) [ /2 width=1/ ] -HTU -HW0
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
index 643bf6569..f00ae1832 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
@@ -29,11 +29,11 @@ definition IH_ssta_cpr_lpr: âh:sh. sd h â relation2 lenv term â
λh,g,L1,T1. â¦h, L1⦠⢠T1 ¡[g] â
âU1,l. â¦h, L1⦠⢠T1 â¢[g] â¦l, U1⦠â
âT2. L1 ⢠T1 â¡ T2 â âL2. L1 ⢠⡠L2 â
- ââU2. â¦h, L2⦠⢠T2 â¢[g] â¦l, U2⦠& L1 ⢠U1 â¬* U2.
+ ââU2. â¦h, L2⦠⢠T2 â¢[g] â¦l, U2⦠& L2 ⢠U1 â¬* U2.
definition IH_snv_ssta: âh:sh. sd h â relation2 lenv term â
- λh,g,L1,T1. â¦h, L1⦠⢠T1 ¡[g] â
- âU1,l. â¦h, L1⦠⢠T1 â¢[g] â¦l+1, U1⦠â â¦h, L1⦠⢠U1 ¡[g].
+ λh,g,L,T. â¦h, L⦠⢠T ¡[g] â
+ âU,l. â¦h, L⦠⢠T â¢[g] â¦l+1, U⦠â â¦h, L⦠⢠U ¡[g].
definition IH_snv_lsubsv: âh:sh. sd h â relation2 lenv term â
λh,g,L2,T. â¦h, L2⦠⢠T ¡[g] â
@@ -55,41 +55,51 @@ fact ssta_cprs_lpr_aux: âh,g,L0,T0.
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
âU1,l. â¦h, L1⦠⢠T1 â¢[g] â¦l, U1⦠â
- âT2. L1 ⢠T1 â¡* T2 â âL2. L1 ⢠⡠L2 â
- ââU2. â¦h, L2⦠⢠T2 â¢[g] â¦l, U2⦠& L1 ⢠U1 â¬* U2.
+ âT2. L1 ⢠T1 â¡* T2 â âL2. L1 ⢠⡠L2 â
+ ââU2. â¦h, L2⦠⢠T2 â¢[g] â¦l, U2⦠& L2 ⢠U1 â¬* U2.
#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #T2 #H
-elim H -T2 [ /2 width=5/ ]
+elim H -T2 [ /2 width=7/ ]
#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
elim (IHT1 L1) // -IHT1 #U #HTU #HU1
-elim (IH1 ⦠HTU ⦠HTT2 ⦠HL12) -IH1 -HTU -HTT2 -HL12
+elim (IH1 ⦠HTU ⦠HTT2 ⦠HL12) -IH1 -HTU -HTT2
[2: /3 width=9 by snv_cprs_lpr_aux/
|3: /5 width=6 by ygt_yprs_trans, cprs_yprs/
] -L0 -T0 -T1 -T #U2 #HTU2 #HU2
+lapply (cpcs_lpr_conf ⦠HL12 ⦠HU1) -L1 #HU1
lapply (cpcs_trans ⦠HU1 ⦠HU2) -U /2 width=3/
qed-.
-fact ssta_cpcs_aux: âh,g,L0,T0.
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
- âL,T1,T2. h ⢠â¦L0, T0⦠>[g] â¦L, T1⦠â h ⢠â¦L0, T0⦠>[g] â¦L, T2⦠â
- â¦h, L⦠⢠T1 ¡[g] â â¦h, L⦠⢠T2 ¡[g] â
- âU1,l1. â¦h, L⦠⢠T1 â¢[g] â¦l1, U1⦠â
- âU2,l2. â¦h, L⦠⢠T2 â¢[g] â¦l2, U2⦠â
- L ⢠T1 â¬* T2 â l1 = l2 ⧠L ⢠U1 â¬* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L #T1 #T2 #HLT01 #HLT02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H
+fact ssta_cpcs_lpr_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
+ âL1,T1,T2. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â h ⢠â¦L0, T0⦠>[g] â¦L1, T2⦠â
+ â¦h, L1⦠⢠T1 ¡[g] â â¦h, L1⦠⢠T2 ¡[g] â
+ âU1,l1. â¦h, L1⦠⢠T1 â¢[g] â¦l1, U1⦠â
+ âU2,l2. â¦h, L1⦠⢠T2 â¢[g] â¦l2, U2⦠â
+ L1 ⢠T1 â¬* T2 â âL2. L1 ⢠⡠L2 â
+ l1 = l2 ⧠L2 ⢠U1 â¬* U2.
+#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #T2 #H01 #H02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H #L2 #HL12
elim (cpcs_inv_cprs ⦠H) -H #T #H1 #H2
-elim (ssta_cprs_lpr_aux ⦠HLT01 HT1 ⦠HTU1 ⦠H1 L) -T1 // /2 width=1/ #W1 #H1 #HUW1
-elim (ssta_cprs_lpr_aux ⦠HLT02 HT2 ⦠HTU2 ⦠H2 L) -T2 // /2 width=1/ #W2 #H2 #HUW2 -L0 -T0
+elim (ssta_cprs_lpr_aux ⦠H01 HT1 ⦠HTU1 ⦠H1 ⦠HL12) -T1 /2 width=1/ #W1 #H1 #HUW1
+elim (ssta_cprs_lpr_aux ⦠H02 HT2 ⦠HTU2 ⦠H2 ⦠HL12) -T2 /2 width=1/ #W2 #H2 #HUW2 -L0 -T0
elim (ssta_mono ⦠H1 ⦠H2) -h -T #H1 #H2 destruct
lapply (cpcs_canc_dx ⦠HUW1 ⦠HUW2) -W2 /2 width=1/
qed-.
fact snv_sstas_aux: âh,g,L0,T0.
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
- âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
- âU1. â¦h, L1⦠⢠T1 â¢*[g] U1 â â¦h, L1⦠⢠U1 ¡[g].
-#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H
-@(sstas_ind ⦠H) -U1 // -HT1 /4 width=5 by ygt_yprs_trans, sstas_yprs/
+ âL,T. h ⢠â¦L0, T0⦠>[g] â¦L, T⦠â â¦h, L⦠⢠T ¡[g] â
+ âU. â¦h, L⦠⢠T â¢*[g] U â â¦h, L⦠⢠U ¡[g].
+#h #g #L0 #T0 #IH #L #T #H01 #HT #U #H
+@(sstas_ind ⦠H) -U // -HT /4 width=5 by ygt_yprs_trans, sstas_yprs/
+qed-.
+
+fact snv_sstas_lpr_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
+ âL1,T. h ⢠â¦L0, T0⦠>[g] â¦L1, T⦠â â¦h, L1⦠⢠T ¡[g] â
+ âU. â¦h, L1⦠⢠T â¢*[g] U â âL2. L1 ⢠⡠L2 â â¦h, L2⦠⢠U ¡[g].
+/4 width=7 by snv_sstas_aux, ygt_yprs_trans, sstas_yprs/
qed-.
fact sstas_cprs_lpr_aux: âh,g,L0,T0.
@@ -97,45 +107,50 @@ fact sstas_cprs_lpr_aux: âh,g,L0,T0.
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
- âT2. L1 ⢠T1 â¡* T2 â âU1. â¦h, L1⦠⢠T1 â¢*[g] U1 â âL2. L1 ⢠⡠L2 â
- ââU2. â¦h, L2⦠⢠T2 â¢*[g] U2 & L1 ⢠U1 â¬* U2.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #L2 #HL12 #T2 #HT12 #U1 #H
-@(sstas_ind ⦠H) -U1 [ /3 width=3/ ]
-#U1 #W1 #l1 #HTU1 #HUW1 * #U2 #HTU2 #HU12
-lapply (snv_ltpr_cprs_aux ⦠IH2 ⦠HT1 ⦠HT12) // #HT2
+ âU1. â¦h, L1⦠⢠T1 â¢*[g] U1 â âT2. L1 ⢠T1 â¡* T2 â âL2. L1 ⢠⡠L2 â
+ ââU2. â¦h, L2⦠⢠T2 â¢*[g] U2 & L2 ⢠U1 â¬* U2.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #H
+@(sstas_ind ⦠H) -U1 [ /3 width=5 by cprs_lpr_conf, ex2_intro/ ]
+#U1 #W1 #l1 #HTU1 #HUW1 #IHTU1 #T2 #HT12 #L2 #HL12
+elim (IHTU1 ⦠HT12 ⦠HL12) -IHTU1 #U2 #HTU2 #HU12
+lapply (snv_cprs_lpr_aux ⦠IH2 ⦠HT1 ⦠HT12 ⦠HL12) // #HT2
elim (snv_sstas_fwd_correct ⦠HTU2) // #W2 #l2 #HUW2
-elim (ssta_ltpr_cpcs_aux ⦠IH2 IH1 ⦠HUW1 ⦠HUW2 ⦠HU12) -IH2 -IH1 -HUW1 -HU12 //
-[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, ltpr_cprs_yprs/
-|3: /3 width=7 by snv_sstas_aux, ygt_yprs_trans, cprs_yprs/
-|4: /4 width=5 by ygt_yprs_trans, ltpr_cprs_yprs, sstas_yprs/
-|5: /3 width=4 by ygt_yprs_trans, cprs_yprs, sstas_yprs/
-] -L0 -T0 -T1 -HT2 #H #HW12 destruct /3 width=4/
+elim (IH1 ⦠HUW1 U1 ⦠HL12) -HUW1 //
+[2: /3 width=7 by snv_sstas_aux/
+|3: /3 width=4 by ygt_yprs_trans, sstas_yprs/
+] #W #HU1W #HW1
+elim (ssta_cpcs_lpr_aux ⦠IH2 IH1 ⦠HU1W ⦠HUW2 ⦠HU12 L2) // -IH1 -HU1W -HU12
+[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, cprs_lpr_yprs/
+|3: /3 width=10 by snv_sstas_lpr_aux/
+|4,5: /4 width=5 by ygt_yprs_trans, cprs_lpr_yprs, sstas_yprs/
+] -L0 -T0 -L1 -T1 -HT2 #H #HW12 destruct
+lapply (cpcs_trans ⦠HW1 ⦠HW12) -W /3 width=4/
qed-.
-fact dxprs_ltpr_cprs_aux: âh,g,L0,T0.
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
- âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
- âU1. â¦h, L1⦠⢠T1 â¢*â¡*[g] U1 â
- âL2. L1 â¡ L2 â âT2. L2 ⢠T1 â¡* T2 â
- ââU2. â¦h, L2⦠⢠T2 â¢*â¡*[g] U2 & L2 ⢠U1 â¡* U2.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #L2 #HL12 #T2 #HT12
-elim (sstas_ltpr_cprs_aux ⦠IH3 IH2 IH1 ⦠H01 ⦠HT12 ⦠HTW1) // -L0 -T0 -T1 #W2 #HTW2 #HW12
-lapply (ltpr_cprs_conf ⦠HL12 ⦠HWU1) -L1 #HWU1
+fact dxprs_cprs_lpr_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
+ âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
+ âU1. â¦h, L1⦠⢠T1 â¢*â¡*[g] U1 â
+ âT2. L1 ⢠T1 â¡* T2 â âL2. L1 ⢠⡠L2 â
+ ââU2. â¦h, L2⦠⢠T2 â¢*â¡*[g] U2 & L2 ⢠U1 â¡* U2.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
+elim (sstas_cprs_lpr_aux ⦠IH3 IH2 IH1 ⦠H01 ⦠HTW1 ⦠HT12 ⦠HL12) // -L0 -T0 -T1 #W2 #HTW2 #HW12
+lapply (cprs_lpr_conf ⦠HL12 ⦠HWU1) -L1 #HWU1
lapply (cpcs_canc_sn ⦠HW12 HWU1) -W1 #H
elim (cpcs_inv_cprs ⦠H) -H /3 width=3/
qed-.
fact ssta_dxprs_aux: âh,g,L0,T0.
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
- âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
- âl,U1. â¦h, L1⦠⢠T1 â¢[g] â¦l+1, U1⦠â âT2. â¦h, L1⦠⢠T1 â¢*â¡*[g] T2 â
- ââU,U2. â¦h, L1⦠⢠U1 â¢*[g] U & â¦h, L1⦠⢠T2 â¢*[g] U2 & L1 ⢠U â¬* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
+ âL,T1. h ⢠â¦L0, T0⦠>[g] â¦L, T1⦠â â¦h, L⦠⢠T1 ¡[g] â
+ âl,U1. â¦h, L⦠⢠T1 â¢[g] â¦l+1, U1⦠â âT2. â¦h, L⦠⢠T1 â¢*â¡*[g] T2 â
+ ââU,U2. â¦h, L⦠⢠U1 â¢*[g] U & â¦h, L⦠⢠T2 â¢*[g] U2 & L ⢠U â¬* U2.
+#h #g #L0 #T0 #IH2 #IH1 #L #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2
elim (sstas_strip ⦠HT1T ⦠HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ]
-[ elim (ssta_ltpr_cprs_aux ⦠IH2 IH1 ⦠HTU1 L1 ⦠HTT2) // -L0 -T0 -T /3 width=5/
+[ elim (ssta_cprs_lpr_aux ⦠IH2 IH1 ⦠HTU1 ⦠HTT2 L) // -L0 -T0 -T /3 width=5/
| @(ex3_2_intro â¦T2 HU1T) // /2 width=1/
]
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
new file mode 100644
index 000000000..44a77627c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
@@ -0,0 +1,140 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/dxprs_dxprs.ma".
+include "basic_2/dynamic/snv_lift.ma".
+include "basic_2/dynamic/snv_cpcs.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on context-free parallel reduction for local environments *****)
+
+fact snv_cpr_lpr_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_lsubsv h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
+ âL1,T1. L0 = L1 â T0 = T1 â IH_snv_cpr_lpr h g L1 T1.
+#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*]
+[ #k #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1
+ >(cpr_inv_sort1 ⦠H2) -X //
+| #i #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_lref ⦠H1) -H1 #I #K1 #V1 #HLK1 #HV1
+ elim (lpr_ldrop_conf ⦠HLK1 ⦠HL12) -HL12 #X #H #HLK2
+ elim (lpr_inv_pair1 ⦠H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ lapply (ldrop_pair2_fwd_fw ⦠HLK1 (#i)) #HKL
+ elim (cpr_inv_lref1 ⦠H2) -H2
+ [ #H destruct -HLK1
+ lapply (IH1 ⦠HV12 ⦠HK12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HKL /2 width=5/
+ | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12
+ lapply (ldrop_mono ⦠H ⦠HLK1) -HLK1 -H #H destruct
+ lapply (ldrop_fwd_ldrop2 ⦠HLK2) -HLK2 #HLK2
+ lapply (IH1 ⦠HVW0 ⦠HK12) -IH1 -HVW0 -HK12 // -HV1 [ /2 width=1/ ] -HKL /3 width=7/
+ ]
+| #p #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
+ elim (snv_inv_gref ⦠H1)
+| #a #I #V1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_bind ⦠H1) -H1 #HV1 #HT1
+ elim (cpr_inv_bind1 ⦠H2) -H2 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct
+ lapply (IH1 ⦠HV12 ⦠HL12) // -HV1 [ /2 width=1/ ] #HV2
+ lapply (IH1 ⦠HT12 (L2.â{I}V2) ?) // -IH1 /2 width=1/
+ | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
+ lapply (IH1 ⦠HT1 ⦠HT12 (L2.âV1) ?) -IH1 [1,2: /2 width=1/ ] -L1 -T1 #HT2
+ lapply (snv_inv_lift ⦠HT2 L2 ⦠HXT2) -T2 // /2 width=1/
+ ]
+| #V1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
+ elim (snv_inv_appl ⦠H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1
+ elim (cpr_inv_appl1 ⦠H2) -H2 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct -IH4
+ lapply (IH1 ⦠HV1 ⦠HV12 ⦠HL12) [ /2 width=1/ ] #HV2
+ lapply (IH1 ⦠HT1 ⦠HT12 ⦠HL12) [ /2 width=1/ ] #HT2
+ elim (IH3 ⦠HVW1 ⦠HV12 ⦠HL12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
+ elim (dxprs_cprs_lpr_aux ⦠IH2 IH1 IH3 ⦠HTU1 ⦠T2 ⦠HL12) // [2,3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #X #HTU2 #H
+ elim (cprs_fwd_abst1 ⦠H Abst W1) -H #W20 #U2 #HW120 #_ #H destruct
+ lapply (cprs_lpr_conf ⦠HL12 ⦠HW10) -L1 #HW10
+ lapply (cpcs_cprs_strap1 ⦠HW10 ⦠HW120) -W1 #HW120
+ lapply (cpcs_canc_sn ⦠HW12 HW120) -W10 #HW20
+ elim (cpcs_inv_cprs ⦠HW20) -HW20 #W0 #HW20 #HW200
+ lapply (dxprs_cprs_trans ⦠(â{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/
+ | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct
+ elim (snv_inv_bind ⦠HT1) -HT1 #HW20 #HT20
+ elim (dxprs_inv_abst1 ⦠HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
+ lapply (cprs_div ⦠HW10 ⦠HW230) -W30 #HW120
+ lapply (cpcs_lpr_conf ⦠HL12 ⦠HW120) -HW120 #HW120
+ elim (IH3 ⦠HVW1 ⦠HV12 ⦠HL12) // [2: /2 width=1/ ] -HVW1 #W2 #HVW2 #HW102
+ lapply (cpcs_canc_sn ⦠HW102 ⦠HW120) -W10 #HW220
+ lapply (IH1 ⦠HV12 ⦠HL12) // [ /2 width=1/ ] #HV2 -HV1
+ lapply (IH1 ⦠HW20 ⦠W20 ⦠HL12) // [ /2 width=1/ ] -HW20 #HW20
+ lapply (IH1 ⦠HT20 ⦠HT202 ⦠(L2.âW20) ?) [1,2: /2 width=1/ ] -HT20 #HT2
+ lapply (IH2 ⦠HVW2) //
+ [ @(ygt_yprs_trans ⦠L1 L1 ⦠V1) (**) (* auto /4 width=5/ is a bit slow even with trace *)
+ [ /2 width=1 by fw_ygt/
+ | /3 width=1 by cprs_lpr_yprs, cpr_cprs/
+ ]
+ ] #HW2
+ elim (snv_fwd_ssta ⦠HW20) #l0 #U20 #HWU20
+ elim (ssta_fwd_correct ⦠HVW2) <minus_plus_m_m #U2 #HWU2
+ elim (ssta_cpcs_lpr_aux ⦠IH1 IH3 ⦠HWU2 ⦠HWU20 ⦠HW220 ⦠L2) // -IH3
+ [2: /4 width=4 by ygt_yprs_trans, fw_ygt, ypr_yprs, ypr_lpr/
+ |3: @(ygt_yprs_trans ⦠L1 L2 ⦠V2) (**) (* auto not tried *)
+ [ @(ygt_yprs_trans ⦠L1 L1 ⦠V1)
+ [ /2 width=1 by fw_ygt/
+ | /3 width=1 by cprs_lpr_yprs, cpr_cprs/
+ ]
+ | /3 width=2 by ypr_ssta, ypr_yprs/
+ ]
+ ] #H #_ destruct -IH2 -U2
+ lapply (IH4 ⦠HT2 (L2.âV2) ?)
+ [ /2 width=6/
+ | @(ygt_yprs_trans ⦠(L1.âW20) ⦠T2) (**) (* auto /5 width=5/ is too slow even with trace timeout=35 *)
+ [ /4 width=4 by ygt_yprs_trans, fw_ygt, ypr_yprs, ypr_cpr/
+ | /4 width=1 by ypr_yprs, ypr_lpr, lpr_pair/
+ ]
+ ] -L1 -V1 -W2 -T20 -U20 -W20 -l0 /2 width=1/
+ | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4
+ elim (snv_inv_bind ⦠HT1) -HT1 #HW0 #HT0
+ elim (dxprs_inv_abbr_abst ⦠HTU1) -HTU1 #X #HTU0 #HX #H destruct
+ elim (lift_inv_bind1 ⦠HX) -HX #W3 #U3 #HW13 #_ #H destruct
+ lapply (cprs_lpr_conf ⦠HL12 ⦠HW10) -HW10 #HW10
+ elim (dxprs_cprs_lpr_aux ⦠IH2 IH1 IH3 ⦠HTU0 T2 ⦠(L2.âW2) ?) // [2,3,4: /2 width=1/ ] -IH2 -HTU0 #X #HTU2 #H
+ elim (cprs_fwd_abst1 ⦠H Abst W3) -H #W #U2 #HW1 #_ #H destruct -U3
+ elim (IH3 ⦠HVW1 ⦠HV10 ⦠HL12) // /2 width=1/ -IH3 -HVW1 #X #H1 #H2
+ lapply (cpcs_canc_sn ⦠H2 HW10) -W10 #H2
+ elim (lift_total X 0 1) #W20 #H3
+ lapply (ssta_lift ⦠H1 (L2.âW2) ⦠HV02 ⦠H3) /2 width=1/ -H1 #HVW20
+ lapply (cpcs_lift (L2.âW2) ⦠H3 ⦠HW13 H2) /2 width=1/ -HW13 -H3 -H2 #HW320
+ lapply (cpcs_cprs_strap1 ⦠HW320 ⦠HW1) -W3 #HW20
+ elim (cpcs_inv_cprs ⦠HW20) -HW20 #W3 #HW203 #HW3
+ lapply (dxprs_cprs_trans ⦠(â{a}W3.U2) HTU2 ?) [ /2 width=1/ ] -HW3 -HTU2 #HTU2
+ lapply (IH1 ⦠HW02 ⦠HL12) // [ /2 width=1/ ] -HW0 #HW2
+ lapply (IH1 ⦠HV10 ⦠HL12) // [ /2 width=1/ ] -HV1 -HV10 #HV0
+ lapply (IH1 ⦠HT02 (L2.âW2) ?) // [1,2: /2 width=1/ ] -L1 #HT2
+ lapply (snv_lift ⦠HV0 (L2.âW2) ⦠HV02) /2 width=1/ -HV0 -HV02 /3 width=8/
+ ]
+| #W1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH2
+ elim (snv_inv_cast ⦠H1) -H1 #U1 #l #HW1 #HT1 #HTU1 #HUW1
+ elim (cpr_inv_cast1 ⦠H2) -H2
+ [ * #W2 #T2 #HW12 #HT12 #H destruct
+ lapply (cpcs_cprs_strap1 ⦠HUW1 W2 ?) [ /2 width=1/ ] -HUW1 #H1
+ lapply (IH1 ⦠HW12 ⦠HL12) // /2 width=1/ -HW1 -HW12 #HW2
+ lapply (IH1 ⦠HT12 ⦠HL12) // /2 width=1/ -IH1 #HT2
+ elim (IH3 ⦠HTU1 ⦠HT12 ⦠HL12) // /2 width=1/ -IH3 -HT1 -HT12 -HTU1 #U2 #HTU2 #HU12
+ lapply (cpcs_lpr_conf ⦠HL12 ⦠H1) -L1 #H1
+ lapply (cpcs_canc_sn ⦠HU12 H1) -U1 /2 width=4/
+ | #H -IH3 -HW1 -HTU1 -HUW1
+ lapply (IH1 ⦠H ⦠HL12) // /2 width=1/
+ ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma
index f6d753d22..b656dbd54 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma
@@ -12,6 +12,7 @@
(* *)
(**************************************************************************)
+include "basic_2/dynamic/snv_lift.ma".
include "basic_2/dynamic/snv_cpcs.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
@@ -19,8 +20,8 @@ include "basic_2/dynamic/snv_cpcs.ma".
(* Properties on stratified static type assignment for terms ****************)
fact snv_ssta_aux: âh,g,L0,T0.
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
- (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
(âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
âL1,T1. L0 = L1 â T0 = T1 â IH_snv_ssta h g L1 T1.
#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [||||*]
@@ -44,7 +45,7 @@ fact snv_ssta_aux: âh,g,L0,T0.
elim (ssta_dxprs_aux ⦠IH3 IH2 ⦠HTU1 ⦠HT10) -IH3 -IH2 // /2 width=2/ -T1 #U #X #HU1U #H #HU0
elim (sstas_inv_bind1 ⦠H) -H #U0 #HTU0 #H destruct
elim (cpcs_inv_abst2 ⦠HU0) -HU0 #W2 #U2 #HU2 #HU02
- elim (cprs_inv_abst ⦠HU02 Abst W0) -HU02 #HW02 #_
+ elim (cprs_fwd_abst ⦠HU02 Abst W0) -HU02 #HW02 #_
lapply (cprs_trans ⦠HW10 ⦠HW02) -W0 /3 width=10 by snv_appl, ex2_intro/ (**) (* auto is too slow without trace *)
| #W1 #T1 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2
elim (snv_inv_cast ⦠H1) -H1 #U1 #l0 #HW1 #HT1 #HTU1 #HUW1
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
new file mode 100644
index 000000000..e03920285
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
@@ -0,0 +1,126 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/equivalence/lsubss_ssta.ma".
+include "basic_2/dynamic/snv_cpcs.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on sn parallel reduction for local environments ***************)
+
+fact ssta_cpr_lpr_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_cpr_lpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_cpr_lpr h g L1 T1) â
+ âL1,T1. L0 = L1 â T0 = T1 â IH_ssta_cpr_lpr h g L1 T1.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *]
+[ #k #_ #_ #_ #X2 #l #H2 #X3 #H3 #L2 #HL12 -IH3 -IH2 -IH1
+ elim (ssta_inv_sort1 ⦠H2) -H2 #Hkl #H destruct
+ >(cpr_inv_sort1 ⦠H3) -X3 /4 width=6/
+| #i #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+ elim (snv_inv_lref ⦠H1) -H1 #I0 #K0 #V0 #H #HV1
+ elim (ssta_inv_lref1 ⦠H2) -H2 * #K1
+ #V1 #W1 [| #l0 ] #HLK1 #HVW1 #HWU1 [| #H destruct ]
+ lapply (ldrop_mono ⦠H ⦠HLK1) -H #H destruct
+ lapply (ldrop_pair2_fwd_fw ⦠HLK1 (#i)) #HKV1
+ elim (lpr_ldrop_conf ⦠HLK1 ⦠HL12) -HL12 #X #H #HLK2
+ elim (lpr_inv_pair1 ⦠H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ lapply (ldrop_fwd_ldrop2 ⦠HLK2) #H2
+ elim (cpr_inv_lref1 ⦠H3) -H3
+ [1,3: #H destruct -HLK1
+ |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
+ lapply (ldrop_mono ⦠H ⦠HLK1) -H -HLK1 #H destruct
+ ]
+ [ elim (IH1 ⦠HVW1 ⦠HV12 ⦠HK12) -IH1 -HVW1 // [2: /2 width=1/ ] -K1 -V1 #W2 #HVW2 #HW12
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (cpcs_lift ⦠H2 ⦠HWU1 ⦠HWU2 HW12) -H2 -W1 /3 width=6/
+ | elim (IH1 ⦠HVW1 ⦠HV12 ⦠HK12) -IH1 -HVW1 // [2: /2 width=1/ ] #W2 #HVW2 #_
+ elim (lift_total V2 0 (i+1)) #U2 #HVU2
+ lapply (lpr_cpr_conf ⦠HK12 ⦠HV12) -HV12 #HV12
+ lapply (cpcs_lift ⦠H2 ⦠HWU1 ⦠HVU2 HV12) -H2 -V1 /3 width=6/
+ | elim (IH1 ⦠HVW1 ⦠HVW0 ⦠HK12) -IH1 -HVW1 // [2: /2 width=1/ ] -K1 -V1 #W2 #HVW2 #HW12
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (ssta_lift ⦠HVW2 ⦠H2 ⦠HW0 ⦠HWU2) -HVW2 -HW0
+ lapply (cpcs_lift ⦠H2 ⦠HWU1 ⦠HWU2 HW12) -H2 -W1 /3 width=6/
+ ]
+| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
+ elim (snv_inv_gref ⦠H1)
+| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+ elim (snv_inv_bind ⦠H1) -H1 #_ #HT1
+ elim (ssta_inv_bind1 ⦠H2) -H2 #U1 #HTU1 #H destruct
+ elim (cpr_inv_bind1 ⦠H3) -H3 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IH1 ⦠HTU1 ⦠HT12 (L2.â{I}V2)) // [2,3: /2 width=1/ ] -T1
+ lapply (lpr_cpr_conf ⦠HL12 ⦠HV12) -L1 /3 width=5/
+ | #T2 #HT12 #HT2 #H1 #H2 destruct
+ elim (IH1 ⦠HTU1 ⦠HT12 (L2.âV1)) -IH1 -HTU1 // [2,3: /2 width=1/ ] -T1 -HL12 #U2 #HTU2 #HU12
+ elim (ssta_inv_lift1 ⦠HTU2 ⦠HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2
+ lapply (cpcs_bind1 true ⦠V1 V1 ⦠HU12) // -HU12 #HU12
+ lapply (cpcs_cpr_strap1 ⦠HU12 U ?) -HU12 /2 width=3/
+ ]
+| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct
+ elim (snv_inv_appl ⦠H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10
+ elim (ssta_inv_appl1 ⦠H2) -H2 #U1 #HTU1 #H destruct
+ elim (cpr_inv_appl1 ⦠H3) -H3 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2
+ elim (IH1 ⦠HTU1 ⦠HT12 ⦠HL12) -IH1 -HTU1 // [2: /2 width=1/ ] -T1 #U2 #HTU2 #HU12
+ lapply (lpr_cpr_conf ⦠HL12 ⦠HV12) -L1 /3 width=5/
+ | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct
+ elim (snv_inv_bind ⦠HT1) -HT1 #HW #HT2
+ elim (ssta_inv_bind1 ⦠HTU1) -HTU1 #U2 #HTU2 #H destruct
+ elim (dxprs_inv_abst1 ⦠HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct
+ lapply (cprs_div ⦠HW10 ⦠HW0) -W0 #HW1W
+ elim (ssta_fwd_correct ⦠HVW1) <minus_plus_m_m #X1 #HWX1
+ elim (snv_fwd_ssta ⦠HW) #l1 #V #HWV
+ lapply (IH3 ⦠HVW1) -IH3 // [ /2 width=1/ ] #HW1
+ elim (ssta_cpcs_lpr_aux ⦠IH2 IH1 ⦠HWX1 ⦠HWV ⦠L1) -IH2 -HWX1 //
+ [2: /2 width=1/
+ |3: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
+ ] #H #_ destruct -X1
+ elim (IH1 ⦠HVW1 ⦠HV12 ⦠HL12) -HVW1 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
+ elim (IH1 ⦠HWV W ⦠HL12) -HWV // -HW [2: /2 width=1/ ] #V0 #HWV0 #_
+ elim (IH1 ⦠HTU2 ⦠HT20 (L2.âW)) -IH1 -HTU2 -HT20 // [2,3: /2 width=1/ ] -HT2 #U20 #HTU20 #HU20
+ lapply (cpcs_lpr_conf ⦠HL12 ⦠HW1W) #HW1W
+ lapply (lpr_cpr_conf ⦠HL12 ⦠HV12) -L1 #HV12
+ lapply (cpcs_ext_bind ⦠HV12 ⦠HU20 b Abbr) -HV12 -HU20 #HU20
+ lapply (cpcs_canc_sn ⦠HW12 HW1W) -W1 #HW2
+ elim (lsubss_ssta_trans ⦠HTU20 (L2.âV2) ?) -HTU20
+ [ #U #HTU20 #HUU20 -HWV0 -W2
+ lapply (cpcs_bind1 b ⦠V2 V2 ⦠HUU20) // -HUU20 #HUU20
+ lapply (cpcs_canc_dx ⦠HU20 ⦠HUU20) -U20 #HU2
+ lapply (cpcs_cpr_strap2 ⦠(âV1.â{b}W.U2) ⦠HU2) [ /2 width=1/ ] /3 width=3/
+ | -b -l -V -V1 -T2 -T20 -U0 -U2 -U20 /2 width=6/
+ ]
+ | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -l0 -W1 -W10 -HV1 -IH3 -IH2
+ elim (ssta_inv_bind1 ⦠HTU1) -HTU1 #U0 #HTU0 #H destruct
+ elim (snv_inv_bind ⦠HT1) -HT1 #_ #HT0
+ elim (IH1 ⦠HTU0 ⦠HT02 (L2.âW2)) -IH1 -HTU0 // [2,3: /2 width=1/ ] -T0 #U2 #HTU2 #HU02
+ lapply (lpr_cpr_conf ⦠HL12 ⦠HV10) -HV10 #HV10
+ lapply (lpr_cpr_conf ⦠HL12 ⦠HW02) -L1 #HW02
+ lapply (cpcs_bind2 b ⦠HW02 ⦠HU02) -HW02 -HU02 #HU02
+ lapply (cpcs_flat ⦠HV10 ⦠HU02 Appl) -HV10 -HU02 #HU02
+ lapply (cpcs_cpr_strap1 ⦠HU02 (â{b}W2.âV2.U2) ?) [ /2 width=3/ ] -V0 /4 width=3/
+ ]
+| #U0 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+ elim (snv_inv_cast ⦠H1) -H1 #T0 #l0 #_ #HT1 #HT10 #_
+ lapply (ssta_inv_cast1 ⦠H2) -H2 #HTU1
+ elim (ssta_mono ⦠HT10 ⦠HTU1) -HT10 #H1 #H2 destruct
+ elim (cpr_inv_cast1 ⦠H3) -H3
+ [ * #U2 #T2 #_ #HT12 #H destruct
+ elim (IH1 ⦠HTU1 ⦠HT12 ⦠HL12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 -U0 /3 width=3/
+ | #HT1X3
+ elim (IH1 ⦠HTU1 ⦠HT1X3 ⦠HL12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -U0 -T1 /2 width=3/
+ ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
index bb4daf0be..2bf1ae018 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
@@ -72,7 +72,7 @@ qed.
lemma lsubsv_yprs: âh,g,L1,L2,T. h ⢠L2 ¡â[g] L1 â h ⢠â¦L1, T⦠â¥[g] â¦L2, Tâ¦.
/3 width=1/ qed.
-lemma lpr_cprs_yprs: âh,g,L1,L2,T1,T2. L1 ⢠⡠L2 â L2 ⢠T1 â¡* T2 â
+lemma cprs_lpr_yprs: âh,g,L1,L2,T1,T2. L1 ⢠T1 â¡* T2 â L1 ⢠⡠L2 â
h ⢠â¦L1, T1⦠â¥[g] â¦L2, T2â¦.
-/3 width=4 by yprs_strap2, ypr_lpr, cprs_yprs/
+/3 width=4 by yprs_strap1, ypr_lpr, cprs_yprs/
qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
index 199e49b07..784c75470 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
@@ -211,13 +211,13 @@ qed.
(* Basic_1: was: pc3_wcpr0_t *)
(* Basic_1: note: pc3_wcpr0_t should be renamed *)
-lemma lpr_cprs_conf: âL1,L2. L1 ⢠⡠L2 â âT1,T2. L1 ⢠T1 â¡* T2 â L2 ⢠T1 â¬* T2.
+lemma cprs_lpr_conf: âL1,L2. L1 ⢠⡠L2 â âT1,T2. L1 ⢠T1 â¡* T2 â L2 ⢠T1 â¬* T2.
#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind ⦠H) -T2 //
/3 width=5 by cpcs_trans, lpr_cpr_conf/
qed-.
(* Basic_1: was: pc3_wcpr0 *)
-lemma lpr_cpcs_conf: âL1,L2. L1 ⢠⡠L2 â âT1,T2. L1 ⢠T1 â¬* T2 â L2 ⢠T1 â¬* T2.
+lemma cpcs_lpr_conf: âL1,L2. L1 ⢠⡠L2 â âT1,T2. L1 ⢠T1 â¬* T2 â L2 ⢠T1 â¬* T2.
#L1 #L2 #HL12 #T1 #T2 #H
-elim (cpcs_inv_cprs ⦠H) -H /3 width=5 by cpcs_canc_dx, lpr_cprs_conf/
+elim (cpcs_inv_cprs ⦠H) -H /3 width=5 by cpcs_canc_dx, cprs_lpr_conf/
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc
index f552d5818..ee362471b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc
@@ -12,6 +12,14 @@
(* *)
(**************************************************************************)
+notation "hvbox( ⦠term 46 L1 , break term 46 T1 ⦠⬠break ⦠term 46 L2 , break term 46 T2 ⦠)"
+ non associative with precedence 45
+ for @{ 'FocalizedPConv $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦠term 46 L1 , break term 46 T1 ⦠⬠⬠break ⦠term 46 L2 , break term 46 T2 ⦠)"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvAlt $L1 $T1 $L2 $T2 }.
+
include "basic_2/reducibility/fpr.ma".
(* CONTEXT-FREE PARALLEL CONVERSION ON CLOSURES *****************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc
index 45be26781..68c946ce8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc
@@ -12,6 +12,14 @@
(* *)
(**************************************************************************)
+notation "hvbox( ⦠term 46 L1 , break term 46 T1 ⦠⬠* break ⦠term 46 L2 , break term 46 T2 ⦠)"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStar $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦠term 46 L1 , break term 46 T1 ⦠⬠⬠* break ⦠term 46 L2 , break term 46 T2 ⦠)"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStarAlt $L1 $T1 $L2 $T2 }.
+
include "basic_2/conversion/fpc.ma".
(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
index 273873abd..b80b290b6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
@@ -12,6 +12,10 @@
(* *)
(**************************************************************************)
+notation "hvbox( ⦠term 46 L1 ⦠⬠⬠break ⦠term 46 L2 ⦠)"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvAlt $L1 $L2 }.
+
include "basic_2/reducibility/lfpr.ma".
(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc
index 5ad9180ac..3674637dd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc
@@ -12,6 +12,10 @@
(* *)
(**************************************************************************)
+notation "hvbox( ⦠term 46 L1 ⦠⬠⬠* break ⦠term 46 L2 ⦠)"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStarAlt $L1 $L2 }.
+
include "basic_2/conversion/lfpc.ma".
(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc
new file mode 100644
index 000000000..9451e34d2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc
@@ -0,0 +1,161 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/unwind/sstas_sstas.ma".
+include "basic_2/equivalence/cpcs_ltpr.ma".
+include "basic_2/dynamic/snv_ltpss_dx.ma".
+include "basic_2/dynamic/snv_sstas.ma".
+include "basic_2/dynamic/ygt.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Inductive premises for the preservation results **************************)
+
+definition IH_snv_ltpr_tpr: âh:sh. sd h â relation2 lenv term â
+ λh,g,L1,T1. â¦h, L1⦠⢠T1 ¡[g] â
+ âL2. L1 â¡ L2 â âT2. T1 â¡ T2 â â¦h, L2⦠⢠T2 ¡[g].
+
+definition IH_ssta_ltpr_tpr: âh:sh. sd h â relation2 lenv term â
+ λh,g,L1,T1. â¦h, L1⦠⢠T1 ¡[g] â
+ âU1,l. â¦h, L1⦠⢠T1 â¢[g] â¦l, U1⦠â
+ âL2. L1 â¡ L2 â âT2. T1 â¡ T2 â
+ ââU2. â¦h, L2⦠⢠T2 â¢[g] â¦l, U2⦠& L2 ⢠U1 â¬* U2.
+
+definition IH_snv_ssta: âh:sh. sd h â relation2 lenv term â
+ λh,g,L1,T1. â¦h, L1⦠⢠T1 ¡[g] â
+ âU1,l. â¦h, L1⦠⢠T1 â¢[g] â¦l+1, U1⦠â â¦h, L1⦠⢠U1 ¡[g].
+
+definition IH_snv_lsubsv: âh:sh. sd h â relation2 lenv term â
+ λh,g,L2,T. â¦h, L2⦠⢠T ¡[g] â
+ âL1. h ⢠L1 ¡â[g] L2 â â¦h, L1⦠⢠T ¡[g].
+
+(* Properties for the preservation results **********************************)
+
+fact snv_ltpr_cpr_aux: âh,g,L1,T1. IH_snv_ltpr_tpr h g L1 T1 â
+ â¦h, L1⦠⢠T1 ¡[g] â
+ âL2. L1 â¡ L2 â âT2. L2 ⢠T1 â¡ T2 â â¦h, L2⦠⢠T2 ¡[g].
+#h #g #L1 #T1 #IH #HT1 #L2 #HL12 #T2 * #T #HT1T #HTT2
+lapply (IH ⦠HL12 ⦠HT1T) -HL12 // -T1 #HT0
+lapply (snv_tpss_conf ⦠HT0 ⦠HTT2) -T //
+qed-.
+
+fact ssta_ltpr_cpr_aux: âh,g,L1,T1. IH_ssta_ltpr_tpr h g L1 T1 â
+ â¦h, L1⦠⢠T1 ¡[g] â
+ âU1,l. â¦h, L1⦠⢠T1 â¢[g] â¦l, U1⦠â
+ âL2. L1 â¡ L2 â âT2. L2 ⢠T1 â¡ T2 â
+ ââU2. â¦h, L2⦠⢠T2 â¢[g] â¦l, U2⦠& L2 ⢠U1 â¬* U2.
+#h #g #L1 #T1 #IH #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 * #T #HT1T #HTT2
+elim (IH ⦠HTU1 ⦠HL12 ⦠HT1T) // -L1 -T1 #U #HTU #HU1
+elim (ssta_tpss_conf ⦠HTU ⦠HTT2) -T #U2 #HTU2 #HU2
+lapply (cpcs_cpr_strap1 ⦠HU1 U2 ?) /2 width=3/
+qed-.
+
+fact snv_ltpr_cprs_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
+ âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
+ âL2. L1 â¡ L2 â âT2. L2 ⢠T1 â¡* T2 â â¦h, L2⦠⢠T2 ¡[g].
+#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #L2 #HL12 #T2 #H
+@(cprs_ind ⦠H) -T2 [ /2 width=6 by snv_ltpr_cpr_aux/ ] -HT1
+/5 width=6 by snv_ltpr_cpr_aux, ygt_yprs_trans, ltpr_cprs_yprs/
+qed-.
+
+fact ssta_ltpr_cprs_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
+ âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
+ âU1,l. â¦h, L1⦠⢠T1 â¢[g] â¦l, U1⦠â
+ âL2. L1 â¡ L2 â âT2. L2 ⢠T1 â¡* T2 â
+ ââU2. â¦h, L2⦠⢠T2 â¢[g] â¦l, U2⦠& L2 ⢠U1 â¬* U2.
+#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 #H
+@(cprs_ind ⦠H) -T2 [ /2 width=7 by ssta_ltpr_cpr_aux/ ]
+#T #T2 #HT1T #HTT2 * #U #HTU #HU1
+elim (ssta_ltpr_cpr_aux ⦠HTU ⦠HTT2) //
+[2: /3 width=9 by snv_ltpr_cprs_aux/
+|3: /5 width=6 by ygt_yprs_trans, ltpr_cprs_yprs/
+] -L0 -L1 -T0 -T1 -T #U2 #HTU2 #HU2
+lapply (cpcs_trans ⦠HU1 ⦠HU2) -U /2 width=3/
+qed-.
+
+fact ssta_ltpr_cpcs_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
+ âL1,L2,T1,T2. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â h ⢠â¦L0, T0⦠>[g] â¦L2, T2⦠â
+ â¦h, L1⦠⢠T1 ¡[g] â â¦h, L2⦠⢠T2 ¡[g] â
+ âU1,l1. â¦h, L1⦠⢠T1 â¢[g] â¦l1, U1⦠â
+ âU2,l2. â¦h, L2⦠⢠T2 â¢[g] â¦l2, U2⦠â
+ L1 â¡ L2 â L2 ⢠T1 â¬* T2 â
+ l1 = l2 ⧠L2 ⢠U1 â¬* U2.
+#h #g #L0 #T0 #IH2 #IH1 #L1 #L2 #T1 #T2 #HLT01 #HLT02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #HL12 #H
+elim (cpcs_inv_cprs ⦠H) -H #T #H1 #H2
+elim (ssta_ltpr_cprs_aux ⦠HLT01 HT1 ⦠HTU1 ⦠H1) -T1 /2 width=1/ #W1 #H1 #HUW1
+elim (ssta_ltpr_cprs_aux ⦠HLT02 HT2 ⦠HTU2 ⦠H2) -T2 /2 width=1/ #W2 #H2 #HUW2 -L1 -L0 -T0
+elim (ssta_mono ⦠H1 ⦠H2) -h -T #H1 #H2 destruct
+lapply (cpcs_canc_dx ⦠HUW1 ⦠HUW2) -W2 /2 width=1/
+qed-.
+
+fact snv_sstas_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
+ âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
+ âU1. â¦h, L1⦠⢠T1 â¢*[g] U1 â â¦h, L1⦠⢠U1 ¡[g].
+#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H
+@(sstas_ind ⦠H) -U1 // -HT1 /4 width=5 by ygt_yprs_trans, sstas_yprs/
+qed-.
+
+fact sstas_ltpr_cprs_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
+ âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
+ âL2. L1 â¡ L2 â âT2. L2 ⢠T1 â¡* T2 â âU1. â¦h, L1⦠⢠T1 â¢*[g] U1 â
+ ââU2. â¦h, L2⦠⢠T2 â¢*[g] U2 & L2 ⢠U1 â¬* U2.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #L2 #HL12 #T2 #HT12 #U1 #H
+@(sstas_ind ⦠H) -U1 [ /3 width=3/ ]
+#U1 #W1 #l1 #HTU1 #HUW1 * #U2 #HTU2 #HU12
+lapply (snv_ltpr_cprs_aux ⦠IH2 ⦠HT1 ⦠HT12) // #HT2
+elim (snv_sstas_fwd_correct ⦠HTU2) // #W2 #l2 #HUW2
+elim (ssta_ltpr_cpcs_aux ⦠IH2 IH1 ⦠HUW1 ⦠HUW2 ⦠HU12) -IH2 -IH1 -HUW1 -HU12 //
+[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, ltpr_cprs_yprs/
+|3: /3 width=7 by snv_sstas_aux, ygt_yprs_trans, cprs_yprs/
+|4: /4 width=5 by ygt_yprs_trans, ltpr_cprs_yprs, sstas_yprs/
+|5: /3 width=4 by ygt_yprs_trans, cprs_yprs, sstas_yprs/
+] -L0 -T0 -T1 -HT2 #H #HW12 destruct /3 width=4/
+qed-.
+
+fact dxprs_ltpr_cprs_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ssta h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
+ âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
+ âU1. â¦h, L1⦠⢠T1 â¢*â¡*[g] U1 â
+ âL2. L1 â¡ L2 â âT2. L2 ⢠T1 â¡* T2 â
+ ââU2. â¦h, L2⦠⢠T2 â¢*â¡*[g] U2 & L2 ⢠U1 â¡* U2.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #L2 #HL12 #T2 #HT12
+elim (sstas_ltpr_cprs_aux ⦠IH3 IH2 IH1 ⦠H01 ⦠HT12 ⦠HTW1) // -L0 -T0 -T1 #W2 #HTW2 #HW12
+lapply (ltpr_cprs_conf ⦠HL12 ⦠HWU1) -L1 #HWU1
+lapply (cpcs_canc_sn ⦠HW12 HWU1) -W1 #H
+elim (cpcs_inv_cprs ⦠H) -H /3 width=3/
+qed-.
+
+fact ssta_dxprs_aux: âh,g,L0,T0.
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_snv_ltpr_tpr h g L1 T1) â
+ (âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â IH_ssta_ltpr_tpr h g L1 T1) â
+ âL1,T1. h ⢠â¦L0, T0⦠>[g] â¦L1, T1⦠â â¦h, L1⦠⢠T1 ¡[g] â
+ âl,U1. â¦h, L1⦠⢠T1 â¢[g] â¦l+1, U1⦠â âT2. â¦h, L1⦠⢠T1 â¢*â¡*[g] T2 â
+ ââU,U2. â¦h, L1⦠⢠U1 â¢*[g] U & â¦h, L1⦠⢠T2 â¢*[g] U2 & L1 ⢠U â¬* U2.
+#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2
+elim (sstas_strip ⦠HT1T ⦠HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ]
+[ elim (ssta_ltpr_cprs_aux ⦠IH2 IH1 ⦠HTU1 L1 ⦠HTT2) // -L0 -T0 -T /3 width=5/
+| @(ex3_2_intro â¦T2 HU1T) // /2 width=1/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ssta_ltpr.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ssta_ltpr.etc
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 753cddf6f..96b64d882 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
@@ -44,7 +44,7 @@ table {
}
]
[ { "stratified native validity" * } {
- [ "snv ( �,?⦠⢠? ¡[?] )" "snv_lift" + "snv_lpss" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_ltpr" + "snv_ltpr" + "snv_cpcs" * ]
+ [ "snv ( �,?⦠⢠? ¡[?] )" "snv_lift" + "snv_lpss" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_lpr" + "snv_lpr" + "snv_cpcs" * ]
}
]
}
--
2.39.5