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).
λ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,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,s,e. ⇩[s, 0, e] L2 ≡ K2 →
∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & R K1 K2.
]
qed-.
-lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R).
-#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-.
-
lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
#R #HR #L1 #L2 #H elim H -L2
[ #L2 #HL12 #K2 #s #e #HLK2 elim (HR … HL12 … HLK2) -HR -L2