include "basic_2/computation/cprs_cprs.ma".
include "basic_2/computation/csn_lift.ma".
include "basic_2/computation/csn_cpr.ma".
include "basic_2/computation/cprs_cprs.ma".
include "basic_2/computation/csn_lift.ma".
include "basic_2/computation/csn_cpr.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* Advanced properties ******************************************************)
lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬇* T → L2 ⊢ ⬇* T.
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* Advanced properties ******************************************************)
lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬇* T → L2 ⊢ ⬇* T.
@csn_intro #T0 #HLT0 #HT0
@IHT /2 width=2/ -IHT -HT0 /2 width=3/
qed.
lemma csn_abbr: ∀L,V. L ⊢ ⬇* V → ∀T. L. ⓓV ⊢ ⬇* T → L ⊢ ⬇* ⓓV. T.
@csn_intro #T0 #HLT0 #HT0
@IHT /2 width=2/ -IHT -HT0 /2 width=3/
qed.
lemma csn_abbr: ∀L,V. L ⊢ ⬇* V → ∀T. L. ⓓV ⊢ ⬇* T → L ⊢ ⬇* ⓓV. T.
fact csn_appl_beta_aux: ∀L,W. L ⊢ ⬇* W → ∀U. L ⊢ ⬇* U →
∀V,T. U = ⓓV. T → L ⊢ ⬇* ⓐV. ⓛW. T.
fact csn_appl_beta_aux: ∀L,W. L ⊢ ⬇* W → ∀U. L ⊢ ⬇* U →
∀V,T. U = ⓓV. T → L ⊢ ⬇* ⓐV. ⓛW. T.
fact csn_appl_theta_aux: ∀L,U. L ⊢ ⬇* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
∀V,T. U = ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T.
fact csn_appl_theta_aux: ∀L,U. L ⊢ ⬇* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
∀V,T. U = ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T.
(* Basic_1: was only: sn3_appl_appl *)
lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1.
L ⊢ ⬇* T1 →
(* Basic_1: was only: sn3_appl_appl *)
lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1.
L ⊢ ⬇* T1 →
#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 (cpr_inv_appl1_simple … HL ?) -HL //
#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 (cpr_inv_appl1_simple … HL ?) -HL //