From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 17 Jan 2014 17:45:00 +0000 (+0000)
Subject: - commit of the "substitution" component
X-Git-Tag: make_still_working~997
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e5378812c068074f0ac627541d3f066e135c8824;p=helm.git
- commit of the "substitution" component
- some renaming
- we disabled the old notation for ldrop to capture its instances
syntactically
---
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
index 3656d36f6..23cc43031 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
@@ -36,7 +36,7 @@ theorem aacr_aaa_csubc_lifts: âRR,RS,RP.
| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
lapply (aacr_acr ⦠H1RP H2RP B) #HB
elim (lifts_inv_lref1 ⦠H) -H #i1 #Hi1 #H destruct
- lapply (ldrop_fwd_ldrop2 ⦠HLK1) #HK1b
+ lapply (ldrop_fwd_drop2 ⦠HLK1) #HK1b
elim (ldrops_ldrop_trans ⦠HL01 ⦠HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1
>(at_mono ⦠Hi1 ⦠Hi0) -i1
elim (ldrops_inv_skip2 ⦠Hdes1 ⦠H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct
@@ -48,7 +48,7 @@ theorem aacr_aaa_csubc_lifts: âRR,RS,RP.
@(s5 ⦠HB ⦠(â) ⦠HV0 HLK2) /3 width=7 by ldrops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *)
| -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0
#K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct
- lapply (ldrop_fwd_ldrop2 ⦠HLK2) #HLK2b
+ lapply (ldrop_fwd_drop2 ⦠HLK2) #HLK2b
lapply (aaa_lifts ⦠HK01 ⦠HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B
lapply (aaa_mono ⦠H2KV0A ⦠HKV0B) #H destruct -H2KV0A -HKV0B
elim (lift_total V0 0 (i0 +1)) #V3 #HV03
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
index e570307ac..6298274bc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
@@ -25,7 +25,7 @@ lemma cprs_delta: âG,L,K,V,V2,i.
âW2. â§[0, i + 1] V2 â¡ W2 â â¦G, L⦠⢠#i â¡* W2.
#G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ]
#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2
-lapply (ldrop_fwd_ldrop2 ⦠HLK) -HLK #HLK
+lapply (ldrop_fwd_drop2 ⦠HLK) -HLK #HLK
elim (lift_total V1 0 (i+1)) /4 width=11 by cpr_lift, cprs_strap1/
qed.
@@ -42,7 +42,7 @@ lemma cprs_inv_lref1: âG,L,T2,i. â¦G, L⦠⢠#i â¡* T2 â
elim (cpr_inv_lref1 ⦠HT2) -HT2 /2 width=1/
* /4 width=6/
| * #K #V1 #T1 #HLK #HVT1 #HT1
- lapply (ldrop_fwd_ldrop2 ⦠HLK) #H0LK
+ lapply (ldrop_fwd_drop2 ⦠HLK) #H0LK
elim (cpr_inv_lift1 ⦠HT2 ⦠H0LK ⦠HT1) -H0LK -T /4 width=6/
]
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
index fa14bfc25..e4c5cea84 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
@@ -142,7 +142,7 @@ lemma fqu_cpxs_trans_neq: âh,g,G1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â â¦G2,
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
#U2 #HVU2 @(ex3_intro ⦠U2)
- [1,3: /3 width=7 by fqu_drop, cpxs_delta, ldrop_pair, ldrop_ldrop/
+ [1,3: /3 width=7 by fqu_drop, cpxs_delta, ldrop_pair, ldrop_drop/
| #H destruct /2 width=7 by lift_inv_lref2_be/
]
| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro ⦠(â¡{I}V2.T))
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
index 0c9cfe1e7..2d6797667 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
@@ -37,7 +37,7 @@ lemma cpxs_delta: âh,g,I,G,L,K,V,V2,i.
âW2. â§[0, i + 1] V2 â¡ W2 â â¦G, L⦠⢠#i â¡*[h, g] W2.
#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2
[ /3 width=9 by cpx_cpxs, cpx_delta/
-| #V1 lapply (ldrop_fwd_ldrop2 ⦠HLK) -HLK
+| #V1 lapply (ldrop_fwd_drop2 ⦠HLK) -HLK
elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/
]
qed.
@@ -54,7 +54,7 @@ lemma cpxs_inv_lref1: âh,g,G,L,T2,i. â¦G, L⦠⢠#i â¡*[h, g] T2 â
elim (cpx_inv_lref1 ⦠HT2) -HT2 /2 width=1 by or_introl/
* /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
| * #I #K #V1 #T1 #HLK #HVT1 #HT1
- lapply (ldrop_fwd_ldrop2 ⦠HLK) #H0LK
+ lapply (ldrop_fwd_drop2 ⦠HLK) #H0LK
elim (cpx_inv_lift1 ⦠HT2 ⦠H0LK ⦠HT1) -H0LK -T
/4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/
]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
index faae2dd87..30745dd38 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
@@ -64,7 +64,7 @@ lemma cpxs_fwd_delta: âh,g,I,G,L,K,V1,i. â©[0, i] L â¡ K.â{I}V1 â
elim (cpxs_inv_lref1 ⦠H) -H /2 width=1/
* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
lapply (ldrop_mono ⦠HLK0 ⦠HLK) -HLK0 #H destruct
-lapply (ldrop_fwd_ldrop2 ⦠HLK) -HLK /3 width=9/
+lapply (ldrop_fwd_drop2 ⦠HLK) -HLK /3 width=9/
qed-.
lemma cpxs_fwd_theta: âh,g,a,G,L,V1,V,T,U. â¦G, L⦠⢠âV1.â{a}V.T â¡*[h, g] U â
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
index 5194bedfe..4f06e7912 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
@@ -48,7 +48,7 @@ lemma csx_inv_lref_bind: âh,g,I,G,L,K,V,i. â©[0, i] L â¡ K.â{I}V â
â¦G, L⦠⢠â¬*[h, g] #i â â¦G, K⦠⢠â¬*[h, g] V.
#h #g #I #G #L #K #V #i #HLK #Hi
elim (lift_total V 0 (i+1))
-/4 width=9 by csx_inv_lift, csx_cpx_trans, cpx_delta, ldrop_fwd_ldrop2/
+/4 width=9 by csx_inv_lift, csx_cpx_trans, cpx_delta, ldrop_fwd_drop2/
qed-.
(* Advanced properties ******************************************************)
@@ -61,7 +61,7 @@ elim (cpx_inv_lref1 ⦠H) -H
[ #H destruct elim Hi //
| -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1
lapply (ldrop_mono ⦠HLK0 ⦠HLK) -HLK #H destruct
- /3 width=7 by csx_lift, csx_cpx_trans, ldrop_fwd_ldrop2/
+ /3 width=7 by csx_lift, csx_cpx_trans, ldrop_fwd_drop2/
]
qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
index f32a267c9..e16b976a7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
@@ -68,7 +68,7 @@ lemma csx_applv_delta: âh,g,I,G,L,K,V1,i. â©[0, i] L â¡ K.â{I}V1 â
âVs. â¦G, L⦠⢠â¬*[h, g] (â¶Vs.V2) â â¦G, L⦠⢠â¬*[h, g] (â¶Vs.#i).
#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
[ #H
- lapply (ldrop_fwd_ldrop2 ⦠HLK) #HLK0
+ lapply (ldrop_fwd_drop2 ⦠HLK) #HLK0
lapply (csx_inv_lift ⦠H ⦠HLK0 HV12) -V2 -HLK0 /2 width=5/
| #V #Vs #IHV #H1T
lapply (csx_fwd_pair_sn ⦠H1T) #HV
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
index 10600383a..c961d137c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
@@ -77,7 +77,7 @@ lemma cpxs_inv_abbr1: âh,g,a,G,L,V1,T1,U2. â¦G, L⦠⢠â{a}V1.T1 â¡*[h,
]
| #U1 #HTU1 #HU01
elim (lift_total U2 0 1) #U #HU2
- /6 width=11 by cpxs_strap1, cpx_lift, ldrop_ldrop, ex3_intro, or_intror/
+ /6 width=11 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/
]
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma
index 500d2f687..8283ea541 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma
@@ -35,7 +35,7 @@ lemma lsubsv_lsstas_trans: âh,g,G,L2,T,U2,l1. â¦G, L2⦠⢠T â¢*[h, g, l1]
elim (lsubsv_inv_pair2 ⦠H) -H * #K1 [ | -HYU -IHXY -HLK1 ]
[ #HK12 #H destruct
elim (IHXY ⦠Hl12 HV0 ⦠HK12) -K2 -l2 #T #HXT #HTY
- lapply (ldrop_fwd_ldrop2 ⦠HLK1) #H
+ lapply (ldrop_fwd_drop2 ⦠HLK1) #H
elim (lift_total T 0 (i+1))
/3 width=11 by lsstas_ldef, cpcs_lift, ex2_intro/
| #V #l0 #_ #_ #_ #_ #_ #_ #_ #H destruct
@@ -50,7 +50,7 @@ lemma lsubsv_lsstas_trans: âh,g,G,L2,T,U2,l1. â¦G, L2⦠⢠T â¢*[h, g, l1]
lapply (lsubsv_fwd_lsubd ⦠HK12) #H
lapply (lsubd_da_trans ⦠HV0 ⦠H) -H
elim (IHXY ⦠Hl12 HV0 ⦠HK12) -K2 -Hl12 #Y0
- lapply (ldrop_fwd_ldrop2 ⦠HLK1)
+ lapply (ldrop_fwd_drop2 ⦠HLK1)
elim (lift_total Y0 0 (i+1))
/3 width=11 by lsstas_ldec, cpcs_lift, ex2_intro/
| #V #l #_ #_ #HVX #_ #HV #HX #HK12 #_ #H destruct
@@ -60,7 +60,7 @@ lemma lsubsv_lsstas_trans: âh,g,G,L2,T,U2,l1. â¦G, L2⦠⢠T â¢*[h, g, l1]
elim (lsstas_total ⦠HVW (l1+1)) -W #W #HVW
lapply (HVX ⦠Hl12 HVW HXY0) -HVX -Hl12 -HXY0 #HWY0
lapply (cpcs_trans ⦠HWY0 ⦠HY0) -Y0
- lapply (ldrop_fwd_ldrop2 ⦠HLK1)
+ lapply (ldrop_fwd_drop2 ⦠HLK1)
elim (lift_total W 0 (i+1))
/4 width=11 by lsstas_ldef, lsstas_cast, cpcs_lift, ex2_intro/
]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
index b44137664..f86f5bd15 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
@@ -45,7 +45,7 @@ fact da_cpr_lpr_aux: âh,g,G0,L0,T0.
lapply (fqup_lref ⦠G1 ⦠HLK1)
elim (lpr_ldrop_conf ⦠HLK1 ⦠HL12) -HLK1 -HL12 #X #H #HLK2
elim (lpr_inv_pair1 ⦠H) -H #K2 #V2 #HK12 #_ #H destruct
- lapply (ldrop_fwd_ldrop2 ⦠HLK2) -V2
+ lapply (ldrop_fwd_drop2 ⦠HLK2) -V2
/4 width=7 by da_lift, fqup_fpbg/
]
| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
@@ -57,7 +57,7 @@ fact da_cpr_lpr_aux: âh,g,G0,L0,T0.
[ #V2 #T2 #HV12 #HT12 #H destruct
/4 width=9 by da_bind, fqup_fpbg, lpr_pair/
| #T2 #HT12 #HT2 #H1 #H2 destruct
- /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_ldrop/
+ /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_drop/
]
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct
elim (snv_inv_appl ⦠H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
index 60e0d2619..75bf56d43 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
@@ -38,7 +38,7 @@ fact snv_cpr_lpr_aux: âh,g,G0,L0,T0.
[ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/
| * #K0 #V0 #W0 #H #HVW0 #W0 -HV12
lapply (ldrop_mono ⦠H ⦠HLK1) -HLK1 -H #H destruct
- lapply (ldrop_fwd_ldrop2 ⦠HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/
+ lapply (ldrop_fwd_drop2 ⦠HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/
]
| #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
elim (snv_inv_gref ⦠H1)
@@ -47,7 +47,7 @@ fact snv_cpr_lpr_aux: âh,g,G0,L0,T0.
elim (cpr_inv_bind1 ⦠H2) -H2 *
[ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/
| #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
- /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_ldrop/
+ /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_drop/
]
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
elim (snv_inv_appl ⦠H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1
@@ -103,17 +103,17 @@ fact snv_cpr_lpr_aux: âh,g,G0,L0,T0.
elim (ssta_cpr_lpr_aux ⦠IH3 ⦠HVW1 ⦠HV10 ⦠HL12) /2 width=2 by fqup_fpbg/ -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 by ldrop_ldrop/ -H1 #HVW20
- lapply (cpcs_lift ⦠(L2.âW2) ⦠H3 ⦠HW13 H2) /2 width=1 by ldrop_ldrop/ -HW13 -H3 -H2 #HW320
+ lapply (ssta_lift ⦠H1 (L2.âW2) ⦠HV02 ⦠H3) /2 width=1 by ldrop_drop/ -H1 #HVW20
+ lapply (cpcs_lift ⦠(L2.âW2) ⦠H3 ⦠HW13 H2) /2 width=1 by ldrop_drop/ -HW13 -H3 -H2 #HW320
lapply (cpcs_cprs_strap1 ⦠HW320 ⦠HW1) -W3 #HW20
elim (cpcs_inv_cprs ⦠HW20) -HW20 #W3 #HW203 #HW3
lapply (cpds_cprs_trans ⦠(â{a}W3.U2) HTU2 ?) /2 width=1 by cprs_bind/ -HW3 -HTU2 #HTU2
lapply (IH2 ⦠Hl0 ⦠HV10 ⦠HL12) /2 width=1 by fqup_fpbg/ -IH2 -Hl0 #Hl0
- lapply (da_lift ⦠Hl0 (L2.âW2) ⦠HV02) /2 width=1 by ldrop_ldrop/ -Hl0 #Hl0
+ lapply (da_lift ⦠Hl0 (L2.âW2) ⦠HV02) /2 width=1 by ldrop_drop/ -Hl0 #Hl0
lapply (IH1 ⦠HW02 ⦠HL12) /2 width=1 by fqup_fpbg/ -HW0 #HW2
lapply (IH1 ⦠HV10 ⦠HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV10 #HV0
lapply (IH1 ⦠HT02 (L2.âW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2
- lapply (snv_lift ⦠HV0 (L2.âW2) ⦠HV02) /3 width=7 by snv_bind, snv_appl, ldrop_ldrop/
+ lapply (snv_lift ⦠HV0 (L2.âW2) ⦠HV02) /3 width=7 by snv_bind, snv_appl, ldrop_drop/
]
| #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4
elim (snv_inv_cast ⦠H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma
index d13c47cd3..739caf494 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma
@@ -37,7 +37,7 @@ fact snv_lsstas_aux: âh,g,G0,L0,T0.
lapply (ldrop_mono ⦠HLK0 ⦠HLK1) -HLK0 #H destruct
[ lapply (le_plus_to_le_r ⦠Hl21) -Hl21 #Hl21 ]
lapply (fqup_lref ⦠G1 ⦠HLK1) #H
- lapply (ldrop_fwd_ldrop2 ⦠HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/
+ lapply (ldrop_fwd_drop2 ⦠HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/
| #p #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
elim (snv_inv_gref ⦠H1)
| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
index d43f443ef..a7b6e3e77 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
@@ -44,7 +44,7 @@ fact lsstas_cpr_lpr_aux: âh,g,G0,L0,T0.
lapply (fqup_lref ⦠G1 ⦠HLK1) #HKV1
elim (lpr_ldrop_conf ⦠HLK1 ⦠HL12) -HL12 #X #H #HLK2
elim (lpr_inv_pair1 ⦠H) -H #K2 [ #W2 | #V2 ] #HK12 [ #HW12 | #HV12 ] #H destruct
- lapply (ldrop_fwd_ldrop2 ⦠HLK2) #H2
+ lapply (ldrop_fwd_drop2 ⦠HLK2) #H2
elim (cpr_inv_lref1 ⦠H3) -H3
[1,3: #H destruct -HLK1
|2,4: * #K0 #V0 #X0 #H #HVX0 #HX0
@@ -73,7 +73,7 @@ fact lsstas_cpr_lpr_aux: âh,g,G0,L0,T0.
| #T3 #HT13 #HXT3 #H1 #H2 destruct
elim (IH1 ⦠Hl1 ⦠HTU1 ⦠HT13 (L2.âV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
elim (lsstas_inv_lift1 ⦠HTU3 L2 ⦠HXT3) -T3
- /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_ldrop, ex2_intro/
+ /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_drop, ex2_intro/
]
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct
elim (snv_inv_appl ⦠H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU10
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index bc5044b6d..0f015cc32 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
@@ -55,7 +55,7 @@ lemma lsubr_cpx_trans: âh,g,G. lsub_trans ⦠(cpx h g G) lsubr.
[ //
| /2 width=2 by cpx_sort/
| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsubr_fwd_ldrop2_bind ⦠HL12 ⦠HLK1) -HL12 -HLK1 *
+ elim (lsubr_fwd_drop2_bind ⦠HL12 ⦠HLK1) -HL12 -HLK1 *
/4 width=7 by cpx_delta, cpx_ti/
|4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_bind/
|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
@@ -88,7 +88,7 @@ lemma cpx_delift: âh,g,I,G,K,V,T1,L,d. â©[0, d] L â¡ (K.â{I}V) â
elim (lift_split ⦠HVW i i) /3 width=7 by cpx_delta, ex2_2_intro/
| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
elim (IHW1 ⦠HLK) -IHW1 #W2 #W #HW12 #HW2
- [ elim (IHU1 (L. â{I} W1) (d+1)) -IHU1 /3 width=9 by cpx_bind, ldrop_ldrop, lift_bind, ex2_2_intro/
+ [ elim (IHU1 (L. â{I} W1) (d+1)) -IHU1 /3 width=9 by cpx_bind, ldrop_drop, lift_bind, ex2_2_intro/
| elim (IHU1 ⦠HLK) -IHU1 -HLK /3 width=8 by cpx_flat, lift_flat, ex2_2_intro/
]
]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
index 505eabf1a..4da4e21c8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -145,7 +145,7 @@ lemma fqu_cpx_trans: âh,g,G1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â â¦G2, L2, T
/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/
[ #I #G #L #V2 #U2 #HVU2
elim (lift_total U2 0 1)
- /4 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
+ /4 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_drop, ex2_intro/
| #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2
elim (lift_total T2 0 (e+1))
/3 width=11 by cpx_lift, fqu_drop, ex2_intro/
@@ -200,7 +200,7 @@ lemma fqu_cpx_trans_neq: âh,g,G1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â â¦G2, L
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
#U2 #HVU2 @(ex3_intro ⦠U2)
- [1,3: /3 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_ldrop/
+ [1,3: /3 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_drop/
| #H destruct /2 width=7 by lift_inv_lref2_be/
]
| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro ⦠(â¡{I}V2.T))
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
index bc56f721e..d810ae175 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
@@ -51,15 +51,15 @@ lemma lleq_cpx_conf_dx: âh,g,G,L2,T1,T2. â¦G, L2⦠⢠T1 â¡[h, g] T2 â
| /3 width=3 by lleq_fwd_length, lleq_sort/
| #I2 #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_inv_lref_ge_dx ⦠H ⦠HLK2) // -H
#I1 #K1 #HLK1 #HV1
- lapply (ldrop_fwd_ldrop2 ⦠HLK1) -HLK1 #HLK1
- lapply (ldrop_fwd_ldrop2 ⦠HLK2) -HLK2 #HLK2
+ lapply (ldrop_fwd_drop2 ⦠HLK1) -HLK1 #HLK1
+ lapply (ldrop_fwd_drop2 ⦠HLK2) -HLK2 #HLK2
@(lleq_lift_le ⦠HLK1 HLK2 ⦠HVW2) -HLK1 -HLK2 -HVW2 /2 width=1 by/ (**) (* full auto too slow *)
| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O ⦠H) -H
/4 width=5 by lleq_bind_repl_SO, lleq_bind/
| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat ⦠H) -H
/3 width=1 by lleq_flat/
| #G #L2 #V #T1 #T2 #T #_ #HT2 #IHT12 #L1 #H elim (lleq_inv_bind_O ⦠H) -H
- /3 width=10 by lleq_inv_lift_le, ldrop_ldrop/
+ /3 width=10 by lleq_inv_lift_le, ldrop_drop/
| #G #L2 #V #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat ⦠H) -H /2 width=1 by/
| #G #L2 #V1 #V2 #T #_ #IHV12 #L1 #H elim (lleq_inv_flat ⦠H) -H /2 width=1 by/
| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat ⦠H) -H
@@ -68,7 +68,7 @@ lemma lleq_cpx_conf_dx: âh,g,G,L2,T1,T2. â¦G, L2⦠⢠T1 â¡[h, g] T2 â
| #a #G #L2 #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat ⦠H) -H
#HV1 #H elim (lleq_inv_bind_O ⦠H) -H
#HW1 #HT1 @lleq_bind_O /2 width=1 by/ @lleq_flat (**) (* full auto too slow *)
- [ /3 width=10 by lleq_lift_le, ldrop_ldrop/
+ [ /3 width=10 by lleq_lift_le, ldrop_drop/
| /3 width=3 by lleq_bind_repl_O/
]
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
index 933bcd637..fb9e9e691 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -40,7 +40,7 @@ elim (lpr_ldrop_conf ⦠HLK0 ⦠HL01) -HL01 #X1 #H1 #HLK1
elim (lpr_inv_pair1 ⦠H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
elim (lpr_ldrop_conf ⦠HLK0 ⦠HL02) -HL02 #X2 #H2 #HLK2
elim (lpr_inv_pair1 ⦠H2) -H2 #K2 #W2 #HK02 #_ #H destruct
-lapply (ldrop_fwd_ldrop2 ⦠HLK2) -W2 #HLK2
+lapply (ldrop_fwd_drop2 ⦠HLK2) -W2 #HLK2
lapply (fqup_lref ⦠G ⦠HLK0) -HLK0 #HLK0
elim (IH ⦠HLK0 ⦠HV01 ⦠HV02 ⦠HK01 ⦠HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1))
@@ -66,10 +66,10 @@ fact cpr_conf_lpr_delta_delta:
lapply (ldrop_mono ⦠H ⦠HLK0) -H #H destruct
elim (lpr_ldrop_conf ⦠HLK0 ⦠HL01) -HL01 #X1 #H1 #HLK1
elim (lpr_inv_pair1 ⦠H1) -H1 #K1 #W1 #HK01 #_ #H destruct
-lapply (ldrop_fwd_ldrop2 ⦠HLK1) -W1 #HLK1
+lapply (ldrop_fwd_drop2 ⦠HLK1) -W1 #HLK1
elim (lpr_ldrop_conf ⦠HLK0 ⦠HL02) -HL02 #X2 #H2 #HLK2
elim (lpr_inv_pair1 ⦠H2) -H2 #K2 #W2 #HK02 #_ #H destruct
-lapply (ldrop_fwd_ldrop2 ⦠HLK2) -W2 #HLK2
+lapply (ldrop_fwd_drop2 ⦠HLK2) -W2 #HLK2
lapply (fqup_lref ⦠G ⦠HLK0) -HLK0 #HLK0
elim (IH ⦠HLK0 ⦠HV01 ⦠HV02 ⦠HK01 ⦠HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) /3 width=11 by cpr_lift, ex2_intro/
@@ -107,7 +107,7 @@ fact cpr_conf_lpr_bind_zeta:
#G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
elim (IH ⦠HT01 ⦠HT02 (L1.âV1) ⦠(L2.âV1)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -V0 -T0 #T #HT1 #HT2
-elim (cpr_inv_lift1 ⦠HT2 L2 ⦠HXT2) -T2 /3 width=3 by cpr_zeta, ldrop_ldrop, ex2_intro/
+elim (cpr_inv_lift1 ⦠HT2 L2 ⦠HXT2) -T2 /3 width=3 by cpr_zeta, ldrop_drop, ex2_intro/
qed-.
fact cpr_conf_lpr_zeta_zeta:
@@ -124,8 +124,8 @@ fact cpr_conf_lpr_zeta_zeta:
#G #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1
#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
elim (IH ⦠HT01 ⦠HT02 (L1.âV0) ⦠(L2.âV0)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -T0 #T #HT1 #HT2
-elim (cpr_inv_lift1 ⦠HT1 L1 ⦠HXT1) -T1 /2 width=1 by ldrop_ldrop/ #T1 #HT1 #HXT1
-elim (cpr_inv_lift1 ⦠HT2 L2 ⦠HXT2) -T2 /2 width=1 by ldrop_ldrop/ #T2 #HT2 #HXT2
+elim (cpr_inv_lift1 ⦠HT1 L1 ⦠HXT1) -T1 /2 width=1 by ldrop_drop/ #T1 #HT1 #HXT1
+elim (cpr_inv_lift1 ⦠HT2 L2 ⦠HXT2) -T2 /2 width=1 by ldrop_drop/ #T2 #HT2 #HXT2
lapply (lift_inj ⦠HT2 ⦠HT1) -T #H destruct /2 width=3 by ex2_intro/
qed-.
@@ -217,7 +217,7 @@ fact cpr_conf_lpr_flat_theta:
#V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
elim (IH ⦠HV01 ⦠HV02 ⦠HL01 ⦠HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
elim (lift_total V 0 1) #U #HVU
-lapply (cpr_lift ⦠HV2 (L2.âW2) ⦠HVU2 ⦠HVU) -HVU2 /2 width=1 by ldrop_ldrop/ #HU2
+lapply (cpr_lift ⦠HV2 (L2.âW2) ⦠HVU2 ⦠HVU) -HVU2 /2 width=1 by ldrop_drop/ #HU2
elim (cpr_inv_abbr1 ⦠H) -H *
[ #W1 #T1 #HW01 #HT01 #H destruct
elim (IH ⦠HW01 ⦠HW02 ⦠HL01 ⦠HL02) /2 width=1 by/
@@ -226,7 +226,7 @@ elim (cpr_inv_abbr1 ⦠H) -H *
| #T1 #HT01 #HXT1 #H destruct
elim (IH ⦠HT01 ⦠HT02 (L1.âW2) ⦠(L2.âW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
elim (cpr_inv_lift1 ⦠HT1 L1 ⦠HXT1) -HXT1
- /4 width=9 by cpr_flat, cpr_zeta, ldrop_ldrop, lift_flat, ex2_intro/
+ /4 width=9 by cpr_flat, cpr_zeta, ldrop_drop, lift_flat, ex2_intro/
]
qed-.
@@ -271,8 +271,8 @@ elim (IH ⦠HV01 ⦠HV02 ⦠HL01 ⦠HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1
elim (IH ⦠HW01 ⦠HW02 ⦠HL01 ⦠HL02) /2 width=1 by/
elim (IH ⦠HT01 ⦠HT02 (L1.âW1) ⦠(L2.âW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0
elim (lift_total V 0 1) #U #HVU
-lapply (cpr_lift ⦠HV1 (L1.âW1) ⦠HVU1 ⦠HVU) -HVU1 /2 width=1 by ldrop_ldrop/
-lapply (cpr_lift ⦠HV2 (L2.âW2) ⦠HVU2 ⦠HVU) -HVU2 /2 width=1 by ldrop_ldrop/
+lapply (cpr_lift ⦠HV1 (L1.âW1) ⦠HVU1 ⦠HVU) -HVU1 /2 width=1 by ldrop_drop/
+lapply (cpr_lift ⦠HV2 (L2.âW2) ⦠HVU2 ⦠HVU) -HVU2 /2 width=1 by ldrop_drop/
/4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
index e21810ea5..3537c8d01 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
@@ -36,7 +36,7 @@ lemma aaa_cpx_lpx_conf: âh,g,G,L1,T1,A. â¦G, L1⦠⢠T1 â A â
lapply (ldrop_mono ⦠H ⦠HLK1) -H #H destruct
elim (lpx_ldrop_conf ⦠HLK1 ⦠HL12) -L1 #Z #H #HLK2
elim (lpx_inv_pair1 ⦠H) -H #K2 #V0 #HK12 #_ #H destruct
- lapply (ldrop_fwd_ldrop2 ⦠HLK2) -V0 /3 width=7/
+ lapply (ldrop_fwd_drop2 ⦠HLK2) -V0 /3 width=7/
]
| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
elim (cpx_inv_abbr1 ⦠H) -H *
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
index 705d5695e..b6c3584ed 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
@@ -61,7 +61,7 @@ lemma lpx_fqu_trans: âh,g,G1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â â¦G2, L2, T
/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/
[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 ⦠H) -H
#K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
- /4 width=7 by cpx_delta, fqu_drop, ldrop_ldrop, ex3_2_intro/
+ /4 width=7 by cpx_delta, fqu_drop, ldrop_drop, ex3_2_intro/
| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
elim (lpx_ldrop_trans_O1 ⦠HL01 ⦠HLK1) -L1
/3 width=5 by fqu_drop, ex3_2_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index b26b7e95b..af0172fdb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -36,11 +36,11 @@ inductive ldrop (s:bool): relation4 nat nat lenv lenv â
interpretation
"basic slicing (local environment) abstract"
'RDrop s d e L1 L2 = (ldrop s d e L1 L2).
-
+(*
interpretation
"basic slicing (local environment) general"
'RDrop d e L1 L2 = (ldrop true d e L1 L2).
-
+*)
interpretation
"basic slicing (local environment) lget"
'RDrop e L1 L2 = (ldrop false O e L1 L2).
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma
index 45cf9cda7..5cccd8fe1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma
@@ -27,7 +27,7 @@ lemma aaa_ssta_conf: âh,g,G,L. Conf3 ⦠(aaa G L) (ssta h g G L).
| #I #G #L #K #V #B #i #HLK #HV #IHV #U #H
elim (ssta_inv_lref1 ⦠H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HU
lapply (ldrop_mono ⦠HLK0 ⦠HLK) -HLK0 #H0 destruct
- lapply (ldrop_fwd_ldrop2 ⦠HLK) -HLK #HLK
+ lapply (ldrop_fwd_drop2 ⦠HLK) -HLK #HLK
@(aaa_lift ⦠HLK ⦠HU) -HU -L // -HV /2 width=2/
| #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #H
elim (ssta_inv_bind1 ⦠H) -H #U #HTU #H destruct /3 width=2/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
index 94aec3b15..ff975d25a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
@@ -108,11 +108,11 @@ lemma ssta_da_conf: âh,g,G,L,T,U. â¦G, L⦠⢠T â¢[h, g] U â
| #G #L #K #V #U #W #i #HLK #_ #HWU #IHVW #l #H
elim (da_inv_lref ⦠H) -H * #K0 #V0 [| #l0] #HLK0 #HV0
lapply (ldrop_mono ⦠HLK0 ⦠HLK) -HLK0 #H destruct
- lapply (ldrop_fwd_ldrop2 ⦠HLK) -HLK /3 width=7/
+ lapply (ldrop_fwd_drop2 ⦠HLK) -HLK /3 width=7/
| #G #L #K #W #U #l0 #i #HLK #_ #HWU #l #H -l0
elim (da_inv_lref ⦠H) -H * #K0 #V0 [| #l1] #HLK0 #HV0 [| #H0 ]
lapply (ldrop_mono ⦠HLK0 ⦠HLK) -HLK0 #H destruct
- lapply (ldrop_fwd_ldrop2 ⦠HLK) -HLK /3 width=7/
+ lapply (ldrop_fwd_drop2 ⦠HLK) -HLK /3 width=7/
| #a #I #G #L #V #T #U #_ #IHTU #l #H
lapply (da_inv_bind ⦠H) -H /3 width=1/
| #G #L #V #T #U #_ #IHTU #l #H
@@ -129,11 +129,11 @@ lemma ssta_fwd_correct: âh,g,G,L,T,U. â¦G, L⦠⢠T â¢[h, g] U â
#h #g #G #L #T #U #H elim H -G -L -T -U
[ /2 width=2/
| #G #L #K #V #U #W #i #HLK #_ #HWU * #T #HWT
- lapply (ldrop_fwd_ldrop2 ⦠HLK) -HLK #HLK
+ lapply (ldrop_fwd_drop2 ⦠HLK) -HLK #HLK
elim (lift_total T 0 (i+1)) /3 width=10/
| #G #L #K #W #U #l #i #HLK #HWl #HWU
elim (da_ssta ⦠HWl) -HWl #T #HWT
- lapply (ldrop_fwd_ldrop2 ⦠HLK) -HLK #HLK
+ lapply (ldrop_fwd_drop2 ⦠HLK) -HLK #HLK
elim (lift_total T 0 (i+1)) /3 width=10/
| #a #I #G #L #V #T #U #_ * /3 width=2/
| #G #L #V #T #U #_ * #T0 #HUT0 /3 width=2/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
index 929007118..3fb179ed2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
@@ -21,7 +21,7 @@ include "basic_2/substitution/cpys_lift.ma".
inductive cpysa: ynat â ynat â relation4 genv lenv term term â
| cpysa_atom : âI,G,L,d,e. cpysa d e G L (âª{I}) (âª{I})
| cpysa_subst: âI,G,L,K,V1,V2,W2,i,d,e. d ⤠yinj i â i < d+e â
- â©[0, i] L â¡ K.â{I}V1 â cpysa 0 (â«°(d+e-i)) G K V1 V2 â
+ â©[i] L â¡ K.â{I}V1 â cpysa 0 (â«°(d+e-i)) G K V1 V2 â
â§[0, i+1] V2 â¡ W2 â cpysa d e G L (#i) W2
| cpysa_bind : âa,I,G,L,V1,V2,T1,T2,d,e.
cpysa d e G L V1 V2 â cpysa (⫯d) e G (L.â{I}V2) T1 T2 â
@@ -58,7 +58,7 @@ lemma cpysa_cpy_trans: âG,L,T1,T,d,e. â¦G, L⦠⢠T1 â¶â¶*Ã[d, e] T â
[ #I #G #L #d #e #X #H
elim (cpy_inv_atom1 ⦠H) -H // * /2 width=7 by cpysa_subst/
| #I #G #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK #_ #HVW2 #IHV12 #T2 #H
- lapply (ldrop_fwd_ldrop2 ⦠HLK) #H0LK
+ lapply (ldrop_fwd_drop2 ⦠HLK) #H0LK
lapply (cpy_weak ⦠H 0 (d+e) ? ?) -H // #H
elim (cpy_inv_lift1_be ⦠H ⦠H0LK ⦠HVW2) -H -H0LK -HVW2
/3 width=7 by cpysa_subst, ylt_fwd_le_succ/
@@ -86,7 +86,7 @@ qed-.
lemma cpys_ind_alt: âR:ynatâynatârelation4 genv lenv term term.
(âI,G,L,d,e. R d e G L (âª{I}) (âª{I})) â
(âI,G,L,K,V1,V2,W2,i,d,e. d ⤠yinj i â i < d + e â
- â©[O, i] L â¡ K.â{I}V1 â â¦G, K⦠⢠V1 â¶*Ã[O, â«°(d+e-i)] V2 â
+ â©[i] L â¡ K.â{I}V1 â â¦G, K⦠⢠V1 â¶*Ã[O, â«°(d+e-i)] V2 â
â§[O, i+1] V2 â¡ W2 â R O (â«°(d+e-i)) G K V1 V2 â R d e G L (#i) W2
) â
(âa,I,G,L,V1,V2,T1,T2,d,e. â¦G, L⦠⢠V1 â¶*Ã[d, e] V2 â
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
index aec0c7913..a3eedc255 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
@@ -59,11 +59,11 @@ lemma cpys_split_up: âG,L,T1,T2,d,e. â¦G, L⦠⢠T1 â¶*Ã[d, e] T2 â
qed-.
lemma cpys_inv_lift1_up: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et] U2 â
- âK,d,e. â©[d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
- d ⤠dt â dt ⤠d + e â d + e ⤠dt + et â
- ââT2. â¦G, K⦠⢠T1 â¶*Ã[d, dt + et - (d + e)] T2 &
+ âK,s,d,e. â©[s, d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
+ d ⤠dt â dt ⤠yinj d + e â yinj d + e ⤠dt + et â
+ ââT2. â¦G, K⦠⢠T1 â¶*Ã[d, dt + et - (yinj d + e)] T2 &
â§[d, e] T2 â¡ U2.
-#G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
+#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
elim (cpys_split_up ⦠HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2
lapply (cpys_weak ⦠HU1 d e ? ?) -HU1 // [ >ymax_pre_sn_comm // ] -Hddt -Hdtde #HU1
lapply (cpys_inv_lift1_eq ⦠HU1 ⦠HTU1) -HU1 #HU1 destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
index c4b9518e6..4a621d7d6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
@@ -21,14 +21,14 @@ include "basic_2/substitution/cpys.ma".
lemma cpys_subst: âI,G,L,K,V,U1,i,d,e.
d ⤠yinj i â i < d + e â
- â©[0, i] L â¡ K.â{I}V â â¦G, K⦠⢠V â¶*Ã[0, â«°(d+e-i)] U1 â
+ â©[i] L â¡ K.â{I}V â â¦G, K⦠⢠V â¶*Ã[0, â«°(d+e-i)] U1 â
âU2. â§[0, i+1] U1 â¡ U2 â â¦G, L⦠⢠#i â¶*Ã[d, e] U2.
#I #G #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(cpys_ind ⦠H) -U1
[ /3 width=5 by cpy_cpys, cpy_subst/
| #U #U1 #_ #HU1 #IHU #U2 #HU12
elim (lift_total U 0 (i+1)) #U0 #HU0
lapply (IHU ⦠HU0) -IHU #H
- lapply (ldrop_fwd_ldrop2 ⦠HLK) -HLK #HLK
+ lapply (ldrop_fwd_drop2 ⦠HLK) -HLK #HLK
lapply (cpy_lift_ge ⦠HU1 ⦠HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02
lapply (cpy_weak ⦠HU02 d e ? ?) -HU02
[2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ]
@@ -38,7 +38,7 @@ qed.
lemma cpys_subst_Y2: âI,G,L,K,V,U1,i,d.
d ⤠yinj i â
- â©[0, i] L â¡ K.â{I}V â â¦G, K⦠⢠V â¶*Ã[0, â] U1 â
+ â©[i] L â¡ K.â{I}V â â¦G, K⦠⢠V â¶*Ã[0, â] U1 â
âU2. â§[0, i+1] U1 â¡ U2 â â¦G, L⦠⢠#i â¶*Ã[d, â] U2.
#I #G #L #K #V #U1 #i #d #Hdi #HLK #HVU1 #U2 #HU12
@(cpys_subst ⦠HLK ⦠HU12) >yminus_Y_inj //
@@ -49,7 +49,7 @@ qed.
lemma cpys_inv_atom1: âI,G,L,T2,d,e. â¦G, L⦠⢠âª{I} â¶*Ã[d, e] T2 â
T2 = âª{I} â¨
ââJ,K,V1,V2,i. d ⤠yinj i & i < d + e &
- â©[O, i] L â¡ K.â{J}V1 &
+ â©[i] L â¡ K.â{J}V1 &
â¦G, K⦠⢠V1 â¶*Ã[0, â«°(d+e-i)] V2 &
â§[O, i+1] V2 â¡ T2 &
I = LRef i.
@@ -59,7 +59,7 @@ lemma cpys_inv_atom1: âI,G,L,T2,d,e. â¦G, L⦠⢠âª{I} â¶*Ã[d, e] T2 â
[ #H destruct
elim (cpy_inv_atom1 ⦠HT2) -HT2 [ /2 width=1 by or_introl/ | * /3 width=11 by ex6_5_intro, or_intror/ ]
| * #J #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
- lapply (ldrop_fwd_ldrop2 ⦠HLK) #H
+ lapply (ldrop_fwd_drop2 ⦠HLK) #H
elim (cpy_inv_lift1_ge_up ⦠HT2 ⦠H ⦠HVT) -HT2 -H -HVT
[2,3,4: /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ ]
/4 width=11 by cpys_strap1, ex6_5_intro, or_intror/
@@ -70,7 +70,7 @@ qed-.
lemma cpys_inv_lref1: âG,L,T2,i,d,e. â¦G, L⦠⢠#i â¶*Ã[d, e] T2 â
T2 = #i â¨
ââI,K,V1,V2. d ⤠i & i < d + e &
- â©[O, i] L â¡ K.â{I}V1 &
+ â©[i] L â¡ K.â{I}V1 &
â¦G, K⦠⢠V1 â¶*Ã[0, â«°(d+e-i)] V2 &
â§[O, i+1] V2 â¡ T2.
#G #L #T2 #i #d #e #H elim (cpys_inv_atom1 ⦠H) -H /2 width=1 by or_introl/
@@ -78,7 +78,7 @@ lemma cpys_inv_lref1: âG,L,T2,i,d,e. â¦G, L⦠⢠#i â¶*Ã[d, e] T2 â
qed-.
lemma cpys_inv_lref1_ldrop: âG,L,T2,i,d,e. â¦G, L⦠⢠#i â¶*Ã[d, e] T2 â
- âI,K,V1. â©[O, i] L â¡ K.â{I}V1 â
+ âI,K,V1. â©[i] L â¡ K.â{I}V1 â
âV2. â§[O, i+1] V2 â¡ T2 â
â§â§ â¦G, K⦠⢠V1 â¶*Ã[0, â«°(d+e-i)] V2
& d ⤠i
@@ -95,10 +95,10 @@ qed-.
(* Properties on relocation *************************************************)
lemma cpys_lift_le: âG,K,T1,T2,dt,et. â¦G, K⦠⢠T1 â¶*Ã[dt, et] T2 â
- âL,U1,d,e. dt + et ⤠yinj d â â©[d, e] L â¡ K â
+ âL,U1,s,d,e. dt + et ⤠yinj d â â©[s, d, e] L â¡ K â
â§[d, e] T1 â¡ U1 â âU2. â§[d, e] T2 â¡ U2 â
â¦G, L⦠⢠U1 â¶*Ã[dt, et] U2.
-#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(cpys_ind ⦠H) -T2
+#G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdetd #HLK #HTU1 @(cpys_ind ⦠H) -T2
[ #U2 #H >(lift_mono ⦠HTU1 ⦠H) -H //
| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
elim (lift_total T d e) #U #HTU
@@ -108,10 +108,10 @@ lemma cpys_lift_le: âG,K,T1,T2,dt,et. â¦G, K⦠⢠T1 â¶*Ã[dt, et] T2 â
qed-.
lemma cpys_lift_be: âG,K,T1,T2,dt,et. â¦G, K⦠⢠T1 â¶*Ã[dt, et] T2 â
- âL,U1,d,e. dt ⤠yinj d â d ⤠dt + et â
- â©[d, e] L â¡ K â â§[d, e] T1 â¡ U1 â
+ âL,U1,s,d,e. dt ⤠yinj d â d ⤠dt + et â
+ â©[s, d, e] L â¡ K â â§[d, e] T1 â¡ U1 â
âU2. â§[d, e] T2 â¡ U2 â â¦G, L⦠⢠U1 â¶*Ã[dt, et + e] U2.
-#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind ⦠H) -T2
+#G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind ⦠H) -T2
[ #U2 #H >(lift_mono ⦠HTU1 ⦠H) -H //
| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
elim (lift_total T d e) #U #HTU
@@ -121,10 +121,10 @@ lemma cpys_lift_be: âG,K,T1,T2,dt,et. â¦G, K⦠⢠T1 â¶*Ã[dt, et] T2 â
qed-.
lemma cpys_lift_ge: âG,K,T1,T2,dt,et. â¦G, K⦠⢠T1 â¶*Ã[dt, et] T2 â
- âL,U1,d,e. yinj d ⤠dt â â©[d, e] L â¡ K â
+ âL,U1,s,d,e. yinj d ⤠dt â â©[s, d, e] L â¡ K â
â§[d, e] T1 â¡ U1 â âU2. â§[d, e] T2 â¡ U2 â
â¦G, L⦠⢠U1 â¶*Ã[dt+e, et] U2.
-#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(cpys_ind ⦠H) -T2
+#G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hddt #HLK #HTU1 @(cpys_ind ⦠H) -T2
[ #U2 #H >(lift_mono ⦠HTU1 ⦠H) -H //
| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
elim (lift_total T d e) #U #HTU
@@ -136,10 +136,10 @@ qed-.
(* Inversion lemmas for relocation ******************************************)
lemma cpys_inv_lift1_le: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et] U2 â
- âK,d,e. â©[d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
+ âK,s,d,e. â©[s, d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
dt + et ⤠d â
ââT2. â¦G, K⦠⢠T1 â¶*Ã[dt, et] T2 & â§[d, e] T2 â¡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind ⦠H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind ⦠H) -U2
[ /2 width=3 by ex2_intro/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
elim (cpy_inv_lift1_le ⦠HU2 ⦠HLK ⦠HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
@@ -147,10 +147,10 @@ lemma cpys_inv_lift1_le: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et] U2
qed-.
lemma cpys_inv_lift1_be: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et] U2 â
- âK,d,e. â©[d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
- dt ⤠d â d + e ⤠dt + et â
+ âK,s,d,e. â©[s, d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
+ dt ⤠d â yinj d + e ⤠dt + et â
ââT2. â¦G, K⦠⢠T1 â¶*Ã[dt, et - e] T2 & â§[d, e] T2 â¡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind ⦠H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind ⦠H) -U2
[ /2 width=3 by ex2_intro/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
elim (cpy_inv_lift1_be ⦠HU2 ⦠HLK ⦠HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
@@ -158,10 +158,10 @@ lemma cpys_inv_lift1_be: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et] U2
qed-.
lemma cpys_inv_lift1_ge: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et] U2 â
- âK,d,e. â©[d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
- d + e ⤠dt â
+ âK,s,d,e. â©[s, d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
+ yinj d + e ⤠dt â
ââT2. â¦G, K⦠⢠T1 â¶*Ã[dt - e, et] T2 & â§[d, e] T2 â¡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind ⦠H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind ⦠H) -U2
[ /2 width=3 by ex2_intro/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
elim (cpy_inv_lift1_ge ⦠HU2 ⦠HLK ⦠HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
@@ -171,11 +171,11 @@ qed-.
(* Advanced inversion lemmas on relocation **********************************)
lemma cpys_inv_lift1_ge_up: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et] U2 â
- âK,d,e. â©[d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
- d ⤠dt â dt ⤠d + e â d + e ⤠dt + et â
- ââT2. â¦G, K⦠⢠T1 â¶*Ã[d, dt + et - (d + e)] T2 &
+ âK,s,d,e. â©[s, d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
+ d ⤠dt â dt ⤠yinj d + e â yinj d + e ⤠dt + et â
+ ââT2. â¦G, K⦠⢠T1 â¶*Ã[d, dt + et - (yinj d + e)] T2 &
â§[d, e] T2 â¡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind ⦠H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind ⦠H) -U2
[ /2 width=3 by ex2_intro/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
elim (cpy_inv_lift1_ge_up ⦠HU2 ⦠HLK ⦠HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
@@ -183,10 +183,10 @@ lemma cpys_inv_lift1_ge_up: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et]
qed-.
lemma cpys_inv_lift1_be_up: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et] U2 â
- âK,d,e. â©[d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
- dt ⤠d â dt + et ⤠d + e â
+ âK,s,d,e. â©[s, d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
+ dt ⤠d â dt + et ⤠yinj d + e â
ââT2. â¦G, K⦠⢠T1 â¶*Ã[dt, d - dt] T2 & â§[d, e] T2 â¡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind ⦠H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind ⦠H) -U2
[ /2 width=3 by ex2_intro/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
elim (cpy_inv_lift1_be_up ⦠HU2 ⦠HLK ⦠HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
@@ -194,10 +194,10 @@ lemma cpys_inv_lift1_be_up: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et]
qed-.
lemma cpys_inv_lift1_le_up: âG,L,U1,U2,dt,et. â¦G, L⦠⢠U1 â¶*Ã[dt, et] U2 â
- âK,d,e. â©[d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
- dt ⤠d â d ⤠dt + et â dt + et ⤠d + e â
+ âK,s,d,e. â©[s, d, e] L â¡ K â âT1. â§[d, e] T1 â¡ U1 â
+ dt ⤠d â d ⤠dt + et â dt + et ⤠yinj d + e â
ââT2. â¦G, K⦠⢠T1 â¶*Ã[dt, d - dt] T2 & â§[d, e] T2 â¡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind ⦠H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind ⦠H) -U2
[ /2 width=3 by ex2_intro/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
elim (cpy_inv_lift1_le_up ⦠HU2 ⦠HLK ⦠HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma
index 82a8f5ed0..e68fe729b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma
@@ -37,7 +37,7 @@ lemma fqup_strap2: âG1,G,G2,L1,L,L2,T1,T,T2.
â¦G1, L1, T1⦠â+ â¦G2, L2, T2â¦.
/2 width=5 by tri_TC_strap/ qed.
-lemma fqup_ldrop: âG1,G2,L1,K1,K2,T1,T2,U1,e. â©[0, e] L1 â¡ K1 â â§[0, e] T1 â¡ U1 â
+lemma fqup_ldrop: âG1,G2,L1,K1,K2,T1,T2,U1,e. â©[e] L1 â¡ K1 â â§[0, e] T1 â¡ U1 â
â¦G1, K1, T1⦠â+ â¦G2, K2, T2⦠â â¦G1, L1, U1⦠â+ â¦G2, K2, T2â¦.
#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt ⦠e) #H destruct
[ >(ldrop_inv_O2 ⦠HLK1) -L1 <(lift_inv_O2 ⦠HTU1) -U1 //
@@ -45,7 +45,7 @@ lemma fqup_ldrop: âG1,G2,L1,K1,K2,T1,T2,U1,e. â©[0, e] L1 â¡ K1 â â§[0, e
]
qed-.
-lemma fqup_lref: âI,G,L,K,V,i. â©[0, i] L â¡ K.â{I}V â â¦G, L, #i⦠â+ â¦G, K, Vâ¦.
+lemma fqup_lref: âI,G,L,K,V,i. â©[i] L â¡ K.â{I}V â â¦G, L, #i⦠â+ â¦G, K, Vâ¦.
/3 width=6 by fqu_lref_O, fqu_fqup, lift_lref_ge, fqup_ldrop/ qed.
lemma fqup_pair_sn: âI,G,L,V,T. â¦G, L, â¡{I}V.T⦠â+ â¦G, L, Vâ¦.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
index 325be4b39..c05bb1145 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
@@ -56,7 +56,7 @@ lemma fqus_strap2: âG1,G,G2,L1,L,L2,T1,T,T2. â¦G1, L1, T1⦠â⸮ â¦G, L,
/2 width=5 by tri_TC_strap/ qed-.
lemma fqus_ldrop: âG1,G2,K1,K2,T1,T2. â¦G1, K1, T1⦠â* â¦G2, K2, T2⦠â
- âL1,U1,e. â©[0, e] L1 â¡ K1 â â§[0, e] T1 â¡ U1 â
+ âL1,U1,e. â©[e] L1 â¡ K1 â â§[0, e] T1 â¡ U1 â
â¦G1, L1, U1⦠â* â¦G2, K2, T2â¦.
#G1 #G2 #K1 #K2 #T1 #T2 #H @(fqus_ind ⦠H) -G2 -K2 -T2
/3 width=5 by fqus_strap1, fquq_fqus, fquq_drop/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
index 912487a44..868b8ec2a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
@@ -13,53 +13,59 @@
(**************************************************************************)
include "basic_2/notation/relations/rdropstar_3.ma".
+include "basic_2/notation/relations/rdropstar_4.ma".
include "basic_2/relocation/ldrop.ma".
include "basic_2/substitution/gr2_minus.ma".
include "basic_2/substitution/lifts.ma".
-(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
+(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
-inductive ldrops: list2 nat nat â relation lenv â
-| ldrops_nil : âL. ldrops (â ) L L
+inductive ldrops (s:bool): list2 nat nat â relation lenv â
+| ldrops_nil : âL. ldrops s (â ) L L
| ldrops_cons: âL1,L,L2,des,d,e.
- ldrops des L1 L â â©[d,e] L â¡ L2 â ldrops ({d, e} @ des) L1 L2
+ ldrops s des L1 L â â©[s, d, e] L â¡ L2 â ldrops s ({d, e} @ des) L1 L2
.
-interpretation "generic local environment slicing"
- 'RDropStar des T1 T2 = (ldrops des T1 T2).
+interpretation "iterated slicing (local environment) abstract"
+ 'RDropStar s des T1 T2 = (ldrops s des T1 T2).
+(*
+interpretation "iterated slicing (local environment) general"
+ 'RDropStar des T1 T2 = (ldrops true des T1 T2).
+*)
(* Basic inversion lemmas ***************************************************)
-fact ldrops_inv_nil_aux: âL1,L2,des. â©*[des] L1 â¡ L2 â des = â â L1 = L2.
-#L1 #L2 #des * -L1 -L2 -des //
+fact ldrops_inv_nil_aux: âL1,L2,s,des. â©*[s, des] L1 â¡ L2 â des = â â L1 = L2.
+#L1 #L2 #s #des * -L1 -L2 -des //
#L1 #L #L2 #d #e #des #_ #_ #H destruct
qed-.
(* Basic_1: was: drop1_gen_pnil *)
-lemma ldrops_inv_nil: âL1,L2. â©*[â ] L1 â¡ L2 â L1 = L2.
-/2 width=3 by ldrops_inv_nil_aux/ qed-.
+lemma ldrops_inv_nil: âL1,L2,s. â©*[s, â ] L1 â¡ L2 â L1 = L2.
+/2 width=4 by ldrops_inv_nil_aux/ qed-.
-fact ldrops_inv_cons_aux: âL1,L2,des. â©*[des] L1 â¡ L2 â
+fact ldrops_inv_cons_aux: âL1,L2,s,des. â©*[s, des] L1 â¡ L2 â
âd,e,tl. des = {d, e} @ tl â
- ââL. â©*[tl] L1 â¡ L & â©[d, e] L â¡ L2.
-#L1 #L2 #des * -L1 -L2 -des
+ ââL. â©*[s, tl] L1 â¡ L & â©[s, d, e] L â¡ L2.
+#L1 #L2 #s #des * -L1 -L2 -des
[ #L #d #e #tl #H destruct
| #L1 #L #L2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
/2 width=3 by ex2_intro/
+]
qed-.
(* Basic_1: was: drop1_gen_pcons *)
-lemma ldrops_inv_cons: âL1,L2,d,e,des. â©*[{d, e} @ des] L1 â¡ L2 â
- ââL. â©*[des] L1 â¡ L & â©[d, e] L â¡ L2.
+lemma ldrops_inv_cons: âL1,L2,s,d,e,des. â©*[s, {d, e} @ des] L1 â¡ L2 â
+ ââL. â©*[s, des] L1 â¡ L & â©[s, d, e] L â¡ L2.
/2 width=3 by ldrops_inv_cons_aux/ qed-.
-lemma ldrops_inv_skip2: âI,des,i,des2. des â i â¡ des2 â
- âL1,K2,V2. â©*[des2] L1 â¡ K2. â{I} V2 â
+lemma ldrops_inv_skip2: âI,s,des,des2,i. des â i â¡ des2 â
+ âL1,K2,V2. â©*[s, des2] L1 â¡ K2. â{I} V2 â
ââK1,V1,des1. des + 1 â i + 1 â¡ des1 + 1 &
- â©*[des1] K1 â¡ K2 &
+ â©*[s, des1] K1 â¡ K2 &
â§*[des1] V2 â¡ V1 &
L1 = K1. â{I} V1.
-#I #des #i #des2 #H elim H -des -i -des2
+#I #s #des #des2 #i #H elim H -des -des2 -i
[ #i #L1 #K2 #V2 #H
>(ldrops_inv_nil ⦠H) -L1 /2 width=7 by lifts_nil, minuss_nil, ex4_3_intro, ldrops_nil/
| #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H
@@ -77,9 +83,9 @@ qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: drop1_skip_bind *)
-lemma ldrops_skip: âL1,L2,des. â©*[des] L1 â¡ L2 â âV1,V2. â§*[des] V2 â¡ V1 â
- âI. â©*[des + 1] L1. â{I} V1 â¡ L2. â{I} V2.
-#L1 #L2 #des #H elim H -L1 -L2 -des
+lemma ldrops_skip: âL1,L2,s,des. â©*[s, des] L1 â¡ L2 â âV1,V2. â§*[des] V2 â¡ V1 â
+ âI. â©*[s, des + 1] L1.â{I}V1 â¡ L2.â{I}V2.
+#L1 #L2 #s #des #H elim H -L1 -L2 -des
[ #L #V1 #V2 #HV12 #I
>(lifts_inv_nil ⦠HV12) -HV12 //
| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #V1 #V2 #H #I
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
index 22eed845f..958052e5b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
@@ -15,21 +15,21 @@
include "basic_2/relocation/ldrop_ldrop.ma".
include "basic_2/substitution/ldrops.ma".
-(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
+(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
(* Properties concerning basic local environment slicing ********************)
-lemma ldrops_ldrop_trans: âL1,L,des. â©*[des] L1 â¡ L â âL2,i. â©[0, i] L â¡ L2 â
- ââL0,des0,i0. â©[0, i0] L1 â¡ L0 & â©*[des0] L0 â¡ L2 &
+lemma ldrops_ldrop_trans: âL1,L,des. â©*[â», des] L1 â¡ L â âL2,i. â©[i] L â¡ L2 â
+ ââL0,des0,i0. â©[i0] L1 â¡ L0 & â©*[â», des0] L0 â¡ L2 &
@â¦i, des⦠⡠i0 & des â i â¡ des0.
#L1 #L #des #H elim H -L1 -L -des
-[ /2 width=7/
+[ /2 width=7 by ldrops_nil, minuss_nil, at_nil, ex4_3_intro/
| #L1 #L3 #L #des3 #d #e #_ #HL3 #IHL13 #L2 #i #HL2
elim (lt_or_ge i d) #Hid
- [ elim (ldrop_trans_le ⦠HL3 ⦠HL2) -L /2 width=2/ #L #HL3 #HL2
- elim (IHL13 ⦠HL3) -L3 /3 width=7/
+ [ elim (ldrop_trans_le ⦠HL3 ⦠HL2) -L /2 width=2 by lt_to_le/
+ #L #HL3 #HL2 elim (IHL13 ⦠HL3) -L3 /3 width=7 by ldrops_cons, minuss_lt, at_lt, ex4_3_intro/
| lapply (ldrop_trans_ge ⦠HL3 ⦠HL2 ?) -L // #HL32
- elim (IHL13 ⦠HL32) -L3 /3 width=7/
+ elim (IHL13 ⦠HL32) -L3 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/
]
]
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma
index a4dbfb02e..474862b8c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma
@@ -14,12 +14,12 @@
include "basic_2/substitution/ldrops_ldrop.ma".
-(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
+(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
(* Main properties **********************************************************)
(* Basic_1: was: drop1_trans *)
-theorem ldrops_trans: âL,L2,des2. â©*[des2] L â¡ L2 â âL1,des1. â©*[des1] L1 â¡ L â
- â©*[des2 @@ des1] L1 â¡ L2.
-#L #L2 #des2 #H elim H -L -L2 -des2 // /3 width=3/
-qed.
+theorem ldrops_trans: âL,L2,s,des2. â©*[s, des2] L â¡ L2 â âL1,des1. â©*[s, des1] L1 â¡ L â
+ â©*[s, des2 @@ des1] L1 â¡ L2.
+#L #L2 #s #des2 #H elim H -L -L2 -des2 /3 width=3 by ldrops_cons/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
index 577343c6e..47d88486d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
@@ -100,14 +100,14 @@ lemma lleq_fwd_length: âL1,L2,T,d. L1 â[T, d] L2 â |L1| = |L2|.
#L1 #L2 #T #d * //
qed-.
-lemma lleq_fwd_ldrop_sn: âL1,L2,T,d. L1 â[d, T] L2 â âK1,i. â©[0, i] L1 â¡ K1 â
- âK2. â©[0, i] L2 â¡ K2.
+lemma lleq_fwd_ldrop_sn: âL1,L2,T,d. L1 â[d, T] L2 â âK1,i. â©[i] L1 â¡ K1 â
+ âK2. â©[i] L2 â¡ K2.
#L1 #L2 #T #d #H #K1 #i #HLK1 lapply (lleq_fwd_length ⦠H) -H
#HL12 lapply (ldrop_fwd_length_le2 ⦠HLK1) -HLK1 /2 width=1 by ldrop_O1_le/
qed-.
-lemma lleq_fwd_ldrop_dx: âL1,L2,T,d. L1 â[d, T] L2 â âK2,i. â©[0, i] L2 â¡ K2 â
- âK1. â©[0, i] L1 â¡ K1.
+lemma lleq_fwd_ldrop_dx: âL1,L2,T,d. L1 â[d, T] L2 â âK2,i. â©[i] L2 â¡ K2 â
+ âK1. â©[i] L1 â¡ K1.
/3 width=6 by lleq_fwd_ldrop_sn, lleq_sym/ qed-.
lemma lleq_fwd_bind_sn: âa,I,L1,L2,V,T,d.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
index 0d99e8e1e..70bd0d615 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
@@ -19,7 +19,7 @@ inductive lleqa: relation4 ynat term lenv lenv â
| lleqa_sort: âL1,L2,d,k. |L1| = |L2| â lleqa d (âk) L1 L2
| lleqa_skip: âL1,L2,d,i. |L1| = |L2| â yinj i < d â lleqa d (#i) L1 L2
| lleqa_lref: âI1,I2,L1,L2,K1,K2,V,d,i. d ⤠yinj i â
- â©[0, i] L1 â¡ K1.â{I1}V â â©[0, i] L2 â¡ K2.â{I2}V â
+ â©[i] L1 â¡ K1.â{I1}V â â©[i] L2 â¡ K2.â{I2}V â
lleqa (yinj 0) V K1 K2 â lleqa d (#i) L1 L2
| lleqa_free: âL1,L2,d,i. |L1| = |L2| â |L1| ⤠i â |L2| ⤠i â lleqa d (#i) L1 L2
| lleqa_gref: âL1,L2,d,p. |L1| = |L2| â lleqa d (§p) L1 L2
@@ -61,7 +61,7 @@ lemma lleq_ind_alt: âR:relation4 ynat term lenv lenv. (
âL1,L2,d,i. |L1| = |L2| â yinj i < d â R d (#i) L1 L2
) â (
âI1,I2,L1,L2,K1,K2,V,d,i. d ⤠yinj i â
- â©[O, i] L1 â¡ K1.â{I1}V â â©[O, i] L2 â¡ K2.â{I2}V â
+ â©[i] L1 â¡ K1.â{I1}V â â©[i] L2 â¡ K2.â{I2}V â
K1 â[V, yinj O] K2 â R (yinj O) V K1 K2 â R d (#i) L1 L2
) â (
âL1,L2,d,i. |L1| = |L2| â |L1| ⤠i â |L2| ⤠i â R d (#i) L1 L2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma
index a1cf4458d..d6bb03fa7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma
@@ -19,7 +19,7 @@ include "basic_2/substitution/lleq_alt.ma".
(* Advanced inversion lemmas ************************************************)
fact lleq_inv_S_aux: âL1,L2,T,d0. L1 â[T, d0] L2 â âd. d0 = d + 1 â
- âK1,K2,I,V. â©[0, d] L1 â¡ K1.â{I}V â â©[0, d] L2 â¡ K2.â{I}V â
+ âK1,K2,I,V. â©[d] L1 â¡ K1.â{I}V â â©[d] L2 â¡ K2.â{I}V â
K1 â[V, 0] K2 â L1 â[T, d] L2.
#L1 #L2 #T #d0 #H @(lleq_ind_alt ⦠H) -L1 -L2 -T -d0
/2 width=1 by lleq_gref, lleq_free, lleq_sort/
@@ -29,14 +29,14 @@ fact lleq_inv_S_aux: âL1,L2,T,d0. L1 â[T, d0] L2 â âd. d0 = d + 1 â
| #I1 #I2 #L1 #L2 #K11 #K22 #V #d0 #i #Hd0i #HLK11 #HLK22 #HV #_ #d #H #K1 #K2 #J #W #_ #_ #_ destruct
/3 width=8 by lleq_lref, yle_pred_sn/
| #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
- /4 width=7 by lleq_bind, ldrop_ldrop/
+ /4 width=7 by lleq_bind, ldrop_drop/
| #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
/3 width=7 by lleq_flat/
]
qed-.
lemma lleq_inv_S: âT,L1,L2,d. L1 â[T, d+1] L2 â
- âK1,K2,I,V. â©[0, d] L1 â¡ K1.â{I}V â â©[0, d] L2 â¡ K2.â{I}V â
+ âK1,K2,I,V. â©[d] L1 â¡ K1.â{I}V â â©[d] L2 â¡ K2.â{I}V â
K1 â[V, 0] K2 â L1 â[T, d] L2.
/2 width=7 by lleq_inv_S_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
index 126da3dd3..9cb597c6f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
@@ -26,7 +26,7 @@ lemma lleq_skip: âL1,L2,d,i. yinj i < d â |L1| = |L2| â L1 â[#i, d] L2.
qed.
lemma lleq_lref: âI1,I2,L1,L2,K1,K2,V,d,i. d ⤠yinj i â
- â©[0, i] L1 â¡ K1.â{I1}V â â©[0, i] L2 â¡ K2.â{I2}V â
+ â©[i] L1 â¡ K1.â{I1}V â â©[i] L2 â¡ K2.â{I2}V â
K1 â[V, 0] K2 â L1 â[#i, d] L2.
#I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 * #HK12 #IH @conj [ -IH | -HK12 ]
[ lapply (ldrop_fwd_length ⦠HLK1) -HLK1 #H1
@@ -50,31 +50,31 @@ qed.
(* Properties on relocation *************************************************)
lemma lleq_lift_le: âK1,K2,T,dt. K1 â[T, dt] K2 â
- âL1,L2,d,e. â©[d, e] L1 â¡ K1 â â©[d, e] L2 â¡ K2 â
+ âL1,L2,d,e. â©[â», d, e] L1 â¡ K1 â â©[â», d, e] L2 â¡ K2 â
âU. â§[d, e] T â¡ U â dt ⤠d â L1 â[U, dt] L2.
#K1 #K2 #T #dt * #HK12 #IHT #L1 #L2 #d #e #HLK1 #HLK2 #U #HTU #Hdtd
lapply (ldrop_fwd_length ⦠HLK1) lapply (ldrop_fwd_length ⦠HLK2)
#H2 #H1 @conj // -HK12 -H1 -H2 #U0 @conj #HU0
[ letin HLKA â HLK1 letin HLKB â HLK2 | letin HLKA â HLK2 letin HLKB â HLK1 ]
elim (cpys_inv_lift1_be ⦠HU0 ⦠HLKA ⦠HTU) // -HU0 >yminus_Y_inj #T0 #HT0 #HTU0
-elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=11 by cpys_lift_be/
+elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=12 by cpys_lift_be/
qed-.
lemma lleq_lift_ge: âK1,K2,T,dt. K1 â[T, dt] K2 â
- âL1,L2,d,e. â©[d, e] L1 â¡ K1 â â©[d, e] L2 â¡ K2 â
+ âL1,L2,d,e. â©[â», d, e] L1 â¡ K1 â â©[â», d, e] L2 â¡ K2 â
âU. â§[d, e] T â¡ U â d ⤠dt â L1 â[U, dt+e] L2.
#K1 #K2 #T #dt * #HK12 #IHT #L1 #L2 #d #e #HLK1 #HLK2 #U #HTU #Hddt
lapply (ldrop_fwd_length ⦠HLK1) lapply (ldrop_fwd_length ⦠HLK2)
#H2 #H1 @conj // -HK12 -H1 -H2 #U0 @conj #HU0
[ letin HLKA â HLK1 letin HLKB â HLK2 | letin HLKA â HLK2 letin HLKB â HLK1 ]
elim (cpys_inv_lift1_ge ⦠HU0 ⦠HLKA ⦠HTU) /2 width=1 by monotonic_yle_plus_dx/ -HU0 >yplus_minus_inj #T0 #HT0 #HTU0
-elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=9 by cpys_lift_ge/
+elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=10 by cpys_lift_ge/
qed-.
(* Inversion lemmas on relocation *******************************************)
lemma lleq_inv_lift_le: âL1,L2,U,dt. L1 â[U, dt] L2 â
- âK1,K2,d,e. â©[d, e] L1 â¡ K1 â â©[d, e] L2 â¡ K2 â
+ âK1,K2,d,e. â©[â», d, e] L1 â¡ K1 â â©[â», d, e] L2 â¡ K2 â
âT. â§[d, e] T â¡ U â dt ⤠d â K1 â[T, dt] K2.
#L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hdtd
lapply (ldrop_fwd_length_minus2 ⦠HLK1) lapply (ldrop_fwd_length_minus2 ⦠HLK2)
@@ -89,8 +89,8 @@ lapply (cpys_lift_be ⦠HT0 ⦠HLKA ⦠HTU ⦠HTU0) // -HT0
qed-.
lemma lleq_inv_lift_ge: âL1,L2,U,dt. L1 â[U, dt] L2 â
- âK1,K2,d,e. â©[d, e] L1 â¡ K1 â â©[d, e] L2 â¡ K2 â
- âT. â§[d, e] T â¡ U â d+e ⤠dt â K1 â[T, dt-e] K2.
+ âK1,K2,d,e. â©[â», d, e] L1 â¡ K1 â â©[â», d, e] L2 â¡ K2 â
+ âT. â§[d, e] T â¡ U â yinj d + e ⤠dt â K1 â[T, dt-e] K2.
#L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hdedt
lapply (ldrop_fwd_length_minus2 ⦠HLK1) lapply (ldrop_fwd_length_minus2 ⦠HLK2)
#H2 #H1 @conj // -HL12 -H1 -H2
@@ -105,8 +105,8 @@ lapply (cpys_lift_ge ⦠HT0 ⦠HLKA ⦠HTU ⦠HTU0) // -HT0 -Hddt
qed-.
lemma lleq_inv_lift_be: âL1,L2,U,dt. L1 â[U, dt] L2 â
- âK1,K2,d,e. â©[d, e] L1 â¡ K1 â â©[d, e] L2 â¡ K2 â
- âT. â§[d, e] T â¡ U â d ⤠dt â dt ⤠d + e â K1 â[T, d] K2.
+ âK1,K2,d,e. â©[â», d, e] L1 â¡ K1 â â©[â», d, e] L2 â¡ K2 â
+ âT. â§[d, e] T â¡ U â d ⤠dt â dt ⤠yinj d + e â K1 â[T, d] K2.
#L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hddt #Hdtde
lapply (ldrop_fwd_length_minus2 ⦠HLK1) lapply (ldrop_fwd_length_minus2 ⦠HLK2)
#H2 #H1 @conj // -HL12 -H1 -H2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
index 97f2dd675..01e08e9f9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
@@ -20,8 +20,8 @@ include "basic_2/substitution/lleq_ldrop.ma".
lemma lleq_fwd_lref: âL1,L2. âd:ynat. âi:nat. L1 â[#i, d] L2 â
â¨â¨ |L1| ⤠i ⧠|L2| ⤠i
| yinj i < d
- | ââI1,I2,K1,K2,V. â©[0, i] L1 â¡ K1.â{I1}V &
- â©[0, i] L2 â¡ K2.â{I2}V &
+ | ââI1,I2,K1,K2,V. â©[i] L1 â¡ K1.â{I1}V &
+ â©[i] L2 â¡ K2.â{I2}V &
K1 â[V, yinj 0] K2 & d ⤠yinj i.
#L1 #L2 #d #i * #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=3 by or3_intro0, conj/
elim (ylt_split i d) /2 width=1 by or3_intro1/ #Hdi #Hi
@@ -46,9 +46,9 @@ lapply (cpys_antisym_eq ⦠H12 ⦠H21) -H12 -H21 #H destruct
qed-.
lemma lleq_fwd_lref_dx: âL1,L2,d,i. L1 â[#i, d] L2 â
- âI2,K2,V. â©[0, i] L2 â¡ K2.â{I2}V â
+ âI2,K2,V. â©[i] L2 â¡ K2.â{I2}V â
i < d â¨
- ââI1,K1. â©[0, i] L1 â¡ K1.â{I1}V & K1 â[V, 0] K2 & d ⤠i.
+ ââI1,K1. â©[i] L1 â¡ K1.â{I1}V & K1 â[V, 0] K2 & d ⤠i.
#L1 #L2 #d #i #H #I2 #K2 #V #HLK2 elim (lleq_fwd_lref ⦠H) -H [ * || * ]
[ #_ #H elim (lt_refl_false i)
lapply (ldrop_fwd_length_lt2 ⦠HLK2) -HLK2
@@ -60,9 +60,9 @@ lemma lleq_fwd_lref_dx: âL1,L2,d,i. L1 â[#i, d] L2 â
qed-.
lemma lleq_fwd_lref_sn: âL1,L2,d,i. L1 â[#i, d] L2 â
- âI1,K1,V. â©[0, i] L1 â¡ K1.â{I1}V â
+ âI1,K1,V. â©[i] L1 â¡ K1.â{I1}V â
i < d â¨
- ââI2,K2. â©[0, i] L2 â¡ K2.â{I2}V & K1 â[V, 0] K2 & d ⤠i.
+ ââI2,K2. â©[i] L2 â¡ K2.â{I2}V & K1 â[V, 0] K2 & d ⤠i.
#L1 #L2 #d #i #HL12 #I1 #K1 #V #HLK1 elim (lleq_fwd_lref_dx L2 ⦠d ⦠HLK1) -HLK1
[2: * ] /4 width=6 by lleq_sym, ex3_2_intro, or_introl, or_intror/
qed-.
@@ -70,8 +70,8 @@ qed-.
(* Advanced inversion lemmas ************************************************)
lemma lleq_inv_lref_ge_dx: âL1,L2,d,i. L1 â[#i, d] L2 â d ⤠i â
- âI2,K2,V. â©[0, i] L2 â¡ K2.â{I2}V â
- ââI1,K1. â©[0, i] L1 â¡ K1.â{I1}V & K1 â[V, 0] K2.
+ âI2,K2,V. â©[i] L2 â¡ K2.â{I2}V â
+ ââI1,K1. â©[i] L1 â¡ K1.â{I1}V & K1 â[V, 0] K2.
#L1 #L2 #d #i #H #Hdi #I2 #K2 #V #HLK2 elim (lleq_fwd_lref_dx ⦠H ⦠HLK2) -L2
[ #H elim (ylt_yle_false ⦠H Hdi)
| * /2 width=4 by ex2_2_intro/
@@ -79,8 +79,8 @@ lemma lleq_inv_lref_ge_dx: âL1,L2,d,i. L1 â[#i, d] L2 â d ⤠i â
qed-.
lemma lleq_inv_lref_ge_sn: âL1,L2,d,i. L1 â[#i, d] L2 â d ⤠i â
- âI1,K1,V. â©[0, i] L1 â¡ K1.â{I1}V â
- ââI2,K2. â©[0, i] L2 â¡ K2.â{I2}V & K1 â[V, 0] K2.
+ âI1,K1,V. â©[i] L1 â¡ K1.â{I1}V â
+ ââI2,K2. â©[i] L2 â¡ K2.â{I2}V & K1 â[V, 0] K2.
#L1 #L2 #d #i #HL12 #Hdi #I1 #K1 #V #HLK1 elim (lleq_inv_lref_ge_dx L2 ⦠Hdi ⦠HLK1) -Hdi -HLK1
/3 width=4 by lleq_sym, ex2_2_intro/
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma
index 3019423b4..6fab6dec6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma
@@ -47,10 +47,10 @@ lemma lsstasa_step_dx: âh,g,G,L,T1,T,l. â¦G, L⦠⢠T1 â¢â¢*[h, g, l] T
[ /2 width=1/
| #G #L #l #k #X #H >(ssta_inv_sort1 ⦠H) -X >commutative_plus //
| #G #L #K #V #W #U #i #l #HLK #_ #HWU #IHVW #U2 #HU2
- lapply (ldrop_fwd_ldrop2 ⦠HLK) #H
+ lapply (ldrop_fwd_drop2 ⦠HLK) #H
elim (ssta_inv_lift1 ⦠HU2 ⦠H ⦠HWU) -H -U /3 width=6/
| #G #L #K #W #V #U #i #l #l0 #HLK #HWl0 #_ #HVU #IHWV #U2 #HU2
- lapply (ldrop_fwd_ldrop2 ⦠HLK) #H
+ lapply (ldrop_fwd_drop2 ⦠HLK) #H
elim (ssta_inv_lift1 ⦠HU2 ⦠H ⦠HVU) -H -U /3 width=8/
| #a #I #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H
elim (ssta_inv_bind1 ⦠H) -H #U #HU1 #H destruct /3 width=1/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma
index c4c27e9fd..76c9c27f3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma
@@ -39,7 +39,7 @@ lemma lsstas_inv_lref1: âh,g,G,L,U,i,l. â¦G, L⦠⢠#i â¢*[h, g, l+1] U
#h #g #G #L #U #i #l #H elim (lsstas_inv_step_sn ⦠H) -H
#X #H #HXU elim (ssta_inv_lref1 ⦠H) -H
* #K [ #V #W | #W #l0 ] #HLK [ #HVW | #HWl0 ] #HWX
-lapply (ldrop_fwd_ldrop2 ⦠HLK) #H0LK
+lapply (ldrop_fwd_drop2 ⦠HLK) #H0LK
elim (lsstas_inv_lift1 ⦠HXU ⦠H0LK ⦠HWX) -H0LK -X /3 width=8/ /4 width=6/
qed-.
@@ -66,7 +66,7 @@ lemma lsstas_ldef: âh,g,G,L,K,V,i. â©[0, i] L â¡ K.âV â
âW,l. â¦G, K⦠⢠V â¢*[h, g, l+1] W â
âU. â§[0, i+1] W â¡ U â â¦G, L⦠⢠#i â¢*[h, g, l+1] U.
#h #g #G #L #K #V #i #HLK #W #l #HVW #U #HWU
-lapply (ldrop_fwd_ldrop2 ⦠HLK)
+lapply (ldrop_fwd_drop2 ⦠HLK)
elim (lsstas_inv_step_sn ⦠HVW) -HVW #W0
elim (lift_total W0 0 (i+1)) /3 width=11/
qed.
@@ -75,7 +75,7 @@ lemma lsstas_ldec: âh,g,G,L,K,W,i. â©[0, i] L â¡ K.âW â âl0. â¦G, K
âV,l. â¦G, K⦠⢠W â¢*[h, g, l] V â
âU. â§[0, i+1] V â¡ U â â¦G, L⦠⢠#i â¢*[h, g, l+1] U.
#h #g #G #L #K #W #i #HLK #T #HWT #V #l #HWV #U #HVU
-lapply (ldrop_fwd_ldrop2 ⦠HLK) #H
+lapply (ldrop_fwd_drop2 ⦠HLK) #H
elim (lift_total W 0 (i+1)) /3 width=11/
qed.
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 da58e39aa..d2d8186af 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
@@ -221,7 +221,7 @@ table {
[ "fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠)" "fqup_fqup" * ]
}
]
- [ { "generic local env. slicing" * } {
+ [ { "iterated local env. slicing" * } {
[ "ldrops ( â©*[?,?] ? â¡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
}
]