(* *)
(**************************************************************************)
-include "basic_2/relocation/lex_tc.ma".
+include "static_2/relocation/lex_tc.ma".
include "basic_2/rt_computation/lprs_ctc.ma".
include "basic_2/rt_computation/cprs_lpr.ma".
(* Properties with transitive closure ***************************************)
lemma lprs_TC (h) (G):
- â\88\80L1,L2. TC â\80¦ (lex (λL.cpm h G L 0)) L1 L2 â\86\92 â¦\83G, L1â¦\84â\8a¢ â\9e¡*[h] L2.
+ â\88\80L1,L2. TC â\80¦ (lex (λL.cpm h G L 0)) L1 L2 â\86\92 â\9d¨G,L1â\9d©â\8a¢ â\9e¡*[h,0] L2.
/4 width=3 by lprs_CTC, lex_CTC, lpr_cprs_trans/ qed.
(* Inversion lemmas with transitive closure *********************************)
lemma lprs_inv_TC (h) (G):
- â\88\80L1,L2. â¦\83G, L1â¦\84â\8a¢ â\9e¡*[h] L2 → TC … (lex (λL.cpm h G L 0)) L1 L2.
+ â\88\80L1,L2. â\9d¨G,L1â\9d©â\8a¢ â\9e¡*[h,0] L2 → TC … (lex (λL.cpm h G L 0)) L1 L2.
/3 width=3 by lprs_inv_CTC, lex_inv_CTC/ qed-.