X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fbdd_term.ma;h=9f8238432a9500c294b2478326efdc46d5c70abb;hb=a4cacf8e269910184348a037106551dbc8a46fd4;hp=6a70f61cb0284030cf8349ffce95619bc520b721;hpb=6c52017b15171aa20ddfd01c1bbf3cc22a86c81c;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 6a70f61cb..9f8238432 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma @@ -14,7 +14,7 @@ include "delayed_updating/syntax/prototerm_constructors.ma". include "delayed_updating/syntax/prototerm_eq.ma". -include "delayed_updating/notation/functions/class_d_phi_0.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". @@ -25,7 +25,7 @@ include "ground/xoa/ex_5_3.ma". inductive bdd: 𝒫❨prototerm❩ ≝ | bdd_oref: ∀n. bdd (⧣n) -| bdd_iref: ∀t,n. bdd t → bdd (𝛗n.t) +| 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 @@ -33,19 +33,19 @@ inductive bdd: 𝒫❨prototerm❩ ≝ 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