1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
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".
21 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
23 (* Example of unprotected balanced β-reduction ******************************)
25 definition l3_t: prototerm ≝
28 definition l3_i1: prototerm ≝
29 (@(⧣𝟏).@(𝛌.⧣𝟏).𝛌.𝛌.⧣𝟏).
31 definition l3_i2: prototerm ≝
32 (@(⧣𝟏).@(𝛌.⧣𝟏).𝛌.𝛌.⧣↑𝟐).
34 definition l3_d1: prototerm ≝
35 (@(⧣𝟏).@(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.⧣𝟏).
37 definition l3_d2: prototerm ≝
38 (@(⧣𝟏).@(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.𝛕𝟏.⧣𝟏).
41 l3_t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_i1.
43 @ibfr_eq_trans [| @ibfr_beta_0 // ]
46 @(subset_eq_canc_sn … (fsubst_empty_rc …))
47 @(subset_eq_canc_sn … (lift_term_abst …))
49 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
53 l3_i1 ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗𝐞] l3_i2.
54 @ibfr_eq_trans [| @ibfr_beta_1 // ]
59 @(subset_eq_canc_sn … (fsubst_empty_rc …))
60 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
64 l3_t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_d1.
66 @dbfr_eq_trans [| @dbfr_beta_0 // ]
69 @(subset_eq_canc_sn … (fsubst_empty_rc …)) //
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 …)) //
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 …)) //