(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
-lemma ltpss_ldrop_conf_ge: â\88\80L0,L1,d1,e1. L0 [d1, e1] â\89«* L1 →
- â\88\80L2,e2. â\87\93[0, e2] L0 ≡ L2 →
- d1 + e1 â\89¤ e2 â\86\92 â\87\93[0, e2] L1 ≡ L2.
+lemma ltpss_ldrop_conf_ge: â\88\80L0,L1,d1,e1. L0 [d1, e1] â\96¶* L1 →
+ â\88\80L2,e2. â\87©[0, e2] L0 ≡ L2 →
+ d1 + e1 â\89¤ e2 â\86\92 â\87©[0, e2] L1 ≡ L2.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 // /3 width=6/
qed.
-lemma ltpss_ldrop_trans_ge: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\89«* L0 →
- â\88\80L2,e2. â\87\93[0, e2] L0 ≡ L2 →
- d1 + e1 â\89¤ e2 â\86\92 â\87\93[0, e2] L1 ≡ L2.
+lemma ltpss_ldrop_trans_ge: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\96¶* L0 →
+ â\88\80L2,e2. â\87©[0, e2] L0 ≡ L2 →
+ d1 + e1 â\89¤ e2 â\86\92 â\87©[0, e2] L1 ≡ L2.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 // /3 width=6/
qed.
-lemma ltpss_ldrop_conf_be: â\88\80L0,L1,d1,e1. L0 [d1, e1] â\89«* L1 →
- â\88\80L2,e2. â\87\93[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- â\88\83â\88\83L. L2 [0, d1 + e1 - e2] â\89«* L & â\87\93[0, e2] L1 ≡ L.
+lemma ltpss_ldrop_conf_be: â\88\80L0,L1,d1,e1. L0 [d1, e1] â\96¶* L1 →
+ â\88\80L2,e2. â\87©[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ â\88\83â\88\83L. L2 [0, d1 + e1 - e2] â\96¶* L & â\87©[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
[ /2 width=3/
| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
]
qed.
-lemma ltpss_ldrop_trans_be: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\89«* L0 →
- â\88\80L2,e2. â\87\93[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- â\88\83â\88\83L. L [0, d1 + e1 - e2] â\89«* L2 & â\87\93[0, e2] L1 ≡ L.
+lemma ltpss_ldrop_trans_be: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\96¶* L0 →
+ â\88\80L2,e2. â\87©[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ â\88\83â\88\83L. L [0, d1 + e1 - e2] â\96¶* L2 & â\87©[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
[ /2 width=3/
| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
]
qed.
-lemma ltpss_ldrop_conf_le: â\88\80L0,L1,d1,e1. L0 [d1, e1] â\89«* L1 →
- â\88\80L2,e2. â\87\93[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- â\88\83â\88\83L. L2 [d1 - e2, e1] â\89«* L & â\87\93[0, e2] L1 ≡ L.
+lemma ltpss_ldrop_conf_le: â\88\80L0,L1,d1,e1. L0 [d1, e1] â\96¶* L1 →
+ â\88\80L2,e2. â\87©[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ â\88\83â\88\83L. L2 [d1 - e2, e1] â\96¶* L & â\87©[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
[ /2 width=3/
| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
]
qed.
-lemma ltpss_ldrop_trans_le: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\89«* L0 →
- â\88\80L2,e2. â\87\93[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- â\88\83â\88\83L. L [d1 - e2, e1] â\89«* L2 & â\87\93[0, e2] L1 ≡ L.
+lemma ltpss_ldrop_trans_le: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\96¶* L0 →
+ â\88\80L2,e2. â\87©[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ â\88\83â\88\83L. L [d1 - e2, e1] â\96¶* L2 & â\87©[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
[ /2 width=3/
| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1