From: Ferruccio Guidi Date: Mon, 28 Mar 2022 23:11:32 +0000 (+0200) Subject: WIP in delayed_updating X-Git-Tag: make_still_working~78 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aeec9312d6f72526a460518a1e889eac71657cdd;p=helm.git WIP in delayed_updating + we re focusing on a special case of the main theorem --- 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 ϵ 𝐓 →