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.ma".
16 include "delayed_updating/substitution/fsubst_constructors.ma".
17 include "delayed_updating/substitution/fsubst_eq.ma".
18 include "delayed_updating/syntax/prototerm_constructors_eq.ma".
20 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
22 (* Constructions with constructors for prototerm ****************************)
24 lemma dbfr_abst_hd (t1) (t2) (r):
25 t1 ā”ššš[r] t2 ā š.t1 ā”ššš[šār] š.t2.
27 #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
28 @(ex6_5_intro ā¦ (šāp) ā¦ Hb Hm Hn) -Hb -Hm -Hn
30 | -Ht2 /2 width=1 by in_comp_abst_hd/
31 | @(subset_eq_trans ā¦ (abst_eq_repl ā¦ Ht2)) -Ht1 -Ht2
32 @(subset_eq_canc_sn ā¦ (fsubst_abst_hd ā¦)) @abst_eq_repl
33 @fsubst_eq_repl // @iref_eq_repl
34 >list_cons_shift @(subset_eq_canc_sn ā¦ (grafted_abst_hd ā¦ )) //
38 lemma dbfr_appl_hd (v) (t1) (t2) (r):
39 t1 ā”ššš[r] t2 ā ļ¼ v.t1 ā”ššš[šār] ļ¼ v.t2.
41 #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
42 @(ex6_5_intro ā¦ (šāp) ā¦ Hb Hm Hn) -Hb -Hm -Hn
44 | -Ht2 /2 width=1 by in_comp_appl_hd/
45 | @(subset_eq_trans ā¦ (appl_eq_repl ā¦ Ht2)) -Ht1 -Ht2 [|*: // ]
46 @(subset_eq_canc_sn ā¦ (fsubst_appl_hd ā¦)) @appl_eq_repl [ // ]
47 @fsubst_eq_repl // @iref_eq_repl
48 >list_cons_shift @(subset_eq_canc_sn ā¦ (grafted_appl_hd ā¦ )) //
52 lemma dbfr_appl_sd (v1) (v2) (t) (r):
53 v1 ā”ššš[r] v2 ā ļ¼ v1.t ā”ššš[š¦ār] ļ¼ v2.t.
55 #p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
56 @(ex6_5_intro ā¦ (š¦āp) ā¦ Hb Hm Hn) -Hb -Hm -Hn
58 | -Hv2 /2 width=1 by in_comp_appl_sd/
59 | @(subset_eq_trans ????? (appl_eq_repl ā¦)) [3: @Hv2 |2,4: // |5: skip ]
60 @(subset_eq_canc_sn ā¦ (fsubst_appl_sd ā¦)) @appl_eq_repl [| // ]
61 @fsubst_eq_repl // @iref_eq_repl
62 >list_cons_shift @(subset_eq_canc_sn ā¦ (grafted_appl_sd ā¦ )) //
66 lemma dbfr_beta_0 (v) (t) (q) (n):
67 q Ļµ šāØā»,nā© ā qāš±ān Ļµ t ā
68 ļ¼ v.š.t ā”ššš[šāšāq] ļ¼ v.š.(t[āqāšān.v]).
70 @(ex6_5_intro ā¦ (š) (š) q (š) ā¦ Hn) -Hn
74 | /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
75 | @(subset_eq_canc_sn ā¦ (fsubst_appl_hd ā¦)) @appl_eq_repl [ // ]
76 @(subset_eq_canc_sn ā¦ (fsubst_abst_hd ā¦)) @abst_eq_repl
77 @fsubst_eq_repl // <nplus_zero_sn @iref_eq_repl
78 >list_cons_comm @(subset_eq_canc_sn ā¦ (grafted_appl_sd ā¦ ))
79 @(subset_eq_canc_sn ā¦ (grafted_empty_dx ā¦ )) //
83 lemma dbfr_beta_1 (v) (v1) (t) (q) (n):
84 q Ļµ šāØā»,nā© ā qāš±ān Ļµ t ā
85 ļ¼ v.ļ¼ v1.š.š.t ā”ššš[šāšāšāšāq] ļ¼ v.ļ¼ v1.š.š.(t[āqāšāān.v]).
86 #v #v1 #t #q #n #Hn #Ht
87 @(ex6_5_intro ā¦ (š) (šāšāš) q (š) ā¦ Hn) -Hn
89 | /2 width=1 by pbc_empty, pbc_redex/
90 | /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
91 | /5 width=1 by in_comp_appl_hd, in_comp_abst_hd/
92 | @(subset_eq_canc_sn ā¦ (fsubst_appl_hd ā¦)) @appl_eq_repl [ // ]
93 @(subset_eq_canc_sn ā¦ (fsubst_appl_hd ā¦)) @appl_eq_repl [ // ]
94 @(subset_eq_canc_sn ā¦ (fsubst_abst_hd ā¦)) @abst_eq_repl
95 @(subset_eq_canc_sn ā¦ (fsubst_abst_hd ā¦)) @abst_eq_repl
96 @fsubst_eq_repl // <nplus_unit_sn @lift_term_eq_repl_dx
97 >list_cons_comm @(subset_eq_canc_sn ā¦ (grafted_appl_sd ā¦ ))
98 @(subset_eq_canc_sn ā¦ (grafted_empty_dx ā¦ )) //