matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_unprotected.etc

   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/dbfr_constructors.ma".
  16 include "delayed_updating/reduction/ibfr_constructors.ma".
  17 include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
  18 include "delayed_updating/substitution/lift_prototerm_constructors.ma".
  19 include "ground/arith/pnat_two.ma".
  20
  21 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
  22
  23 (* Example of unprotected balanced β-reduction ******************************)
  24
  25 definition l3_t: prototerm ≝
  26            (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.⧣𝟏).
  27
  28 definition l3_i1: prototerm ≝
  29            (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣𝟏).
  30
  31 definition l3_i2: prototerm ≝
  32            (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣↑𝟐).
  33
  34 definition l3_d1: prototerm ≝
  35            (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.⧣𝟏).
  36
  37 definition l3_d2: prototerm ≝
  38            (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.𝛕𝟏.⧣𝟏).
  39
  40 lemma l3_ti1:
  41       l3_t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_i1.
  42 @ibfr_appl_hd
  43 @ibfr_eq_trans [| @ibfr_beta_0 // ]
  44 @appl_eq_repl [ // ]
  45 @abst_eq_repl
  46 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  47 @(subset_eq_canc_sn … (lift_term_abst …))
  48 @abst_eq_repl
  49 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
  50 qed.
  51
  52 lemma l3_i12:
  53       l3_i1 ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗𝐞] l3_i2.
  54 @ibfr_eq_trans [| @ibfr_beta_1 // ]
  55 @appl_eq_repl [ // ]
  56 @appl_eq_repl [ // ]
  57 @abst_eq_repl
  58 @abst_eq_repl
  59 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  60 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
  61 qed.
  62
  63 lemma l3_td1:
  64       l3_t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_d1.
  65 @dbfr_appl_hd
  66 @dbfr_eq_trans [| @dbfr_beta_0 // ]
  67 @appl_eq_repl [ // ]
  68 @abst_eq_repl
  69 @(subset_eq_canc_sn … (fsubst_empty_rc …)) //
  70 qed.
  71
  72 lemma ld_di2:
  73       l3_i2 ⇔ ▼[𝐢]l3_d2.
  74 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
  75 [ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) // ]
  76 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
  77 [ @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
  78   @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
  79 ]
  80 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
  81 @(subset_eq_canc_sn … (unwind2_term_iref …))
  82 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
  83 @(subset_eq_canc_sn … (unwind2_term_iref …))
  84 @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
  85 qed.