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_k/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 un_t: prototerm ≝
26 @(𝛌.⧣𝟏).𝛌.𝛌.@(⧣𝟐).𝛌.@(⧣𝟐).⧣𝟏.
28 definition un_i1: prototerm ≝
29 @(𝛌.⧣𝟏).𝛌.𝛌.@(𝛌.⧣𝟏).𝛌.@(⧣𝟐).⧣𝟏.
32 un_t ➡𝐢𝐛𝐟[𝗔◗𝗟◗𝗟◗𝗦◗𝐞] un_i1.
33 @(ibfr_eq_trans … (ibfr_beta_0 …))
34 [ >list_append_lcons_sn
35 /3 width=1 by in_comp_appl_sd, in_comp_abst_hd/
36 | /3 width=3 by pcc_S_sn, pcc_L_sn/
39 @appl_eq_repl [ // ] @abst_eq_repl
40 @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
41 @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
42 @(subset_eq_canc_sn … (fsubst_empty_rc …))
43 @(subset_eq_canc_sn … (lift_term_abst …)) @abst_eq_repl
44 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
47 definition un_i2: prototerm ≝
48 @(𝛌.⧣𝟏).𝛌.𝛌.@(𝛌.⧣𝟏).𝛌.@(⧣𝟐).𝛌.⧣𝟏.
51 un_i1 ➡𝐢𝐛𝐟[𝗔◗𝗟◗𝗟◗𝗔◗𝗟◗𝗔◗𝐞] un_i2.
55 @(ibfr_eq_trans … (ibfr_beta_0 …))
56 [ >list_append_lcons_sn
57 /2 width=1 by in_comp_appl_hd/
58 | /2 width=1 by pcc_A_sn, pcc_empty/
61 @appl_eq_repl [ // ] @abst_eq_repl
62 @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
63 @(subset_eq_canc_sn … (fsubst_empty_rc …))
64 @(subset_eq_canc_sn … (lift_term_abst …)) @abst_eq_repl
65 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
68 definition un_i3: prototerm ≝
69 @(𝛌.⧣𝟏).𝛌.𝛌.@(𝛌.⧣𝟏).𝛌.@(⧣𝟐).𝛌.⧣↑𝟐.
72 un_i2 ➡𝐢𝐛𝐟[𝗔◗𝗟◗𝗟◗𝗔◗𝗟◗𝗔◗𝗟◗𝐞] un_i3.
78 @(ibfr_eq_trans … (ibfr_beta_0 …))
80 @appl_eq_repl [ // ] @abst_eq_repl
81 @(subset_eq_canc_sn … (fsubst_empty_rc …))
82 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
85 definition un_d1: prototerm ≝
86 @(𝛌.⧣𝟏).𝛌.𝛌.@(𝛕𝟐.𝛌.⧣𝟏).𝛌.@(⧣𝟐).⧣𝟏.
89 un_t ➡𝐝𝐛𝐟[𝗔◗𝗟◗𝗟◗𝗦◗𝐞] un_d1.
90 @(dbfr_eq_trans … (dbfr_beta_0 …))
91 [ >list_append_lcons_sn
92 /3 width=1 by in_comp_appl_sd, in_comp_abst_hd/
93 | /3 width=3 by pcc_S_sn, pcc_L_sn/
96 @appl_eq_repl [ // ] @abst_eq_repl
97 @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
98 @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
99 @(subset_eq_canc_sn … (fsubst_empty_rc …))
103 definition un_d2: prototerm ≝
104 @(𝛌.⧣𝟏).𝛌.𝛌.@(𝛕𝟐.𝛌.⧣𝟏).𝛌.@(⧣𝟐).𝛕𝟏.𝛕𝟐.𝛌.⧣𝟏.
107 un_d1 ➡𝐝𝐛𝐟[𝗔◗𝗟◗𝗟◗𝗔◗𝗟◗𝗔◗𝐞] un_d2.
111 @(dbfr_eq_trans … (dbfr_beta_0 …))
112 [ >list_append_lcons_sn /2 width=1 by in_comp_appl_hd/
113 | /2 width=1 by pcc_A_sn/
116 @appl_eq_repl [ // ] @abst_eq_repl
117 @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
118 @(subset_eq_canc_sn … (fsubst_empty_rc …))
119 @iref_eq_repl @iref_eq_repl //
122 definition un_d3: prototerm ≝
123 @(𝛌.⧣𝟏).𝛌.𝛌.@(𝛕𝟐.𝛌.⧣𝟏).𝛌.@(⧣𝟐).𝛌.𝛕𝟏.⧣𝟐.
127 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
128 [ @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
129 @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
131 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
132 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
133 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
134 [ @(subset_eq_canc_sn … (unwind2_term_iref …))
135 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
136 @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
138 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
139 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
140 [ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
142 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
143 @(subset_eq_canc_sn … (unwind2_term_iref …))
144 @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //