From aeec9312d6f72526a460518a1e889eac71657cdd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi <ferruccio.guidi@unibo.it> Date: Tue, 29 Mar 2022 01:11:32 +0200 Subject: [PATCH] WIP in delayed_updating + we re focusing on a special case of the main theorem --- .../contribs/lambdadelta/delayed_updating/reduction/dfr.ma | 2 +- .../lambdadelta/delayed_updating/reduction/dfr_ifr.ma | 6 ++++++ .../contribs/lambdadelta/delayed_updating/reduction/ifr.ma | 2 +- 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma index 3c328fcb2..576df6ec6 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â = (â¼[r]ð¢)@â¨nâ© & râð±n ϵ t1 & + â§â§ (âb ϵ ð ⧠ð = âbâ) & ââqâ = (â¼[r]ð¢)@â¨nâ© & râð±n ϵ t1 & t1[ârâð(n+âbâ).(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 77e303f05..dd24f8568 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma @@ -20,6 +20,7 @@ include "delayed_updating/unwind1/unwind_preterm_eq.ma". include "delayed_updating/unwind1/unwind_structure_depth.ma". include "delayed_updating/unwind1/unwind_depth.ma". include "delayed_updating/substitution/fsubst_eq.ma". +include "delayed_updating/substitution/lift_prototerm_eq.ma". include "delayed_updating/syntax/prototerm_proper_constructors.ma". include "delayed_updating/syntax/path_structure_depth.ma". include "ground/relocation/tr_uni_compose.ma". @@ -83,6 +84,11 @@ lemma dfr_unwind_id_bi (p) (q) (t1) (t2): t1 ϵ ð â <depth_append <depth_L_sn <depth_structure <depth_structure @fsubst_eq_repl [ // ] @(subset_eq_trans ⦠(unwind_iref â¦)) + + elim Hb -Hb #Hb #H0 <H0 -H0 <nrplus_zero_dx <nplus_zero_dx <Hn + @(subset_eq_canc_sn ⦠(lift_term_eq_repl_dx â¦)) + [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ] + (* @(subset_eq_canc_sn ⦠(unwind_term_eq_repl_dx â¦)) [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ] diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma index 54ad4f2f6..8d0cfc52d 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma @@ -28,7 +28,7 @@ include "ground/xoa/and_4.ma". definition ifr (p) (q): relation2 prototerm prototerm â λt1,t2. ââb,n. let r â pâðâbâðâq in - â§â§ âb ϵ ð & ââqâ = (â¼[r]ð¢)@â¨nâ© & râð±n ϵ t1 & + â§â§ (âb ϵ ð ⧠ð = âbâ) & ââqâ = (â¼[r]ð¢)@â¨nâ© & râð±n ϵ t1 & t1[ârââ[ð®â¨âbâðâqââ©](t1â(pâð¦))] â t2 . -- 2.39.2