(**************************************************************************)
include "static_2/static/rex_lex.ma".
-include "basic_2/rt_transition/cpx_req.ma".
+include "basic_2/rt_transition/rpx_reqg.ma".
include "basic_2/rt_transition/lpx.ma".
(* EXTENDED PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS **********)
(* Properties with syntactic equivalence for referred local environments ****)
lemma req_rpx (G) (T):
- â\88\80L1,L2. L1 â\89¡[T] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[T] L2.
+ â\88\80L1,L2. L1 â\89¡[T] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T] L2.
/2 width=1 by req_fwd_rex/ qed.
(* Properties with extended rt-transition for full local envs ***************)
lemma lpx_rpx (G) (T):
- â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â¬\88 L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[T] L2.
+ â\88\80L1,L2. â\9d¨G,L1â\9d© â\8a¢ â¬\88 L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T] L2.
/2 width=1 by rex_lex/ qed.
(* Inversion lemmas with extended rt-transition for full local envs *********)
lemma rpx_inv_req_lpx (G) (T):
- â\88\80L1,L2. â\9dªG,L1â\9d« ⊢ ⬈[T] L2 →
- â\88\83â\88\83L. L1 â\89¡[T] L & â\9dªG,Lâ\9d« ⊢ ⬈ L2.
-/4 width=13 by cpx_req_conf, rex_inv_req_lex, rex_conf1_next/ qed-.
+ â\88\80L1,L2. â\9d¨G,L1â\9d© ⊢ ⬈[T] L2 →
+ â\88\83â\88\83L. L1 â\89¡[T] L & â\9d¨G,Lâ\9d© ⊢ ⬈ L2.
+/4 width=13 by cpx_reqg_conf, rex_inv_req_lex, rex_conf1_next/ qed-.
(* Forward lemmas with extended rt-transition for full local envs ***********)
lemma rpx_fwd_lpx_req (G) (T):
- â\88\80L1,L2. â\9dªG,L1â\9d« ⊢ ⬈[T] L2 →
- â\88\83â\88\83L. â\9dªG,L1â\9d« ⊢ ⬈ L & L ≡[T] L2.
+ â\88\80L1,L2. â\9d¨G,L1â\9d© ⊢ ⬈[T] L2 →
+ â\88\83â\88\83L. â\9d¨G,L1â\9d© ⊢ ⬈ L & L ≡[T] L2.
/3 width=3 by rpx_fsge_comp, rex_fwd_lex_req/ qed-.