include "basic_2/reduction/crr_lift.ma".
include "basic_2/reduction/cir.ma".
-(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION ************************)
(* Properties on relocation *************************************************)
-lemma cir_lift: ∀K,T. K ⊢ 𝐈⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
- â\88\80U. â\87§[d, e] T â\89¡ U â\86\92 L â\8a¢ 𝐈⦃U⦄.
-/3 width=7 by crr_inv_lift/ qed.
+lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ ➡ 𝐈⦃T⦄ → ∀L,s,l,m. ⬇[s, l, m] L ≡ K →
+ â\88\80U. â¬\86[l, m] T â\89¡ U â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\9e¡ 𝐈⦃U⦄.
+/3 width=8 by crr_inv_lift/ qed.
-lemma cir_inv_lift: ∀L,U. L ⊢ 𝐈⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
- â\88\80T. â\87§[d, e] T â\89¡ U â\86\92 K â\8a¢ 𝐈⦃T⦄.
-/3 width=7/ qed-.
+lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ ➡ 𝐈⦃U⦄ → ∀K,s,l,m. ⬇[s, l, m] L ≡ K →
+ â\88\80T. â¬\86[l, m] T â\89¡ U â\86\92 â¦\83G, Kâ¦\84 â\8a¢ â\9e¡ 𝐈⦃T⦄.
+/3 width=8 by crr_lift/ qed-.