(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92
- d1 + e1 â\89¤ e2 â\86\92 â\86\93[0, e2] L1 â\89¡ L2.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92
+ d1 + e1 â\89¤ e2 â\86\92 â\87\93[0, e2] L1 â\89¡ L2.
#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
| //
qed.
lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92
- d1 + e1 â\89¤ e2 â\86\92 â\86\93[0, e2] L1 â\89¡ L2.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92
+ d1 + e1 â\89¤ e2 â\86\92 â\87\93[0, e2] L1 â\89¡ L2.
#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
| //
qed.
lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
- â\88\83â\88\83L. L2 [0, d1 + e1 - e2] â\89« L & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
+ â\88\83â\88\83L. L2 [0, d1 + e1 - e2] â\89« L & â\87\93[0, e2] L1 â\89¡ L.
#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
qed.
lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
- â\88\83â\88\83L. L [0, d1 + e1 - e2] â\89« L2 & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
+ â\88\83â\88\83L. L [0, d1 + e1 - e2] â\89« L2 & â\87\93[0, e2] L1 â\89¡ L.
#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
qed.
lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
- â\88\83â\88\83L. L2 [d1 - e2, e1] â\89« L & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
+ â\88\83â\88\83L. L2 [d1 - e2, e1] â\89« L & â\87\93[0, e2] L1 â\89¡ L.
#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
| /2 width=3/
qed.
lemma ltps_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
- â\88\83â\88\83L. L [d1 - e2, e1] â\89« L2 & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
+ â\88\83â\88\83L. L [d1 - e2, e1] â\89« L2 & â\87\93[0, e2] L1 â\89¡ L.
#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
| /2 width=3/