(* *)
(**************************************************************************)
+include "basic_2/grammar/genv.ma".
include "basic_2/substitution/ldrops.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
-definition CP1 ≝ λRR:lenv→relation term. λRS:relation term.
- ∀L. ∃k. NF … (RR L) RS (⋆k).
+definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
+ ∀G,L. ∃k. NF … (RR G L) RS (⋆k).
-definition CP2 ≝ λRR:lenv→relation term. λRS:relation term.
- ∀L0,L,T,T0,d,e. NF … (RR L) RS T →
- ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR L0) RS T0.
+definition CP2 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
+ ∀G,L0,L,T,T0,d,e. NF … (RR G L) RS T →
+ ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0.
-definition CP2s ≝ λRR:lenv→relation term. λRS:relation term.
- ∀L0,L,des. ⇩*[des] L0 ≡ L →
+definition CP2s ≝ λRR:relation4 genv lenv term term. λRS:relation term.
+ ∀G,L0,L,des. ⇩*[des] L0 ≡ L →
∀T,T0. ⇧*[des] T ≡ T0 →
- NF … (RR L) RS T → NF … (RR L0) RS T0.
+ NF … (RR G L) RS T → NF … (RR G L0) RS T0.
-definition CP3 ≝ λRP:lenv→predicate term.
- ∀L,T,k. RP L (ⓐ⋆k.T) → RP L T.
+definition CP3 ≝ λRP:relation3 genv lenv term.
+ ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T.
-definition CP4 ≝ λRP:lenv→predicate term.
- ∀L,W,T. RP L W → RP L T → RP L (ⓝW.T).
+definition CP4 ≝ λRP:relation3 genv lenv term.
+ ∀G,L,W,T. RP G L W → RP G L T → RP G L (ⓝW.T).
(* requirements for abstract computation properties *)
-record acp (RR:lenv->relation term) (RS:relation term) (RP:lenv→predicate term) : Prop ≝
+record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:relation3 genv lenv term) : Prop ≝
{ cp1: CP1 RR RS;
cp2: CP2 RR RS;
cp3: CP3 RP;
(* Basic_1: was: nf2_lift1 *)
lemma acp_lifts: ∀RR,RS. CP2 RR RS → CP2s RR RS.
-#RR #RS #HRR #L1 #L2 #des #H elim H -L1 -L2 -des
+#RR #RS #HRR #G #L1 #L2 #des #H elim H -L1 -L2 -des
[ #L #T1 #T2 #H #HT1
<(lifts_inv_nil … H) -H //
| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2
(* Basic_1: was: sc3_arity_csubc *)
theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
- acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
- ∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 ⊑[RP] L0 →
- ⦃L2, T0⦄ ϵ[RP] 〚A〛.
-#RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
-[ #L #k #L0 #des #HL0 #X #H #L2 #HL20
+ acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+ ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
+ ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⊑[RP] L0 →
+ ⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
+#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A
+[ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20
>(lifts_inv_sort1 … H) -H
lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom
@(s4 … HAtom … ◊) //
-| #I #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
+| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
lapply (aacr_acr … H1RP H2RP B) #HB
elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct
lapply (ldrop_fwd_ldrop2 … HLK1) #HK1b
@(s5 … HB … ◊ … (ⓝV3.V) … HLK2) [2: /2 width=1/ ]
@(s7 … HB … ◊) [ @(s8 … HB … HKV2A) // | @(s8 … HB … H1KV0A) // ]
]
-| #a #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
+| #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (aacr_acr … H1RP H2RP A) #HA
lapply (aacr_acr … H1RP H2RP B) #HB
lapply (s1 … HB) -HB #HB
@(s6 … HA … ◊ ◊) // /3 width=5/
-| #a #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
+| #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
@(aacr_abst … H1RP H2RP) [ /2 width=5/ ]
#L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B
elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=3/ #HLW2B
@(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /2 width=3/ /3 width=5/
-| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
+| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
/3 width=10/
-| #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20
- elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
+| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20
+ elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (aacr_acr … H1RP H2RP A) #HA
@(s7 … HA … ◊) /2 width=5/
]
qed.
(* Basic_1: was: sc3_arity *)
-lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃L, T⦄ ϵ[RP] 〚A〛.
+lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+ ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛.
/2 width=8/ qed.
-lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP L T.
-#RR #RS #RP #H1RP #H2RP #L #T #A #HT
+lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+ ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T.
+#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
lapply (aacr_acr … H1RP H2RP A) #HA
@(s1 … HA) /2 width=4/
qed.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/ineint_4.ma".
+include "basic_2/notation/relations/ineint_5.ma".
include "basic_2/grammar/aarity.ma".
-include "basic_2/substitution/gr2_gr2.ma".
+include "basic_2/grammar/genv.ma". (**) (* not needed, disambiguation error *)
+include "basic_2/substitution/gr2_gr2.ma".
include "basic_2/substitution/lifts_lift_vector.ma".
include "basic_2/substitution/ldrops_ldrop.ma".
include "basic_2/computation/acp.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
(* Note: this is Girard's CR1 *)
-definition S1 ≝ λRP,C:lenv→predicate term.
- ∀L,T. C L T → RP L T.
+definition S1 ≝ λRP,C:relation3 genv lenv term.
+ ∀G,L,T. C G L T → RP G L T.
(* Note: this is Tait's iii, or Girard's CR4 *)
-definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term.
- ∀L,Vs. all … (RP L) Vs →
- ∀T. 𝐒⦃T⦄ → NF … (RR L) RS T → C L (ⒶVs.T).
+definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:relation3 genv lenv term.
+ ∀G,L,Vs. all … (RP G L) Vs →
+ ∀T. 𝐒⦃T⦄ → NF … (RR G L) RS T → C G L (ⒶVs.T).
(* Note: this generalizes Tait's ii *)
-definition S3 ≝ λC:lenv→predicate term.
- ∀a,L,Vs,V,T,W. C L (ⒶVs.ⓓ{a}ⓝW.V.T) → C L (ⒶVs.ⓐV.ⓛ{a}W.T).
+definition S3 ≝ λC:relation3 genv lenv term.
+ ∀a,G,L,Vs,V,T,W.
+ C G L (ⒶVs.ⓓ{a}ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ{a}W.T).
-definition S4 ≝ λRP,C:lenv→predicate term.
- ∀L,Vs. all … (RP L) Vs → ∀k. C L (ⒶVs.⋆k).
+definition S4 ≝ λRP,C:relation3 genv lenv term.
+ ∀G,L,Vs. all … (RP G L) Vs → ∀k. C G L (ⒶVs.⋆k).
-definition S5 ≝ λC:lenv→predicate term. ∀I,L,K,Vs,V1,V2,i.
- C L (ⒶVs.V2) → ⇧[0, i + 1] V1 ≡ V2 →
- ⇩[0, i] L ≡ K.ⓑ{I}V1 → C L (Ⓐ Vs.#i).
+definition S5 ≝ λC:relation3 genv lenv term. ∀I,G,L,K,Vs,V1,V2,i.
+ C G L (ⒶVs.V2) → ⇧[0, i + 1] V1 ≡ V2 →
+ ⇩[0, i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
-definition S6 ≝ λRP,C:lenv→predicate term.
- ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀a,V,T. C (L.ⓓV) (ⒶV2s.T) → RP L V → C L (ⒶV1s.ⓓ{a}V.T).
+definition S6 ≝ λRP,C:relation3 genv lenv term.
+ ∀G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀a,V,T. C G (L.ⓓV) (ⒶV2s.T) → RP G L V → C G L (ⒶV1s.ⓓ{a}V.T).
-definition S7 ≝ λC:lenv→predicate term.
- ∀L,Vs,T,W. C L (ⒶVs.T) → C L (ⒶVs.W) → C L (ⒶVs.ⓝW.T).
+definition S7 ≝ λC:relation3 genv lenv term.
+ ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T).
-definition S8 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e.
- C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2.
+definition S8 ≝ λC:relation3 genv lenv term. ∀G,L2,L1,T1,d,e.
+ C G L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2.
-definition S8s ≝ λC:lenv→predicate term.
- ∀L1,L2,des. ⇩*[des] L2 ≡ L1 →
- ∀T1,T2. ⇧*[des] T1 ≡ T2 → C L1 T1 → C L2 T2.
+definition S8s ≝ λC:relation3 genv lenv term.
+ ∀G,L1,L2,des. ⇩*[des] L2 ≡ L1 →
+ ∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2.
(* properties of the abstract candidate of reducibility *)
-record acr (RR:lenv->relation term) (RS:relation term) (RP,C:lenv→predicate term) : Prop ≝
+record acr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:relation3 genv lenv term) : Prop ≝
{ s1: S1 RP C;
s2: S2 RR RS RP C;
s3: S3 C;
}.
(* the abstract candidate of reducibility associated to an atomic arity *)
-let rec aacr (RP:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝
+let rec aacr (RP:relation3 genv lenv term) (A:aarity) (G:genv) (L:lenv) on A: predicate term ≝
λT. match A with
-[ AAtom ⇒ RP L T
-| APair B A ⇒ ∀L0,V0,T0,des. aacr RP B L0 V0 → ⇩*[des] L0 ≡ L → ⇧*[des] T ≡ T0 →
- aacr RP A L0 (ⓐV0.T0)
+[ AAtom ⇒ RP G L T
+| APair B A ⇒ ∀L0,V0,T0,des.
+ aacr RP B G L0 V0 → ⇩*[des] L0 ≡ L → ⇧*[des] T ≡ T0 →
+ aacr RP A G L0 (ⓐV0.T0)
].
interpretation
"candidate of reducibility of an atomic arity (abstract)"
- 'InEInt RP L T A = (aacr RP A L T).
+ 'InEInt RP G L T A = (aacr RP A G L T).
(* Basic properties *********************************************************)
(* Basic_1: was: sc3_lift1 *)
lemma acr_lifts: ∀C. S8 C → S8s C.
-#C #HC #L1 #L2 #des #H elim H -L1 -L2 -des
+#C #HC #G #L1 #L2 #des #H elim H -L1 -L2 -des
[ #L #T1 #T2 #H #HT1
<(lifts_inv_nil … H) -H //
| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2
]
qed.
-lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
- ∀des,L0,L,V,V0. ⇩*[des] L0 ≡ L → ⇧*[des] V ≡ V0 →
- RP L V → RP L0 V0.
-#RR #RS #RP #HRP #des #L0 #L #V #V0 #HL0 #HV0 #HV
+lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) →
+ ∀des,G,L0,L,V,V0. ⇩*[des] L0 ≡ L → ⇧*[des] V ≡ V0 →
+ RP G L V → RP G L0 V0.
+#RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV
@acr_lifts /width=6/
@(s8 … HRP)
qed.
(* Basic_1: was only: sns3_lifts1 *)
-lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
- ∀des,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L →
- all … (RP L) Vs → all … (RP L0) V0s.
-#RR #RS #RP #HRP #des #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize //
+lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) →
+ ∀des,G,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L →
+ all … (RP G L) Vs → all … (RP G L0) V0s.
+#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize //
#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * #HT1 #HT1s
@conj /2 width=1/ /2 width=6 by rp_lifts/
qed.
(* Basic_1: was:
sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift
*)
-lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
∀A. acr RR RS RP (aacr RP A).
#RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
#B #A #IHB #IHA @mk_acr normalize
-[ #L #T #H
- elim (cp1 … H1RP L) #k #HK
+[ #G #L #T #H
+ elim (cp1 … H1RP G L) #k #HK
lapply (H ? (⋆k) ? ⟠ ? ? ?) -H
[1,3: // |2,4: skip
| @(s2 … IHB … ◊) //
| #H @(cp3 … H1RP … k) @(s1 … IHA) //
]
-| #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H
+| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
lapply (s1 … IHB … HB) #HV0
@(s2 … IHA … (V0 @ V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/
-| #a #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H
+| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
@(s3 … IHA … (V0 @ V0s)) /5 width=5/
-| #L #Vs #HVs #k #L0 #V0 #X #hdes #HB #HL0 #H
+| #G #L #Vs #HVs #k #L0 #V0 #X #hdes #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
>(lifts_inv_sort1 … HY) -Y
lapply (s1 … IHB … HB) #HV0
@(s4 … IHA … (V0 @ V0s)) /3 width=6/
-| #I #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
+| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
elim (ldrops_ldrop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0
elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
>(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
@(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4/
-| #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
+| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
elim (lift_total V10 0 1) #V20 #HV120
elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
>(liftv_mono … HV12s … HV10s) -V1s //
]
-| #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
+| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
@(s7 … IHA … (V0 @ V0s)) /3 width=4/
]
qed.
-lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀a,L,W,T,A,B. ⦃L, W⦄ ϵ[RP] 〚B〛 → (
+lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+ ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
∀L0,V0,W0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des ] W ≡ W0 → ⇧*[des + 1] T ≡ T0 →
- ⦃L0, V0⦄ ϵ[RP] 〚B〛 → ⦃L0, W0⦄ ϵ[RP] 〚B〛 → ⦃L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
+ ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
) →
- ⦃L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛.
-#RR #RS #RP #H1RP #H2RP #a #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H
+ ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛.
+#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H
lapply (aacr_acr … H1RP H2RP A) #HCA
lapply (aacr_acr … H1RP H2RP B) #HCB
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/dpredstar_5.ma".
+include "basic_2/notation/relations/dpredstar_6.ma".
include "basic_2/unfold/sstas.ma".
include "basic_2/computation/cprs.ma".
(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-definition cpds: ∀h. sd h → lenv → relation term ≝ λh,g,L,T1,T2.
+definition cpds: ∀h. sd h → relation4 genv lenv term term ≝
+ λh,g,G,L,T1,T2.
∃∃T. ⦃G, L⦄ ⊢ T1 •*[h, g] T & ⦃G, L⦄ ⊢ T ➡* T2.
interpretation "decomposed extended parallel computation (term)"
- 'DPRedStar h g L T1 T2 = (cpds h g L T1 T2).
+ 'DPRedStar h g G L T1 T2 = (cpds h g G L T1 T2).
(* Basic properties *********************************************************)
-lemma cpds_refl: ∀h,g,L. reflexive … (cpds h g L).
+lemma cpds_refl: ∀h,g,G,L. reflexive … (cpds h g G L).
/2 width=3/ qed.
-lemma sstas_cpds: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
+lemma sstas_cpds: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
/2 width=3/ qed.
-lemma cprs_cpds: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
+lemma cprs_cpds: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
/2 width=3/ qed.
-lemma cpds_strap1: ∀h,g,L,T1,T,T2.
+lemma cpds_strap1: ∀h,g,G,L,T1,T,T2.
⦃G, L⦄ ⊢ T1 •*➡*[h, g] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-#h #g #L #T1 #T #T2 * /3 width=5/
+#h #g #G #L #T1 #T #T2 * /3 width=5/
qed.
-lemma cpds_strap2: ∀h,g,L,T1,T,T2,l.
+lemma cpds_strap2: ∀h,g,G,L,T1,T,T2,l.
⦃G, L⦄ ⊢ T1 •[h, g] ⦃l+1, T⦄ → ⦃G, L⦄ ⊢ T •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-#h #g #L #T1 #T #T2 #l #HT1 * /3 width=4/
+#h #g #G #L #T1 #T #T2 #l #HT1 * /3 width=4/
qed.
-lemma ssta_cprs_cpds: ∀h,g,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 •[h, g] ⦃l+1, T⦄ →
+lemma ssta_cprs_cpds: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 •[h, g] ⦃l+1, T⦄ →
⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
/3 width=3/ qed.
(* Properties on atomic arity assignment for terms **************************)
-lemma cpds_aaa: ∀h,g,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀U. ⦃G, L⦄ ⊢ T •*➡*[h, g] U → ⦃G, L⦄ ⊢ U ⁝ A.
-#h #g #L #T #A #HT #U * /3 width=5 by sstas_aaa, aaa_cprs_conf/
+lemma cpds_aaa: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀U. ⦃G, L⦄ ⊢ T •*➡*[h, g] U → ⦃G, L⦄ ⊢ U ⁝ A.
+#h #g #G #L #T #A #HT #U * /3 width=5 by sstas_aaa, aaa_cprs_conf/
qed.
(* Advanced properties ******************************************************)
-lemma cpds_cprs_trans: ∀h,g,L,T1,T,T2.
+lemma cpds_cprs_trans: ∀h,g,G,L,T1,T,T2.
⦃G, L⦄ ⊢ T1 •*➡*[h, g] T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-#h #g #L #T1 #T #T2 * #T0 #HT10 #HT0 #HT2
+#h #g #G #L #T1 #T #T2 * #T0 #HT10 #HT0 #HT2
lapply (cprs_trans … HT0 … HT2) -T /2 width=3/
qed-.
-lemma sstas_cpds_trans: ∀h,g,L,T1,T,T2.
+lemma sstas_cpds_trans: ∀h,g,G,L,T1,T,T2.
⦃G, L⦄ ⊢ T1 •*[h, g] T → ⦃G, L⦄ ⊢ T •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-#h #g #L #T1 #T #T2 #HT1 * #T0 #HT0 #HT02
+#h #g #G #L #T1 #T #T2 #HT1 * #T0 #HT0 #HT02
lapply (sstas_trans … HT1 … HT0) -T /2 width=3/
qed-.
(* Advanced inversion lemmas ************************************************)
-lemma cpds_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1. T1 •*➡*[h, g] U2 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃h, L.ⓛV1⦄ ⊢ T1 •*➡*[h, g] T2 &
- U2 = ⓛ{a}V2. T2.
-#h #g #a #L #V1 #T1 #U2 * #X #H1 #H2
+lemma cpds_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, g] U2 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, g] T2 &
+ U2 = ⓛ{a}V2.T2.
+#h #g #a #G #L #V1 #T1 #U2 * #X #H1 #H2
elim (sstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct /3 width=5/
qed-.
-lemma cpds_inv_abbr_abst: ∀h,g,a1,a2,L,V1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, g] ⓛ{a2}W2.T2 →
- ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 •*➡*[h, g] T & ⇧[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
-#h #g #a1 #a2 #L #V1 #W2 #T1 #T2 * #X #H1 #H2
+lemma cpds_inv_abbr_abst: ∀h,g,a1,a2,G,L,V1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, g] ⓛ{a2}W2.T2 →
+ ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, g] T & ⇧[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
+#h #g #a1 #a2 #G #L #V1 #W2 #T1 #T2 * #X #H1 #H2
elim (sstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
elim (cprs_inv_abbr1 … H2) -H2 *
[ #V2 #U2 #HV12 #HU12 #H destruct
(* Advanced forward lemmas **************************************************)
-lemma cpds_fwd_cpxs: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
-#h #g #L #T1 #T2 * /3 width=3 by cpxs_trans, sstas_cpxs, cprs_cpxs/
+lemma cpds_fwd_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
+#h #g #G #L #T1 #T2 * /3 width=3 by cpxs_trans, sstas_cpxs, cprs_cpxs/
qed-.
(* Relocation properties ****************************************************)
-lemma cpds_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 →
- ∀h,g,T2. ⦃h, K⦄ ⊢ T1 •*➡*[h, g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 →
- ⦃G, L⦄ ⊢ U1 •*➡*[h, g] U2.
-#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #T2 * #T
-elim (lift_total T d e) /3 width=11/
+lemma cpds_lift: ∀h,g,G. l_liftable (cpds h g G).
+#h #g #G #K #T1 #T2 * #T #HT1 #HT2 #L #d #e
+elim (lift_total T d e)
+/3 width=11 by cprs_lift, sstas_lift, ex2_intro/
qed.
-lemma cpds_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K →
- ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃G, L⦄ ⊢ U1 •*➡*[h, g] U2 →
- ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •*➡*[h, g] T2.
-#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * #U #HU1 #HU2
+lemma cpds_inv_lift1: ∀h,g,G. l_deliftable_sn (cpds h g G).
+#h #g #G #L #U1 #U2 * #U #HU1 #HU2 #K #d #e #HLK #T1 #HTU1
elim (sstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HT1 #HTU
elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L /3 width=5/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/peval_3.ma".
+include "basic_2/notation/relations/peval_4.ma".
include "basic_2/computation/cprs.ma".
include "basic_2/computation/csn.ma".
(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
-definition cpre: lenv → relation term ≝
- λL,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 ∧ ⦃G, L⦄ ⊢ 𝐍⦃T2⦄.
+definition cpre: relation4 genv lenv term term ≝
+ λG,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 ∧ ⦃G, L⦄ ⊢ 𝐍⦃T2⦄.
interpretation "context-sensitive parallel evaluation (term)"
- 'PEval L T1 T2 = (cpre L T1 T2).
+ 'PEval G L T1 T2 = (cpre G L T1 T2).
(* Basic_properties *********************************************************)
(* Basic_1: was just: nf2_sn3 *)
-lemma csn_cpre: ∀h,g,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄.
-#h #g #L #T1 #H @(csn_ind … H) -T1
+lemma csn_cpre: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄.
+#h #g #G #L #T1 #H @(csn_ind … H) -T1
#T1 #_ #IHT1
-elim (cnr_dec L T1) /3 width=3/
+elim (cnr_dec G L T1) /3 width=3/
* #T #H1T1 #H2T1
elim (IHT1 … H2T1) -IHT1 -H2T1 [2: /2 width=2/ ] #T2 * /4 width=3/
qed.
(* Main properties *********************************************************)
(* Basic_1: was: nf2_pr3_confluence *)
-theorem cpre_mono: ∀L,T,T1. ⦃G, L⦄ ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. ⦃G, L⦄ ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2.
-#L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2
+theorem cpre_mono: ∀G,L,T,T1. ⦃G, L⦄ ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. ⦃G, L⦄ ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2.
+#G #L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2
elim (cprs_conf … H1T1 … H1T2) -T #T #HT1
>(cprs_inv_cnr1 … HT1 H2T1) -T1 #HT2
>(cprs_inv_cnr1 … HT2 H2T2) -T2 //
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predstar_3.ma".
+include "basic_2/notation/relations/predstar_4.ma".
include "basic_2/reduction/cnr.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
(* Basic_1: includes: pr1_pr0 *)
-definition cprs: lenv → relation term ≝ LTC … cpr.
+definition cprs: relation4 genv lenv term term ≝
+ λG. LTC … (cpr G).
interpretation "context-sensitive parallel computation (term)"
- 'PRedStar L T1 T2 = (cprs L T1 T2).
+ 'PRedStar G L T1 T2 = (cprs G L T1 T2).
(* Basic eliminators ********************************************************)
-lemma cprs_ind: ∀L,T1. ∀R:predicate term. R T1 →
+lemma cprs_ind: ∀G,L,T1. ∀R:predicate term. R T1 →
(∀T,T2. ⦃G, L⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ T ➡ T2 → R T → R T2) →
∀T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → R T2.
-#L #T1 #R #HT1 #IHT1 #T2 #HT12
+#G #L #T1 #R #HT1 #IHT1 #T2 #HT12
@(TC_star_ind … HT1 IHT1 … HT12) //
qed-.
-lemma cprs_ind_dx: ∀L,T2. ∀R:predicate term. R T2 →
+lemma cprs_ind_dx: ∀G,L,T2. ∀R:predicate term. R T2 →
(∀T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ⦃G, L⦄ ⊢ T ➡* T2 → R T → R T1) →
∀T1. ⦃G, L⦄ ⊢ T1 ➡* T2 → R T1.
-#L #T2 #R #HT2 #IHT2 #T1 #HT12
+#G #L #T2 #R #HT2 #IHT2 #T1 #HT12
@(TC_star_ind_dx … HT2 IHT2 … HT12) //
qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: pr3_pr2 *)
-lemma cpr_cprs: ∀L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
+lemma cpr_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
/2 width=1/ qed.
(* Basic_1: was: pr3_refl *)
-lemma cprs_refl: ∀L,T. ⦃G, L⦄ ⊢ T ➡* T.
+lemma cprs_refl: ∀G,L,T. ⦃G, L⦄ ⊢ T ➡* T.
/2 width=1/ qed.
-lemma cprs_strap1: ∀L,T1,T,T2.
+lemma cprs_strap1: ∀G,L,T1,T,T2.
⦃G, L⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
normalize /2 width=3/ qed.
(* Basic_1: was: pr3_step *)
-lemma cprs_strap2: ∀L,T1,T,T2.
+lemma cprs_strap2: ∀G,L,T1,T,T2.
⦃G, L⦄ ⊢ T1 ➡ T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
normalize /2 width=3/ qed.
-lemma lsubr_cprs_trans: lsub_trans … cprs lsubr.
+lemma lsubr_cprs_trans: ∀G. lsub_trans … (cprs G) lsubr.
/3 width=5 by lsubr_cpr_trans, TC_lsub_trans/
qed-.
(* Basic_1: was: pr3_pr1 *)
-lemma tprs_cprs: ∀L,T1,T2. ⋆ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-#L #T1 #T2 #H @(lsubr_cprs_trans … H) -H //
+lemma tprs_cprs: ∀G,L,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
+#G #L #T1 #T2 #H @(lsubr_cprs_trans … H) -H //
qed.
-lemma cprs_bind_dx: ∀L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 →
+lemma cprs_bind_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡* T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
-#L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1
+#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1
/3 width=1/ /3 width=3/
qed.
(* Basic_1: was only: pr3_thin_dx *)
-lemma cprs_flat_dx: ∀I,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 →
+lemma cprs_flat_dx: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
-#I #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 /3 width=1/
+#I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 /3 width=1/
#T #T2 #_ #HT2 #IHT1
@(cprs_strap1 … IHT1) -V1 -T1 /2 width=1/
qed.
-lemma cprs_flat_sn: ∀I,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 →
+lemma cprs_flat_sn: ∀I,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 →
⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
-#I #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind … H) -V2 /3 width=1/
+#I #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind … H) -V2 /3 width=1/
#V #V2 #_ #HV2 #IHV1
@(cprs_strap1 … IHV1) -V1 -T1 /2 width=1/
qed.
-lemma cprs_zeta: ∀L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
- L.ⓓV ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡* T2.
-#L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/
+lemma cprs_zeta: ∀G,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
+ ⦃G, L.ⓓV⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡* T2.
+#G #L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/
qed.
-lemma cprs_tau: ∀L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡* T2.
-#L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/
+lemma cprs_tau: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡* T2.
+#G #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/
qed.
-lemma cprs_beta_dx: ∀a,L,V1,V2,W1,W2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ➡ V2 → ⦃G, L⦄ ⊢ W1 ➡ W2 → L.ⓛW1 ⊢ T1 ➡* T2 →
+lemma cprs_beta_dx: ∀a,G,L,V1,V2,W1,W2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ➡ V2 → ⦃G, L⦄ ⊢ W1 ➡ W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2.
-#a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 * -T2 /3 width=1/
+#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 * -T2 /3 width=1/
/4 width=7 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_beta/ (**) (* auto too slow without trace *)
qed.
-lemma cprs_theta_dx: ∀a,L,V1,V,V2,W1,W2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → L.ⓓW1 ⊢ T1 ➡* T2 →
+lemma cprs_theta_dx: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ W1 ➡ W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
-#a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ]
+#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ]
/4 width=9 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_theta/ (**) (* auto too slow without trace *)
qed.
(* Basic inversion lemmas ***************************************************)
(* Basic_1: was: pr3_gen_sort *)
-lemma cprs_inv_sort1: ∀L,U2,k. ⦃G, L⦄ ⊢ ⋆k ➡* U2 → U2 = ⋆k.
-#L #U2 #k #H @(cprs_ind … H) -U2 //
+lemma cprs_inv_sort1: ∀G,L,U2,k. ⦃G, L⦄ ⊢ ⋆k ➡* U2 → U2 = ⋆k.
+#G #L #U2 #k #H @(cprs_ind … H) -U2 //
#U2 #U #_ #HU2 #IHU2 destruct
>(cpr_inv_sort1 … HU2) -HU2 //
qed-.
(* Basic_1: was: pr3_gen_cast *)
-lemma cprs_inv_cast1: ∀L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡* U2 → ⦃G, L⦄ ⊢ T1 ➡* U2 ∨
+lemma cprs_inv_cast1: ∀G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡* U2 → ⦃G, L⦄ ⊢ T1 ➡* U2 ∨
∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L⦄ ⊢ T1 ➡* T2 & U2 = ⓝW2.T2.
-#L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#G #L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
#U2 #U #_ #HU2 * /3 width=3/ *
#W #T #HW1 #HT1 #H destruct
elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ *
qed-.
(* Basic_1: was: nf2_pr3_unfold *)
-lemma cprs_inv_cnr1: ∀L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → T = U.
-#L #T #U #H @(cprs_ind_dx … H) -T //
+lemma cprs_inv_cnr1: ∀G,L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → T = U.
+#G #L #T #U #H @(cprs_ind_dx … H) -T //
#T0 #T #H1T0 #_ #IHT #H2T0
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
qed-.
(* Basic_1: was: pr3_t *)
(* Basic_1: includes: pr1_t *)
-theorem cprs_trans: ∀L. Transitive … (cprs L).
-#L #T1 #T #HT1 #T2 @trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
+theorem cprs_trans: ∀G,L. Transitive … (cprs G L).
+#G #L #T1 #T #HT1 #T2 @trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
(* Basic_1: was: pr3_confluence *)
(* Basic_1: includes: pr1_confluence *)
-theorem cprs_conf: ∀L. confluent2 … (cprs L) (cprs L).
-#L @TC_confluent2 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
+theorem cprs_conf: ∀G,L. confluent2 … (cprs G L) (cprs G L).
+#G #L @TC_confluent2 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
-theorem cprs_bind: ∀a,I,L,V1,V2,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
- ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
-#a #I #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/
+theorem cprs_bind: ∀a,I,G,L,V1,V2,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
+ ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
+#a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/
#V #V2 #_ #HV2 #IHV1
@(cprs_trans … IHV1) -V1 /2 width=1/
qed.
(* Basic_1: was: pr3_flat *)
-theorem cprs_flat: ∀I,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
- ⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
-#I #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/
+theorem cprs_flat: ∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
+ ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡* ⓕ{I}V2.T2.
+#I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/
#V #V2 #_ #HV2 #IHV1
@(cprs_trans … IHV1) -IHV1 /2 width=1/
qed.
-theorem cprs_beta_rc: ∀a,L,V1,V2,W1,W2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ➡ V2 → L.ⓛW1 ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 →
+theorem cprs_beta_rc: ∀a,G,L,V1,V2,W1,W2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ➡ V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 →
⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2.
-#a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cprs_ind … H) -W2 /2 width=1/
+#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cprs_ind … H) -W2 /2 width=1/
#W #W2 #_ #HW2 #IHW1
@(cprs_trans … IHW1) -IHW1 /3 width=1/
qed.
-theorem cprs_beta: ∀a,L,V1,V2,W1,W2,T1,T2.
- L.ⓛW1 ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
+theorem cprs_beta: ∀a,G,L,V1,V2,W1,W2,T1,T2.
+ ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2.
-#a #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cprs_ind … H) -V2 /2 width=1/
+#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cprs_ind … H) -V2 /2 width=1/
#V #V2 #_ #HV2 #IHV1
@(cprs_trans … IHV1) -IHV1 /3 width=1/
qed.
-theorem cprs_theta_rc: ∀a,L,V1,V,V2,W1,W2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → L.ⓓW1 ⊢ T1 ➡* T2 →
+theorem cprs_theta_rc: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
-#a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/
+#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/
#W #W2 #_ #HW2 #IHW1
@(cprs_trans … IHW1) /2 width=1/
qed.
-theorem cprs_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2.
- ⇧[0, 1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → L.ⓓW1 ⊢ T1 ➡* T2 →
+theorem cprs_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
+ ⇧[0, 1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ V1 ➡* V → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
-#a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/
+#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/
#V1 #V0 #HV10 #_ #IHV0
@(cprs_trans … IHV0) /2 width=1/
qed.
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was pr3_gen_appl *)
-lemma cprs_inv_appl1: ∀L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 →
+lemma cprs_inv_appl1: ∀G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 →
∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L⦄ ⊢ T1 ➡* T2 &
U2 = ⓐV2. T2
| ∃∃a,W,T. ⦃G, L⦄ ⊢ T1 ➡* ⓛ{a}W.T &
| ∃∃a,V0,V2,V,T. ⦃G, L⦄ ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 &
⦃G, L⦄ ⊢ T1 ➡* ⓓ{a}V.T &
⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡* U2.
-#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 [ /3 width=5/ ]
+#G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 [ /3 width=5/ ]
#U #U2 #_ #HU2 * *
[ #V0 #T0 #HV10 #HT10 #H destruct
elim (cpr_inv_appl1 … HU2) -HU2 *
(* Basic_1: was just: pr3_pr2_pr2_t *)
(* Basic_1: includes: pr3_pr0_pr2_t *)
-lemma lpr_cpr_trans: s_r_trans … cpr lpr.
-#L2 #T1 #T2 #HT12 elim HT12 -L2 -T1 -T2
+lemma lpr_cpr_trans: ∀G. s_r_trans … (cpr G) (lpr G).
+#G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
[ /2 width=3/
-| #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
+| #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
elim (lpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
lapply (IHV02 … HK12) -K2 #HV02
lapply (cprs_strap2 … HV10 … HV02) -V0 /2 width=6/
-| #a #I #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
+| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /2 width=1/ /3 width=1/
|4,6: /3 width=1/
-| #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
+| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=1/ /2 width=3/
-| #a #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12
+| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12
lapply (IHT12 (L1.ⓛW1) ?) -IHT12 /2 width=1/ /3 width=1/
-| #a #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12
+| #a #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12
lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /2 width=1/ /3 width=3/
]
qed-.
-lemma cpr_bind2: ∀L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡ T2 →
- ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
-#L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+lemma cpr_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡ T2 →
+ ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
+#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
lapply (lpr_cpr_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
qed.
(* Advanced properties ******************************************************)
(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
-lemma lpr_cprs_trans: s_rs_trans … cpr lpr.
+lemma lpr_cprs_trans: ∀G. s_rs_trans … (cpr G) (lpr G).
/3 width=5 by s_r_trans_TC1, lpr_cpr_trans/ qed-.
(* Basic_1: was: pr3_strip *)
(* Basic_1: includes: pr1_strip *)
-lemma cprs_strip: ∀L. confluent2 … (cprs L) (cpr L).
-#L @TC_strip1 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
+lemma cprs_strip: ∀G,L. confluent2 … (cprs G L) (cpr G L).
+#G #L @TC_strip1 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
-lemma cprs_lpr_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡ L1 →
- ∃∃T. L1 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
-#L0 #T0 #T1 #H elim H -T1
+lemma cprs_lpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
+#G #L0 #T0 #T1 #H elim H -T1
[ #T1 #HT01 #L1 #HL01
elim (lpr_cpr_conf_dx … HT01 … HL01) -L0 /3 width=3/
| #T #T1 #_ #HT1 #IHT0 #L1 #HL01
]
qed-.
-lemma cprs_lpr_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡ L1 →
- ∃∃T. L0 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
-#L0 #T0 #T1 #HT01 #L1 #HL01
+lemma cprs_lpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 →
+ ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
+#G #L0 #T0 #T1 #HT01 #L1 #HL01
elim (cprs_lpr_conf_dx … HT01 … HL01) -HT01 #T #HT1
lapply (lpr_cprs_trans … HT1 … HL01) -HT1 /2 width=3/
qed-.
-lemma cprs_bind2_dx: ∀L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 →
- ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
-#L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+lemma cprs_bind2_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 →
+ ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
+#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
lapply (lpr_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
qed.
(* Advanced properties ******************************************************)
(* Note: apparently this was missing in basic_1 *)
-lemma cprs_delta: ∀L,K,V,V2,i.
- ⇩[0, i] L ≡ K. ⓓV → K ⊢ V ➡* V2 →
+lemma cprs_delta: ∀G,L,K,V,V2,i.
+ ⇩[0, i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡* V2 →
∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡* W2.
-#L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ]
+#G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ]
#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2
lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
elim (lift_total V1 0 (i+1)) /4 width=11 by cpr_lift, cprs_strap1/
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was: pr3_gen_lref *)
-lemma cprs_inv_lref1: ∀L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 →
+lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 →
T2 = #i ∨
- ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 &
- K ⊢ V1 ➡* T1 &
+ ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡* T1 &
⇧[0, i + 1] T1 ≡ T2.
-#L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1/
+#G #L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1/
#T #T2 #_ #HT2 *
[ #H destruct
elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1/
(* Relocation properties ****************************************************)
(* Basic_1: was: pr3_lift *)
-lemma cprs_lift: l_liftable cprs.
+lemma cprs_lift: ∀G. l_liftable (cprs G).
/3 width=9/ qed.
(* Basic_1: was: pr3_gen_lift *)
-lemma cprs_inv_lift1: l_deliftable_sn cprs.
+lemma cprs_inv_lift1: ∀G. l_deliftable_sn (cprs G).
/3 width=5 by l_deliftable_sn_LTC, cpr_inv_lift1/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/peval_5.ma".
+include "basic_2/notation/relations/peval_6.ma".
include "basic_2/computation/cpxs.ma".
include "basic_2/computation/csn.ma".
(* CONTEXT-SENSITIVE EXTENDED PARALLEL EVALUATION ON TERMS ******************)
-definition cpxe: ∀h. sd h → lenv → relation term ≝
- λh,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 ∧ ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T2⦄.
+definition cpxe: ∀h. sd h → relation4 genv lenv term term ≝
+ λh,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 ∧ ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T2⦄.
interpretation "context-sensitive extended parallel evaluation (term)"
- 'PEval h g L T1 T2 = (cpxe h g L T1 T2).
+ 'PEval h g G L T1 T2 = (cpxe h g G L T1 T2).
(* Basic_properties *********************************************************)
-lemma csn_cpxe: ∀h,g,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] 𝐍⦃T2⦄.
-#h #g #L #T1 #H @(csn_ind … H) -T1
+lemma csn_cpxe: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] 𝐍⦃T2⦄.
+#h #g #G #L #T1 #H @(csn_ind … H) -T1
#T1 #_ #IHT1
-elim (cnx_dec h g L T1) /3 width=3/
+elim (cnx_dec h g G L T1) /3 width=3/
* #T #H1T1 #H2T1
elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1 #T2 * /4 width=3/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predstar_5.ma".
+include "basic_2/notation/relations/predstar_6.ma".
include "basic_2/unfold/sstas.ma".
include "basic_2/reduction/cnx.ma".
include "basic_2/computation/cprs.ma".
(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
-definition cpxs: ∀h. sd h → lenv → relation term ≝
- λh,g. LTC … (cpx h g).
+definition cpxs: ∀h. sd h → relation4 genv lenv term term ≝
+ λh,g,G. LTC … (cpx h g G).
interpretation "extended context-sensitive parallel computation (term)"
- 'PRedStar h g L T1 T2 = (cpxs h g L T1 T2).
+ 'PRedStar h g G L T1 T2 = (cpxs h g G L T1 T2).
(* Basic eliminators ********************************************************)
-lemma cpxs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 →
+lemma cpxs_ind: ∀h,g,G,L,T1. ∀R:predicate term. R T1 →
(∀T,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T → ⦃G, L⦄ ⊢ T ➡[h, g] T2 → R T → R T2) →
∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → R T2.
-#h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12
+#h #g #L #G #T1 #R #HT1 #IHT1 #T2 #HT12
@(TC_star_ind … HT1 IHT1 … HT12) //
qed-.
-lemma cpxs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 →
+lemma cpxs_ind_dx: ∀h,g,G,L,T2. ∀R:predicate term. R T2 →
(∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T → ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → R T → R T1) →
∀T1. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → R T1.
-#h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12
+#h #g #G #L #T2 #R #HT2 #IHT2 #T1 #HT12
@(TC_star_ind_dx … HT2 IHT2 … HT12) //
qed-.
(* Basic properties *********************************************************)
-lemma cpxs_refl: ∀h,g,L,T. ⦃G, L⦄ ⊢ T ➡*[h, g] T.
+lemma cpxs_refl: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ➡*[h, g] T.
/2 width=1/ qed.
-lemma cpx_cpxs: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
+lemma cpx_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
/2 width=1/ qed.
-lemma cpxs_strap1: ∀h,g,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T →
+lemma cpxs_strap1: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T →
∀T2. ⦃G, L⦄ ⊢ T ➡[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
normalize /2 width=3/ qed.
-lemma cpxs_strap2: ∀h,g,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T →
+lemma cpxs_strap2: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T →
∀T2. ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
normalize /2 width=3/ qed.
-lemma lsubr_cpxs_trans: ∀h,g. lsub_trans … (cpxs h g) lsubr.
+lemma lsubr_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) lsubr.
/3 width=5 by lsubr_cpx_trans, TC_lsub_trans/
qed-.
-lemma sstas_cpxs: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 •* [h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
-#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 //
+lemma sstas_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •* [h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
+#h #g #G #L #T1 #T2 #H @(sstas_ind … H) -T2 //
/3 width=4 by cpxs_strap1, ssta_cpx/
qed.
-lemma cprs_cpxs: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
-#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/
+lemma cprs_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
+#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/
qed.
-lemma cpxs_bind_dx: ∀h,g,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
- ∀I,T1,T2. ⦃h, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[h, g] T2 →
+lemma cpxs_bind_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
+ ∀I,T1,T2. ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[h, g] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1
+#h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1
/3 width=1/ /3 width=3/
qed.
-lemma cpxs_flat_dx: ∀h,g,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
+lemma cpxs_flat_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
- ∀I. ⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡*[h, g] ⓕ{I} V2. T2.
-#h #g #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2 /3 width=1/ /3 width=5/
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡*[h, g] ⓕ{I}V2.T2.
+#h #g #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2 /3 width=1/ /3 width=5/
qed.
-lemma cpxs_flat_sn: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
+lemma cpxs_flat_sn: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
- ∀I. ⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡*[h, g] ⓕ{I} V2. T2.
-#h #g #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2 /3 width=1/ /3 width=5/
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡*[h, g] ⓕ{I}V2.T2.
+#h #g #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2 /3 width=1/ /3 width=5/
qed.
-lemma cpxs_zeta: ∀h,g,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
- ⦃h, L.ⓓV⦄ ⊢ T1 ➡*[h, g] T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡*[h, g] T2.
-#h #g #L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/
+lemma cpxs_zeta: ∀h,g,G,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
+ ⦃G, L.ⓓV⦄ ⊢ T1 ➡*[h, g] T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡*[h, g] T2.
+#h #g #G #L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/
qed.
-lemma cpxs_tau: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡*[h, g] T2.
-#h #g #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/
+lemma cpxs_tau: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
+ ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡*[h, g] T2.
+#h #g #G #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/
qed.
-lemma cpxs_ti: ∀h,g,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → ∀T. ⦃G, L⦄ ⊢ ⓝV1.T ➡*[h, g] V2.
-#h #g #L #V1 #V2 #H elim H -V2 /2 width=3/ /3 width=1/
+lemma cpxs_ti: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
+ ∀T. ⦃G, L⦄ ⊢ ⓝV1.T ➡*[h, g] V2.
+#h #g #G #L #V1 #V2 #H elim H -V2 /2 width=3/ /3 width=1/
qed.
-lemma cpxs_beta_dx: ∀h,g,a,L,V1,V2,W1,W2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡[h, g] W2 →
+lemma cpxs_beta_dx: ∀h,g,a,G,L,V1,V2,W1,W2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡[h, g] W2 →
⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[h, g] ⓓ{a}ⓝW2.V2.T2.
-#h #g #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2 /3 width=1/
+#h #g #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2 /3 width=1/
/4 width=7 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ (**) (* auto too slow without trace *)
qed.
-lemma cpxs_theta_dx: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ➡[h, g] V → ⇧[0, 1] V ≡ V2 → ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 →
+lemma cpxs_theta_dx: ∀h,g,a,G,L,V1,V,V2,W1,W2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ➡[h, g] V → ⇧[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 →
⦃G, L⦄ ⊢ W1 ➡[h, g] W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[h, g] ⓓ{a}W2.ⓐV2.T2.
-#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ]
+#h #g #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ]
/4 width=9 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/ (**) (* auto too slow without trace *)
qed.
(* Basic inversion lemmas ***************************************************)
-lemma cpxs_inv_sort1: ∀h,g,L,U2,k. ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] U2 →
+lemma cpxs_inv_sort1: ∀h,g,G,L,U2,k. ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] U2 →
∃∃n,l. deg h g k (n+l) & U2 = ⋆((next h)^n k).
-#h #g #L #U2 #k #H @(cpxs_ind … H) -U2
+#h #g #G #L #U2 #k #H @(cpxs_ind … H) -U2
[ elim (deg_total h g k) #l #Hkl
@(ex2_2_intro … 0 … Hkl) -Hkl //
| #U #U2 #_ #HU2 * #n #l #Hknl #H destruct
]
qed-.
-lemma cpxs_inv_cast1: ∀h,g,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡*[h, g] U2 →
+lemma cpxs_inv_cast1: ∀h,g,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡*[h, g] U2 →
∨∨ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 & ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 & U2 = ⓝW2.T2
| ⦃G, L⦄ ⊢ T1 ➡*[h, g] U2
| ⦃G, L⦄ ⊢ W1 ➡*[h, g] U2.
-#h #g #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/
+#h #g #G #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/
#U2 #U #_ #HU2 * /3 width=3/ *
#W #T #HW1 #HT1 #H destruct
elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3/ *
lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5/
qed-.
-lemma cpxs_inv_cnx1: ∀h,g,L,T,U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → T = U.
-#h #g #L #T #U #H @(cpxs_ind_dx … H) -T //
+lemma cpxs_inv_cnx1: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → T = U.
+#h #g #G #L #T #U #H @(cpxs_ind_dx … H) -T //
#T0 #T #H1T0 #_ #IHT #H2T0
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
qed-.
(* Properties about atomic arity assignment on terms ************************)
-lemma aaa_cpxs_conf: ∀h,g,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
+lemma aaa_cpxs_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-#h #g #L #T1 #A #HT1 #T2 #HT12
+#h #g #G #L #T1 #A #HT1 #T2 #HT12
@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by aaa_cpx_conf/
qed-.
-lemma aaa_cprs_conf: ∀L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+lemma aaa_cprs_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
/3 width=5 by aaa_cpxs_conf, cprs_cpxs/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/reduction/lpx_ldrop.ma".
include "basic_2/computation/cpxs_lift.ma".
+include "basic_2/reduction/lpx_ldrop.ma". (**) (* disambiguation error *)
(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
(* Main properties **********************************************************)
-theorem cpxs_trans: ∀h,g,L. Transitive … (cpxs h g L).
-#h #g #L #T1 #T #HT1 #T2 @trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
+theorem cpxs_trans: ∀h,g,G,L. Transitive … (cpxs h g G L).
+#h #g #G #L #T1 #T #HT1 #T2 @trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
-theorem cpxs_bind: ∀h,g,a,I,L,V1,V2,T1,T2. ⦃h, L.ⓑ{I}V1⦄ ⊢ T1 ➡*[h, g] T2 →
+theorem cpxs_bind: ∀h,g,a,I,G,L,V1,V2,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡*[h, g] T2 →
⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-#h #g #a #I #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/
+#h #g #a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/
#V #V2 #_ #HV2 #IHV1
@(cpxs_trans … IHV1) -V1 /2 width=1/
qed.
-theorem cpxs_flat: ∀h,g,I,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
+theorem cpxs_flat: ∀h,g,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
- ⦃G, L⦄ ⊢ ⓕ{I} V1.T1 ➡*[h, g] ⓕ{I} V2.T2.
-#h #g #I #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/
+ ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡*[h, g] ⓕ{I}V2.T2.
+#h #g #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/
#V #V2 #_ #HV2 #IHV1
@(cpxs_trans … IHV1) -IHV1 /2 width=1/
qed.
-theorem cpxs_beta_rc: ∀h,g,a,L,V1,V2,W1,W2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 →
+theorem cpxs_beta_rc: ∀h,g,a,G,L,V1,V2,W1,W2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 →
⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[h, g] ⓓ{a}ⓝW2.V2.T2.
-#h #g #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2 /2 width=1/
+#h #g #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2 /2 width=1/
#W #W2 #_ #HW2 #IHW1
@(cpxs_trans … IHW1) -IHW1 /3 width=1/
qed.
-theorem cpxs_beta: ∀h,g,a,L,V1,V2,W1,W2,T1,T2.
- ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 → ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
+theorem cpxs_beta: ∀h,g,a,G,L,V1,V2,W1,W2,T1,T2.
+ ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 → ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[h, g] ⓓ{a}ⓝW2.V2.T2.
-#h #g #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cpxs_ind … H) -V2 /2 width=1/
+#h #g #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cpxs_ind … H) -V2 /2 width=1/
#V #V2 #_ #HV2 #IHV1
@(cpxs_trans … IHV1) -IHV1 /3 width=1/
qed.
-theorem cpxs_theta_rc: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2.
+theorem cpxs_theta_rc: ∀h,g,a,G,L,V1,V,V2,W1,W2,T1,T2.
⦃G, L⦄ ⊢ V1 ➡[h, g] V → ⇧[0, 1] V ≡ V2 →
- ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 →
+ ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 →
⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[h, g] ⓓ{a}W2.ⓐV2.T2.
-#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/
+#h #g #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/
#W #W2 #_ #HW2 #IHW1
@(cpxs_trans … IHW1) -IHW1 /2 width=1/
qed.
-theorem cpxs_theta: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2.
+theorem cpxs_theta: ∀h,g,a,G,L,V1,V,V2,W1,W2,T1,T2.
⇧[0, 1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ➡*[h, g] W2 →
- ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ V1 ➡*[h, g] V →
+ ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ V1 ➡*[h, g] V →
⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[h, g] ⓓ{a}W2.ⓐV2.T2.
-#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/
+#h #g #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/
#V1 #V0 #HV10 #_ #IHV0
@(cpxs_trans … IHV0) -IHV0 /2 width=1/
qed.
(* Advanced inversion lemmas ************************************************)
-lemma cpxs_inv_appl1: ∀h,g,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡*[h, g] U2 →
+lemma cpxs_inv_appl1: ∀h,g,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡*[h, g] U2 →
∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 &
U2 = ⓐV2. T2
| ∃∃a,W,T. ⦃G, L⦄ ⊢ T1 ➡*[h, g] ⓛ{a}W.T & ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V1.T ➡*[h, g] U2
| ∃∃a,V0,V2,V,T. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V0 & ⇧[0,1] V0 ≡ V2 &
⦃G, L⦄ ⊢ T1 ➡*[h, g] ⓓ{a}V.T & ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U2.
-#h #g #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5/ ]
+#h #g #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5/ ]
#U #U2 #_ #HU2 * *
[ #V0 #T0 #HV10 #HT10 #H destruct
elim (cpx_inv_appl1 … HU2) -HU2 *
(* Properties on sn extended parallel reduction for local environments ******)
-lemma lpx_cpx_trans: ∀h,g. s_r_trans … (cpx h g) (lpx h g).
-#h #g #L2 #T1 #T2 #HT12 elim HT12 -L2 -T1 -T2
+lemma lpx_cpx_trans: ∀h,g,G. s_r_trans … (cpx h g G) (lpx h g G).
+#h #g #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
[ /2 width=3/
| /3 width=2/
-| #I #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
+| #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
lapply (IHV02 … HK12) -K2 #HV02
lapply (cpxs_strap2 … HV10 … HV02) -V0 /2 width=7/
-| #a #I #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
+| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /2 width=1/ /3 width=1/
|5,7,8: /3 width=1/
-| #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
+| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=1/ /2 width=3/
-| #a #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12
+| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12
lapply (IHT12 (L1.ⓛW1) ?) -IHT12 /2 width=1/ /3 width=1/
-| #a #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12
+| #a #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12
lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /2 width=1/ /3 width=3/
]
qed-.
-lemma cpx_bind2: ∀h,g,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
- ∀I,T1,T2. ⦃h, L.ⓑ{I}V2⦄ ⊢ T1 ➡[h, g] T2 →
+lemma cpx_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡[h, g] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+#h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
lapply (lpx_cpx_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
qed.
(* Advanced properties ******************************************************)
-lemma lpx_cpxs_trans: ∀h,g. s_rs_trans … (cpx h g) (lpx h g).
+lemma lpx_cpxs_trans: ∀h,g,G. s_rs_trans … (cpx h g G) (lpx h g G).
/3 width=5 by s_r_trans_TC1, lpx_cpx_trans/ qed-.
-lemma cpxs_bind2_dx: ∀h,g,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
- ∀I,T1,T2. ⦃h, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
+lemma cpxs_bind2_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+#h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
lapply (lpx_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
qed.
(* Advanced properties ******************************************************)
-lemma cpxs_delta: ∀h,g,I,L,K,V,V2,i.
- ⇩[0, i] L ≡ K. ⓑ{I}V → ⦃h, K⦄ ⊢ V ➡*[h, g] V2 →
+lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i.
+ ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ➡*[h, g] V2 →
∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2.
-#h #g #I #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=9/ ]
+#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=9/ ]
#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2
lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/
(* Advanced inversion lemmas ************************************************)
-lemma cpxs_inv_lref1: ∀h,g,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 →
+lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 →
T2 = #i ∨
- ∃∃I,K,V1,T1. ⇩[0, i] L ≡ K.ⓑ{I}V1 & ⦃h, K⦄ ⊢ V1 ➡*[h, g] T1 &
+ ∃∃I,K,V1,T1. ⇩[0, i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ➡*[h, g] T1 &
⇧[0, i + 1] T1 ≡ T2.
-#h #g #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1/
+#h #g #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1/
#T #T2 #_ #HT2 *
[ #H destruct
elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1/
(* Relocation properties ****************************************************)
-lemma cpxs_lift: ∀h,g. l_liftable (cpxs h g).
+lemma cpxs_lift: ∀h,g,G. l_liftable (cpxs h g G).
/3 width=9/ qed.
-lemma cpxs_inv_lift1: ∀h,g. l_deliftable_sn (cpxs h g).
+lemma cpxs_inv_lift1: ∀h,g,G. l_deliftable_sn (cpxs h g G).
/3 width=5 by l_deliftable_sn_LTC, cpx_inv_lift1/
qed-.
(* Properties on supclosure *************************************************)
-lemma fsupq_cpxs_trans: ∀h,g,L1,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 ➡*[h, g] U2 →
- ∀T1. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ →
- ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄.
-#h #g #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 [ /3 width=3/ ]
+lemma fsupq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
+ ∀T1. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 [ /3 width=3/ ]
#T #T2 #HT2 #_ #IHTU2 #T1 #HT1
elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2
elim (IHTU2 … HT2) -T2 /3 width=3/
qed-.
-lemma fsups_cpxs_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ →
- ∀U2. ⦃h, L2⦄ ⊢ T2 ➡*[h, g] U2 →
- ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄.
-#h #g #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 [ /2 width=3/ ]
-#L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
+lemma fsups_cpxs_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 [ /2 width=3/ ]
+#G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
elim (fsupq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2
elim (IHT1 … HT2) -T #T #HT1 #HT2
-lapply (fsups_trans … HT2 … HTU2) -L -T2 /2 width=3/
+lapply (fsups_trans … HT2 … HTU2) -G -L -T2 /2 width=3/
qed-.
-lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
- ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l+1, U2⦄ →
- ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
+lemma fsup_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀U2,l. ⦃G2, L2⦄ ⊢ T2 •[h, g] ⦃l+1, U2⦄ →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
/3 width=4 by fsup_cpx_trans, ssta_cpx/ qed-.
(* Forward lemmas involving same top term constructor ***********************)
-lemma cpxs_fwd_cnx: ∀h,g,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≃ U.
-#h #g #L #T #HT #U #H
->(cpxs_inv_cnx1 … H HT) -L -T //
+lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≃ U.
+#h #g #G #L #T #HT #U #H
+>(cpxs_inv_cnx1 … H HT) -G -L -T //
qed-.
-lemma cpxs_fwd_sort: ∀h,g,L,U,k. ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] U →
+lemma cpxs_fwd_sort: ∀h,g,G,L,U,k. ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] U →
⋆k ≃ U ∨ ⦃G, L⦄ ⊢ ⋆(next h k) ➡*[h, g] U.
-#h #g #L #U #k #H
+#h #g #G #L #U #k #H
elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus … n) -n
[ #k #_ #H -l destruct /2 width=1/
| #n #IHn #k >plus_plus_comm_23 #Hnl #H destruct
qed-.
(* Basic_1: was just: pr3_iso_beta *)
-lemma cpxs_fwd_beta: ∀h,g,a,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[h, g] U →
+lemma cpxs_fwd_beta: ∀h,g,a,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[h, g] U →
ⓐV.ⓛ{a}W.T ≃ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V.T ➡*[h, g] U.
-#h #g #a #L #V #W #T #U #H
+#h #g #a #G #L #V #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
[ #V0 #T0 #_ #_ #H destruct /2 width=1/
| #b #W0 #T0 #HT0 #HU
qed-.
(* Note: probably this is an inversion lemma *)
-lemma cpxs_fwd_delta: ∀h,g,I,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
+lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
∀V2. ⇧[0, i + 1] V1 ≡ V2 →
∀U. ⦃G, L⦄ ⊢ #i ➡*[h, g] U →
#i ≃ U ∨ ⦃G, L⦄ ⊢ V2 ➡*[h, g] U.
-#h #g #I #L #K #V1 #i #HLK #V2 #HV12 #U #H
+#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H
elim (cpxs_inv_lref1 … H) -H /2 width=1/
* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/
qed-.
-lemma cpxs_fwd_theta: ∀h,g,a,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U →
+lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U →
∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≃ U ∨
⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U.
-#h #g #a #L #V1 #V #T #U #H #V2 #HV12
+#h #g #a #G #L #V1 #V #T #U #H #V2 #HV12
elim (cpxs_inv_appl1 … H) -H *
[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1/
| #b #W #T0 #HT0 #HU
]
qed-.
-lemma cpxs_fwd_cast: ∀h,g,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ➡*[h, g] U →
+lemma cpxs_fwd_cast: ∀h,g,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ➡*[h, g] U →
∨∨ ⓝW. T ≃ U | ⦃G, L⦄ ⊢ T ➡*[h, g] U | ⦃G, L⦄ ⊢ W ➡*[h, g] U.
-#h #g #L #W #T #U #H
+#h #g #G #L #W #T #U #H
elim (cpxs_inv_cast1 … H) -H /2 width=1/ *
#W0 #T0 #_ #_ #H destruct /2 width=1/
qed-.
(* Vector form of forward lemmas involving same top term constructor ********)
(* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector: ∀h,g,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ →
+lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ →
∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≃ U.
-#h #g #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
+#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
#V #Vs #IHVs #U #H
elim (cpxs_inv_appl1 … H) -H *
[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
]
qed-.
-lemma cpxs_fwd_sort_vector: ∀h,g,L,k,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆k ➡*[h, g] U →
+lemma cpxs_fwd_sort_vector: ∀h,g,G,L,k,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆k ➡*[h, g] U →
ⒶVs.⋆k ≃ U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h k) ➡*[h, g] U.
-#h #g #L #k #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/
+#h #g #G #L #k #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/
#V #Vs #IHVs #U #H
elim (cpxs_inv_appl1 … H) -H *
[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/
(* Basic_1: was just: pr3_iso_appls_beta *)
-lemma cpxs_fwd_beta_vector: ∀h,g,a,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[h, g] U →
+lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[h, g] U →
ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[h, g] U.
-#h #g #a #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
+#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
#V0 #Vs #IHVs #V #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/
]
qed-.
-lemma cpxs_fwd_delta_vector: ∀h,g,I,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
+lemma cpxs_fwd_delta_vector: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
∀V2. ⇧[0, i + 1] V1 ≡ V2 →
∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ➡*[h, g] U →
ⒶVs.#i ≃ U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ➡*[h, g] U.
-#h #g #I #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/
+#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/
#V #Vs #IHVs #U #H -K -V1
elim (cpxs_inv_appl1 … H) -H *
[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
qed-.
(* Basic_1: was just: pr3_iso_appls_abbr *)
-lemma cpxs_fwd_theta_vector: ∀h,g,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U →
ⒶV1s. ⓓ{a}V. T ≃ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U.
-#h #g #L #V1s #V2s * -V1s -V2s /3 width=1/
+#h #g #G #L #V1s #V2s * -V1s -V2s /3 width=1/
#V1s #V2s #V1a #V2a #HV12a #HV12s #a
generalize in match HV12a; -HV12a
generalize in match V2a; -V2a
qed-.
(* Basic_1: was just: pr3_iso_appls_cast *)
-lemma cpxs_fwd_cast_vector: ∀h,g,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[h, g] U →
+lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[h, g] U →
∨∨ ⒶVs. ⓝW. T ≃ U
| ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U
| ⦃G, L⦄ ⊢ ⒶVs.W ➡*[h, g] U.
-#h #g #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
+#h #g #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
#V #Vs #IHVs #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/sn_4.ma".
+include "basic_2/notation/relations/sn_5.ma".
include "basic_2/reduction/cnx.ma".
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-definition csn: ∀h. sd h → lenv → predicate term ≝
- λh,g,L. SN … (cpx h g L) (eq …).
+definition csn: ∀h. sd h → relation3 genv lenv term ≝
+ λh,g,G,L. SN … (cpx h g G L) (eq …).
interpretation
"context-sensitive extended strong normalization (term)"
- 'SN h g L T = (csn h g L T).
+ 'SN h g G L T = (csn h g G L T).
(* Basic eliminators ********************************************************)
-lemma csn_ind: ∀h,g,L. ∀R:predicate term.
+lemma csn_ind: ∀h,g,G,L. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
(∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → R T2) →
R T1
) →
∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R T.
-#h #g #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
+#h #g #G #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
@H0 -H0 /3 width=1/ -IHT1 /4 width=1/
qed-.
(* Basic properties *********************************************************)
(* Basic_1: was just: sn3_pr2_intro *)
-lemma csn_intro: ∀h,g,L,T1.
+lemma csn_intro: ∀h,g,G,L,T1.
(∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] T2) →
⦃G, L⦄ ⊢ ⬊*[h, g] T1.
/4 width=1/ qed.
-lemma csn_cpx_trans: ∀h,g,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
+lemma csn_cpx_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ ⬊*[h, g] T2.
-#h #g #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
+#h #g #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
@csn_intro #T #HLT2 #HT2
elim (term_eq_dec T1 T2) #HT12
[ -IHT1 -HLT12 destruct /3 width=1/
qed-.
(* Basic_1: was just: sn3_nf2 *)
-lemma cnx_csn: ∀h,g,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+lemma cnx_csn: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
/2 width=1/ qed.
-lemma cnx_sort: ∀h,g,L,k. ⦃G, L⦄ ⊢ ⬊*[h, g] ⋆k.
-#h #g #L #k elim (deg_total h g k)
+lemma cnx_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ⬊*[h, g] ⋆k.
+#h #g #G #L #k elim (deg_total h g k)
#l generalize in match k; -k @(nat_ind_plus … l) -l /3 width=1/
#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
#Hkl @csn_intro #X #H #HX elim (cpx_inv_sort1 … H) -H
qed.
(* Basic_1: was just: sn3_cast *)
-lemma csn_cast: ∀h,g,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
+lemma csn_cast: ∀h,g,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓝW.T.
-#h #g #L #W #HW @(csn_ind … HW) -W #W #HW #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
+#h #g #G #L #W #HW @(csn_ind … HW) -W #W #HW #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
elim (cpx_inv_cast1 … H1) -H1
[ * #W0 #T0 #HLW0 #HLT0 #H destruct
(* Basic forward lemmas *****************************************************)
-fact csn_fwd_pair_sn_aux: ∀h,g,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U →
+fact csn_fwd_pair_sn_aux: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U →
∀I,V,T. U = ②{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] V.
-#h #g #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
+#h #g #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csn_intro #V2 #HLV2 #HV2
@(IH (②{I}V2.T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/
qed-.
(* Basic_1: was just: sn3_gen_head *)
-lemma csn_fwd_pair_sn: ∀h,g,I,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ②{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] V.
+lemma csn_fwd_pair_sn: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ②{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] V.
/2 width=5 by csn_fwd_pair_sn_aux/ qed-.
-fact csn_fwd_bind_dx_aux: ∀h,g,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U →
- ∀a,I,V,T. U = ⓑ{a,I}V.T → ⦃h, L.ⓑ{I}V⦄ ⊢ ⬊*[h, g] T.
-#h #g #L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct
+fact csn_fwd_bind_dx_aux: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U →
+ ∀a,I,V,T. U = ⓑ{a,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct
@csn_intro #T2 #HLT2 #HT2
-@(IH (ⓑ{a,I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
+@(IH (ⓑ{a,I}V.T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
qed-.
(* Basic_1: was just: sn3_gen_bind *)
-lemma csn_fwd_bind_dx: ∀h,g,a,I,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓑ{a,I}V.T → ⦃h, L.ⓑ{I}V⦄ ⊢ ⬊*[h, g] T.
+lemma csn_fwd_bind_dx: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓑ{a,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬊*[h, g] T.
/2 width=4 by csn_fwd_bind_dx_aux/ qed-.
-fact csn_fwd_flat_dx_aux: ∀h,g,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U →
+fact csn_fwd_flat_dx_aux: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U →
∀I,V,T. U = ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
+#h #g #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csn_intro #T2 #HLT2 #HT2
@(IH (ⓕ{I}V.T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
qed-.
(* Basic_1: was just: sn3_gen_flat *)
-lemma csn_fwd_flat_dx: ∀h,g,I,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+lemma csn_fwd_flat_dx: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
/2 width=5 by csn_fwd_flat_dx_aux/ qed-.
(* Basic_1: removed theorems 14:
(* Main properties concerning atomic arity assignment ***********************)
-theorem csn_aaa: ∀h,g,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #L #T #A #H
+theorem aaa_csn: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L #T #A #H
@(acp_aaa … (csn_acp h g) (csn_acr h g) … H)
qed.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/snalt_4.ma".
+include "basic_2/notation/relations/snalt_5.ma".
include "basic_2/computation/cpxs.ma".
include "basic_2/computation/csn.ma".
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
(* alternative definition of csn *)
-definition csna: ∀h. sd h → lenv → predicate term ≝
- λh,g,L. SN … (cpxs h g L) (eq …).
+definition csna: ∀h. sd h → relation3 genv lenv term ≝
+ λh,g,G,L. SN … (cpxs h g G L) (eq …).
interpretation
"context-sensitive extended strong normalization (term) alternative"
- 'SNAlt h g L T = (csna h g L T).
+ 'SNAlt h g G L T = (csna h g G L T).
(* Basic eliminators ********************************************************)
-lemma csna_ind: ∀h,g,L. ∀R:predicate term.
+lemma csna_ind: ∀h,g,G,L. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1 →
(∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1
) →
∀T. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T → R T.
-#h #g #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
+#h #g #G #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
@H0 -H0 /3 width=1/ -IHT1 /4 width=1/
qed-.
(* Basic properties *********************************************************)
(* Basic_1: was just: sn3_intro *)
-lemma csna_intro: ∀h,g,L,T1.
+lemma csna_intro: ∀h,g,G,L,T1.
(∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2) →
⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1.
/4 width=1/ qed.
-fact csna_intro_aux: ∀h,g,L,T1. (
+fact csna_intro_aux: ∀h,g,G,L,T1. (
∀T,T2. ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → T1 = T → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2
) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1.
/4 width=3/ qed-.
(* Basic_1: was just: sn3_pr3_trans (old version) *)
-lemma csna_cpxs_trans: ∀h,g,L,T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1 →
+lemma csna_cpxs_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1 →
∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2.
-#h #g #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
+#h #g #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
@csna_intro #T #HLT2 #HT2
elim (term_eq_dec T1 T2) #HT12
[ -IHT1 -HLT12 destruct /3 width=1/
qed.
(* Basic_1: was just: sn3_pr2_intro (old version) *)
-lemma csna_intro_cpx: ∀h,g,L,T1. (
+lemma csna_intro_cpx: ∀h,g,G,L,T1. (
∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2
) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1.
-#h #g #L #T1 #H
+#h #g #G #L #T1 #H
@csna_intro_aux #T #T2 #H @(cpxs_ind_dx … H) -T
[ -H #H destruct #H
elim H //
(* Main properties **********************************************************)
-theorem csn_csna: ∀h,g,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T.
-#h #g #L #T #H @(csn_ind … H) -T /4 width=1/
+theorem csn_csna: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T.
+#h #g #G #L #T #H @(csn_ind … H) -T /4 width=1/
qed.
-theorem csna_csn: ∀h,g,L,T. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #L #T #H @(csna_ind … H) -T /4 width=1/
+theorem csna_csn: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L #T #H @(csna_ind … H) -T /4 width=1/
qed.
(* Basic_1: was just: sn3_pr3_trans *)
-lemma csn_cpxs_trans: ∀h,g,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
+lemma csn_cpxs_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ ⬊*[h, g] T2.
-#h #g #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 // /2 width=3 by csn_cpx_trans/
+#h #g #G #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 // /2 width=3 by csn_cpx_trans/
qed-.
(* Main eliminators *********************************************************)
-lemma csn_ind_alt: ∀h,g,L. ∀R:predicate term.
+lemma csn_ind_alt: ∀h,g,G,L. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
(∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1
) →
∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R T.
-#h #g #L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1
+#h #g #G #L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1
@H0 -H0 /2 width=1/ -HT1 /3 width=1/
qed-.
(* *)
(**************************************************************************)
+include "basic_2/computation/csn.ma". (**) (* disambiguation error *)
include "basic_2/reduction/cnx_lift.ma".
include "basic_2/computation/acp.ma".
-include "basic_2/computation/csn.ma".
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
(* Relocation properties ****************************************************)
(* Basic_1: was just: sn3_lift *)
-lemma csn_lift: ∀h,g,L2,L1,T1,d,e. ⦃h, L1⦄ ⊢ ⬊*[h, g] T1 →
- ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → ⦃h, L2⦄ ⊢ ⬊*[h, g] T2.
-#h #g #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12
+lemma csn_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 →
+ ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2.
+#h #g #G #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12
@csn_intro #T #HLT2 #HT2
elim (cpx_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10
@(IHT1 … HLT10) // -L1 -L2 #H destruct
qed.
(* Basic_1: was just: sn3_gen_lift *)
-lemma csn_inv_lift: ∀h,g,L2,L1,T1,d,e. ⦃h, L1⦄ ⊢ ⬊*[h, g] T1 →
- ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → ⦃h, L2⦄ ⊢ ⬊*[h, g] T2.
-#h #g #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21
+lemma csn_inv_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 →
+ ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2.
+#h #g #G #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21
@csn_intro #T #HLT2 #HT2
elim (lift_total T d e) #T0 #HT0
lapply (cpx_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10
(* Advanced properties ******************************************************)
(* Basic_1: was just: sn3_abbr *)
-lemma csn_lref_bind: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃h, K⦄ ⊢ ⬊*[h, g] V → ⦃G, L⦄ ⊢ ⬊*[h, g] #i.
-#h #g #I #L #K #V #i #HLK #HV
+lemma csn_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ⬊*[h, g] V → ⦃G, L⦄ ⊢ ⬊*[h, g] #i.
+#h #g #I #G #L #K #V #i #HLK #HV
@csn_intro #X #H #Hi
elim (cpx_inv_lref1 … H) -H
[ #H destruct elim Hi //
]
qed.
-lemma csn_appl_simple: ∀h,g,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1.
+lemma csn_appl_simple: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1.
(∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.
-#h #g #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1
+#h #g #G #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1
@csn_intro #X #H1 #H2
elim (cpx_inv_appl1_simple … H1) // -H1
#V0 #T0 #HLV0 #HLT10 #H destruct
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was: sn3_gen_def *)
-lemma csn_inv_lref_bind: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V →
- ⦃G, L⦄ ⊢ ⬊*[h, g] #i → ⦃h, K⦄ ⊢ ⬊*[h, g] V.
-#h #g #I #L #K #V #i #HLK #Hi
+lemma csn_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V →
+ ⦃G, L⦄ ⊢ ⬊*[h, g] #i → ⦃G, K⦄ ⊢ ⬊*[h, g] V.
+#h #g #I #G #L #K #V #i #HLK #Hi
elim (lift_total V 0 (i+1)) #V0 #HV0
lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
@(csn_inv_lift … H0LK … HV0) -H0LK
theorem csn_acp: ∀h,g. acp (cpx h g) (eq …) (csn h g).
#h #g @mk_acp
-[ #L elim (deg_total h g 0)
+[ #G #L elim (deg_total h g 0)
#l #Hl lapply (cnx_sort_iter … L … Hl) /2 width=2/
| @cnx_lift
| /2 width=3 by csn_fwd_flat_dx/
(* Advanced properties ******************************************************)
-lemma csn_lpx_conf: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[h, g] L2 →
- ∀T. ⦃h, L1⦄ ⊢ ⬊*[h, g] T → ⦃h, L2⦄ ⊢ ⬊*[h, g] T.
-#h #g #L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT
+lemma csn_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+ ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT
@csn_intro #T0 #HLT0 #HT0
@IHT /2 width=2/ -IHT -HT0 /2 width=3 by lpx_cpx_trans/
qed.
-lemma csn_abst: ∀h,g,a,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
- ∀T. ⦃h, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T.
-#h #g #a #L #W #HW @(csn_ind … HW) -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
+lemma csn_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
+ ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T.
+#h #g #a #G #L #W #HW @(csn_ind … HW) -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
elim (cpx_inv_abst1 … H1) -H1
#W0 #T0 #HLW0 #HLT0 #H destruct
]
qed.
-lemma csn_abbr: ∀h,g,a,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V →
- ∀T. ⦃h, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T.
-#h #g #a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT
+lemma csn_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V →
+ ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T.
+#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
elim (cpx_inv_abbr1 … H1) -H1 *
[ #V1 #T1 #HLV1 #HLT1 #H destruct
elim (eq_false_inv_tpair_sn … H2) -H2
[ #HV1 @IHV // /2 width=1/ -HV1
- @(csn_lpx_conf … (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csn_cpx_trans/
+ @(csn_lpx_conf … (L.ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csn_cpx_trans/
| -IHV -HLV1 * #H destruct /3 width=1/
]
| -IHV -IHT -H2 #T0 #HLT0 #HT0
]
qed.
-fact csn_appl_beta_aux: ∀h,g,a,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 →
+fact csn_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 →
∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1.
-#h #g #a #L #X #H @(csn_ind … H) -X
+#h #g #a #G #L #X #H @(csn_ind … H) -X
#X #HT1 #IHT1 #V #W #T1 #H1 destruct
@csn_intro #X #H1 #H2
elim (cpx_inv_appl1 … H1) -H1 *
qed-.
(* Basic_1: was just: sn3_beta *)
-lemma csn_appl_beta: ∀h,g,a,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T.
+lemma csn_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T.
/2 width=3 by csn_appl_beta_aux/ qed.
-fact csn_appl_theta_aux: ∀h,g,a,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
+fact csn_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
-#h #g #a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
+#h #g #a #G #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
lapply (csn_fwd_pair_sn … HVT) #HV
lapply (csn_fwd_bind_dx … HVT) -HVT #HVT
@csn_intro #X #HL #H
qed-.
lemma csn_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
+ ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
/2 width=5 by csn_appl_theta_aux/ qed.
(* Basic_1: was just: sn3_appl_appl *)
-lemma csn_appl_simple_tstc: ∀h,g,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
+lemma csn_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
(∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.
-#h #g #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
+#h #g #G #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
@csn_intro #X #HL #H
elim (cpx_inv_appl1_simple … HL) -HL //
#V0 #T0 #HLV0 #HLT10 #H0 destruct
(* Advanced properties ******************************************************)
(* Basic_1: was just: sn3_appls_lref *)
-lemma csn_applv_cnx: ∀h,g,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ →
+lemma csn_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ →
∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T.
-#h #g #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csn … H2T) ] (**) (* /2 width=1/ does not work *)
+#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csn … H2T) ] (**) (* /2 width=1/ does not work *)
#V #Vs #IHV #H
elim (csnv_inv_cons … H) -H #HV #HVs
@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -HVs
elim (H0) -H0 //
qed.
-lemma csn_applv_sort: ∀h,g,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
-#h #g #L #k elim (deg_total h g k)
+lemma csn_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
+#h #g #G #L #k elim (deg_total h g k)
#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=1/ ]
#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
#Hkl #Vs elim Vs -Vs /2 width=1/
qed.
(* Basic_1: was just: sn3_appls_beta *)
-lemma csn_applv_beta: ∀h,g,a,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T →
+lemma csn_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T →
⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T.
-#h #g #a #L #Vs elim Vs -Vs /2 width=1/
+#h #g #a #G #L #Vs elim Vs -Vs /2 width=1/
#V0 #Vs #IHV #V #W #T #H1T
lapply (csn_fwd_pair_sn … H1T) #HV0
lapply (csn_fwd_flat_dx … H1T) #H2T
]
qed.
-lemma csn_applv_delta: ∀h,g,I,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
+lemma csn_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
∀V2. ⇧[0, i + 1] V1 ≡ V2 →
∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i).
-#h #g #I #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
+#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
[ #H
lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
lapply (csn_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=5/
qed.
(* Basic_1: was just: sn3_appls_abbr *)
-lemma csn_applv_theta: ∀h,g,a,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+lemma csn_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T →
⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T.
-#h #g #a #L #V1s #V2s * -V1s -V2s /2 width=1/
+#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1/
#V1s #V2s #V1 #V2 #HV12 #H
generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
elim H -V1s -V2s /2 width=3/
qed.
(* Basic_1: was just: sn3_appls_cast *)
-lemma csn_applv_cast: ∀h,g,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T →
+lemma csn_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T →
⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T.
-#h #g #L #Vs elim Vs -Vs /2 width=1/
+#h #g #G #L #Vs elim Vs -Vs /2 width=1/
#V #Vs #IHV #W #T #H1W #H1T
lapply (csn_fwd_pair_sn … H1W) #HV
lapply (csn_fwd_flat_dx … H1W) #H2W
]
qed.
-theorem csn_acr: ∀h,g. acr (cpx h g) (eq …) (csn h g) (λL,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T).
+theorem csn_acr: ∀h,g. acr (cpx h g) (eq …) (csn h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T).
#h #g @mk_acr //
[ /3 width=1/
|2,3,6: /2 width=1/
| /2 width=7/
-| #L #V1s #V2s #HV12s #a #V #T #H #HV
+| #G #L #V1s #V2s #HV12s #a #V #T #H #HV
@(csn_applv_theta … HV12s) -HV12s
@(csn_abbr) //
| @csn_lift
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************)
-definition csnv: ∀h. sd h → lenv → predicate (list term) ≝
- λh,g,L. all … (csn h g L).
+definition csnv: ∀h. sd h → relation3 genv lenv (list term) ≝
+ λh,g,G,L. all … (csn h g G L).
interpretation
"context-sensitive strong normalization (term vector)"
- 'SN h g L Ts = (csnv h g L Ts).
+ 'SN h g G L Ts = (csnv h g G L Ts).
(* Basic inversion lemmas ***************************************************)
-lemma csnv_inv_cons: ∀h,g,L,T,Ts. ⦃G, L⦄ ⊢ ⬊*[h, g] T @ Ts →
+lemma csnv_inv_cons: ∀h,g,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬊*[h, g] T @ Ts →
⦃G, L⦄ ⊢ ⬊*[h, g] T ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] Ts.
normalize // qed-.
(* Basic forward lemmas *****************************************************)
-lemma csn_fwd_applv: ∀h,g,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T →
+lemma csn_fwd_applv: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T →
⦃G, L⦄ ⊢ ⬊*[h, g] Vs ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #L #T #Vs elim Vs -Vs /2 width=1/
+#h #g #G #L #T #Vs elim Vs -Vs /2 width=1/
#V #Vs #IHVs #HVs
lapply (csn_fwd_pair_sn … HVs) #HV
lapply (csn_fwd_flat_dx … HVs) -HVs #HVs
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predsnstar_2.ma".
+include "basic_2/notation/relations/predsnstar_3.ma".
+include "basic_2/reduction/lpr.ma". (**) (* disambiguation error *)
include "basic_2/grammar/lpx_sn_tc.ma".
-include "basic_2/reduction/lpr.ma".
(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
-definition lprs: relation lenv ≝ TC … lpr.
+definition lprs: relation3 genv lenv lenv ≝
+ λG. TC … (lpr G).
interpretation "parallel computation (local environment, sn variant)"
- 'PRedSnStar L1 L2 = (lprs L1 L2).
+ 'PRedSnStar G L1 L2 = (lprs G L1 L2).
(* Basic eliminators ********************************************************)
-lemma lprs_ind: ∀L1. ∀R:predicate lenv. R L1 →
- (∀L,L2. L1 ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → R L → R L2) →
- ∀L2. L1 ⊢ ➡* L2 → R L2.
-#L1 #R #HL1 #IHL1 #L2 #HL12
+lemma lprs_ind: ∀G,L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → R L → R L2) →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L2.
+#G #L1 #R #HL1 #IHL1 #L2 #HL12
@(TC_star_ind … HL1 IHL1 … HL12) //
qed-.
-lemma lprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 →
- (∀L1,L. L1 ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → R L → R L1) →
- ∀L1. L1 ⊢ ➡* L2 → R L1.
-#L2 #R #HL2 #IHL2 #L1 #HL12
+lemma lprs_ind_dx: ∀G,L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → R L → R L1) →
+ ∀L1. ⦃G, L1⦄ ⊢ ➡* L2 → R L1.
+#G #L2 #R #HL2 #IHL2 #L1 #HL12
@(TC_star_ind_dx … HL2 IHL2 … HL12) //
qed-.
(* Basic properties *********************************************************)
-lemma lpr_lprs: ∀L1,L2. L1 ⊢ ➡ L2 → L1 ⊢ ➡* L2.
+lemma lpr_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2.
/2 width=1/ qed.
-lemma lprs_refl: ∀L. ⦃G, L⦄ ⊢ ➡* L.
+lemma lprs_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡* L.
/2 width=1/ qed.
-lemma lprs_strap1: ∀L1,L,L2. L1 ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → L1 ⊢ ➡* L2.
+lemma lprs_strap1: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2.
/2 width=3/ qed.
-lemma lprs_strap2: ∀L1,L,L2. L1 ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → L1 ⊢ ➡* L2.
+lemma lprs_strap2: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2.
/2 width=3/ qed.
-lemma lprs_pair_refl: ∀L1,L2. L1 ⊢ ➡* L2 → ∀I,V. L1. ⓑ{I} V ⊢ ➡* L2. ⓑ{I} V.
+lemma lprs_pair_refl: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡* L2.ⓑ{I}V.
/2 width=1 by TC_lpx_sn_pair_refl/ qed.
(* Basic inversion lemmas ***************************************************)
-lemma lprs_inv_atom1: ∀L2. ⋆ ⊢ ➡* L2 → L2 = ⋆.
+lemma lprs_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ➡* L2 → L2 = ⋆.
/2 width=2 by TC_lpx_sn_inv_atom1/ qed-.
-lemma lprs_inv_atom2: ∀L1. L1 ⊢ ➡* ⋆ → L1 = ⋆.
+lemma lprs_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ➡* ⋆ → L1 = ⋆.
/2 width=2 by TC_lpx_sn_inv_atom2/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma lprs_fwd_length: ∀L1,L2. L1 ⊢ ➡* L2 → |L1| = |L2|.
+lemma lprs_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → |L1| = |L2|.
/2 width=2 by TC_lpx_sn_fwd_length/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predsnstaralt_2.ma".
+include "basic_2/notation/relations/predsnstaralt_3.ma".
include "basic_2/computation/cprs_cprs.ma".
include "basic_2/computation/lprs.ma".
(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
(* alternative definition *)
-definition lprsa: relation lenv ≝ lpx_sn … cprs.
+definition lprsa: relation3 genv lenv lenv ≝
+ λG. lpx_sn … (cprs G).
interpretation "parallel computation (local environment, sn variant) alternative"
- 'PRedSnStarAlt L1 L2 = (lprsa L1 L2).
+ 'PRedSnStarAlt G L1 L2 = (lprsa G L1 L2).
(* Main properties on the alternative definition ****************************)
-theorem lprsa_lprs: ∀L1,L2. L1 ⊢ ➡➡* L2 → L1 ⊢ ➡* L2.
+theorem lprsa_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2.
/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
(* Main inversion lemmas on the alternative definition **********************)
-theorem lprs_inv_lprsa: ∀L1,L2. L1 ⊢ ➡* L2 → L1 ⊢ ➡➡* L2.
+theorem lprs_inv_lprsa: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡➡* L2.
/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpr_cprs_trans/ qed-.
(* Alternative eliminators **************************************************)
-lemma lprs_ind_alt: ∀R:relation lenv.
+lemma lprs_ind_alt: ∀G. ∀R:relation lenv.
R (⋆) (⋆) → (
∀I,K1,K2,V1,V2.
- K1 ⊢ ➡* K2 → K1 ⊢ V1 ➡* V2 →
+ ⦃G, K1⦄ ⊢ ➡* K2 → ⦃G, K1⦄ ⊢ V1 ➡* V2 →
R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
) →
- ∀L1,L2. L1 ⊢ ➡* L2 → R L1 L2.
+ ∀L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L1 L2.
/3 width=4 by TC_lpx_sn_ind, lpr_cprs_trans/ qed-.
(* Advanced properties ******************************************************)
-lemma lprs_pair: ∀I,L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L1 ⊢ V1 ➡* V2 →
- L1. ⓑ{I} V1 ⊢ ➡* L2.ⓑ{I} V2.
+lemma lprs_pair: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
+ ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2.
/2 width=1 by TC_lpx_sn_pair/ qed.
(* Advanced inversion lemmas ************************************************)
-lemma lprs_inv_pair1: ∀I,K1,L2,V1. K1. ⓑ{I} V1 ⊢ ➡* L2 →
- ∃∃K2,V2. K1 ⊢ ➡* K2 & K1 ⊢ V1 ➡* V2 & L2 = K2. ⓑ{I} V2.
+lemma lprs_inv_pair1: ∀I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡* L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡* K2 & ⦃G, K1⦄ ⊢ V1 ➡* V2 &
+ L2 = K2.ⓑ{I}V2.
/3 width=3 by TC_lpx_sn_inv_pair1, lpr_cprs_trans/ qed-.
-lemma lprs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ➡* K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 ⊢ ➡* K2 & K1 ⊢ V1 ➡* V2 & L1 = K1. ⓑ{I} V1.
+lemma lprs_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡* K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡* K2 & ⦃G, K1⦄ ⊢ V1 ➡* V2 &
+ L1 = K1.ⓑ{I}V1.
/3 width=3 by TC_lpx_sn_inv_pair2, lpr_cprs_trans/ qed-.
(* Properties on context-sensitive parallel computation for terms ***********)
-lemma lprs_cpr_trans: s_r_trans … cpr lprs.
+lemma lprs_cpr_trans: ∀G. s_r_trans … (cpr G) (lprs G).
/3 width=5 by s_r_trans_TC2, lpr_cprs_trans/ qed-.
(* Basic_1: was just: pr3_pr3_pr3_t *)
-lemma lprs_cprs_trans: s_rs_trans … cpr lprs.
+lemma lprs_cprs_trans: ∀G. s_rs_trans … (cpr G) (lprs G).
/3 width=5 by s_r_trans_TC1, lprs_cpr_trans/ qed-.
-lemma lprs_cprs_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡* L1 →
- ∃∃T. L1 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
-#L0 #T0 #T1 #HT01 #L1 #H elim H -L1
+lemma lprs_cprs_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
+#G #L0 #T0 #T1 #HT01 #L1 #H elim H -L1
[ #L1 #HL01
elim (cprs_lpr_conf_dx … HT01 … HL01) -L0 /2 width=3/
| #L #L1 #_ #HL1 * #T #HT1 #HT0 -L0
]
qed-.
-lemma lprs_cpr_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ➡* L1 →
- ∃∃T. L1 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
+lemma lprs_cpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
/3 width=3 by lprs_cprs_conf_dx, cpr_cprs/ qed-.
-lemma lprs_cprs_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡* L1 →
- ∃∃T. L0 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
-#L0 #T0 #T1 #HT01 #L1 #HL01
+lemma lprs_cprs_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
+ ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
+#G #L0 #T0 #T1 #HT01 #L1 #HL01
elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01 #T #HT1
lapply (lprs_cprs_trans … HT1 … HL01) -HT1 /2 width=3/
qed-.
-lemma lprs_cpr_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ➡* L1 →
- ∃∃T. L0 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
+lemma lprs_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
+ ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
/3 width=3 by lprs_cprs_conf_sn, cpr_cprs/ qed-.
-lemma cprs_bind2: ∀L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 →
- ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
-#L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+lemma cprs_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 →
+ ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
+#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
lapply (lprs_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
qed.
(* Inversion lemmas on context-sensitive parallel computation for terms *****)
(* Basic_1: was: pr3_gen_abst *)
-lemma cprs_inv_abst1: ∀a,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* U2 →
- ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & L.ⓛW1 ⊢ T1 ➡* T2 &
+lemma cprs_inv_abst1: ∀a,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* U2 →
+ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 &
U2 = ⓛ{a}W2.T2.
-#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/
+#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/
#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
elim (cpr_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
lapply (lprs_cpr_trans … HT02 (L.ⓛV1) ?) /2 width=1/ -HT02 #HT02
lapply (cprs_trans … HT10 … HT02) -T0 /2 width=5/
qed-.
-lemma cprs_inv_abst: ∀a,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2 →
- ⦃G, L⦄ ⊢ W1 ➡* W2 ∧ L.ⓛW1 ⊢ T1 ➡* T2.
-#a #L #W1 #W2 #T1 #T2 #H
+lemma cprs_inv_abst: ∀a,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2 →
+ ⦃G, L⦄ ⊢ W1 ➡* W2 ∧ ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2.
+#a #G #L #W1 #W2 #T1 #T2 #H
elim (cprs_inv_abst1 … H) -H #W #T #HW1 #HT1 #H destruct /2 width=1/
qed-.
(* Basic_1: was pr3_gen_abbr *)
-lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 → (
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 &
+lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 → (
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 &
U2 = ⓓ{a}V2.T2
) ∨
- ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
-#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+ ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
+#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
#U0 #U2 #_ #HU02 * *
[ #V0 #T0 #HV10 #HT10 #H destruct
elim (cpr_inv_abbr1 … HU02) -HU02 *
(* More advanced properties *************************************************)
-lemma lprs_pair2: ∀I,L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 →
- L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2.
+lemma lprs_pair2: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
+ ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2.
/3 width=3 by lprs_pair, lprs_cprs_trans/ qed.
(* Properies on local environment slicing ***********************************)
-lemma lprs_ldrop_conf: dropable_sn lprs.
+lemma lprs_ldrop_conf: ∀G. dropable_sn (lprs G).
/3 width=3 by dropable_sn_TC, lpr_ldrop_conf/ qed-.
-lemma ldrop_lprs_trans: dedropable_sn lprs.
+lemma ldrop_lprs_trans: ∀G. dedropable_sn (lprs G).
/3 width=3 by dedropable_sn_TC, ldrop_lpr_trans/ qed-.
-lemma lprs_ldrop_trans_O1: dropable_dx lprs.
+lemma lprs_ldrop_trans_O1: ∀G. dropable_dx (lprs G).
/3 width=3 by dropable_dx_TC, lpr_ldrop_trans_O1/ qed-.
(* Advanced properties ******************************************************)
-lemma lprs_strip: confluent2 … lprs lpr.
+lemma lprs_strip: ∀G. confluent2 … (lprs G) (lpr G).
/3 width=3 by TC_strip1, lpr_conf/ qed-.
(* Main properties **********************************************************)
-theorem lprs_conf: confluent2 … lprs lprs.
+theorem lprs_conf: ∀G. confluent2 … (lprs G) (lprs G).
/3 width=3 by TC_confluent2, lpr_conf/ qed-.
-theorem lprs_trans: Transitive … lprs.
+theorem lprs_trans: ∀G. Transitive … (lprs G).
/2 width=3/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predsnstar_4.ma".
+include "basic_2/notation/relations/predsnstar_5.ma".
include "basic_2/reduction/lpx.ma".
include "basic_2/computation/lprs.ma".
(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-definition lpxs: ∀h. sd h → relation lenv ≝ λh,g. TC … (lpx h g).
+definition lpxs: ∀h. sd h → relation3 genv lenv lenv ≝
+ λh,g,G. TC … (lpx h g G).
interpretation "extended parallel computation (local environment, sn variant)"
- 'PRedSnStar h g L1 L2 = (lpxs h g L1 L2).
+ 'PRedSnStar h g G L1 L2 = (lpxs h g G L1 L2).
(* Basic eliminators ********************************************************)
-lemma lpxs_ind: ∀h,g,L1. ∀R:predicate lenv. R L1 →
- (∀L,L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → R L → R L2) →
- ∀L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → R L2.
-#h #g #L1 #R #HL1 #IHL1 #L2 #HL12
+lemma lpxs_ind: ∀h,g,G,L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → R L → R L2) →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L2.
+#h #g #G #L1 #R #HL1 #IHL1 #L2 #HL12
@(TC_star_ind … HL1 IHL1 … HL12) //
qed-.
-lemma lpxs_ind_dx: ∀h,g,L2. ∀R:predicate lenv. R L2 →
- (∀L1,L. ⦃h, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → R L → R L1) →
- ∀L1. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → R L1.
-#h #g #L2 #R #HL2 #IHL2 #L1 #HL12
+lemma lpxs_ind_dx: ∀h,g,G,L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → R L → R L1) →
+ ∀L1. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1.
+#h #g #G #L2 #R #HL2 #IHL2 #L1 #HL12
@(TC_star_ind_dx … HL2 IHL2 … HL12) //
qed-.
(* Basic properties *********************************************************)
-lemma lprs_lpxs: ∀h,g,L1,L2. L1 ⊢ ➡* L2 → ⦃h, L1⦄ ⊢ ➡*[h, g] L2.
+lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
/3 width=3/ qed.
-lemma lpx_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[h, g] L2 → ⦃h, L1⦄ ⊢ ➡*[h, g] L2.
+lemma lpx_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
/2 width=1/ qed.
-lemma lpxs_refl: ∀h,g,L. ⦃G, L⦄ ⊢ ➡*[h, g] L.
+lemma lpxs_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡*[h, g] L.
/2 width=1/ qed.
-lemma lpxs_strap1: ∀h,g,L1,L,L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → ⦃h, L1⦄ ⊢ ➡*[h, g] L2.
+lemma lpxs_strap1: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
/2 width=3/ qed.
-lemma lpxs_strap2: ∀h,g,L1,L,L2. ⦃h, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃h, L1⦄ ⊢ ➡*[h, g] L2.
+lemma lpxs_strap2: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
/2 width=3/ qed.
-lemma lpxs_pair_refl: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → ∀I,V. ⦃h, L1. ⓑ{I}V⦄ ⊢ ➡*[h, g] L2. ⓑ{I}V.
+lemma lpxs_pair_refl: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V.
/2 width=1 by TC_lpx_sn_pair_refl/ qed.
(* Basic inversion lemmas ***************************************************)
-lemma lpxs_inv_atom1: ∀h,g,L2. ⦃h, ⋆⦄ ⊢ ➡*[h, g] L2 → L2 = ⋆.
+lemma lpxs_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡*[h, g] L2 → L2 = ⋆.
/2 width=2 by TC_lpx_sn_inv_atom1/ qed-.
-lemma lpxs_inv_atom2: ∀h,g,L1. ⦃h, L1⦄ ⊢ ➡*[h, g] ⋆ → L1 = ⋆.
+lemma lpxs_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡*[h, g] ⋆ → L1 = ⋆.
/2 width=2 by TC_lpx_sn_inv_atom2/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma lpxs_fwd_length: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → |L1| = |L2|.
+lemma lpxs_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → |L1| = |L2|.
/2 width=2 by TC_lpx_sn_fwd_length/ qed-.
(* Properties about atomic arity assignment on terms ************************)
-lemma aaa_lpxs_conf: ∀h,g,L1,T,A.
- L1 ⊢ T ⁝ A → ∀L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → L2 ⊢ T ⁝ A.
-#h #g #L1 #T #A #HT #L2 #HL12
+lemma aaa_lpxs_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+#h #g #G #L1 #T #A #HT #L2 #HL12
@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/
qed-.
-lemma aaa_lprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A.
-#L1 #T #A #HT #L2 #HL12
+lemma aaa_lprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+#G #L1 #T #A #HT #L2 #HL12
@(aaa_lpxs_conf … HT) -A -T /2 width=3/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predsnstaralt_4.ma".
+include "basic_2/notation/relations/predsnstaralt_5.ma".
include "basic_2/computation/cpxs_cpxs.ma".
include "basic_2/computation/lpxs.ma".
(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
(* alternative definition *)
-definition lpxsa: ∀h. sd h → relation lenv ≝ λh,g. lpx_sn … (cpxs h g).
+definition lpxsa: ∀h. sd h → relation3 genv lenv lenv ≝
+ λh,g,G. lpx_sn … (cpxs h g G).
interpretation "extended parallel computation (local environment, sn variant) alternative"
- 'PRedSnStarAlt h g L1 L2 = (lpxsa h g L1 L2).
+ 'PRedSnStarAlt h g G L1 L2 = (lpxsa h g G L1 L2).
(* Main properties on the alternative definition ****************************)
-theorem lpxsa_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡➡*[h, g] L2 → ⦃h, L1⦄ ⊢ ➡*[h, g] L2.
+theorem lpxsa_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
(* Main inversion lemmas on the alternative definition **********************)
-theorem lpxs_inv_lpxsa: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → ⦃h, L1⦄ ⊢ ➡➡*[h, g] L2.
+theorem lpxs_inv_lpxsa: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2.
/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpx_cpxs_trans/ qed-.
(* Alternative eliminators **************************************************)
-lemma lpxs_ind_alt: ∀h,g. ∀R:relation lenv.
+lemma lpxs_ind_alt: ∀h,g,G. ∀R:relation lenv.
R (⋆) (⋆) → (
∀I,K1,K2,V1,V2.
- ⦃h, K1⦄ ⊢ ➡*[h, g] K2 → ⦃h, K1⦄ ⊢ V1 ➡*[h, g] V2 →
+ ⦃G, K1⦄ ⊢ ➡*[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 →
R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
) →
- ∀L1,L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → R L1 L2.
+ ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1 L2.
/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-.
(* Advanced properties ******************************************************)
-lemma lpxs_pair: ∀h,g,I,L1,L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → ∀V1,V2. ⦃h, L1⦄ ⊢ V1 ➡*[h, g] V2 →
- ⦃h, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
+lemma lpxs_pair: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡*[h, g] V2 →
+ ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
/2 width=1 by TC_lpx_sn_pair/ qed.
(* Advanced inversion lemmas ************************************************)
-lemma lpxs_inv_pair1: ∀h,g,I,K1,L2,V1. ⦃h, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2 →
- ∃∃K2,V2. ⦃h, K1⦄ ⊢ ➡*[h, g] K2 & ⦃h, K1⦄ ⊢ V1 ➡*[h, g] V2 & L2 = K2.ⓑ{I}V2.
+lemma lpxs_inv_pair1: ∀h,g,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L2 = K2.ⓑ{I}V2.
/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-.
-lemma lpxs_inv_pair2: ∀h,g,I,L1,K2,V2. ⦃h, L1⦄ ⊢ ➡*[h, g] K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⦃h, K1⦄ ⊢ ➡*[h, g] K2 & ⦃h, K1⦄ ⊢ V1 ➡*[h, g] V2 & L1 = K1.ⓑ{I}V1.
+lemma lpxs_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, g] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L1 = K1.ⓑ{I}V1.
/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-.
(* Properties on context-sensitive extended parallel computation for terms **)
-lemma lpxs_cpx_trans: ∀h,g. s_r_trans … (cpx h g) (lpxs h g).
+lemma lpxs_cpx_trans: ∀h,g,G. s_r_trans … (cpx h g G) (lpxs h g G).
/3 width=5 by s_r_trans_TC2, lpx_cpxs_trans/ qed-.
-lemma lpxs_cpxs_trans: ∀h,g. s_rs_trans … (cpx h g) (lpxs h g).
+lemma lpxs_cpxs_trans: ∀h,g,G. s_rs_trans … (cpx h g G) (lpxs h g G).
/3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ qed-.
-lemma cpxs_bind2: ∀h,g,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
- ∀I,T1,T2. ⦃h, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
+lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+#h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
lapply (lpxs_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
qed.
(* Inversion lemmas on context-sensitive ext parallel computation for terms *)
-lemma cpxs_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, g] U2 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃h, L.ⓛV1⦄ ⊢ T1 ➡*[h, g] T2 &
+lemma cpxs_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, g] U2 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[h, g] T2 &
U2 = ⓛ{a}V2.T2.
-#h #g #a #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5/
+#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5/
#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?) /2 width=1/ -HT02 #HT02
lapply (cpxs_trans … HT10 … HT02) -T0 /2 width=5/
qed-.
-lemma cpxs_inv_abbr1: ∀h,g,a,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, g] U2 → (
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃h, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 &
+lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, g] U2 → (
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 &
U2 = ⓓ{a}V2.T2
) ∨
- ∃∃T2. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
-#h #g #a #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/
+ ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
+#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/
#U0 #U2 #_ #HU02 * *
[ #V0 #T0 #HV10 #HT10 #H destruct
elim (cpx_inv_abbr1 … HU02) -HU02 *
(* More advanced properties *************************************************)
-lemma lpxs_pair2: ∀h,g,I,L1,L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 →
- ∀V1,V2. ⦃h, L2⦄ ⊢ V1 ➡*[h, g] V2 → ⦃h, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
+lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.
(* Properies on local environment slicing ***********************************)
-lemma lpxs_ldrop_conf: ∀h,g. dropable_sn (lpxs h g).
+lemma lpxs_ldrop_conf: ∀h,g,G. dropable_sn (lpxs h g G).
/3 width=3 by dropable_sn_TC, lpx_ldrop_conf/ qed-.
-lemma ldrop_lpxs_trans: ∀h,g. dedropable_sn (lpxs h g).
+lemma ldrop_lpxs_trans: ∀h,g,G. dedropable_sn (lpxs h g G).
/3 width=3 by dedropable_sn_TC, ldrop_lpx_trans/ qed-.
-lemma lpxs_ldrop_trans_O1: ∀h,g. dropable_dx (lpxs h g).
+lemma lpxs_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpxs h g G).
/3 width=3 by dropable_dx_TC, lpx_ldrop_trans_O1/ qed-.
(* Main properties **********************************************************)
-theorem lpxs_trans: ∀h,g. Transitive … (lpxs h g).
+theorem lpxs_trans: ∀h,g,G. Transitive … (lpxs h g G).
/2 width=3/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lrsubeq_3.ma".
+include "basic_2/notation/relations/lrsubeq_4.ma".
include "basic_2/static/aaa.ma".
include "basic_2/computation/acp_cr.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
-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_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)
+inductive lsubc (RP) (G): relation lenv ≝
+| lsubc_atom: lsubc RP G (⋆) (⋆)
+| lsubc_pair: ∀I,L1,L2,V. lsubc RP G L1 L2 → lsubc RP G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsubc_abbr: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A →
+ lsubc RP G L1 L2 → lsubc RP G (L1. ⓓⓝW.V) (L2.ⓛW)
.
interpretation
"local environment refinement (abstract candidates of reducibility)"
- 'LRSubEq RP L1 L2 = (lsubc RP L1 L2).
+ 'LRSubEq RP G L1 L2 = (lsubc RP G L1 L2).
(* Basic inversion lemmas ***************************************************)
-fact lsubc_inv_atom1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L1 = ⋆ → L2 = ⋆.
-#RP #L1 #L2 * -L1 -L2
+fact lsubc_inv_atom1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⊑[RP] L2 → L1 = ⋆ → L2 = ⋆.
+#RP #G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct
qed-.
(* Basic_1: was just: csubc_gen_sort_r *)
-lemma lsubc_inv_atom1: ∀RP,L2. ⋆ ⊑[RP] L2 → L2 = ⋆.
-/2 width=4 by lsubc_inv_atom1_aux/ qed-.
+lemma lsubc_inv_atom1: ∀RP,G,L2. G ⊢ ⋆ ⊑[RP] L2 → L2 = ⋆.
+/2 width=5 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,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
- K1 ⊑[RP] K2 &
+fact lsubc_inv_pair1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⊑[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+ (∃∃K2. G ⊢ K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+ G ⊢ K1 ⊑[RP] K2 &
L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
-#RP #L1 #L2 * -L1 -L2
+#RP #G #L1 #L2 * -L1 -L2
[ #I #K1 #V #H destruct
| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10/
qed-.
(* Basic_1: was: csubc_gen_head_r *)
-lemma lsubc_inv_pair1: ∀RP,I,K1,L2,X. K1.ⓑ{I}X ⊑[RP] L2 →
- (∃∃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 &
+lemma lsubc_inv_pair1: ∀RP,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⊑[RP] L2 →
+ (∃∃K2. G ⊢ K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+ G ⊢ K1 ⊑[RP] K2 &
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 = ⋆.
-#RP #L1 #L2 * -L1 -L2
+fact lsubc_inv_atom2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⊑[RP] L2 → L2 = ⋆ → L1 = ⋆.
+#RP #G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct
qed-.
(* Basic_1: was just: csubc_gen_sort_l *)
-lemma lsubc_inv_atom2: ∀RP,L1. L1 ⊑[RP] ⋆ → L1 = ⋆.
-/2 width=4 by lsubc_inv_atom2_aux/ qed-.
+lemma lsubc_inv_atom2: ∀RP,G,L1. G ⊢ L1 ⊑[RP] ⋆ → L1 = ⋆.
+/2 width=5 by lsubc_inv_atom2_aux/ qed-.
-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 &
+fact lsubc_inv_pair2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2.ⓑ{I} W →
+ (∃∃K1. G ⊢ K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨
+ ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+ G ⊢ K1 ⊑[RP] K2 &
L1 = K1.ⓓⓝW.V & I = Abst.
-#RP #L1 #L2 * -L1 -L2
+#RP #G #L1 #L2 * -L1 -L2
[ #I #K2 #W #H destruct
| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8/
qed-.
(* Basic_1: was just: csubc_gen_head_l *)
-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 &
+lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⊑[RP] K2.ⓑ{I} W →
+ (∃∃K1. G ⊢ K1 ⊑[RP] K2 & L1 = K1.ⓑ{I} W) ∨
+ ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+ G ⊢ K1 ⊑[RP] K2 &
L1 = K1.ⓓⓝW.V & I = Abst.
/2 width=3 by lsubc_inv_pair2_aux/ qed-.
(* Basic properties *********************************************************)
(* Basic_1: was just: csubc_refl *)
-lemma lsubc_refl: ∀RP,L. L ⊑[RP] L.
-#RP #L elim L -L // /2 width=1/
+lemma lsubc_refl: ∀RP,G,L. G ⊢ L ⊑[RP] L.
+#RP #G #L elim L -L // /2 width=1/
qed.
(* Basic_1: removed theorems 3:
(* Basic_1: was: csubc_drop_conf_O *)
(* Note: the constant 0 can not be generalized *)
-lemma lsubc_ldrop_O1_trans: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ⊑[RP] K2.
-#RP #L1 #L2 #H elim H -L1 -L2
+lemma lsubc_ldrop_O1_trans: ∀RP,G,L1,L2. G ⊢ L1 ⊑[RP] L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. ⇩[0, e] L1 ≡ K1 & G ⊢ K1 ⊑[RP] K2.
+#RP #G #L1 #L2 #H elim H -L1 -L2
[ #X #e #H elim (ldrop_inv_atom1 … H) -H /2 width=3/
| #I #L1 #L2 #V #_ #IHL12 #X #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #H destruct
(* Basic_1: was: csubc_drop_conf_rev *)
lemma ldrop_lsubc_trans: ∀RR,RS,RP.
- acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ⊑[RP] K2 →
- ∃∃L2. L1 ⊑[RP] L2 & ⇩[d, e] L2 ≡ K2.
-#RR #RS #RP #Hacp #Hacr #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+ acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+ ∀G,L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 →
+ ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩[d, e] L2 ≡ K2.
+#RR #RS #RP #Hacp #Hacr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
[ #d #X #H elim (lsubc_inv_atom1 … H) -H /2 width=3/
| #L1 #I #V1 #X #H
elim (lsubc_inv_pair1 … H) -H *
(* Basic_1: was: csubc_drop1_conf_rev *)
lemma ldrops_lsubc_trans: ∀RR,RS,RP.
- acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 ⊑[RP] K2 →
- ∃∃L2. L1 ⊑[RP] L2 & ⇩*[des] L2 ≡ K2.
-#RR #RS #RP #Hacp #Hacr #L1 #K1 #des #H elim H -L1 -K1 -des
+ acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+ ∀G,L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 →
+ ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩*[des] L2 ≡ K2.
+#RR #RS #RP #Hacp #Hacr #G #L1 #K1 #des #H elim H -L1 -K1 -des
[ /2 width=3/
| #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12
elim (ldrop_lsubc_trans … Hacp Hacr … HLK1 … HK12) -Hacp -Hacr -K1 #K #HLK #HK2
(* properties concerning lenv refinement for atomic arity assignment ********)
-lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L1,L2. L1 ⁝⊑ L2 → L1 ⊑[RP] L2.
-#RR #RS #RP #H1RP #H2RP #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+ ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → G ⊢ L1 ⊑[RP] L2.
+#RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4/
qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 g ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'DPRedStar $h $g $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 h , break term 46 g ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'DPRedStar $h $g $G $L $T1 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 L, break term 46 T ⦄ ϵ break [ term 46 R ] break 〚term 46 A 〛 )"
- non associative with precedence 45
- for @{ 'InEInt $R $L $T $A }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L, break term 46 T ⦄ ϵ break [ term 46 R ] break 〚term 46 A 〛 )"
+ non associative with precedence 45
+ for @{ 'InEInt $R $G $L $T $A }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( T1 ⊑ break [ term 46 R ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'LRSubEq $R $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( G ⊢ break term 46 L1 ⊑ break [ term 46 R ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LRSubEq $R $G $L1 $L2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃G, L⦄ ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'PEval $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PEval $G $L $T1 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 g ] break 𝐍 ⦃ term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'PEval $h $g $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 h , break term 46 g ] break 𝐍 ⦃ term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PEval $h $g $G $L $T1 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 ⊢ ➡* break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PRedSnStar $L1 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡* break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedSnStar $G $L1 $L2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 h, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 g ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PRedSnStar $h $g $L1 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedSnStar $h $g $G $L1 $L2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 ⊢ ➡ ➡ * break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PRedSnStarAlt $L1 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡ ➡ * break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedSnStarAlt $G $L1 $L2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 h, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 g ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PRedSnStarAlt $h $g $L1 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedSnStarAlt $h $g $G $L1 $L2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃G, L⦄ ⊢ break term 46 T1 ➡ * break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PRedStar $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , term 46 L ⦄ ⊢ break term 46 T1 ➡ * break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStar $G $L $T1 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 g ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PRedStar $h $g $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 h , break term 46 g ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStar $h $g $G $L $T1 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 g ] break term 46 T )"
- non associative with precedence 45
- for @{ 'SN $h $g $L $T }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 h , break term 46 g ] break term 46 T )"
+ non associative with precedence 45
+ for @{ 'SN $h $g $G $L $T }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ ⬊ * break [ term 46 g ] break term 46 T )"
- non associative with precedence 45
- for @{ 'SNAlt $h $g $L $T }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ ⬊ * break [ term 46 h , break term 46 g ] break term 46 T )"
+ non associative with precedence 45
+ for @{ 'SNAlt $h $g $G $L $T }.
class "cyan"
[ { "computation" * } {
[ { "context-sensitive extended evaluation" * } {
- [ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?] 𝐍⦃?⦄ )" * ]
+ [ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ]
}
]
[ { "context-sensitive evaluation" * } {
- [ "cpre ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
+ [ "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
}
]
[ { "strongly normalizing computation" * } {
- [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_tstc_vector" + "csn_aaa" * ]
- [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_lpx" * ]
+ [ "csn_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csn_tstc_vector" + "csn_aaa" * ]
+ [ "csn ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csn_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csn_lift" + "csn_lpx" * ]
}
]
[ { "decomposed extended computation" * } {
- [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_aaa" + "dxprs_dxprs" * ]
+ [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )" "dxprs_lift" + "dxprs_aaa" + "dxprs_dxprs" * ]
}
]
[ { "context-sensitive extended computation" * } {
- [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?] ? )" "lpxs_ldrop" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_aaa" + "cpxs_cpxs" * ]
+ [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_aaa" + "cpxs_cpxs" * ]
}
]
[ { "context-sensitive computation" * } {
- [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_cprs" + "lprs_lprs" * ]
- [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
+ [ "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_alt ( ⦃?,?⦄ ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_cprs" + "lprs_lprs" * ]
+ [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
}
]
[ { "local env. ref. for abstract candidates of reducibility" * } {
- [ "lsubc ( ? ⊑[?] ? )" "lsubc_ldrop" + "lsubc_ldrops" + "lsubc_lsuba" * ]
+ [ "lsubc ( ? â\8a¢ ? â\8a\91[?] ? )" "lsubc_ldrop" + "lsubc_ldrops" + "lsubc_lsuba" * ]
}
]
[ { "support for abstract computation properties" * } {
- [ "acp" "acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )" "acp_aaa" * ]
+ [ "acp" "acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "acp_aaa" * ]
}
]
}
projects / helm.git / commitdiff