From 8d8863982ca95225551e9659ed431db046c34e81 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 23 Jan 2022 23:01:15 +0100 Subject: [PATCH] update un delayed_updating + bugs fixed in dfr and ifr --- .../lambdadelta/delayed_updating/reduction/dfr.ma | 2 +- .../lambdadelta/delayed_updating/reduction/dfr_ifr.ma | 10 +++++----- .../lambdadelta/delayed_updating/reduction/ifr.ma | 2 +- .../lambdadelta/delayed_updating/substitution/lift.ma | 4 ++++ 4 files changed, 11 insertions(+), 7 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma index 67c22257b..3cdf0d47e 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma @@ -28,7 +28,7 @@ include "ground/xoa/and_4.ma". definition dfr (p) (q): relation2 prototerm prototerm ≝ λt1,t2. ∃∃b,n. let r ≝ p●𝗔◗b●𝗟◗q in - ∧∧ ⊗b ϵ 𝐁 & ❘q❘ = (↑[q]𝐢)@❨n❩ & r◖𝗱n ϵ t1 & + ∧∧ ⊗b ϵ 𝐁 & ∀f. ❘q❘ = (↑[q]⫯f)@❨n❩ & r◖𝗱n ϵ t1 & t1[⋔r←𝛗n.(t1⋔(p◖𝗦))] ⇔ t2 . diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma index fb39e209a..a8d9469dd 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma @@ -18,8 +18,7 @@ include "delayed_updating/substitution/fsubst_lift.ma". include "delayed_updating/substitution/lift_structure_depth.ma". include "delayed_updating/syntax/prototerm_proper_constructors.ma". include "delayed_updating/syntax/path_structure_depth.ma". -include "ground/relocation/tr_id_pap.ma". -include "ground/relocation/tr_id_pushs.ma". +include "ground/relocation/tr_pap_pushs.ma". (* DELAYED FOCUSED REDUCTION ************************************************) @@ -29,9 +28,10 @@ lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 → * #b #n * #Hb #Hn #Ht1 #Ht2 @(ex1_2_intro … (⊗b) (❘⊗q❘)) @and4_intro [ // -| // -| lapply (in_comp_lift_bi f … Ht1) -Ht1 -H0t1 -Hb -Ht2 #Ht1 - tr_pushs_swap