From 2815c74c03f38089d0e27aba00e2280223b0f76f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 28 Dec 2022 17:47:38 +0100 Subject: [PATCH] update in delayed_updating + some renaming --- .../delayed_updating/reduction/dbfr_ibfr.ma | 10 +++++----- .../delayed_updating/reduction/dbfr_unprotected_neg.ma | 2 +- .../delayed_updating/reduction/ibfr_unwind.ma | 8 ++++---- .../{unwind => unwind_k}/preunwind2_rmap.ma | 0 .../{unwind => unwind_k}/preunwind2_rmap_eq.ma | 2 +- .../{unwind => unwind_k}/preunwind2_rmap_lift.ma | 2 +- .../{unwind => unwind_k}/unwind2_path.ma | 2 +- .../{unwind => unwind_k}/unwind2_path_after.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_path_append.ma | 2 +- .../{unwind => unwind_k}/unwind2_path_eq.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_path_lift.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_preterm_eq.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_preterm_fsubst.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_prototerm.ma | 2 +- .../{unwind => unwind_k}/unwind2_prototerm_after.ma | 4 ++-- .../unwind2_prototerm_constructors.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_prototerm_eq.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_prototerm_inner.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_prototerm_lift.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_rmap.ma | 2 +- .../{unwind => unwind_k}/unwind2_rmap_after.ma | 2 +- .../{unwind => unwind_k}/unwind2_rmap_closed.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_rmap_crux.ma | 2 +- .../{unwind => unwind_k}/unwind2_rmap_depth.ma | 2 +- .../{unwind => unwind_k}/unwind2_rmap_eq.ma | 4 ++-- .../{unwind => unwind_k}/unwind2_rmap_lift.ma | 6 +++--- .../{unwind => unwind_k}/unwind2_rmap_structure.ma | 2 +- 27 files changed, 47 insertions(+), 47 deletions(-) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/preunwind2_rmap.ma (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/preunwind2_rmap_eq.ma (96%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/preunwind2_rmap_lift.ma (96%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_path.ma (99%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_path_after.ma (92%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_path_append.ma (99%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_path_eq.ma (92%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_path_lift.ma (94%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_preterm_eq.ma (96%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_preterm_fsubst.ma (97%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_prototerm.ma (96%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_prototerm_after.ma (91%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_prototerm_constructors.ma (95%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_prototerm_eq.ma (93%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_prototerm_inner.ma (92%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_prototerm_lift.ma (93%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_rmap.ma (98%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_rmap_after.ma (97%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_rmap_closed.ma (97%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_rmap_crux.ma (97%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_rmap_depth.ma (97%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_rmap_eq.ma (93%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_rmap_lift.ma (91%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind => unwind_k}/unwind2_rmap_structure.ma (96%) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma index 387dc8f15..48b6d1dfd 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma @@ -15,11 +15,11 @@ include "delayed_updating/reduction/dbfr.ma". include "delayed_updating/reduction/ibfr.ma". -include "delayed_updating/unwind/unwind2_prototerm_constructors.ma". -include "delayed_updating/unwind/unwind2_preterm_fsubst.ma". -include "delayed_updating/unwind/unwind2_preterm_eq.ma". -include "delayed_updating/unwind/unwind2_prototerm_lift.ma". -include "delayed_updating/unwind/unwind2_rmap_crux.ma". +include "delayed_updating/unwind_k/unwind2_prototerm_constructors.ma". +include "delayed_updating/unwind_k/unwind2_preterm_fsubst.ma". +include "delayed_updating/unwind_k/unwind2_preterm_eq.ma". +include "delayed_updating/unwind_k/unwind2_prototerm_lift.ma". +include "delayed_updating/unwind_k/unwind2_rmap_crux.ma". include "delayed_updating/substitution/fsubst_eq.ma". include "delayed_updating/substitution/lift_prototerm_eq.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_neg.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_neg.ma index a83a71d5f..ed87aa714 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_neg.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_neg.ma @@ -14,7 +14,7 @@ include "delayed_updating/reduction/dbfr_constructors.ma". include "delayed_updating/reduction/ibfr_constructors.ma". -include "delayed_updating/unwind/unwind2_prototerm_constructors.ma". +include "delayed_updating/unwind_k/unwind2_prototerm_constructors.ma". include "delayed_updating/substitution/lift_prototerm_constructors.ma". include "ground/arith/pnat_two.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma index 34feec243..56cfaa6ca 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma @@ -14,10 +14,10 @@ include "delayed_updating/reduction/ibfr.ma". -include "delayed_updating/unwind/unwind2_preterm_fsubst.ma". -include "delayed_updating/unwind/unwind2_preterm_eq.ma". -include "delayed_updating/unwind/unwind2_prototerm_lift.ma". -include "delayed_updating/unwind/unwind2_rmap_crux.ma". +include "delayed_updating/unwind_k/unwind2_preterm_fsubst.ma". +include "delayed_updating/unwind_k/unwind2_preterm_eq.ma". +include "delayed_updating/unwind_k/unwind2_prototerm_lift.ma". +include "delayed_updating/unwind_k/unwind2_rmap_crux.ma". include "delayed_updating/substitution/fsubst_eq.ma". include "delayed_updating/substitution/lift_prototerm_eq.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_eq.ma similarity index 96% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_eq.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_eq.ma index 32efd9f04..6c85da3d1 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_eq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/preunwind2_rmap.ma". +include "delayed_updating/unwind_k/preunwind2_rmap.ma". include "ground/relocation/tr_compose_eq.ma". include "ground/relocation/tr_pn_eq.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_lift.ma similarity index 96% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_lift.ma index cc5b351ad..ff3e3c8aa 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/preunwind2_rmap.ma". +include "delayed_updating/unwind_k/preunwind2_rmap.ma". include "delayed_updating/substitution/prelift_label.ma". include "delayed_updating/substitution/prelift_rmap.ma". include "ground/relocation/tr_uni_compose.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path.ma index 08115e1e4..85bc220d9 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_rmap.ma". +include "delayed_updating/unwind_k/unwind2_rmap.ma". include "delayed_updating/syntax/path_structure.ma". include "delayed_updating/notation/functions/black_downtriangle_2.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_after.ma similarity index 92% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_after.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_after.ma index c7a3bcf0f..955f4b1c8 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_after.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_after.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_path_eq.ma". -include "delayed_updating/unwind/unwind2_rmap_after.ma". +include "delayed_updating/unwind_k/unwind2_path_eq.ma". +include "delayed_updating/unwind_k/unwind2_rmap_after.ma". (* TAILED UNWIND FOR PATH ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_append.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_append.ma index 8796ce86f..cdff0a580 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_append.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_path.ma". +include "delayed_updating/unwind_k/unwind2_path.ma". include "delayed_updating/syntax/path_inner.ma". include "delayed_updating/syntax/path_proper.ma". include "ground/xoa/ex_4_2.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_eq.ma similarity index 92% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_eq.ma index c1b188b60..fb44a3fba 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_eq.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_path.ma". -include "delayed_updating/unwind/unwind2_rmap_eq.ma". +include "delayed_updating/unwind_k/unwind2_path.ma". +include "delayed_updating/unwind_k/unwind2_rmap_eq.ma". (* TAILED UNWIND FOR PATH ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_lift.ma similarity index 94% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_lift.ma index 140dd6f8a..abd752471 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_path.ma". -include "delayed_updating/unwind/unwind2_rmap_lift.ma". +include "delayed_updating/unwind_k/unwind2_path.ma". +include "delayed_updating/unwind_k/unwind2_rmap_lift.ma". include "delayed_updating/substitution/lift_path_structure.ma". (* TAILED UNWIND FOR PATH ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_eq.ma similarity index 96% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_eq.ma index a78d4b9ed..8264293d1 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_eq.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_prototerm.ma". -include "delayed_updating/unwind/unwind2_path_append.ma". +include "delayed_updating/unwind_k/unwind2_prototerm.ma". +include "delayed_updating/unwind_k/unwind2_path_append.ma". include "delayed_updating/syntax/preterm.ma". include "delayed_updating/syntax/path_structure_inner.ma". include "ground/lib/subset_equivalence.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_fsubst.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_fsubst.ma index ecf0eaf0f..708ac32a2 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_fsubst.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_prototerm_eq.ma". -include "delayed_updating/unwind/unwind2_path_append.ma". +include "delayed_updating/unwind_k/unwind2_prototerm_eq.ma". +include "delayed_updating/unwind_k/unwind2_path_append.ma". include "delayed_updating/substitution/fsubst.ma". include "delayed_updating/syntax/preterm.ma". include "delayed_updating/syntax/prototerm_proper.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm.ma similarity index 96% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm.ma index e4e480c66..9a21490c4 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_path.ma". +include "delayed_updating/unwind_k/unwind2_path.ma". include "delayed_updating/syntax/prototerm.ma". include "ground/lib/subset_ext.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_after.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_after.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_after.ma index 9e7dd82f2..0edc58e1f 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_after.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_after.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_prototerm_eq.ma". -include "delayed_updating/unwind/unwind2_path_after.ma". +include "delayed_updating/unwind_k/unwind2_prototerm_eq.ma". +include "delayed_updating/unwind_k/unwind2_path_after.ma". (* TAILED UNWIND FOR PROTOTERM **********************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_constructors.ma similarity index 95% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_constructors.ma index 6e3c96fe7..7a6d0ef06 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_constructors.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_prototerm_eq.ma". -include "delayed_updating/unwind/unwind2_path_append.ma". +include "delayed_updating/unwind_k/unwind2_prototerm_eq.ma". +include "delayed_updating/unwind_k/unwind2_path_append.ma". include "delayed_updating/syntax/prototerm_constructors.ma". (* TAILED UNWIND FOR PROTOTERM **********************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_eq.ma similarity index 93% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_eq.ma index 24e3c7086..46e539e4e 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_eq.ma @@ -14,8 +14,8 @@ (**) (* reverse include *) include "ground/lib/subset_ext_equivalence.ma". -include "delayed_updating/unwind/unwind2_path_eq.ma". -include "delayed_updating/unwind/unwind2_prototerm.ma". +include "delayed_updating/unwind_k/unwind2_path_eq.ma". +include "delayed_updating/unwind_k/unwind2_prototerm.ma". (* TAILED UNWIND FOR PROTOTERM **********************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_inner.ma similarity index 92% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_inner.ma index 6ad293f09..1831a18f2 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_inner.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_prototerm.ma". -include "delayed_updating/unwind/unwind2_path_append.ma". +include "delayed_updating/unwind_k/unwind2_prototerm.ma". +include "delayed_updating/unwind_k/unwind2_path_append.ma". include "ground/lib/subset_overlap.ma". (* TAILED UNWIND FOR PROTOTERM **********************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_lift.ma similarity index 93% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_lift.ma index 251d7ba72..e37e7f71b 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_lift.ma @@ -15,8 +15,8 @@ (**) (* reverse include *) include "ground/lib/subset_ext_equivalence.ma". include "delayed_updating/substitution/lift_prototerm.ma". -include "delayed_updating/unwind/unwind2_path_lift.ma". -include "delayed_updating/unwind/unwind2_prototerm.ma". +include "delayed_updating/unwind_k/unwind2_path_lift.ma". +include "delayed_updating/unwind_k/unwind2_prototerm.ma". (* TAILED UNWIND FOR PROTOTERM **********************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap.ma similarity index 98% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap.ma index 5177fd7ee..22a9c6f18 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/preunwind2_rmap.ma". +include "delayed_updating/unwind_k/preunwind2_rmap.ma". include "delayed_updating/syntax/path.ma". (* TAILED UNWIND FOR RELOCATION MAP *****************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_after.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_after.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_after.ma index 7fda762da..b33afdf76 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_after.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_after.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_rmap.ma". +include "delayed_updating/unwind_k/unwind2_rmap.ma". include "delayed_updating/syntax/path_structure.ma". include "ground/relocation/tr_compose_compose.ma". include "ground/relocation/tr_compose_pn.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_closed.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_closed.ma index f38a72ac9..3d357e0c7 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_closed.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_rmap_lift.ma". -include "delayed_updating/unwind/unwind2_rmap_eq.ma". +include "delayed_updating/unwind_k/unwind2_rmap_lift.ma". +include "delayed_updating/unwind_k/unwind2_rmap_eq.ma". include "delayed_updating/substitution/lift_rmap_structure.ma". include "delayed_updating/syntax/path_closed.ma". include "delayed_updating/syntax/path_depth.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_crux.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_crux.ma index a5127cc45..2f5b3c8b6 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_crux.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_rmap_closed.ma". +include "delayed_updating/unwind_k/unwind2_rmap_closed.ma". (* TAILED UNWIND FOR RELOCATION MAP *****************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_depth.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_depth.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_depth.ma index cb806673d..6aa48f280 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_depth.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_depth.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_path_append.ma". +include "delayed_updating/unwind_k/unwind2_path_append.ma". include "delayed_updating/syntax/path_depth.ma". include "ground/relocation/tr_id_compose.ma". include "ground/relocation/tr_compose_compose.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_eq.ma similarity index 93% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_eq.ma index b93aabf0f..374a2312a 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_eq.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_rmap.ma". -include "delayed_updating/unwind/preunwind2_rmap_eq.ma". +include "delayed_updating/unwind_k/unwind2_rmap.ma". +include "delayed_updating/unwind_k/preunwind2_rmap_eq.ma". include "ground/relocation/tr_uni_compose.ma". include "ground/arith/nat_rplus_pplus.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_lift.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_lift.ma index b42274ef8..1d3d54458 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_lift.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_rmap.ma". -include "delayed_updating/unwind/preunwind2_rmap_lift.ma". -include "delayed_updating/unwind/preunwind2_rmap_eq.ma". +include "delayed_updating/unwind_k/unwind2_rmap.ma". +include "delayed_updating/unwind_k/preunwind2_rmap_lift.ma". +include "delayed_updating/unwind_k/preunwind2_rmap_eq.ma". include "delayed_updating/substitution/lift_path.ma". include "delayed_updating/syntax/path_structure.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_structure.ma similarity index 96% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_structure.ma index 0d949e3b5..c11158af5 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_structure.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_rmap.ma". +include "delayed_updating/unwind_k/unwind2_rmap.ma". include "delayed_updating/syntax/path_structure.ma". include "delayed_updating/syntax/path_depth.ma". include "ground/relocation/tr_pushs.ma". -- 2.39.2