(* 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-.