From 9b4e20442ec5a4028cfe2b6fe836c94acdb033b8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 17 May 2022 21:09:39 +0200 Subject: [PATCH] update in delayed_updating + generic unwind meeds to be even more generic --- .../delayed_updating/unwind/unwind_gen.ma | 4 ++-- .../delayed_updating/unwind/unwind_gen_after.ma | 3 ++- .../delayed_updating/unwind/unwind_gen_eq.ma | 12 ++++++++---- .../delayed_updating/unwind/unwind_gen_structure.ma | 4 ++-- 4 files changed, 14 insertions(+), 9 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma index 4c592528e..bff50807d 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma @@ -25,7 +25,7 @@ match p with match l with [ label_d n ⇒ match q with - [ list_empty ⇒ 𝗱(f@❨n❩)◗(unwind_gen f q) + [ list_empty ⇒ 𝗱((f n)@❨n❩)◗(unwind_gen f q) | list_lcons _ _ ⇒ unwind_gen f q ] | label_m ⇒ unwind_gen f q @@ -46,7 +46,7 @@ lemma unwind_gen_empty (f): // qed. lemma unwind_gen_d_empty (f) (n): - 𝗱(f@❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞). + 𝗱((f n)@❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞). // qed. lemma unwind_gen_d_lcons (f) (p) (l) (n): diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma index 2954be831..9d4955ff9 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma @@ -20,6 +20,7 @@ include "ground/relocation/tr_compose_pap.ma". (* Properties with tr_compose ***********************************************) lemma unwind_gen_after (f2) (f1) (p): - ◆[f2]◆[f1]p = ◆[f2∘f1]p. + ◆[f2]◆[f1]p = ◆[λn.(f2 ((f1 n)@❨n❩))∘(f1 n)]p. #f2 #f1 #p @(path_ind_unwind … p) -p // +#n #_