From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 10 Jan 2022 11:55:35 +0000 (+0100)
Subject: update in delayed updating
X-Git-Tag: make_still_working~112
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f83215ca9b8d0019c85a991ec90c6c658c0aaff8

update in delayed updating

+ notation for "proper element"
+ bug fixed ub the notation of predicates
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma
index f95126621..15767cf59 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( 𝗱❨ break term 46 a ❩ )"
+notation "hvbox( 𝗱 break term 70 a )"
   non associative with precedence 70
   for @{ 'NodeLabelD $a }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_p_tail_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_p_tail_1.ma
new file mode 100644
index 000000000..73397b8d9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_p_tail_1.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( Ꝕ term 70 x )"
+  non associative with precedence 45
+  for @{ 'PredicatePTail $x }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma
index dbe1a242d..64e50fc91 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( ⊓ term 46 p )"
+notation "hvbox( ⊓ term 70 p )"
   non associative with precedence 45
   for @{ 'PredicateSquareCap $p }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 689003106..3dca53142 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -22,8 +22,8 @@ include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
 
 inductive dfr (p) (q) (t): predicate preterm ≝
 | dfr_beta (b):
-  let r ≝ p●𝗔◗b●𝗟◗q◖𝗱❨↑❘q❘❩ in
-  r ϵ t → ⊓⊗b → dfr p q t (t[⋔r←t⋔(p◖𝗦)])
+  let r ≝ p●𝗔◗b●𝗟◗q◖𝗱(↑❘q❘) in
+  r ϵ t → ⊓(⊗b) → dfr p q t (t[⋔r←t⋔(p◖𝗦)])
 .
 
 interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index 4f8c282b1..746def177 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -24,7 +24,7 @@ include "delayed_updating/notation/relations/black_rightarrow_f_4.ma".
 inductive ifr (p) (q) (t): predicate preterm ≝
 | ifr_beta (b):
   let r ≝ p●𝗔◗b●𝗟◗q in
-  r◖𝗱❨↑❘q❘❩ ϵ t → ⊓⊗b → ifr p q t (t[⋔r←↑[𝐮❨↑❘q❘❩]t⋔(p◖𝗦)])
+  r◖𝗱(↑❘q❘) ϵ t → ⊓(⊗b) → ifr p q t (t[⋔r←↑[𝐮❨↑❘q❘❩]t⋔(p◖𝗦)])
 .
 
 interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index 0293e8666..b1ed76623 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -31,7 +31,7 @@ match p with
   match l with
   [ label_node_d n ⇒
     match q with
-    [ list_empty     ⇒ lift_gen (A) (λp. k (𝗱❨f@❨n❩❩◗p)) q (f∘𝐮❨n❩)
+    [ list_empty     ⇒ lift_gen (A) (λp. k (𝗱(f@❨n❩)◗p)) q (f∘𝐮❨n❩)
     | list_lcons _ _ ⇒ lift_gen (A) k q (f∘𝐮❨n❩)
     ]
   | label_edge_L   ⇒ lift_gen (A) (λp. k (𝗟◗p)) q (⫯f)
@@ -63,11 +63,11 @@ lemma lift_empty (A) (k) (f):
 // qed.
 
 lemma lift_d_empty_sn (A) (k) (n) (f):
-      ↑❨(λp. k (𝗱❨f@❨n❩❩◗p)), 𝐞, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱❨n❩◗𝐞, f❩.
+      ↑❨(λp. k (𝗱(f@❨n❩)◗p)), 𝐞, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱n◗𝐞, f❩.
 // qed.
 
 lemma lift_d_lcons_sn (A) (k) (p) (l) (n) (f):
-      ↑❨k, l◗p, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱❨n❩◗l◗p, f❩.
+      ↑❨k, l◗p, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱n◗l◗p, f❩.
 // qed.
 
 lemma lift_L_sn (A) (k) (p) (f):
@@ -85,17 +85,17 @@ lemma lift_S_sn (A) (k) (p) (f):
 (* Basic constructions with proj_path ***************************************)
 
 lemma lift_path_d_empty_sn (f) (n):
-      𝗱❨f@❨n❩❩◗𝐞 = ↑[f](𝗱❨n❩◗𝐞).
+      𝗱(f@❨n❩)◗𝐞 = ↑[f](𝗱n◗𝐞).
 // qed.
 
 lemma lift_path_d_lcons_sn (f) (p) (l) (n):
-      ↑[f∘𝐮❨ninj n❩](l◗p) = ↑[f](𝗱❨n❩◗l◗p).
+      ↑[f∘𝐮❨ninj n❩](l◗p) = ↑[f](𝗱n◗l◗p).
 // qed.
 
 (* Basic constructions with proj_rmap ***************************************)
 
 lemma lift_rmap_d_sn (f) (p) (n):
-      ↑[p](f∘𝐮❨ninj n❩) = ↑[𝗱❨n❩◗p]f.
+      ↑[p](f∘𝐮❨ninj n❩) = ↑[𝗱n◗p]f.
 #f * // qed.
 
 lemma lift_rmap_L_sn (f) (p):
@@ -124,8 +124,8 @@ qed.
 
 lemma path_ind_lift (Q:predicate …):
       Q (𝐞) →
-      (∀n. Q (𝐞) → Q (𝗱❨n❩◗𝐞)) →
-      (∀n,l,p. Q (l◗p) → Q (𝗱❨n❩◗l◗p)) →
+      (∀n. Q (𝐞) → Q (𝗱n◗𝐞)) →
+      (∀n,l,p. Q (l◗p) → Q (𝗱n◗l◗p)) →
       (∀p. Q p → Q (𝗟◗p)) →
       (∀p. Q p → Q (𝗔◗p)) →
       (∀p. Q p → Q (𝗦◗p)) →
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
index 4577a65b6..d18f72b52 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
@@ -20,7 +20,7 @@ include "delayed_updating/substitution/lift_eq.ma".
 (* Constructions with structure ********************************************)
 
 lemma lift_d_empty_dx (n) (p) (f):
-      (⊗p)◖𝗱❨(↑[p]f)@❨n❩❩ = ↑[f](p◖𝗱❨n❩).
+      (⊗p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
 #n #p @(path_ind_lift … p) -p // [ #m #l #p |*: #p ] #IH #f
 [ <lift_rmap_d_sn <lift_path_d_lcons_sn //
 | <lift_rmap_L_sn <lift_path_L_sn <IH //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
index d9f371823..0101b8d93 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
@@ -39,8 +39,8 @@ interpretation
 
 lemma bdd_inv_in_comp_gen:
       ∀t,p. t ϵ 𝐃𝛗 → p ϵ t →
-      ∨∨ ∃∃n. #n ⇔ t & 𝗱❨n❩◗𝐞 = p
-       | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱❨n❩◗q = p
+      ∨∨ ∃∃n. #n ⇔ t & 𝗱n◗𝐞 = p
+       | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱n◗q = p
        | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p
        | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p
        | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t & 𝗦◗q = p
@@ -62,7 +62,7 @@ lemma bdd_inv_in_comp_gen:
 qed-.
 
 lemma bdd_inv_in_comp_d:
-      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩◗q ϵ t →
+      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ t →
       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
        | ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t
 .
@@ -77,7 +77,7 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_root_d:
-      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩◗q ϵ ▵t →
+      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ ▵t →
       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
        | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛗n.u ⇔ t
 .
@@ -165,7 +165,7 @@ qed-.
 (* Advanced inversions ******************************************************)
 
 lemma bbd_mono_in_root_d:
-      ∀l,n,p,t. t ϵ 𝐃𝛗 → p◖𝗱❨n❩ ϵ ▵t → p◖l ϵ ▵t → 𝗱❨n❩ = l.
+      ∀l,n,p,t. t ϵ 𝐃𝛗 → p◖𝗱n ϵ ▵t → p◖l ϵ ▵t → 𝗱n = l.
 #l #n #p elim p -p
 [ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
   elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
index e76c4943b..efeaf86b4 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -39,7 +39,7 @@ interpretation
 lemma depth_empty: 𝟎 = ❘𝐞❘.
 // qed.
 
-lemma depth_d (q) (n): ❘q❘ = ❘𝗱❨n❩◗q❘.
+lemma depth_d (q) (n): ❘q❘ = ❘𝗱n◗q❘.
 // qed.
 
 lemma depth_L (q): ↑❘q❘ = ❘𝗟◗q❘.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
index 6ba6e937b..8c60eea75 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -40,7 +40,7 @@ lemma structure_empty:
 // qed.
 
 lemma structure_d_sn (p) (n):
-      ⊗p = ⊗(𝗱❨n❩◗p).
+      ⊗p = ⊗(𝗱n◗p).
 // qed.
 
 lemma structure_L_sn (p):
@@ -71,7 +71,7 @@ qed.
 (* Constructions with list_rcons ********************************************)
 
 lemma structure_d_dx (p) (n):
-      ⊗p = ⊗(p◖𝗱❨n❩).
+      ⊗p = ⊗(p◖𝗱n).
 #p #n <structure_append //
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
index 003b8d1ce..852fa0a59 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
@@ -51,7 +51,7 @@ interpretation
 
 lemma preterm_in_root_inv_lcons_oref:
       ∀p,l,n. l◗p ϵ ▵#n →
-      ∧∧ 𝗱❨n❩ = l & 𝐞 = p.
+      ∧∧ 𝗱n = l & 𝐞 = p.
 #p #l #n * #q
 <list_append_lcons_sn #H0 destruct -H0
 elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
@@ -60,7 +60,7 @@ qed-.
 
 lemma preterm_in_root_inv_lcons_iref:
       ∀t,p,l,n. l◗p ϵ ▵𝛗n.t →
-      ∧∧ 𝗱❨n❩ = l & p ϵ ▵t.
+      ∧∧ 𝗱n = l & p ϵ ▵t.
 #t #p #l #n * #q
 <list_append_lcons_sn * #r #Hr #H0 destruct
 /3 width=2 by ex_intro, conj/
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index d8528aae2..cc2953e4d 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1565,7 +1565,7 @@ let predefined_classes = [
  ["o"; "θ"; "ϑ"; "𝕠"; "∘";  "⊚"; "ø"; "○"; "●"; "◖"; "◗"; "𝐨"; "𝛉"; "ⓞ"; ] ;
  ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ;
  ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ;
- ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; "𝒫"; ] ;
+ ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; "𝒫"; "Ꝕ"; ] ;
  ["q"; "𝕢"; "𝐪"; "ⓠ"; ] ;
  ["Q"; "ℚ"; "𝐐"; "Ⓠ"; ] ;
  ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; "ⓡ"; ] ;