matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basic_2/reducibility/cpr_cpr.ma".
  16 include "basic_2/computation/csn.ma".
  17
  18 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
  19
  20 (* Advanced forvard lemmas **************************************************)
  21
  22 fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬊* V.
  23 #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
  24 @csn_intro #V2 #HLV2 #HV2
  25 @(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/
  26 qed.
  27
  28 (* Basic_1: was: sn3_gen_head *)
  29 lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬊* ②{I} V. T → L ⊢ ⬊* V.
  30 /2 width=5/ qed.
  31
  32 fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬊* U →
  33                           ∀a,I,V,T. U = ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T.
  34 #L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct
  35 @csn_intro #T2 #HLT2 #HT2
  36 @(IH (ⓑ{a,I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
  37 qed.
  38
  39 (* Basic_1: was: sn3_gen_bind *)
  40 lemma csn_fwd_bind_dx: ∀a,I,L,V,T. L ⊢ ⬊* ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T.
  41 /2 width=4/ qed.