matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.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 "delayed_updating/reduction/ibfr_constructors.ma".
  16 include "delayed_updating/substitution/lift_prototerm_constructors.ma".
  17 include "ground/arith/pnat_two.ma".
  18
  19 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
  20
  21 (* Prerequisites ************************************************************)
  22
  23 lemma list_rcons_prop_1 (A) (a1) (a2):
  24       ⓔ ⨭ a1 ⨭{A} a2 = a1 ⨮ (ⓔ ⨭ a2).
  25 // qed.
  26
  27 (* Example of unprotected balanced β-reduction ******************************)
  28
  29 definition l3_t0: prototerm ≝
  30            (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.⧣𝟏).
  31
  32 definition l3_t1: prototerm ≝
  33            (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.(𝛌.＠(⧣↑𝟐).⧣𝟏)).
  34
  35 definition l3_t2: prototerm ≝
  36            (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.(𝛌.＠(⧣↑𝟐).⧣↑𝟐)).
  37
  38 lemma l3_t01:
  39       l3_t0 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗔◗𝗟◗𝐞] l3_t1.
  40 @ibfr_abst_hd
  41 @ibfr_appl_hd
  42 @ibfr_eq_trans [| @ibfr_beta_0 // ]
  43 @appl_eq_repl [ // ]
  44 @abst_eq_repl
  45 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  46 @(subset_eq_canc_sn … (lift_term_abst …))
  47 @abst_eq_repl
  48 @(subset_eq_canc_sn … (lift_term_appl … ))
  49 @appl_eq_repl
  50 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
  51 qed.
  52
  53 lemma l3_t12:
  54       l3_t1 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗔◗𝗟◗𝗟◗𝗔◗𝐞] l3_t2.
  55 @ibfr_abst_hd
  56 @ibfr_eq_trans
  57 [| @(ibfr_beta_1 … (𝟎)) [| <list_rcons_prop_1 ]
  58    /2 width=3 by pcc_A_sn, in_comp_appl_hd/
  59 ]
  60 @appl_eq_repl [ // ]
  61 @appl_eq_repl [ // ]
  62 @abst_eq_repl
  63 @abst_eq_repl
  64 @(subset_eq_canc_sn … (fsubst_appl_hd …))
  65 @appl_eq_repl [ // ]
  66 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  67 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
  68 qed.