From 2e97c767bc072f5ba238725ff1f738fc91a0135a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 10 Feb 2022 11:38:29 +0100 Subject: [PATCH] update in delayed_updating + relationship between grafted trees and updating clarified in the case of interest so far --- .../delayed_updating/reduction/dfr_ifr.ma | 8 +++- .../substitution/lift_preterm_eq.ma | 48 +++++++++---------- .../ground/lib/subset_equivalence.ma | 8 ++++ 3 files changed, 37 insertions(+), 27 deletions(-) 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 66affad94..839b4fdfa 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma @@ -16,7 +16,8 @@ include "delayed_updating/reduction/dfr.ma". include "delayed_updating/reduction/ifr.ma". include "delayed_updating/substitution/fsubst_lift.ma". include "delayed_updating/substitution/fsubst_eq.ma". -include "delayed_updating/substitution/lift_constructors.ma". +include "delayed_updating/substitution/lift_constructors.ma". +include "delayed_updating/substitution/lift_preterm_eq.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". @@ -40,6 +41,11 @@ lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 → [ lift_rmap_S_dx >structure_S_dx + @lift_grafted_sn // +| /2 width=1 by lift_grafted_S_dx/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma index cddb51e89..622ee0f55 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma @@ -56,3 +56,11 @@ theorem subset_eq_trans (A): #A #u1 #u2 * #H12 #H21 #u3 * #H23 #H32 /3 width=5 by subset_le_trans, conj/ qed-. + +theorem subset_eq_canc_sn (A): + left_cancellable … (subset_eq A). +/3 width=3 by subset_eq_trans, subset_eq_sym/ qed-. + +theorem subset_eq_canc_dx (A): + right_cancellable … (subset_eq A). +/3 width=3 by subset_eq_trans, subset_eq_sym/ qed-. -- 2.39.2