--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "delayed_updating/reduction/ibfr.ma".
+include "delayed_updating/substitution/fsubst_constructors.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
+include "delayed_updating/syntax/prototerm_constructors_eq.ma".
+
+(* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma ibfr_abst_hd (t1) (t2) (r):
+ t1 ā”š¢šš[r] t2 ā š.t1 ā”š¢šš[šār] š.t2.
+#t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro ā¦ (šāp) ā¦ Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_abst_hd/
+| @(subset_eq_trans ā¦ (abst_eq_repl ā¦ Ht2)) -Ht1 -Ht2
+ @(subset_eq_canc_sn ā¦ (fsubst_abst_hd ā¦)) @abst_eq_repl
+ @fsubst_eq_repl // @lift_term_eq_repl_dx
+ >list_cons_shift @(subset_eq_canc_sn ā¦ (grafted_abst_hd ā¦ )) //
+]
+qed.
+
+lemma ibfr_appl_hd (v) (t1) (t2) (r):
+ t1 ā”š¢šš[r] t2 ā ļ¼ v.t1 ā”š¢šš[šār] ļ¼ v.t2.
+#v #t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro ā¦ (šāp) ā¦ Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_appl_hd/
+| @(subset_eq_trans ā¦ (appl_eq_repl ā¦ Ht2)) -Ht1 -Ht2 [|*: // ]
+ @(subset_eq_canc_sn ā¦ (fsubst_appl_hd ā¦)) @appl_eq_repl [ // ]
+ @fsubst_eq_repl // @lift_term_eq_repl_dx
+ >list_cons_shift @(subset_eq_canc_sn ā¦ (grafted_appl_hd ā¦ )) //
+]
+qed.
+
+lemma ibfr_appl_sd (v1) (v2) (t) (r):
+ v1 ā”š¢šš[r] v2 ā ļ¼ v1.t ā”š¢šš[š¦ār] ļ¼ v2.t.
+#v1 #v2 #t #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
+@(ex6_5_intro ā¦ (š¦āp) ā¦ Hb Hm Hn) -Hb -Hm -Hn
+[ -Hv2 //
+| -Hv2 /2 width=1 by in_comp_appl_sd/
+| @(subset_eq_trans ????? (appl_eq_repl ā¦)) [3: @Hv2 |2,4: // |5: skip ]
+ @(subset_eq_canc_sn ā¦ (fsubst_appl_sd ā¦)) @appl_eq_repl [| // ]
+ @fsubst_eq_repl // @lift_term_eq_repl_dx
+ >list_cons_shift @(subset_eq_canc_sn ā¦ (grafted_appl_sd ā¦ )) //
+]
+qed.
+
+lemma ibfr_beta_0 (v) (t) (q) (n):
+ q Ļµ šāØā»,nā© ā qāš±ān Ļµ t ā
+ ļ¼ v.š.t ā”š¢šš[šāšāq] ļ¼ v.š.(t[āqāš ”[š®āØānā©]v]).
+#v #t #q #n #Hn #Ht
+@(ex6_5_intro ā¦ (š) (š) q (š) ā¦ Hn) -Hn //
+[ /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn ā¦ (fsubst_appl_hd ā¦)) @appl_eq_repl [ // ]
+ @(subset_eq_canc_sn ā¦ (fsubst_abst_hd ā¦)) @abst_eq_repl
+ @fsubst_eq_repl // <nplus_zero_sn @lift_term_eq_repl_dx
+ >list_cons_comm @(subset_eq_canc_sn ā¦ (grafted_appl_sd ā¦ ))
+ @(subset_eq_canc_sn ā¦ (grafted_empty_dx ā¦ )) //
+]
+qed.