X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fprototerm_constructors.ma;h=8bffdb64ae0555df03894b6793f712f21b92e81a;hb=797a607af83f82102033270087722a7e59ddcd17;hp=fd86ef975a39b862aaf05ac99dc5efd298fb10ed;hpb=13584a37bbcde10e03c8a488f5b93e1e042da0a6;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma index fd86ef975..8bffdb64a 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma @@ -15,7 +15,8 @@ include "delayed_updating/syntax/prototerm.ma". include "delayed_updating/notation/functions/m_hook_1.ma". include "delayed_updating/notation/functions/hash_1.ma". -include "delayed_updating/notation/functions/phi_2.ma". +include "delayed_updating/notation/functions/tau_2.ma". +include "delayed_updating/notation/functions/tau_3.ma". include "delayed_updating/notation/functions/lamda_1.ma". include "delayed_updating/notation/functions/at_2.ma". @@ -41,11 +42,15 @@ interpretation interpretation "outer variable reference by depth (prototerm)" - 'Hash n = (prototerm_node_0 (label_d n)). + 'Hash k = (prototerm_node_0 (label_d k)). interpretation "inner variable reference by depth (prototerm)" - 'Phi n t = (prototerm_node_1_2 (label_d n) label_m t). + 'Tau k t = (prototerm_node_1_2 (label_d k) label_m t). + +interpretation + "inner variable reference by depth with offset (prototerm)" + 'Tau k d t = (prototerm_node_1_2 (label_d2 k d) label_m t). interpretation "name-free functional abstraction (prototerm)" @@ -55,8 +60,33 @@ interpretation "application (prototerm)" 'At u t = (prototerm_node_2 label_S label_A u t). -(* Basic Inversions *********************************************************) +(* Basic constructions *******************************************************) + +lemma in_comp_iref (t) (q) (k): + q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t. +/2 width=3 by ex2_intro/ qed. + +lemma in_comp_iref2 (t) (q) (k) (d): + q ϵ t → 𝗱❨k,d❩◗𝗺◗q ϵ 𝛕❨k,d❩.t. +/2 width=3 by ex2_intro/ qed. + +(* Basic inversions *********************************************************) + +lemma in_comp_inv_iref (t) (p) (k): + p ϵ 𝛕k.t → + ∃∃q. 𝗱k◗𝗺◗q = p & q ϵ t. +#t #p #k * #q #Hq #Hp +/2 width=3 by ex2_intro/ +qed-. + +lemma in_comp_inv_iref2 (t) (p) (k) (d): + p ϵ 𝛕❨k,d❩.t → + ∃∃q. 𝗱❨k,d❩◗𝗺◗q = p & q ϵ t. +#t #p #k #d * #q #Hq #Hp +/2 width=3 by ex2_intro/ +qed-. +(* COMMENT lemma prototerm_in_root_inv_lcons_oref: ∀p,l,n. l◗p ϵ ▵#n → ∧∧ 𝗱n = l & 𝐞 = p. @@ -67,7 +97,7 @@ elim (eq_inv_list_empty_append … e0) -e0 #H0 #_ qed-. lemma prototerm_in_root_inv_lcons_iref: - ∀t,p,l,n. l◗p ϵ ▵𝛗n.t → + ∀t,p,l,n. l◗p ϵ ▵𝛕n.t → ∧∧ 𝗱n = l & p ϵ ▵ɱ.t. #t #p #l #n * #q * #r #Hr