-theorem tpss_trans_down: â\88\80L,T1,T0,d1,e1. L â\8a¢ T1 [d1, e1] â\89«* T0 →
- â\88\80T2,d2,e2. L â\8a¢ T0 [d2, e2] â\89«* T2 → d2 + e2 ≤ d1 →
- â\88\83â\88\83T. L â\8a¢ T1 [d2, e2] â\89«* T & L â\8a¢ T [d1, e1] â\89«* T2.
+theorem tpss_trans_down: â\88\80L,T1,T0,d1,e1. L â\8a¢ T1 [d1, e1] â\96¶* T0 →
+ â\88\80T2,d2,e2. L â\8a¢ T0 [d2, e2] â\96¶* T2 → d2 + e2 ≤ d1 →
+ â\88\83â\88\83T. L â\8a¢ T1 [d2, e2] â\96¶* T & L â\8a¢ T [d1, e1] â\96¶* T2.