update in delayed_updating

+ terms are defined modulo logical equivalence

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma
new file mode 100644 (file)
index 0000000..2e2651d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.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( 𝐃𝛗 )"
+  non associative with precedence 75
+  for @{ 'ClassDPhi }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_1.ma
new file mode 100644 (file)
index 0000000..09ceac1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_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 75 t )"
+  non associative with precedence 75
+  for @{ 'UpTriangle $t }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_1.ma
deleted file mode 100644 (file)
index 7942fed..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_1.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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( t ϵ break 𝐃𝛗 )"
-  non associative with precedence 45
-  for @{ 'InPredicateDPhi $t }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_2.ma
deleted file mode 100644 (file)
index 1c4f842..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_2.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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( p ϵ▵ break term 46 t )"
-  non associative with precedence 45
-  for @{ 'UpArrowEpsilon $p $t }.

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 e7d140231dacc30c35f06002fe935b9618b81ff4..26fb80e561757d7ba359140d507c971467d8be38 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
@@ -17,44 +17,54 @@ include "ground/xoa/ex_3_1.ma".
 include "ground/xoa/ex_4_2.ma".
 include "ground/xoa/ex_4_3.ma".
 include "ground/xoa/ex_5_3.ma".
+include "delayed_updating/syntax/preterm_equivalence.ma".
 include "delayed_updating/syntax/preterm_constructors.ma".
-include "delayed_updating/notation/relations/in_predicate_d_phi_1.ma".
+include "delayed_updating/notation/functions/class_d_phi_0.ma".
 
 (* BY-DEPTH DELAYED (BDD) TERM **********************************************)
 
-inductive bdd: predicate preterm ≝
+inductive bdd: 𝒫❨preterm❩ ≝
 | bdd_oref: ∀n. bdd #n
 | bdd_iref: ∀t,n. bdd t → bdd 𝛗n.t
 | bdd_abst: ∀t. bdd t → bdd 𝛌.t
 | bdd_appl: ∀u,t. bdd u → bdd t → bdd @u.t
+| bdd_conv: ∀t1,t2. t1 ⇔ t2 → bdd t1 → bdd t2
 .
 
 interpretation
-  "well-formed by-depth delayed (preterm)"
-  'InPredicateDPhi t = (bdd t).
+  "by-depth delayed (preterm)"
+  'ClassDPhi = (bdd).
 
 (* Basic inversions *********************************************************)
 
 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
-       | ∃∃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
+      ∀t,p. t ϵ 𝐃𝛗 → p ϵ t →
+      ∨∨ ∃∃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
 .
-#t #p *
+#t #p #H elim H -H
 [ #n * /3 width=3 by or5_intro0, ex2_intro/
-| #u #n #Hu * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
-| #u #Hu * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
-| #v #u #Hv #Hu * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
+| #u #n #Hu #_ * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
+| #u #Hu #_ * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
+| #v #u #Hv #Hu #_ #_ * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
+| #t1 #t2 #Ht12 #_ #IH #Ht2
+  elim IH -IH [6: /2 width=3 by subset_in_eq_repl_fwd/ ] *
+  [ /4 width=3 by subset_eq_trans, or5_intro0, ex2_intro/
+  | /4 width=7 by subset_eq_trans, ex4_3_intro, or5_intro1/
+  | /4 width=6 by subset_eq_trans, or5_intro2, ex4_2_intro/
+  | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro3/
+  | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro4/
+  ]
 ]
 qed-.
 
 lemma bdd_inv_in_comp_d:
-      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ⬦ t →
-      ∨∨ ∧∧ #n = t & 𝐞 = q
-       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛗n.u = t
+      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ t →
+      ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
+       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t
 .
 #t #q #n #Ht #Hq
 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
@@ -67,9 +77,9 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_root_d:
-      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ▵ t →
-      ∨∨ ∧∧ #n = t & 𝐞 = q
-       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ▵ u & 𝛗n.u = t
+      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ ▵t →
+      ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
+       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛗n.u ⇔ t
 .
 #t #q #n #Ht * #r #Hq
 elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq *
@@ -82,8 +92,8 @@ elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_comp_L:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ⬦ t →
-      ∃∃u. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛌.u = t
+      ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ t →
+      ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t
 .
 #t #q #Ht #Hq
 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
@@ -96,8 +106,8 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_root_L:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ▵ t →
-      ∃∃u. u ϵ 𝐃𝛗 & q ϵ▵ u & 𝛌.u = t.
+      ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ ▵t →
+      ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛌.u ⇔ t.
 #t #q #Ht * #r #Hq
 elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq
 #u #Hu #Hq #H0 destruct
@@ -105,8 +115,8 @@ elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq
 qed-.
 
 lemma bdd_inv_in_comp_A:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ⬦ t →
-      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ⬦ u & @v.u = t
+      ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ t →
+      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t
 .
 #t #q #Ht #Hq
 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
@@ -119,8 +129,8 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_root_A:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ▵ t →
-      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ▵ u & @v.u = t
+      ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ ▵t →
+      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵u & @v.u ⇔ t
 .
 #t #q #Ht * #r #Hq
 elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq
@@ -129,8 +139,8 @@ elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq
 qed-.
 
 lemma bdd_inv_in_comp_S:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ⬦ t →
-      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ⬦ v & @v.u = t
+      ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ t →
+      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t
 .
 #t #q #Ht #Hq
 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
@@ -143,8 +153,8 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_root_S:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ▵ t →
-      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ▵ v & @v.u = t
+      ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ ▵t →
+      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵v & @v.u ⇔ t
 .
 #t #q #Ht * #r #Hq
 elim (bdd_inv_in_comp_S … Ht Hq) -Ht -Hq
@@ -155,13 +165,17 @@ 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 *
-  [ #H0 #_ destruct
+  [ #H0 #_
+    lapply (preterm_root_eq_repl … H0) -H0 #H0
+    lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
     elim (preterm_in_root_inv_lcons_oref … Hl) -Hl //
-  | #u #_ #_ #H0 destruct
+  | #u #_ #_ #H0
+    lapply (preterm_root_eq_repl … H0) -H0 #H0
+    lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
     elim (preterm_in_root_inv_lcons_iref … Hl) -Hl //
   ]
 | * [ #m ] #p #IH #t #Ht
@@ -169,20 +183,28 @@ lemma bbd_mono_in_root_d:
   [ elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
     [ #_ #H0
       elim (eq_inv_list_empty_rcons ??? H0)
-    | #u #Hu #Hp #H0 destruct
+    | #u #Hu #Hp #H0
+      lapply (preterm_root_eq_repl … H0) -H0 #H0
+      lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
       elim (preterm_in_root_inv_lcons_iref … Hl) -Hl #_ #Hl
       /2 width=4 by/
     ]
   | elim (bdd_inv_in_root_L … Ht Hn) -Ht -Hn
-    #u #Hu #Hp #H0 destruct
+    #u #Hu #Hp #H0
+    lapply (preterm_root_eq_repl … H0) -H0 #H0
+    lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl  
     elim (preterm_in_root_inv_lcons_abst … Hl) -Hl #_ #Hl
     /2 width=4 by/
   | elim (bdd_inv_in_root_A … Ht Hn) -Ht -Hn
-    #v #u #_ #Hu #Hp #H0 destruct
+    #v #u #_ #Hu #Hp #H0
+    lapply (preterm_root_eq_repl … H0) -H0 #H0
+    lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
     elim (preterm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
     /2 width=4 by/
   | elim (bdd_inv_in_root_S … Ht Hn) -Ht -Hn
-    #v #u #Hv #_ #Hp #H0 destruct
+    #v #u #Hv #_ #Hp #H0
+    lapply (preterm_root_eq_repl … H0) -H0 #H0
+    lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
     elim (preterm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
     /2 width=4 by/
   ]

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
index 1da2d0174a8ddc1f188b5dadbc9131620bfc4968..44d923d9bb742b2b8b49fc247031c9e8c40916d4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
@@ -12,31 +12,25 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/lib/subset.ma".
 include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma".
-include "delayed_updating/notation/relations/up_arrow_epsilon_2.ma".
+include "delayed_updating/notation/functions/uptriangle_1.ma".
 
 (* PRETERM ******************************************************************)
 
-definition preterm: Type[0] ≝ predicate path.
+(* Note: preterms are subsets of complete paths *)
+definition preterm: Type[0] ≝ 𝒫❨path❩.
 
-definition preterm_in_comp: relation2 path preterm ≝
-           λp,t. t p.
+definition preterm_root: preterm → preterm ≝
+           λt,p. ∃q. p;;q ϵ t.
 
 interpretation
-  "belongs to complete (preterm)"
-  'UpDownArrowEpsilon p t = (preterm_in_comp p t).
-
-definition preterm_in_root: relation2 path preterm ≝
-           λp,t. ∃q. p;;q ϵ⬦ t.
-
-interpretation
-  "belongs to root (preterm)"
-  'UpArrowEpsilon p t = (preterm_in_root p t).
+  "root (preterm)"
+  'UpTriangle t = (preterm_root t).
 
 (* Basic constructions ******************************************************)
 
 lemma preterm_in_comp_root (p) (t):
-      p ϵ⬦ t → p ϵ▵ t.
+      p ϵ t → p ϵ ▵t.
 /2 width=2 by ex_intro/
 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 03394c5bf6349fe99c6ab14b648259bea5fe8334..0cd0158c05e16f3016b4af5e1f24c4f2a8f0d363 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
@@ -24,12 +24,12 @@ definition preterm_node_0 (l): preterm ≝
            λp. l;𝐞 = p.
 
 definition preterm_node_1 (l): preterm → preterm ≝
-           λt,p. ∃∃q. q ϵ⬦ t & l;q = p.
+           λt,p. ∃∃q. q ϵ t & l;q = p.
 
 definition preterm_node_2 (l1) (l2): preterm → preterm → preterm ≝
            λt1,t2,p.
-           ∨∨ ∃∃q. q ϵ⬦ t1 & l1;q = p
-            | ∃∃q. q ϵ⬦ t2 & l2;q = p.
+           ∨∨ ∃∃q. q ϵ t1 & l1;q = p
+            | ∃∃q. q ϵ t2 & l2;q = p.
 
 interpretation
   "outer variable reference by depth (preterm)"
@@ -50,7 +50,7 @@ interpretation
 (* Basic Inversions *********************************************************)
 
 lemma preterm_in_root_inv_lcons_oref:
-      ∀p,l,n. l;p ϵ▵ #n →
+      ∀p,l,n. l;p ϵ ▵#n →
       ∧∧ 𝗱❨n❩ = l & 𝐞 = p.
 #p #l #n * #q
 <list_append_lcons_sn #H0 destruct -H0
@@ -59,25 +59,25 @@ elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
 qed-.
 
 lemma preterm_in_root_inv_lcons_iref:
-      ∀t,p,l,n. l;p ϵ▵ 𝛗n.t →
-      ∧∧ 𝗱❨n❩ = l & p ϵ▵ t.
+      ∀t,p,l,n. l;p ϵ ▵𝛗n.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/
 qed-.
 
 lemma preterm_in_root_inv_lcons_abst:
-      ∀t,p,l. l;p ϵ▵ 𝛌.t →
-      ∧∧ 𝗟 = l & p ϵ▵ t.
+      ∀t,p,l. l;p ϵ ▵𝛌.t →
+      ∧∧ 𝗟 = l & p ϵ ▵t.
 #t #p #l * #q
 <list_append_lcons_sn * #r #Hr #H0 destruct
 /3 width=2 by ex_intro, conj/
 qed-.
 
 lemma preterm_in_root_inv_lcons_appl:
-      ∀u,t,p,l. l;p ϵ▵ @u.t →
-      ∨∨ ∧∧ 𝗦 = l & p ϵ▵ u
-       | ∧∧ 𝗔 = l & p ϵ▵ t.
+      ∀u,t,p,l. l;p ϵ ▵@u.t →
+      ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
+       | ∧∧ 𝗔 = l & p ϵ ▵t.
 #u #t #p #l * #q
 <list_append_lcons_sn * * #r #Hr #H0 destruct
 /4 width=2 by ex_intro, or_introl, or_intror, conj/

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma
index 67aa029d70af910f5833f87c9dba5dec5658d18f..60c5a4a41f7bdf191bc194a4a7460607c0ea8efb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma
@@ -12,9 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "delayed_updating/syntax/path_dephi.ma".
 include "delayed_updating/syntax/preterm_constructors.ma".
 
 (* DEPHI FOR PRETERM ********************************************************)
 
-definition preterm_dephi (f) (t) ≝
-           λp. ∃∃q. q ϵ⬦ t & p = path_dephi f q. 
+definition preterm_dephi (f) (t): preterm ≝
+           λp. ∃∃q. q ϵ t & p = path_dephi f q. 

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_equivalence.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_equivalence.ma
new file mode 100644 (file)
index 0000000..6f788a7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_equivalence.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground/lib/subset_equivalence.ma".
+include "delayed_updating/syntax/preterm.ma".
+
+(* EQUIVALENCE FOR PRETERM **************************************************)
+
+(* Constructions with preterm_root ******************************************)
+
+lemma preterm_root_incl_repl:
+      ∀t1,t2. t1 ⊆ t2 → ▵t1 ⊆ ▵t2.
+#t1 #t2 #Ht #p * #q #Hq
+/3 width=2 by ex_intro/
+qed.
+
+lemma preterm_root_eq_repl:
+      ∀t1,t2. t1 ⇔ t2 → ▵t1 ⇔ ▵t2.
+#t1 #t2 * #H1 #H2
+/3 width=3 by conj, preterm_root_incl_repl/
+qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma
index bab6b26e1677fa3dbca1f0d37083eb1037c26d8d..b3957eaf304a6079d1dd03c0ccdbbcd9738b40ce 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/white_harrow_2.ma".
+include "ground/notation/relations/arroweq_2.ma".
 include "ground/lib/subset_inclusion.ma".
 
 (* EQUIVALENCE FOR SUBSETS **************************************************)
@@ -22,7 +22,21 @@ definition subset_eq (A): relation2 𝒫❨A❩ 𝒫❨A❩ ≝
 
 interpretation
   "equivalence (subset)"
-  'WhiteHArrow u1 u2 = (subset_eq ? u1 u2).
+  'ArrowEq u1 u2 = (subset_eq ? u1 u2).
+
+(* Basic destructions *******************************************************)
+
+lemma subset_in_eq_repl_back (A) (a:A):
+      ∀u1. a ϵ u1 → ∀u2. u1 ⇔ u2 → a ϵ u2.
+#A #a #u1 #Hu1 #u2 *
+/2 width=1 by/
+qed-.
+
+lemma subset_in_eq_repl_fwd (A) (a:A):
+      ∀u1. a ϵ u1 → ∀u2. u2 ⇔ u1 → a ϵ u2.
+#A #a #u1 #Hu1 #u2 *
+/2 width=1 by/
+qed-.
 
 (* Basic constructions ******************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/arroweq_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/arroweq_2.ma
new file mode 100644 (file)
index 0000000..d8fbac4
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/arroweq_2.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( a1 ⇔ break term 46 a2 )"
+  non associative with precedence 45
+  for @{ 'ArrowEq $a1 $a2 }.

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/white_harrow_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/white_harrow_2.ma
deleted file mode 100644 (file)
index b7130df..0000000
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/white_harrow_2.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GROUND NOTATION **********************************************************)
-
-notation "hvbox( a1 ⇔ break term 46 a2 )"
-  non associative with precedence 45
-  for @{ 'WhiteHArrow $a1 $a2 }.