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 f95126621d5c55d1fbf6c0011595e810bde01dc5..15767cf59cc43743b6c105e8d0dd31464553b051 100644 (file)
--- 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 (file)
index 0000000..73397b8
--- /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 dbe1a242db04e9edeb31eff54e3784ccad632c5d..64e50fc912645c9f3d6bac7803d4e8e9cc1850c7 100644 (file)
--- 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 6890031062b55e008868119ea09cb6021a5f172e..3dca53142fb3a3e6fabc1d31a0fd34f1795831d1 100644 (file)
--- 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 4f8c282b16a113c8aabb93a36cb986964075cb3f..746def17755b3f147022f07cb5773bb27121cbc5 100644 (file)
--- 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 0293e8666246edbb81fc0e9dc9e9c9f57eb7ab73..b1ed7662361b232de071f08b4972c6fe1cb3247d 100644 (file)
--- 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 4577a65b69ea451d9719d30152e3ca4865136a12..d18f72b52d1c152285d8643c05b3a7eac40d93e2 100644 (file)
--- 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 d9f371823579474ec24bba792624aceb4388e81c..0101b8d9361671cef4edcdb00f89c8fa34d70c05 100644 (file)
--- 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 e76c4943b704ce2729085a27fe150c8decb87448..efeaf86b40fb7087219bef1d55b705fd4c0c8ce0 100644 (file)
--- 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 6ba6e937b48778b995bae2d16e1ca16f326ce13f..8c60eea7595c8a88c43250865500b11010701dee 100644 (file)
--- 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 003b8d1ce8ed74e479393a001c15145d578fb3cc..852fa0a59f204028bec097b7d212fbb0c51e8568 100644 (file)
--- 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 d8528aae253cbee5ad729ea7b092726630a4b9e1..cc2953e4dd28cfcf8766f7c6387485afd489374c 100644 (file)
--- 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"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; "ⓡ"; ] ;