the other components will be committed shortly ...
m,n : reserved: future use
o :
p,q : global reference position
-r,s :
+r : reduction kind parameter (true = ordinary, false = extended)
+s : local dropping kind parameter (true = general, false = restricted)
t,u : local reference position level (de Bruijn's)
v,w :
x,y,z : reserved: transient objet denoted by a small letter
2: binary
A: application to vector
+F: boolean false
+T: boolean true
a: application
b: binder
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⇩ [ term 46 s , break term 46 d , break term 46 e ] break term 46 L1 ≡ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'RDrop $s $d $e $L1 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⇩ * [ term 46 s , break term 46 e ] break term 46 L1 ≡ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'RDropStar $s $e $L1 $L2 }.
inductive cpy: ynat → ynat → relation4 genv lenv term term ≝
| cpy_atom : ∀I,G,L,d,e. cpy d e G L (⓪{I}) (⓪{I})
| cpy_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ yinj i → i < d+e →
- ⇩[0, i] L ≡ K.ⓑ{I}V → ⇧[0, i+1] V ≡ W → cpy d e G L (#i) W
+ ⇩[i] L ≡ K.ⓑ{I}V → ⇧[0, i+1] V ≡ W → cpy d e G L (#i) W
| cpy_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
cpy d e G L V1 V2 → cpy (⫯d) e G (L.ⓑ{I}V2) T1 T2 →
cpy d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
(* Basic properties *********************************************************)
-lemma lsuby_cpy_trans: ∀G,d,e. lsub_trans … (cpy d e G) (lsuby d e).
+lemma lsuby_cpy_trans: ∀G,d,e. lsub_trans … (cpy d e G) (lsuby d e).
#G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e
[ //
| #I #G #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
#G #T elim T -T // * /2 width=1 by cpy_bind, cpy_flat/
qed.
-lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[0, d] L ≡ K.ⓑ{I}V →
+lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[d] L ≡ K.ⓑ{I}V →
∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶×[d, 1] T2 & ⇧[d, 1] T ≡ T2.
#I #G #K #V #T1 elim T1 -T1
[ * #i #L #d #HLK
| * [ #a ] #J #W1 #U1 #IHW1 #IHU1 #L #d #HLK
elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
[ elim (IHU1 (L.ⓑ{J}W2) (d+1)) -IHU1
- /3 width=9 by cpy_bind, ldrop_ldrop, lift_bind, ex2_2_intro/
+ /3 width=9 by cpy_bind, ldrop_drop, lift_bind, ex2_2_intro/
| elim (IHU1 … HLK) -IHU1 -HLK
/3 width=8 by cpy_flat, lift_flat, ex2_2_intro/
]
fact cpy_inv_atom1_aux: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀J. T1 = ⓪{J} →
T2 = ⓪{J} ∨
∃∃I,K,V,i. d ≤ yinj i & i < d + e &
- ⇩[O, i] L ≡ K.ⓑ{I}V &
+ ⇩[i] L ≡ K.ⓑ{I}V &
⇧[O, i+1] V ≡ T2 &
J = LRef i.
#G #L #T1 #T2 #d #e * -G -L -T1 -T2 -d -e
lemma cpy_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶×[d, e] T2 →
T2 = ⓪{I} ∨
∃∃J,K,V,i. d ≤ yinj i & i < d + e &
- ⇩[O, i] L ≡ K.ⓑ{J}V &
+ ⇩[i] L ≡ K.ⓑ{J}V &
⇧[O, i+1] V ≡ T2 &
I = LRef i.
/2 width=4 by cpy_inv_atom1_aux/ qed-.
lemma cpy_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶×[d, e] T2 →
T2 = #i ∨
∃∃I,K,V. d ≤ i & i < d + e &
- ⇩[O, i] L ≡ K.ⓑ{I}V &
+ ⇩[i] L ≡ K.ⓑ{I}V &
⇧[O, i+1] V ≡ T2.
#G #L #T2 #i #d #e #H
elim (cpy_inv_atom1 … H) -H /2 width=1 by or_introl/
(* Properties on relocation *************************************************)
lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
- ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K →
+ ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
dt + et ≤ d → ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2.
#G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et
-[ #I #G #K #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_
+[ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_
>(lift_mono … H1 … H2) -H1 -H2 //
-| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hdetd
+| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #s #d #e #HLK #H #HWU2 #Hdetd
lapply (ylt_yle_trans … Hdetd … Hidet) -Hdetd #Hid
lapply (ylt_inv_inj … Hid) -Hid #Hid
lapply (lift_inv_lref1_lt … H … Hid) -H #H destruct
elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K #Y #_ #HVY
>(lift_mono … HVY … HVW) -Y -HVW #H destruct /2 width=5 by cpy_subst/
-| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd
+| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdetd
elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
- /4 width=6 by cpy_bind, ldrop_skip, yle_succ/
-| #G #I #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd
+ /4 width=7 by cpy_bind, ldrop_skip, yle_succ/
+| #G #I #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdetd
elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
- /3 width=6 by cpy_flat/
+ /3 width=7 by cpy_flat/
]
qed-.
lemma cpy_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
- ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K →
+ ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
dt ≤ d → d ≤ dt + et → ⦃G, L⦄ ⊢ U1 ▶×[dt, et + e] U2.
#G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et
-[ #I #G #K #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ #_
+[ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ #_
>(lift_mono … H1 … H2) -H1 -H2 //
-| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hdtd #_
+| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #s #d #e #HLK #H #HWU2 #Hdtd #_
elim (lift_inv_lref1 … H) -H * #Hid #H destruct
[ -Hdtd
lapply (ylt_yle_trans … (dt+et+e) … Hidet) // -Hidet #Hidete
lapply (transitive_le … Hdtd Hid) -Hdtd #Hdti
lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid
- /4 width=5 by cpy_subst, monotonic_ylt_plus_dx, yle_plus_dx1_trans, yle_inj/
+ /4 width=5 by cpy_subst, ldrop_inv_gen, monotonic_ylt_plus_dx, yle_plus_dx1_trans, yle_inj/
]
-| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdtd #Hddet
+| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdtd #Hddet
elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
- /4 width=6 by cpy_bind, ldrop_skip, yle_succ/
-| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd
+ /4 width=7 by cpy_bind, ldrop_skip, yle_succ/
+| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdetd
elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
- /3 width=6 by cpy_flat/
+ /3 width=7 by cpy_flat/
]
qed-.
lemma cpy_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
- ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K →
+ ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
d ≤ dt → ⦃G, L⦄ ⊢ U1 ▶×[dt+e, et] U2.
#G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et
-[ #I #G #K #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_
+[ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_
>(lift_mono … H1 … H2) -H1 -H2 //
-| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hddt
+| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #s #d #e #HLK #H #HWU2 #Hddt
lapply (yle_trans … Hddt … Hdti) -Hddt #Hid
elim (yle_inv_inj2 … Hid) -Hid #dd #Hddi #H0 destruct
lapply (lift_inv_lref1_ge … H … Hddi) -H #H destruct
lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hddi
- /3 width=5 by cpy_subst, monotonic_ylt_plus_dx, monotonic_yle_plus_dx/
-| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt
+ /3 width=5 by cpy_subst, ldrop_inv_gen, monotonic_ylt_plus_dx, monotonic_yle_plus_dx/
+| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hddt
elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
- /4 width=5 by cpy_bind, ldrop_skip, yle_succ/
-| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt
+ /4 width=6 by cpy_bind, ldrop_skip, yle_succ/
+| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hddt
elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
- /3 width=5 by cpy_flat/
+ /3 width=6 by cpy_flat/
]
qed-.
(* Inversion lemmas on relocation *******************************************)
lemma cpy_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 elim H -G -L -U1 -U2 -dt -et
-[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_
+[ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_
[ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
| elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
| lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
]
-| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdetd
+| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #s #d #e #HLK #T1 #H #Hdetd
lapply (ylt_yle_trans … Hdetd … Hidet) -Hdetd #Hid
lapply (ylt_inv_inj … Hid) -Hid #Hid
lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct
elim (ldrop_conf_lt … HLK … HLKV) -L // #L #U #HKL #_ #HUV
elim (lift_trans_le … HUV … HVW) -V // >minus_plus <plus_minus_m_m // -Hid /3 width=5 by cpy_subst, ex2_intro/
-| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
elim (IHU12 … HTU1) -IHU12 -HTU1
- /3 width=5 by cpy_bind, yle_succ, ldrop_skip, lift_bind, ex2_intro/
-| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+ /3 width=6 by cpy_bind, yle_succ, ldrop_skip, lift_bind, ex2_intro/
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
elim (IHW12 … HLK … HVW1) -W1 //
elim (IHU12 … HLK … HTU1) -U1 -HLK
qed-.
lemma cpy_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 elim H -G -L -U1 -U2 -dt -et
-[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_ #_
+[ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_ #_
[ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
| elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
| lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
]
-| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdtd #Hdedet
+| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #s #d #e #HLK #T1 #H #Hdtd #Hdedet
lapply (yle_fwd_plus_ge_inj … Hdtd Hdedet) #Heet
elim (lift_inv_lref2 … H) -H * #Hid #H destruct [ -Hdtd -Hidet | -Hdti -Hdedet ]
[ lapply (ylt_yle_trans i d (dt+(et-e)) ? ?) /2 width=1 by ylt_inj/
@(ex2_intro … H) @(cpy_subst … HKV HV1) // (**) (* explicit constructor *)
>yplus_minus_assoc_inj /3 width=1 by monotonic_ylt_minus_dx, yle_inj/
]
-| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdtd #Hdedet
elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
elim (IHU12 … HTU1) -U1
- /3 width=5 by cpy_bind, ldrop_skip, lift_bind, yle_succ, ex2_intro/
-| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
+ /3 width=6 by cpy_bind, ldrop_skip, lift_bind, yle_succ, ex2_intro/
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdtd #Hdedet
elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
elim (IHW12 … HLK … HVW1) -W1 //
elim (IHU12 … HLK … HTU1) -U1 -HLK //
qed-.
lemma cpy_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 elim H -G -L -U1 -U2 -dt -et
-[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_
+[ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_
[ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
| elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
| lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
]
-| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt
+| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #s #d #e #HLK #T1 #H #Hdedt
lapply (yle_trans … Hdedt … Hdti) #Hdei
elim (yle_inv_plus_inj2 … Hdedt) -Hdedt #_ #Hedt
elim (yle_inv_plus_inj2 … Hdei) #Hdie #Hei
[ /2 width=1 by monotonic_yle_minus_dx/
| <yplus_minus_comm_inj /2 width=1 by monotonic_ylt_minus_dx/
]
-| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
elim (yle_inv_plus_inj2 … Hdetd) #_ #Hedt
elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
- elim (IHU12 … HTU1) -U1 [4: @ldrop_skip // |2: skip |3: /2 width=1 by yle_succ/ ]
+ elim (IHU12 … HTU1) -U1 [4: @ldrop_skip // |2,5: skip |3: /2 width=1 by yle_succ/ ]
>yminus_succ1_inj /3 width=5 by cpy_bind, lift_bind, ex2_intro/
-| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
elim (IHW12 … HLK … HVW1) -W1 //
elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpy_flat, lift_flat, ex2_intro/
(* Advancd inversion lemmas on relocation ***********************************)
lemma cpy_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 & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
+ ∀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 #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
elim (cpy_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2
lapply (cpy_weak … HU1 d e ? ?) -HU1 // [ >ymax_pre_sn_comm // ] -Hddt -Hdtde #HU1
lapply (cpy_inv_lift1_eq … HTU1 … HU1) -HU1 #HU1 destruct
qed-.
lemma cpy_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 #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde
+#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde
lapply (cpy_weak … HU12 dt (d+e-dt) ? ?) -HU12 //
[ >ymax_pre_sn_comm /2 width=1 by yle_plus_dx1_trans/ ] -Hdetde #HU12
elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) -U1 -L /2 width=3 by ex2_intro/
qed-.
lemma cpy_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 #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde
+#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde
elim (cpy_split_up … HU12 d) -HU12 // #U #HU1 #HU2
elim (cpy_inv_lift1_le … HU1 … HLK … HTU1) -U1
[2: >ymax_pre_sn_comm // ] -Hdtd #T #HT1 #HTU
| fqu_bind_dx: ∀a,I,G,L,V,T. fqu G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
| fqu_flat_dx: ∀I,G,L,V,T. fqu G L (ⓕ{I}V.T) G L T
| fqu_drop : ∀G,L,K,T,U,e.
- ⇩[0, e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fqu G L U G K T
+ ⇩[e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fqu G L U G K T
.
interpretation
(* Basic properties *********************************************************)
lemma fqu_drop_lt: ∀G,L,K,T,U,e. 0 < e →
- ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃ ⦃G, K, T⦄.
+ ⇩[e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃ ⦃G, K, T⦄.
#G #L #K #T #U #e #He >(plus_minus_m_m e 1) /2 width=3 by fqu_drop/
qed.
lemma fqu_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄.
-/3 width=3 by fqu_drop, ldrop_ldrop, lift_lref_ge_minus/
+/3 width=3 by fqu_drop, ldrop_drop, lift_lref_ge_minus/
qed.
(* Basic forward lemmas *****************************************************)
| fquq_bind_dx: ∀a,I,G,L,V,T. fquq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
| fquq_flat_dx: ∀I,G, L,V,T. fquq G L (ⓕ{I}V.T) G L T
| fquq_drop : ∀G,L,K,T,U,e.
- ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fquq G L U G K T
+ ⇩[e] L ≡ K → ⇧[0, e] T ≡ U → fquq G L U G K T
.
interpretation
/2 width=3 by fquq_drop/ qed.
lemma fqu_fquq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=3 by fquq_drop/
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 /2 width=3 by fquq_drop/
qed.
(* Basic forward lemmas *****************************************************)
// qed.
lemma fquqa_drop: ∀G,L,K,T,U,e.
- ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
+ ⇩[e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
#G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e)
/3 width=5 by fqu_drop_lt, or_introl/ #H destruct
>(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
(* *)
(**************************************************************************)
+include "ground_2/lib/bool.ma".
include "ground_2/lib/lstar.ma".
+include "basic_2/notation/relations/rdrop_5.ma".
include "basic_2/notation/relations/rdrop_4.ma".
+include "basic_2/notation/relations/rdrop_3.ma".
include "basic_2/grammar/lenv_length.ma".
include "basic_2/grammar/cl_restricted_weight.ma".
include "basic_2/relocation/lift.ma".
(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
(* Basic_1: includes: drop_skip_bind *)
-inductive ldrop: relation4 nat nat lenv lenv ≝
-| ldrop_atom : ∀d. ldrop d 0 (⋆) (⋆)
-| ldrop_pair : ∀L,I,V. ldrop 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
-| ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. ⓑ{I} V) L2
-| ldrop_skip : ∀L1,L2,I,V1,V2,d,e.
- ldrop d e L1 L2 → ⇧[d,e] V2 ≡ V1 →
- ldrop (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
+inductive ldrop (s:bool): relation4 nat nat lenv lenv ≝
+| ldrop_atom: ∀d,e. (s = Ⓕ → e = 0) → ldrop s d e (⋆) (⋆)
+| ldrop_pair: ∀I,L,V. ldrop s 0 0 (L.ⓑ{I}V) (L.ⓑ{I}V)
+| ldrop_drop: ∀I,L1,L2,V,e. ldrop s 0 e L1 L2 → ldrop s 0 (e+1) (L1.ⓑ{I}V) L2
+| ldrop_skip: ∀I,L1,L2,V1,V2,d,e.
+ ldrop s d e L1 L2 → ⇧[d, e] V2 ≡ V1 →
+ ldrop s (d+1) e (L1.ⓑ{I}V1) (L2.ⓑ{I}V2)
.
interpretation
- "basic slicing (local environment)"
- 'RDrop d e L1 L2 = (ldrop d e L1 L2).
+ "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).
definition l_liftable: predicate (lenv → relation term) ≝
- λR. ∀K,T1,T2. R K T1 T2 → ∀L,d,e. ⇩[d, e] L ≡ K →
+ λR. ∀K,T1,T2. R K T1 T2 → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
∀U1. ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → R L U1 U2.
definition l_deliftable_sn: predicate (lenv → relation term) ≝
- λR. ∀L,U1,U2. R L U1 U2 → ∀K,d,e. ⇩[d, e] L ≡ K →
+ λR. ∀L,U1,U2. R L U1 U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
∀T1. ⇧[d, e] T1 ≡ U1 →
∃∃T2. ⇧[d, e] T2 ≡ U2 & R K T1 T2.
definition dropable_sn: predicate (relation lenv) ≝
- λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. R L1 L2 →
- ∃∃K2. R K1 K2 & ⇩[d, e] L2 ≡ K2.
+ λR. ∀L1,K1,s,d,e. ⇩[s, d, e] L1 ≡ K1 → ∀L2. R L1 L2 →
+ ∃∃K2. R K1 K2 & ⇩[s, d, e] L2 ≡ K2.
definition dedropable_sn: predicate (relation lenv) ≝
- λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. R K1 K2 →
- ∃∃L2. R L1 L2 & ⇩[d, e] L2 ≡ K2.
+ λR. ∀L1,K1,s,d,e. ⇩[s, d, e] L1 ≡ K1 → ∀K2. R K1 K2 →
+ ∃∃L2. R L1 L2 & ⇩[s, d, e] L2 ≡ K2.
definition dropable_dx: predicate (relation lenv) ≝
- λR. ∀L1,L2. R L1 L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. ⇩[0, e] L1 ≡ K1 & R K1 K2.
+ λR. ∀L1,L2. R L1 L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 →
+ ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & R K1 K2.
(* Basic inversion lemmas ***************************************************)
-fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → L1 = ⋆ →
- L2 = ⋆ ∧ e = 0.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ /2 width=1 by conj/
-| #L #I #V #H destruct
-| #L1 #L2 #I #V #e #_ #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+fact ldrop_inv_atom1_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → L1 = ⋆ →
+ L2 = ⋆ ∧ (s = Ⓕ → e = 0).
+#L1 #L2 #s #d #e * -L1 -L2 -d -e
+[ /3 width=1 by conj/
+| #I #L #V #H destruct
+| #I #L1 #L2 #V #e #_ #H destruct
+| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #H destruct
]
qed-.
(* Basic_1: was: drop_gen_sort *)
-lemma ldrop_inv_atom1: ∀d,e,L2. ⇩[d, e] ⋆ ≡ L2 → L2 = ⋆ ∧ e = 0.
+lemma ldrop_inv_atom1: ∀L2,s,d,e. ⇩[s, d, e] ⋆ ≡ L2 → L2 = ⋆ ∧ (s = Ⓕ → e = 0).
/2 width=4 by ldrop_inv_atom1_aux/ qed-.
-fact ldrop_inv_O1_pair1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 →
- ∀K,I,V. L1 = K. ⓑ{I} V →
- (e = 0 ∧ L2 = K. ⓑ{I} V) ∨
- (0 < e ∧ ⇩[d, e - 1] K ≡ L2).
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #_ #K #I #V #H destruct
-| #L #I #V #_ #K #J #W #HX destruct /3 width=1 by or_introl, conj/
-| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1 by or_intror, conj/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
+fact ldrop_inv_O1_pair1_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → d = 0 →
+ ∀K,I,V. L1 = K.ⓑ{I}V →
+ (e = 0 ∧ L2 = K.ⓑ{I}V) ∨
+ (0 < e ∧ ⇩[s, d, e-1] K ≡ L2).
+#L1 #L2 #s #d #e * -L1 -L2 -d -e
+[ #d #e #_ #_ #K #J #W #H destruct
+| #I #L #V #_ #K #J #W #HX destruct /3 width=1 by or_introl, conj/
+| #I #L1 #L2 #V #e #HL12 #_ #K #J #W #H destruct /3 width=1 by or_intror, conj/
+| #I #L1 #L2 #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
]
qed-.
-lemma ldrop_inv_O1_pair1: ∀e,K,I,V,L2. ⇩[0, e] K. ⓑ{I} V ≡ L2 →
- (e = 0 ∧ L2 = K. ⓑ{I} V) ∨
- (0 < e ∧ ⇩[0, e - 1] K ≡ L2).
+lemma ldrop_inv_O1_pair1: ∀I,K,L2,V,s,e. ⇩[s, 0, e] K. ⓑ{I} V ≡ L2 →
+ (e = 0 ∧ L2 = K.ⓑ{I}V) ∨
+ (0 < e ∧ ⇩[s, 0, e-1] K ≡ L2).
/2 width=3 by ldrop_inv_O1_pair1_aux/ qed-.
-lemma ldrop_inv_pair1: ∀K,I,V,L2. ⇩[0, 0] K. ⓑ{I} V ≡ L2 → L2 = K. ⓑ{I} V.
-#K #I #V #L2 #H
+lemma ldrop_inv_pair1: ∀I,K,L2,V,s. ⇩[s, 0, 0] K.ⓑ{I}V ≡ L2 → L2 = K.ⓑ{I}V.
+#I #K #L2 #V #s #H
elim (ldrop_inv_O1_pair1 … H) -H * // #H destruct
elim (lt_refl_false … H)
qed-.
(* Basic_1: was: drop_gen_drop *)
-lemma ldrop_inv_ldrop1_lt: ∀e,K,I,V,L2.
- ⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2.
-#e #K #I #V #L2 #H #He
+lemma ldrop_inv_drop1_lt: ∀I,K,L2,V,s,e.
+ ⇩[s, 0, e] K.ⓑ{I}V ≡ L2 → 0 < e → ⇩[s, 0, e-1] K ≡ L2.
+#I #K #L2 #V #s #e #H #He
elim (ldrop_inv_O1_pair1 … H) -H * // #H destruct
elim (lt_refl_false … He)
qed-.
-lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2.
- ⇩[0, e+1] K. ⓑ{I} V ≡ L2 → ⇩[0, e] K ≡ L2.
-#e #K #I #V #L2 #H lapply (ldrop_inv_ldrop1_lt … H ?) -H //
+lemma ldrop_inv_drop1: ∀I,K,L2,V,s,e.
+ ⇩[s, 0, e+1] K.ⓑ{I}V ≡ L2 → ⇩[s, 0, e] K ≡ L2.
+#I #K #L2 #V #s #e #H lapply (ldrop_inv_drop1_lt … H ?) -H //
qed-.
-fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
- ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
- ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 &
- ⇧[d - 1, e] V2 ≡ V1 &
- L2 = K2. ⓑ{I} V2.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #_ #I #K #V #H destruct
-| #L #I #V #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H)
-| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct /2 width=5 by ex3_2_intro/
+fact ldrop_inv_skip1_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → 0 < d →
+ ∀I,K1,V1. L1 = K1.ⓑ{I}V1 →
+ ∃∃K2,V2. ⇩[s, d-1, e] K1 ≡ K2 &
+ ⇧[d-1, e] V2 ≡ V1 &
+ L2 = K2.ⓑ{I}V2.
+#L1 #L2 #s #d #e * -L1 -L2 -d -e
+[ #d #e #_ #_ #J #K1 #W1 #H destruct
+| #I #L #V #H elim (lt_refl_false … H)
+| #I #L1 #L2 #V #e #_ #H elim (lt_refl_false … H)
+| #I #L1 #L2 #V1 #V2 #d #e #HL12 #HV21 #_ #J #K1 #W1 #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
(* Basic_1: was: drop_gen_skip_l *)
-lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < d →
- ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 &
- ⇧[d - 1, e] V2 ≡ V1 &
- L2 = K2. ⓑ{I} V2.
+lemma ldrop_inv_skip1: ∀I,K1,V1,L2,s,d,e. ⇩[s, d, e] K1.ⓑ{I}V1 ≡ L2 → 0 < d →
+ ∃∃K2,V2. ⇩[s, d-1, e] K1 ≡ K2 &
+ ⇧[d-1, e] V2 ≡ V1 &
+ L2 = K2.ⓑ{I}V2.
/2 width=3 by ldrop_inv_skip1_aux/ qed-.
-lemma ldrop_inv_O1_pair2: ∀I,K,V,e,L1. ⇩[0, e] L1 ≡ K. ⓑ{I} V →
- (e = 0 ∧ L1 = K. ⓑ{I} V) ∨
- ∃∃I1,K1,V1. ⇩[0, e - 1] K1 ≡ K. ⓑ{I} V & L1 = K1.ⓑ{I1}V1 & 0 < e.
-#I #K #V #e *
+lemma ldrop_inv_O1_pair2: ∀I,K,V,s,e,L1. ⇩[s, 0, e] L1 ≡ K.ⓑ{I}V →
+ (e = 0 ∧ L1 = K.ⓑ{I}V) ∨
+ ∃∃I1,K1,V1. ⇩[s, 0, e-1] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & 0 < e.
+#I #K #V #s #e *
[ #H elim (ldrop_inv_atom1 … H) -H #H destruct
| #L1 #I1 #V1 #H
elim (ldrop_inv_O1_pair1 … H) -H *
[ #H1 #H2 destruct /3 width=1 by or_introl, conj/
- | /3 width=5/
+ | /3 width=5 by ex3_3_intro, or_intror/
]
]
qed-.
-fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
- ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
- ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 &
- ⇧[d - 1, e] V2 ≡ V1 &
- L1 = K1. ⓑ{I} V1.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #_ #I #K #V #H destruct
-| #L #I #V #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H)
-| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct /2 width=5 by ex3_2_intro/
+fact ldrop_inv_skip2_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → 0 < d →
+ ∀I,K2,V2. L2 = K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⇩[s, d-1, e] K1 ≡ K2 &
+ ⇧[d-1, e] V2 ≡ V1 &
+ L1 = K1.ⓑ{I}V1.
+#L1 #L2 #s #d #e * -L1 -L2 -d -e
+[ #d #e #_ #_ #J #K2 #W2 #H destruct
+| #I #L #V #H elim (lt_refl_false … H)
+| #I #L1 #L2 #V #e #_ #H elim (lt_refl_false … H)
+| #I #L1 #L2 #V1 #V2 #d #e #HL12 #HV21 #_ #J #K2 #W2 #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
(* Basic_1: was: drop_gen_skip_r *)
-lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. ⓑ{I} V2 → 0 < d →
- ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 & ⇧[d - 1, e] V2 ≡ V1 &
- L1 = K1. ⓑ{I} V1.
+lemma ldrop_inv_skip2: ∀I,L1,K2,V2,s,d,e. ⇩[s, d, e] L1 ≡ K2.ⓑ{I}V2 → 0 < d →
+ ∃∃K1,V1. ⇩[s, d-1, e] K1 ≡ K2 & ⇧[d-1, e] V2 ≡ V1 &
+ L1 = K1.ⓑ{I}V1.
/2 width=3 by ldrop_inv_skip2_aux/ qed-.
(* Basic properties *********************************************************)
+lemma ldrop_refl_atom_O2: ∀s,d. ⇩[s, d, O] ⋆ ≡ ⋆.
+/2 width=1 by ldrop_atom/ qed.
+
(* Basic_1: was by definition: drop_refl *)
-lemma ldrop_refl: ∀L,d. ⇩[d, 0] L ≡ L.
+lemma ldrop_refl: ∀L,d,s. ⇩[s, d, 0] L ≡ L.
#L elim L -L //
-#L #I #V #IHL #d @(nat_ind_plus … d) -d /2 width=1 by ldrop_pair, ldrop_skip/
+#L #I #V #IHL #d #s @(nat_ind_plus … d) -d /2 width=1 by ldrop_pair, ldrop_skip/
qed.
-lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e.
- ⇩[0, e - 1] L1 ≡ L2 → 0 < e → ⇩[0, e] L1. ⓑ{I} V ≡ L2.
-#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2 width=1 by ldrop_ldrop/
+lemma ldrop_drop_lt: ∀I,L1,L2,V,s,e.
+ ⇩[s, 0, e-1] L1 ≡ L2 → 0 < e → ⇩[s, 0, e] L1.ⓑ{I}V ≡ L2.
+#I #L1 #L2 #V #s #e #HL12 #He >(plus_minus_m_m e 1) /2 width=1 by ldrop_drop/
qed.
-lemma ldrop_skip_lt: ∀L1,L2,I,V1,V2,d,e.
- ⇩[d - 1, e] L1 ≡ L2 → ⇧[d - 1, e] V2 ≡ V1 → 0 < d →
- ⇩[d, e] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) /2 width=1 by ldrop_skip/
+lemma ldrop_skip_lt: ∀I,L1,L2,V1,V2,s,d,e.
+ ⇩[s, d-1, e] L1 ≡ L2 → ⇧[d-1, e] V2 ≡ V1 → 0 < d →
+ ⇩[s, d, e] L1. ⓑ{I} V1 ≡ L2.ⓑ{I}V2.
+#I #L1 #L2 #V1 #V2 #s #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) /2 width=1 by ldrop_skip/
qed.
-lemma ldrop_O1_le: ∀e,L. e ≤ |L| → ∃K. ⇩[0, e] L ≡ K.
-#e @(nat_ind_plus … e) -e /2 width=2/
+lemma ldrop_O1_le: ∀e,L. e ≤ |L| → ∃K. ⇩[e] L ≡ K.
+#e @(nat_ind_plus … e) -e /2 width=2 by ex_intro/
#e #IHe *
[ #H lapply (le_n_O_to_eq … H) -H >commutative_plus normalize #H destruct
| #L #I #V normalize #H
- elim (IHe L) -IHe /2 width=1/ -H /3 width=2 by ldrop_ldrop, ex_intro/
+ elim (IHe L) -IHe /3 width=2 by ldrop_drop, monotonic_pred, ex_intro/
]
-qed.
+qed-.
-lemma ldrop_O1_lt: ∀L,e. e < |L| → ∃∃I,K,V. ⇩[0, e] L ≡ K.ⓑ{I}V.
+lemma ldrop_O1_lt: ∀L,e. e < |L| → ∃∃I,K,V. ⇩[e] L ≡ K.ⓑ{I}V.
#L elim L -L
[ #e #H elim (lt_zero_false … H)
| #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4 by ldrop_pair, ex1_3_intro/
#e #_ normalize #H
- elim (IHL e) -IHL /3 width=4 by ldrop_ldrop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
+ elim (IHL e) -IHL /3 width=4 by ldrop_drop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
]
+qed-.
+
+lemma ldrop_FT: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → ⇩[Ⓣ, d, e] L1 ≡ L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+/3 width=1 by ldrop_atom, ldrop_drop, ldrop_skip/
qed.
+lemma ldrop_gen: ∀L1,L2,s,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → ⇩[s, d, e] L1 ≡ L2.
+#L1 #L2 * /2 width=1 by ldrop_FT/
+qed-.
+
+lemma ldrop_T: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → ⇩[Ⓣ, d, e] L1 ≡ L2.
+#L1 #L2 * /2 width=1 by ldrop_FT/
+qed-.
+
lemma l_liftable_LTC: ∀R. l_liftable R → l_liftable (LTC … R).
#R #HR #K #T1 #T2 #H elim H -T2
-[ /3 width=9/
-| #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2
- elim (lift_total T d e) /4 width=11 by step/
+[ /3 width=10 by inj/
+| #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #HTU1 #U2 #HTU2
+ elim (lift_total T d e) /4 width=12 by step/
]
-qed.
+qed-.
lemma l_deliftable_sn_LTC: ∀R. l_deliftable_sn R → l_deliftable_sn (LTC … R).
#R #HR #L #U1 #U2 #H elim H -U2
-[ #U2 #HU12 #K #d #e #HLK #T1 #HTU1
+[ #U2 #HU12 #K #s #d #e #HLK #T1 #HTU1
elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3 by inj, ex2_intro/
-| #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+| #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #T1 #HTU1
elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by step, ex2_intro/
]
-qed.
+qed-.
lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (TC … R).
-#R #HR #L1 #K1 #d #e #HLK1 #L2 #H elim H -L2
-[ #L2 #HL12
- elim (HR … HLK1 … HL12) -HR -L1 /3 width=3 by inj, ex2_intro/
-| #L #L2 #_ #HL2 * #K #HK1 #HLK
- elim (HR … HLK … HL2) -HR -L /3 width=3 by step, ex2_intro/
+#R #HR #L1 #K1 #s #d #e #HLK1 #L2 #H elim H -L2
+[ #L2 #HL12 elim (HR … HLK1 … HL12) -HR -L1
+ /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 * #K #HK1 #HLK elim (HR … HLK … HL2) -HR -L
+ /3 width=3 by step, ex2_intro/
]
-qed.
+qed-.
lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R).
-#R #HR #L1 #K1 #d #e #HLK1 #K2 #H elim H -K2
-[ #K2 #HK12
- elim (HR … HLK1 … HK12) -HR -K1 /3 width=3 by inj, ex2_intro/
-| #K #K2 #_ #HK2 * #L #HL1 #HLK
- elim (HR … HLK … HK2) -HR -K /3 width=3 by step, ex2_intro/
+#R #HR #L1 #K1 #s #d #e #HLK1 #K2 #H elim H -K2
+[ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1
+ /3 width=3 by inj, ex2_intro/
+| #K #K2 #_ #HK2 * #L #HL1 #HLK elim (HR … HLK … HK2) -HR -K
+ /3 width=3 by step, ex2_intro/
]
-qed.
+qed-.
lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
#R #HR #L1 #L2 #H elim H -L2
-[ #L2 #HL12 #K2 #e #HLK2
- elim (HR … HL12 … HLK2) -HR -L2 /3 width=3 by inj, ex2_intro/
-| #L #L2 #_ #HL2 #IHL1 #K2 #e #HLK2
- elim (HR … HL2 … HLK2) -HR -L2 #K #HLK #HK2
- elim (IHL1 … HLK) -L /3 width=5 by step, ex2_intro/
+[ #L2 #HL12 #K2 #s #e #HLK2 elim (HR … HL12 … HLK2) -HR -L2
+ /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IHL1 #K2 #s #e #HLK2 elim (HR … HL2 … HLK2) -HR -L2
+ #K #HLK #HK2 elim (IHL1 … HLK) -L
+ /3 width=5 by step, ex2_intro/
]
-qed.
+qed-.
lemma l_deliftable_sn_llstar: ∀R. l_deliftable_sn R →
∀l. l_deliftable_sn (llstar … R l).
#R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2
[ /2 width=3 by lstar_O, ex2_intro/
-| #l #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+| #l #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #T1 #HTU1
elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/
]
-qed.
+qed-.
(* Basic forvard lemmas *****************************************************)
(* Basic_1: was: drop_S *)
-lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 →
- ⇩[O, e + 1] L1 ≡ K2.
+lemma ldrop_fwd_drop2: ∀L1,I2,K2,V2,s,e. ⇩[s, O, e] L1 ≡ K2. ⓑ{I2} V2 →
+ ⇩[s, O, e + 1] L1 ≡ K2.
#L1 elim L1 -L1
-[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H * #H destruct
-| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
+[ #I2 #K2 #V2 #s #e #H lapply (ldrop_inv_atom1 … H) -H * #H destruct
+| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #s #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #H
- [ -IHL1 destruct /2 width=1/
- | @ldrop_ldrop >(plus_minus_m_m e 1) /2 width=3 by /
+ [ -IHL1 destruct /2 width=1 by ldrop_drop/
+ | @ldrop_drop >(plus_minus_m_m e 1) /2 width=3 by/
]
]
qed-.
-lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L1| = |L2| + e.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1 by /
+lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L1| = |L2| + e.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1 by/
qed-.
-lemma ldrop_fwd_length_minus2: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| = |L1| - e.
+lemma ldrop_fwd_length_minus2: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L2| = |L1| - e.
#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1 by plus_minus, le_n/
qed-.
-lemma ldrop_fwd_length_minus4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → e = |L1| - |L2|.
+lemma ldrop_fwd_length_minus4: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → e = |L1| - |L2|.
#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H //
qed-.
-lemma ldrop_fwd_length_le2: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → e ≤ |L1|.
+lemma ldrop_fwd_length_le2: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → e ≤ |L1|.
#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H //
qed-.
-lemma ldrop_fwd_length_le4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| ≤ |L1|.
+lemma ldrop_fwd_length_le4: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L2| ≤ |L1|.
#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H //
qed-.
lemma ldrop_fwd_length_lt2: ∀L1,I2,K2,V2,d,e.
- ⇩[d, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|.
+ ⇩[Ⓕ, d, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|.
#L1 #I2 #K2 #V2 #d #e #H
lapply (ldrop_fwd_length … H) normalize in ⊢ (%→?); -I2 -V2 //
qed-.
-lemma ldrop_fwd_length_lt4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 0 < e → |L2| < |L1|.
+lemma ldrop_fwd_length_lt4: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → 0 < e → |L2| < |L1|.
#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1 by lt_minus_to_plus_r/
qed-.
-lemma ldrop_fwd_length_eq1: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+lemma ldrop_fwd_length_eq1: ∀L1,L2,K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
|L1| = |L2| → |K1| = |K2|.
#L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12
lapply (ldrop_fwd_length … HLK1) -HLK1
/2 width=2 by injective_plus_r/
qed-.
-lemma ldrop_fwd_length_eq2: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+lemma ldrop_fwd_length_eq2: ∀L1,L2,K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
|K1| = |K2| → |L1| = |L2|.
#L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12
lapply (ldrop_fwd_length … HLK1) -HLK1
lapply (ldrop_fwd_length … HLK2) -HLK2 //
qed-.
-lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
+lemma ldrop_fwd_lw: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e // normalize
[ /2 width=3 by transitive_le/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
+| #I #L1 #L2 #V1 #V2 #d #e #_ #HV21 #IHL12
>(lift_fwd_tw … HV21) -HV21 /2 width=1 by monotonic_le_plus_l/
]
qed-.
-lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 0 < e → ♯{L2} < ♯{L1}.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e //
-[ #L #I #V #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V #e #HL12 #_ #_
+lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → 0 < e → ♯{L2} < ♯{L1}.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #H >H -H //
+| #I #L #V #H elim (lt_refl_false … H)
+| #I #L1 #L2 #V #e #HL12 #_ #_
lapply (ldrop_fwd_lw … HL12) -HL12 #HL12
@(le_to_lt_to_lt … HL12) -HL12 //
-| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 #H normalize in ⊢ (?%%); -I
+| #I #L1 #L2 #V1 #V2 #d #e #_ #HV21 #IHL12 #H normalize in ⊢ (?%%); -I
>(lift_fwd_tw … HV21) -V2 /3 by lt_minus_to_plus/
]
qed-.
-lemma ldrop_fwd_rfw: ∀I,L,K,V,i. ⇩[O, i] L ≡ K.ⓑ{I}V → ♯{K, V} < ♯{L, #i}.
+lemma ldrop_fwd_rfw: ∀I,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ♯{K, V} < ♯{L, #i}.
#I #L #K #V #i #HLK lapply (ldrop_fwd_lw … HLK) -HLK
normalize in ⊢ (%→?%%); /2 width=1 by le_S_S/
qed-.
(* Advanced inversion lemmas ************************************************)
-fact ldrop_inv_O2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → e = 0 → L1 = L2.
-#d #e #L1 #L2 #H elim H -d -e -L1 -L2
+fact ldrop_inv_O2_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → e = 0 → L1 = L2.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e
[ //
| //
-| #L1 #L2 #I #V #e #_ #_ >commutative_plus normalize #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 #H
+| #I #L1 #L2 #V #e #_ #_ >commutative_plus normalize #H destruct
+| #I #L1 #L2 #V1 #V2 #d #e #_ #HV21 #IHL12 #H
>(IHL12 H) -L1 >(lift_inv_O2_aux … HV21 … H) -V2 -d -e //
]
qed-.
(* Basic_1: was: drop_gen_refl *)
-lemma ldrop_inv_O2: ∀L1,L2,d. ⇩[d, 0] L1 ≡ L2 → L1 = L2.
-/2 width=4 by ldrop_inv_O2_aux/ qed-.
+lemma ldrop_inv_O2: ∀L1,L2,s,d. ⇩[s, d, 0] L1 ≡ L2 → L1 = L2.
+/2 width=5 by ldrop_inv_O2_aux/ qed-.
-lemma ldrop_inv_length_eq: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L1| = |L2| → e = 0.
+lemma ldrop_inv_length_eq: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L1| = |L2| → e = 0.
#L1 #L2 #d #e #H #HL12 lapply (ldrop_fwd_length_minus4 … H) //
qed-.
-lemma ldrop_inv_refl: ∀L,d,e. ⇩[d, e] L ≡ L → e = 0.
+lemma ldrop_inv_refl: ∀L,d,e. ⇩[Ⓕ, d, e] L ≡ L → e = 0.
/2 width=5 by ldrop_inv_length_eq/ qed-.
+fact ldrop_inv_FT_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 →
+ ∀I,K,V. L2 = K.ⓑ{I}V → s = Ⓣ → d = 0 →
+ ⇩[Ⓕ, d, e] L1 ≡ K.ⓑ{I}V.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #_ #J #K #W #H destruct
+| #I #L #V #J #K #W #H destruct //
+| #I #L1 #L2 #V #e #_ #IHL12 #J #K #W #H1 #H2 destruct
+ /3 width=1 by ldrop_drop/
+| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #_ #J #K #W #_ #_
+ <plus_n_Sm #H destruct
+]
+qed-.
+
+lemma ldrop_inv_FT: ∀I,L,K,V,e. ⇩[Ⓣ, 0, e] L ≡ K.ⓑ{I}V → ⇩[e] L ≡ K.ⓑ{I}V.
+/2 width=5 by ldrop_inv_FT_aux/ qed.
+
+lemma ldrop_inv_gen: ∀I,L,K,V,s,e. ⇩[s, 0, e] L ≡ K.ⓑ{I}V → ⇩[e] L ≡ K.ⓑ{I}V.
+#I #L #K #V * /2 width=1 by ldrop_inv_FT/
+qed-.
+
+lemma ldrop_inv_T: ∀I,L,K,V,s,e. ⇩[Ⓣ, 0, e] L ≡ K.ⓑ{I}V → ⇩[s, 0, e] L ≡ K.ⓑ{I}V.
+#I #L #K #V * /2 width=1 by ldrop_inv_FT/
+qed-.
+
(* Basic_1: removed theorems 50:
drop_ctail drop_skip_flat
cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
(* Properties on append for local environments ******************************)
-fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
+fact ldrop_O1_append_sn_le_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 →
d = 0 → e ≤ |L1| →
- ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
-/4 width=1 by ldrop_skip_lt, ldrop_ldrop, arith_b1, lt_minus_to_plus_r, monotonic_pred/
+ ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e normalize
+[2,3,4: /4 width=1 by ldrop_skip_lt, ldrop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ]
+#d #e #_ #_ #H <(le_n_O_to_eq … H) -H //
qed-.
-lemma ldrop_O1_append_sn_le: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → e ≤ |L1| →
- ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
+lemma ldrop_O1_append_sn_le: ∀L1,L2,s,e. ⇩[s, 0, e] L1 ≡ L2 → e ≤ |L1| →
+ ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
/2 width=3 by ldrop_O1_append_sn_le_aux/ qed.
(* Inversion lemmas on append for local environments ************************)
-lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
- |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
+lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K →
+ |L2| ≤ e → ⇩[s, 0, e - |L2|] L1 ≡ K.
#K #L1 #L2 elim L2 -L2 normalize //
-#L2 #I #V #IHL2 #e #H #H1e
+#L2 #I #V #IHL2 #s #e #H #H1e
elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct
[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2
>commutative_plus normalize #H destruct
]
qed-.
-lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e ≤ |L2| →
- ∀K2. ⇩[0, e] L2 ≡ K2 → K = L1 @@ K2.
+lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| →
+ ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2.
#K #L1 #L2 elim L2 -L2 normalize
-[ #e #H1 #H2 #K2 #H3
- lapply (le_n_O_to_eq … H2) -H2 #H2
- elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct
+[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2
+ #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct
>(ldrop_inv_O2 … H1) -H1 //
-| #L2 #I #V #IHL2 #e @(nat_ind_plus … e) -e [ -IHL2 ]
+| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ]
[ #H1 #_ #K2 #H2
lapply (ldrop_inv_O2 … H1) -H1 #H1
lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct //
- | /4 width=6 by ldrop_inv_ldrop1, le_plus_to_le_r/
+ | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/
]
]
qed-.
(* Main properties **********************************************************)
(* Basic_1: was: drop_mono *)
-theorem ldrop_mono: ∀d,e,L,L1. ⇩[d, e] L ≡ L1 →
- ∀L2. ⇩[d, e] L ≡ L2 → L1 = L2.
-#d #e #L #L1 #H elim H -d -e -L -L1
-[ #d #L2 #H elim (ldrop_inv_atom1 … H) -H //
-| #K #I #V #L2 #HL12 <(ldrop_inv_O2 … HL12) -L2 //
-| #L #K #I #V #e #_ #IHLK #L2 #H
- lapply (ldrop_inv_ldrop1 … H) -H /2 width=1 by/
-| #L #K1 #I #T #V1 #d #e #_ #HVT1 #IHLK1 #X #H
+theorem ldrop_mono: ∀L,L1,s1,d,e. ⇩[s1, d, e] L ≡ L1 →
+ ∀L2,s2. ⇩[s2, d, e] L ≡ L2 → L1 = L2.
+#L #L1 #s1 #d #e #H elim H -L -L1 -d -e
+[ #d #e #He #L2 #s2 #H elim (ldrop_inv_atom1 … H) -H //
+| #I #K #V #L2 #s2 #HL12 <(ldrop_inv_O2 … HL12) -L2 //
+| #I #L #K #V #e #_ #IHLK #L2 #s2 #H
+ lapply (ldrop_inv_drop1 … H) -H /2 width=2 by/
+| #I #L #K1 #T #V1 #d #e #_ #HVT1 #IHLK1 #X #s2 #H
elim (ldrop_inv_skip1 … H) -H // <minus_plus_m_m #K2 #V2 #HLK2 #HVT2 #H destruct
>(lift_inj … HVT1 … HVT2) -HVT1 -HVT2
>(IHLK1 … HLK2) -IHLK1 -HLK2 //
qed-.
(* Basic_1: was: drop_conf_ge *)
-theorem ldrop_conf_ge: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
- ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 + e1 ≤ e2 →
- ⇩[0, e2 - e1] L1 ≡ L2.
-#d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1 //
-[ #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
- lapply (ldrop_inv_ldrop1_lt … H ?) -H /2 width=2 by ltn_to_ltO/ #HL2
+theorem ldrop_conf_ge: ∀L,L1,s1,d1,e1. ⇩[s1, d1, e1] L ≡ L1 →
+ ∀L2,s2,e2. ⇩[s2, 0, e2] L ≡ L2 → d1 + e1 ≤ e2 →
+ ⇩[s2, 0, e2 - e1] L1 ≡ L2.
+#L #L1 #s1 #d1 #e1 #H elim H -L -L1 -d1 -e1 //
+[ #d #e #_ #L2 #s2 #e2 #H #_ elim (ldrop_inv_atom1 … H) -H
+ #H #He destruct
+ @ldrop_atom #H >He // (**) (* explicit constructor *)
+| #I #L #K #V #e #_ #IHLK #L2 #s2 #e2 #H #He2
+ lapply (ldrop_inv_drop1_lt … H ?) -H /2 width=2 by ltn_to_ltO/ #HL2
<minus_plus >minus_minus_comm /3 width=1 by monotonic_pred/
-| #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2
+| #I #L #K #V1 #V2 #d #e #_ #_ #IHLK #L2 #s2 #e2 #H #Hdee2
lapply (transitive_le 1 … Hdee2) // #He2
- lapply (ldrop_inv_ldrop1_lt … H ?) -H // -He2 #HL2
+ lapply (ldrop_inv_drop1_lt … H ?) -H // -He2 #HL2
lapply (transitive_le (1 + e) … Hdee2) // #Hee2
- @ldrop_ldrop_lt >minus_minus_comm /3 width=1 by O, lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *)
+ @ldrop_drop_lt >minus_minus_comm /3 width=1 by lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *)
]
qed.
(* Note: apparently this was missing in basic_1 *)
-theorem ldrop_conf_be: ∀L0,L1,d1,e1. ⇩[d1, e1] L0 ≡ L1 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. ⇩[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
-[ #d1 #L2 #e2 #H #Hd1 #_ elim (ldrop_inv_atom1 … H) -H #H1 #H2 destruct
- <(le_n_O_to_eq … Hd1) -d1 /2 width=3 by ldrop_atom, ex2_intro/
-| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+theorem ldrop_conf_be: ∀L0,L1,s1,d1,e1. ⇩[s1, d1, e1] L0 ≡ L1 →
+ ∀L2,e2. ⇩[e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. ⇩[s1, 0, d1 + e1 - e2] L2 ≡ L & ⇩[d1] L1 ≡ L.
+#L0 #L1 #s1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #He1 #L2 #e2 #H #Hd1 #_ elim (ldrop_inv_atom1 … H) -H #H #He2 destruct
+ >(He2 ?) in Hd1; // -He2 #Hd1 <(le_n_O_to_eq … Hd1) -d1
+ /4 width=3 by ldrop_atom, ex2_intro/
+| normalize #I #L #V #L2 #e2 #HL2 #_ #He2
lapply (le_n_O_to_eq … He2) -He2 #H destruct
lapply (ldrop_inv_O2 … HL2) -HL2 #H destruct /2 width=3 by ldrop_pair, ex2_intro/
-| normalize #L0 #K0 #I #V1 #e1 #HLK0 #IHLK0 #L2 #e2 #H #_ #He21
+| normalize #I #L0 #K0 #V1 #e1 #HLK0 #IHLK0 #L2 #e2 #H #_ #He21
lapply (ldrop_inv_O1_pair1 … H) -H * * #He2 #HL20
- [ -IHLK0 -He21 destruct <minus_n_O /3 width=3 by ldrop_ldrop, ex2_intro/
+ [ -IHLK0 -He21 destruct <minus_n_O /3 width=3 by ldrop_drop, ex2_intro/
| -HLK0 <minus_le_minus_minus_comm //
elim (IHLK0 … HL20) -L0 /2 width=3 by monotonic_pred, ex2_intro/
]
-| #L0 #K0 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHLK0 #L2 #e2 #H #Hd1e2 #He2de1
+| #I #L0 #K0 #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHLK0 #L2 #e2 #H #Hd1e2 #He2de1
elim (le_inv_plus_l … Hd1e2) #_ #He2
<minus_le_minus_minus_comm //
- lapply (ldrop_inv_ldrop1_lt … H ?) -H // #HL02
- elim (IHLK0 … HL02) -L0 /3 width=3 by ldrop_ldrop, monotonic_pred, ex2_intro/
+ lapply (ldrop_inv_drop1_lt … H ?) -H // #HL02
+ elim (IHLK0 … HL02) -L0 /3 width=3 by ldrop_drop, monotonic_pred, ex2_intro/
]
-qed.
+qed-.
(* Note: apparently this was missing in basic_1 *)
-theorem ldrop_conf_le: ∀L0,L1,d1,e1. ⇩[d1, e1] L0 ≡ L1 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. ⇩[0, e2] L1 ≡ L & ⇩[d1 - e2, e1] L2 ≡ L.
-#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
-[ #d1 #L2 #e2 #H
- elim (ldrop_inv_atom1 … H) -H #H destruct /2 width=3 by ldrop_atom, ex2_intro/
-| #K0 #I #V0 #L2 #e2 #H1 #H2
+theorem ldrop_conf_le: ∀L0,L1,s1,d1,e1. ⇩[s1, d1, e1] L0 ≡ L1 →
+ ∀L2,s2,e2. ⇩[s2, 0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. ⇩[s2, 0, e2] L1 ≡ L & ⇩[s1, d1 - e2, e1] L2 ≡ L.
+#L0 #L1 #s1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #He1 #L2 #s2 #e2 #H elim (ldrop_inv_atom1 … H) -H
+ #H #He2 #_ destruct /4 width=3 by ldrop_atom, ex2_intro/
+| #I #K0 #V0 #L2 #s2 #e2 #H1 #H2
lapply (le_n_O_to_eq … H2) -H2 #H destruct
lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /2 width=3 by ldrop_pair, ex2_intro/
-| #K0 #K1 #I #V0 #e1 #HK01 #_ #L2 #e2 #H1 #H2
+| #I #K0 #K1 #V0 #e1 #HK01 #_ #L2 #s2 #e2 #H1 #H2
lapply (le_n_O_to_eq … H2) -H2 #H destruct
- lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /3 width=3 by ldrop_ldrop, ex2_intro/
-| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV10 #IHK01 #L2 #e2 #H #He2d1
+ lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /3 width=3 by ldrop_drop, ex2_intro/
+| #I #K0 #K1 #V0 #V1 #d1 #e1 #HK01 #HV10 #IHK01 #L2 #s2 #e2 #H #He2d1
elim (ldrop_inv_O1_pair1 … H) -H *
[ -IHK01 -He2d1 #H1 #H2 destruct /3 width=5 by ldrop_pair, ldrop_skip, ex2_intro/
| -HK01 -HV10 #He2 #HK0L2
elim (IHK01 … HK0L2) -IHK01 -HK0L2 /2 width=1 by monotonic_pred/
- >minus_le_minus_minus_comm /3 width=3 by ldrop_ldrop_lt, ex2_intro/
+ >minus_le_minus_minus_comm /3 width=3 by ldrop_drop_lt, ex2_intro/
]
]
-qed.
+qed-.
+(* Note: with "s2", the conclusion parameter is "s1 ∨ s2" *)
(* Basic_1: was: drop_trans_ge *)
-theorem ldrop_trans_ge: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
- ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
-#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L //
-[ /3 width=1/
-| #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2
+theorem ldrop_trans_ge: ∀L1,L,s1,d1,e1. ⇩[s1, d1, e1] L1 ≡ L →
+ ∀L2,e2. ⇩[e2] L ≡ L2 → d1 ≤ e2 → ⇩[s1, 0, e1 + e2] L1 ≡ L2.
+#L1 #L #s1 #d1 #e1 #H elim H -L1 -L -d1 -e1
+[ #d1 #e1 #He1 #L2 #e2 #H #_ elim (ldrop_inv_atom1 … H) -H
+ #H #He2 destruct /4 width=1 by ldrop_atom, eq_f2/
+| /2 width=1 by ldrop_gen/
+| /3 width=1 by ldrop_drop/
+| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #IHL12 #L #e2 #H #Hde2
lapply (lt_to_le_to_lt 0 … Hde2) // #He2
lapply (lt_to_le_to_lt … (e + e2) He2 ?) // #Hee2
- lapply (ldrop_inv_ldrop1_lt … H ?) -H // #HL2
- @ldrop_ldrop_lt // >le_plus_minus /3 width=1 by monotonic_pred/
+ lapply (ldrop_inv_drop1_lt … H ?) -H // #HL2
+ @ldrop_drop_lt // >le_plus_minus /3 width=1 by monotonic_pred/
]
qed.
(* Basic_1: was: drop_trans_le *)
-theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
- ∀e2,L2. ⇩[0, e2] L ≡ L2 → e2 ≤ d1 →
- ∃∃L0. ⇩[0, e2] L1 ≡ L0 & ⇩[d1 - e2, e1] L0 ≡ L2.
-#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L
-[ #d #e2 #L2 #H
- elim (ldrop_inv_atom1 … H) -H /2 width=3 by ldrop_atom, ex2_intro/
-| #K #I #V #e2 #L2 #HL2 #H
- lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3 by ldrop_pair, ex2_intro/
-| #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H
- lapply (le_n_O_to_eq … H) -H #H destruct
- elim (IHL12 … HL2) -IHL12 -HL2 // #L0 #H #HL0
- lapply (ldrop_inv_O2 … H) -H #H destruct /3 width=5 by ldrop_pair, ldrop_ldrop, ex2_intro/
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d
+theorem ldrop_trans_le: ∀L1,L,s1,d1,e1. ⇩[s1, d1, e1] L1 ≡ L →
+ ∀L2,s2,e2. ⇩[s2, 0, e2] L ≡ L2 → e2 ≤ d1 →
+ ∃∃L0. ⇩[s2, 0, e2] L1 ≡ L0 & ⇩[s1, d1 - e2, e1] L0 ≡ L2.
+#L1 #L #s1 #d1 #e1 #H elim H -L1 -L -d1 -e1
+[ #d1 #e1 #He1 #L2 #s2 #e2 #H #_ elim (ldrop_inv_atom1 … H) -H
+ #H #He2 destruct /4 width=3 by ldrop_atom, ex2_intro/
+| #I #K #V #L2 #s2 #e2 #HL2 #H lapply (le_n_O_to_eq … H) -H
+ #H destruct /2 width=3 by ldrop_pair, ex2_intro/
+| #I #L1 #L2 #V #e #_ #IHL12 #L #s2 #e2 #HL2 #H lapply (le_n_O_to_eq … H) -H
+ #H destruct elim (IHL12 … HL2) -IHL12 -HL2 //
+ #L0 #H #HL0 lapply (ldrop_inv_O2 … H) -H #H destruct
+ /3 width=5 by ldrop_pair, ldrop_drop, ex2_intro/
+| #I #L1 #L2 #V1 #V2 #d #e #HL12 #HV12 #IHL12 #L #s2 #e2 #H #He2d
elim (ldrop_inv_O1_pair1 … H) -H *
[ -He2d -IHL12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ldrop_skip, ex2_intro/
| -HL12 -HV12 #He2 #HL2
- elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3 by ldrop_ldrop_lt, ex2_intro/ | /2 width=1 by monotonic_pred/ ]
+ elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3 by ldrop_drop_lt, ex2_intro/ | /2 width=1 by monotonic_pred/ ]
]
]
-qed.
-
-(* Basic_1: was: drop_conf_rev *)
-axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L →
- ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1.
+qed-.
(* Advanced properties ******************************************************)
lemma l_liftable_llstar: ∀R. l_liftable R → ∀l. l_liftable (llstar … R l).
#R #HR #l #K #T1 #T2 #H @(lstar_ind_r … l T2 H) -l -T2
-[ #L #d #e #_ #U1 #HTU1 #U2 #HTU2 -HR -K
+[ #L #s #d #e #_ #U1 #HTU1 #U2 #HTU2 -HR -K
>(lift_mono … HTU2 … HTU1) -T1 -U2 -d -e //
-| #l #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2
- elim (lift_total T d e) /3 width=11 by lstar_dx/
+| #l #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #HTU1 #U2 #HTU2
+ elim (lift_total T d e) /3 width=12 by lstar_dx/
]
-qed.
+qed-.
(* Basic_1: was: drop_conf_lt *)
-lemma ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
- ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 →
+lemma ldrop_conf_lt: ∀L,L1,s1,d1,e1. ⇩[s1, d1, e1] L ≡ L1 →
+ ∀I,K2,V2,s2,e2. ⇩[s2, 0, e2] L ≡ K2.ⓑ{I}V2 →
e2 < d1 → let d ≝ d1 - e2 - 1 in
- ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 &
- ⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
-#d1 #e1 #L #L1 #H1 #e2 #K2 #I #V2 #H2 #He2d1
+ ∃∃K1,V1. ⇩[s2, 0, e2] L1 ≡ K1.ⓑ{I}V1 &
+ ⇩[s1, d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
+#L #L1 #s1 #d1 #e1 #H1 #I #K2 #V2 #s2 #e2 #H2 #He2d1
elim (ldrop_conf_le … H1 … H2) -L /2 width=2 by lt_to_le/ #K #HL1K #HK2
-elim (ldrop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/ #K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/
-qed.
+elim (ldrop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/
+#K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
(* Note: apparently this was missing in basic_1 *)
-lemma ldrop_trans_lt: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
- ∀e2,L2,I,V2. ⇩[0, e2] L ≡ L2.ⓑ{I}V2 →
+lemma ldrop_trans_lt: ∀L1,L,s1,d1,e1. ⇩[s1, d1, e1] L1 ≡ L →
+ ∀I,L2,V2,s2,e2. ⇩[s2, 0, e2] L ≡ L2.ⓑ{I}V2 →
e2 < d1 → let d ≝ d1 - e2 - 1 in
- ∃∃L0,V0. ⇩[0, e2] L1 ≡ L0.ⓑ{I}V0 &
- ⇩[d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0.
-#d1 #e1 #L1 #L #HL1 #e2 #L2 #I #V2 #HL2 #Hd21
+ ∃∃L0,V0. ⇩[s2, 0, e2] L1 ≡ L0.ⓑ{I}V0 &
+ ⇩[s1, d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0.
+#L1 #L #s1 #d1 #e1 #HL1 #I #L2 #V2 #s2 #e2 #HL2 #Hd21
elim (ldrop_trans_le … HL1 … HL2) -L /2 width=1 by lt_to_le/ #L0 #HL10 #HL02
elim (ldrop_inv_skip2 … HL02) -HL02 /2 width=1 by lt_plus_to_minus_r/ #L #V1 #HL2 #HV21 #H destruct /2 width=5 by ex3_2_intro/
qed-.
-lemma ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L.
- ⇩[d1, e1] L1 ≡ L → ⇩[0, e2] L ≡ L2 → d1 ≤ e2 →
- ⇩[0, e2 + e1] L1 ≡ L2.
-#e1 #e1 #e2 >commutative_plus /2 width=5 by ldrop_trans_ge/
+lemma ldrop_trans_ge_comm: ∀L1,L,L2,s1,d1,e1,e2.
+ ⇩[s1, d1, e1] L1 ≡ L → ⇩[e2] L ≡ L2 → d1 ≤ e2 →
+ ⇩[s1, 0, e2 + e1] L1 ≡ L2.
+#L1 #L #L2 #s1 #d1 #e1 #e2
+>commutative_plus /2 width=5 by ldrop_trans_ge/
qed.
-lemma ldrop_conf_div: ∀I1,L,K,V1,e1. ⇩[0, e1] L ≡ K. ⓑ{I1} V1 →
- ∀I2,V2,e2. ⇩[0, e2] L ≡ K. ⓑ{I2} V2 →
+lemma ldrop_conf_div: ∀I1,L,K,V1,e1. ⇩[e1] L ≡ K.ⓑ{I1}V1 →
+ ∀I2,V2,e2. ⇩[e2] L ≡ K.ⓑ{I2}V2 →
∧∧ e1 = e2 & I1 = I2 & V1 = V2.
#I1 #L #K #V1 #e1 #HLK1 #I2 #V2 #e2 #HLK2
elim (le_or_ge e1 e2) #He
(* Advanced forward lemmas **************************************************)
-lemma ldrop_fwd_be: ∀L,K,d,e,i. ⇩[d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i.
-#L #K #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) //
+lemma ldrop_fwd_be: ∀L,K,s,d,e,i. ⇩[s, d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i.
+#L #K #s #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) //
#HL elim (ldrop_O1_lt … HL) #I #K0 #V #HLK0 -HL
elim (ldrop_conf_lt … HLK … HLK0) // -HLK -HLK0 -Hd
#K1 #V1 #HK1 #_ #_ lapply (ldrop_fwd_length_lt2 … HK1) -I -K1 -V1
(* Properties on sn pointwise extension *************************************)
lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R).
-#R #HR #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
-[ #d #X #H >(lpx_sn_inv_atom1 … H) -H /2 width=3/
-| #K1 #I #V1 #X #H
- elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
- elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
- elim (IHLK1 … HL12) -L1 /3 width=3/
-| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+#R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
+ /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
+| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
+ #L2 #V2 #HL12 #HV12 #H destruct
+ /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
+| #I #L1 #K1 #V1 #e #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H
+ #L2 #V2 #HL12 #HV12 #H destruct
+ elim (IHLK1 … HL12) -L1 /3 width=3 by ldrop_drop, ex2_intro/
+| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
elim (HR … HV12 … HLK1 … HWV1) -V1
- elim (IHLK1 … HL12) -L1 /3 width=5/
+ elim (IHLK1 … HL12) -L1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/
]
qed-.
lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
l_liftable R → dedropable_sn (lpx_sn R).
-#R #H1R #H2R #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
-[ #d #X #H >(lpx_sn_inv_atom1 … H) -H /2 width=3/
-| #K1 #I #V1 #X #H
- elim (lpx_sn_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
- elim (IHLK1 … HK12) -K1 /3 width=5/
-| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
+ /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
+| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
+ #K2 #V2 #HK12 #HV12 #H destruct
+ /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
+| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1
+ /3 width=5 by ldrop_drop, lpx_sn_pair, ex2_intro/
+| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
elim (lift_total W2 d e) #V2 #HWV2
lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1
- elim (IHLK1 … HK12) -K1 /3 width=5/
+ elim (IHLK1 … HK12) -K1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/
]
qed-.
-fact lpx_sn_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
- d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & lpx_sn R K1 K2.
-#R #L2 #K2 #d #e #H elim H -L2 -K2 -d -e
-[ #d #X #H >(lpx_sn_inv_atom2 … H) -H /2 width=3/
-| #K2 #I #V2 #X #H
- elim (lpx_sn_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/
-| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_
- elim (lpx_sn_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct
- elim (IHLK2 … HL12) -L2 // /3 width=3/
-| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
- >commutative_plus normalize #H destruct
+fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⇩[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
+ d = 0 → ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2.
+#R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e
+[ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H
+ /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
+| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H
+ #K1 #V1 #HK12 #HV12 #H destruct
+ /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
+| #I #L2 #K2 #V2 #e #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H
+ #L1 #V1 #HL12 #HV12 #H destruct
+ elim (IHLK2 … HL12) -L2 /3 width=3 by ldrop_drop, ex2_intro/
+| #I #L2 #K2 #V2 #W2 #d #e #_ #_ #_ #L1 #_
+ <plus_n_Sm #H destruct
]
qed-.
(* Basic properties *********************************************************)
lemma lsubr_refl: ∀L. L ⊑ L.
-#L elim L -L // /2 width=1/
+#L elim L -L /2 width=1 by lsubr_sort, lsubr_bind/
qed.
(* Basic inversion lemmas ***************************************************)
fact lsubr_inv_abst1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W. L1 = K1.ⓛW →
L2 = ⋆ ∨ ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓛW.
#L1 #L2 * -L1 -L2
-[ #L #K1 #W #H destruct /2 width=1/
-| #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3/
+[ #L #K1 #W #H destruct /2 width=1 by or_introl/
+| #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3 by ex2_intro, or_intror/
| #L1 #L2 #V1 #V2 #_ #K1 #W #H destruct
]
qed-.
∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
#L1 #L2 * -L1 -L2
[ #L #K2 #W #H destruct
-| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3/
+| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3 by ex2_intro/
| #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
]
qed-.
(* Basic forward lemmas *****************************************************)
lemma lsubr_fwd_length: ∀L1,L2. L1 ⊑ L2 → |L2| ≤ |L1|.
-#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+#L1 #L2 #H elim H -L1 -L2 /2 width=1 by monotonic_le_plus_l/
qed-.
lemma lsubr_fwd_ldrop2_bind: ∀L1,L2. L1 ⊑ L2 →
- ∀I,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I}W →
- (∃∃K1. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I}W) ∨
- ∃∃K1,V. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
+ ∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W →
+ (∃∃K1. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W) ∨
+ ∃∃K1,V. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
#L1 #L2 #H elim H -L1 -L2
-[ #L #I #K2 #W #i #H
+[ #L #I #K2 #W #s #i #H
elim (ldrop_inv_atom1 … H) -H #H destruct
-| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #i #H
+| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #s #i #H
elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
- [ /3 width=3/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
+ [ /3 width=3 by ldrop_pair, ex2_intro, or_introl/
+ | elim (IHL12 … HLK2) -IHL12 -HLK2 *
+ /4 width=4 by ldrop_drop_lt, ex3_2_intro, ex2_intro, or_introl, or_intror/
]
-| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #i #H
+| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #s #i #H
elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
- [ /3 width=4/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
+ [ /3 width=4 by ldrop_pair, ex3_2_intro, or_intror/
+ | elim (IHL12 … HLK2) -IHL12 -HLK2 *
+ /4 width=4 by ldrop_drop_lt, ex3_2_intro, ex2_intro, or_introl, or_intror/
]
]
qed-.
lemma lsubr_fwd_ldrop2_abbr: ∀L1,L2. L1 ⊑ L2 →
- ∀K2,V,i. ⇩[0, i] L2 ≡ K2.ⓓV →
- ∃∃K1. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓV.
-#L1 #L2 #HL12 #K2 #V #i #HLK2 elim (lsubr_fwd_ldrop2_bind … HL12 … HLK2) -L2 // *
+ ∀K2,V,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓓV →
+ ∃∃K1. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓV.
+#L1 #L2 #HL12 #K2 #V #s #i #HLK2 elim (lsubr_fwd_ldrop2_bind … HL12 … HLK2) -L2 // *
#K1 #W #_ #_ #H destruct
qed-.
| ∃∃K2,V,W. K1 ⊑ K2 & L2 = K2.ⓛW &
I = Abbr & X = ⓝW.V.
#L1 #L2 * -L1 -L2
-[ #L #J #K1 #X #H destruct /2 width=1/
-| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/
-| #L1 #L2 #V #W #HL12 #J #K1 #X #H destruct /3 width=6/
+[ #L #J #K1 #X #H destruct /2 width=1 by or3_intro0/
+| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by or3_intro1, ex2_intro/
+| #L1 #L2 #V #W #HL12 #J #K1 #X #H destruct /3 width=6 by or3_intro2, ex4_3_intro/
]
qed-.
lapply (lsubr_inv_atom1 … H) -H //
| #I #L1 #L #V #_ #IHL1 #X #H
elim (lsubr_inv_bind1 … H) -H // *
- #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1/
+ #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1 by lsubr_bind, lsubr_abst/
| #L1 #L #V1 #W #_ #IHL1 #X #H
elim (lsubr_inv_abst1 … H) -H // *
- #L2 #HL2 #H destruct /3 width=1/
+ #L2 #HL2 #H destruct /3 width=1 by lsubr_abst/
]
qed-.
qed-.
lemma lsuby_fwd_ldrop2_be: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
- ∀I2,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I2}W →
+ ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W →
d ≤ i → i < d + e →
- ∃∃I1,K1. K1 ⊑×[0, ⫰(d+e-i)] K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I1}W.
+ ∃∃I1,K1. K1 ⊑×[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #L1 #d #e #J2 #K2 #W #i #H
+[ #L1 #d #e #J2 #K2 #W #s #i #H
elim (ldrop_inv_atom1 … H) -H #H destruct
-| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #i #_ #_ #H
+| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #s #i #_ #_ #H
elim (ylt_yle_false … H) //
-| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #i #H #_ >yplus_O1
+| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #s #i #H #_ >yplus_O1
elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ]
[ #_ destruct -I2 >ypred_succ
/2 width=4 by ldrop_pair, ex2_2_intro/
| lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/
#H <H -H #H lapply (ylt_inv_succ … H) -H
#Hie elim (IHL12 … HLK1) -IHL12 -HLK1 // -Hie
- >yminus_succ <yminus_inj /3 width=4 by ldrop_ldrop_lt, ex2_2_intro/
+ >yminus_succ <yminus_inj /3 width=4 by ldrop_drop_lt, ex2_2_intro/
]
-| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #J2 #K2 #W #i #HLK2 #Hdi
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #J2 #K2 #W #s #i #HLK2 #Hdi
elim (yle_inv_succ1 … Hdi) -Hdi
#Hdi #Hi <Hi >yplus_succ1 #H lapply (ylt_inv_succ … H) -H
- #Hide lapply (ldrop_inv_ldrop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/
+ #Hide lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/
#HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 <yminus_inj >yminus_SO2
- /4 width=4 by ylt_O, ldrop_ldrop_lt, ex2_2_intro/
+ /4 width=4 by ylt_O, ldrop_drop_lt, ex2_2_intro/
]
qed-.
}
]
[ { "generic local env. slicing" * } {
- [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
+ [ "ldrops ( ⇩*[?,?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
}
]
[ { "generic term relocation" * } {
}
]
[ { "basic local env. slicing" * } {
- [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
+ [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
}
]
[ { "basic term relocation" * } {
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basics/bool.ma".
+include "ground_2/notation/constructors/no_0.ma".
+include "ground_2/notation/constructors/yes_0.ma".
+
+(* BOOLEAN PROPERTIES *******************************************************)
+
+interpretation "boolean false" 'no = false.
+
+interpretation "boolean true" 'yes = true.
+
+lemma orb_false_r: ∀b1,b2:bool. (b1 ∨ b2) = false → b1 = false ∧ b2 = false.
+* normalize /2 width=1 by conj/ #b2 #H destruct
+qed-.
+
+lemma commutative_orb: commutative … orb.
+* * // qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "Ⓕ"
+ non associative with precedence 55
+ for @{'no}.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "Ⓣ"
+ non associative with precedence 55
+ for @{'yes}.
projects / helm.git / commitdiff