(* *)
(**************************************************************************)
-include "basic_2/notation/relations/crsubeq_3.ma".
+include "basic_2/notation/relations/lrsubeq_3.ma".
include "basic_2/static/aaa.ma".
include "basic_2/computation/acp_cr.ma".
inductive lsubc (RP:lenv→predicate term): relation lenv ≝
| lsubc_atom: lsubc RP (⋆) (⋆)
-| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. ⓑ{I} V) (L2. ⓑ{I} V)
+| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1.ⓑ{I}V) (L2.ⓑ{I}V)
| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ ϵ[RP] 〚A〛 → ⦃L1, W⦄ ϵ[RP] 〚A〛 → L2 ⊢ W ⁝ A →
- lsubc RP L1 L2 → lsubc RP (L1. ⓓⓝW.V) (L2. ⓛW)
+ lsubc RP L1 L2 → lsubc RP (L1. ⓓⓝW.V) (L2.ⓛW)
.
interpretation
"local environment refinement (abstract candidates of reducibility)"
- 'CrSubEq L1 RP L2 = (lsubc RP L1 L2).
+ 'LRSubEq RP L1 L2 = (lsubc RP L1 L2).
(* Basic inversion lemmas ***************************************************)
/2 width=4 by lsubc_inv_atom1_aux/ qed-.
fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
- (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I}X) ∨
+ (∃∃K2. K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨
∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
K1 ⊑[RP] K2 &
L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
(∃∃K2. K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨
∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
K1 ⊑[RP] K2 &
- L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
+ L2 = K2.ⓛW & X = ⓝW.V & I = Abbr.
/2 width=3 by lsubc_inv_pair1_aux/ qed-.
fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L2 = ⋆ → L1 = ⋆.
lemma lsubc_inv_atom2: ∀RP,L1. L1 ⊑[RP] ⋆ → L1 = ⋆.
/2 width=4 by lsubc_inv_atom2_aux/ qed-.
-fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
+fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2.ⓑ{I} W →
(∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨
∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
K1 ⊑[RP] K2 &
- L1 = K1. ⓓⓝW.V & I = Abst.
+ L1 = K1.ⓓⓝW.V & I = Abst.
#RP #L1 #L2 * -L1 -L2
[ #I #K2 #W #H destruct
| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
qed-.
(* Basic_1: was just: csubc_gen_head_l *)
-lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 ⊑[RP] K2. ⓑ{I} W →
+lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 ⊑[RP] K2.ⓑ{I} W →
(∃∃K1. K1 ⊑[RP] K2 & L1 = K1.ⓑ{I} W) ∨
∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
K1 ⊑[RP] K2 &