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 (* Example of unprotected balanced β-reduction ******************************)
  22
  23 definition l3_t0: prototerm ≝
  24            (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.⧣𝟏).
  25
  26 definition l3_t1: prototerm ≝
  27            (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.(𝛌.＠(⧣↑𝟐).⧣𝟏)).
  28
  29 lemma l3_t01:
  30       l3_t0 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗔◗𝗟◗𝐞] l3_t1.
  31 @ibfr_abst_hd
  32 @ibfr_appl_hd
  33 @ibfr_eq_trans [| @ibfr_beta_0 // ]
  34 @appl_eq_repl [ // ]
  35 @abst_eq_repl
  36 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  37 @(subset_eq_canc_sn … (lift_term_abst …))
  38 @abst_eq_repl
  39 @(subset_eq_canc_sn … (lift_term_appl … ))
  40 @appl_eq_repl
  41 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
  42 qed.