.
interpretation "global slicing"
- 'RLDrop e G1 G2 = (gdrop e G1 G2).
+ 'RDrop e G1 G2 = (gdrop e G1 G2).
(* basic inversion lemmas ***************************************************)
-lemma gdrop_inv_gt: â\88\80G1,G2,e. â\87\93[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
+lemma gdrop_inv_gt: â\88\80G1,G2,e. â\87©[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
#G1 #G2 #e * -G1 -G2 //
[ #G #H >H -H >commutative_plus #H
lapply (le_plus_to_le_r … 0 H) -H #H
]
qed-.
-lemma gdrop_inv_eq: â\88\80G1,G2,e. â\87\93[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
+lemma gdrop_inv_eq: â\88\80G1,G2,e. â\87©[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
#G1 #G2 #e * -G1 -G2 //
[ #G #H1 #H2 >H2 in H1; -H2 >commutative_plus #H
lapply (le_plus_to_le_r … 0 H) -H #H
]
qed-.
-fact gdrop_inv_lt_aux: â\88\80I,G,G1,G2,V,e. â\87\93[e] G ≡ G2 → G = G1. 𝕓{I} V →
- e < |G1| â\86\92 â\87\93[e] G1 ≡ G2.
+fact gdrop_inv_lt_aux: â\88\80I,G,G1,G2,V,e. â\87©[e] G ≡ G2 → G = G1. 𝕓{I} V →
+ e < |G1| â\86\92 â\87©[e] G1 ≡ G2.
#I #G #G1 #G2 #V #e * -G -G2
[ #G #H1 #H destruct #H2
lapply (le_to_lt_to_lt … H1 H2) -H1 -H2 normalize in ⊢ (? % ? → ?); >commutative_plus #H
qed.
lemma gdrop_inv_lt: ∀I,G1,G2,V,e.
- â\87\93[e] G1. ð\9d\95\93{I} V â\89¡ G2 â\86\92 e < |G1| â\86\92 â\87\93[e] G1 ≡ G2.
+ â\87©[e] G1. ð\9d\95\93{I} V â\89¡ G2 â\86\92 e < |G1| â\86\92 â\87©[e] G1 ≡ G2.
/2 width=5/ qed-.
(* Basic properties *********************************************************)
-lemma gdrop_total: â\88\80e,G1. â\88\83G2. â\87\93[e] G1 ≡ G2.
+lemma gdrop_total: â\88\80e,G1. â\88\83G2. â\87©[e] G1 ≡ G2.
#e #G1 elim G1 -G1 /3 width=2/
#I #V #G1 * #G2 #HG12
elim (lt_or_eq_or_gt e (|G1|)) #He