X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fbdd_term.ma;h=1eb11fc030bc8c9f0676f2d82b52b9450ad371aa;hb=306205b6853874cf485152222593b57249c6e7fa;hp=897773a42d64d67b19e83d777b87fcca6975cd2d;hpb=13584a37bbcde10e03c8a488f5b93e1e042da0a6;p=helm.git

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 897773a42..1eb11fc03 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/prototerm_constructors.ma".
-include "delayed_updating/syntax/prototerm_equivalence.ma".
-include "delayed_updating/notation/functions/class_d_phi_0.ma".
+include "delayed_updating/syntax/prototerm_eq.ma".
+include "delayed_updating/notation/functions/class_d_tau_0.ma".
 include "ground/xoa/or_5.ma".
 include "ground/xoa/ex_3_1.ma".
 include "ground/xoa/ex_4_2.ma".
@@ -24,28 +24,28 @@ include "ground/xoa/ex_5_3.ma".
 (* BY-DEPTH DELAYED (BDD) TERM **********************************************)
 
 inductive bdd: 𝒫❨prototerm❩ ≝
-| bdd_oref: ∀n. bdd (#n)
-| bdd_iref: ∀t,n. bdd t → bdd (𝛗n.t)
+| bdd_oref: ∀k. bdd (⧣k)
+| bdd_iref: ∀t,k. bdd t → bdd (𝛕k.t)
 | bdd_abst: ∀t. bdd t → bdd (𝛌.t)
-| bdd_appl: ∀u,t. bdd u → bdd t → bdd (@u.t)
+| bdd_appl: ∀u,t. bdd u → bdd t → bdd (＠u.t)
 | bdd_conv: ∀t1,t2. t1 ⇔ t2 → bdd t1 → bdd t2
 .
 
 interpretation
   "by-depth delayed (prototerm)"
-  'ClassDPhi = (bdd).
+  'ClassDTau = (bdd).
 
-(*
+(* COMMENT
 
 (* Basic inversions *********************************************************)
 
 lemma bdd_inv_in_comp_gen:
-      ∀t,p. t ϵ 𝐃𝛗 → p ϵ t →
+      ∀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
+       | ∃∃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 #H elim H -H
 [ #n * /3 width=3 by or5_intro0, ex2_intro/
@@ -64,9 +64,9 @@ 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
+       | ∃∃u. u ϵ 𝐃𝛕 & q ϵ ɱ.u & 𝛕n.u ⇔ t
 .
 #t #q #n #Ht #Hq
 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
@@ -80,9 +80,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 →
+      ∀t,q,n. t ϵ 𝐃𝛕 → 𝗱n◗q ϵ ▵t →
       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
-       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵ɱ.u & 𝛗n.u ⇔ t
+       | ∃∃u. u ϵ 𝐃𝛕 & q ϵ ▵ɱ.u & 𝛕n.u ⇔ t
 .
 #t #q #n #Ht * #r #Hq
 elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq *
@@ -95,8 +95,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 *
@@ -109,8 +109,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
@@ -118,8 +118,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 *
@@ -132,8 +132,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
@@ -142,8 +142,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 *
@@ -156,8 +156,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
@@ -168,7 +168,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 *
@@ -213,4 +213,4 @@ lemma bbd_mono_in_root_d:
   ]
 ]
 qed-.
-*)
\ No newline at end of file
+*)