update in delayed_updating

+ WIP on lift
+ notation changed for delayed updating (term constructor)
+ minor corrections

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/phi_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/phi_2.etc
new file mode 100644 (file)
index 0000000..1278154
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/phi_2.etc
@@ -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( 𝛗 break term 76 n. break term 70 t )"
+  non associative with precedence 70
+  for @{ 'Phi $n $t }.

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
deleted file mode 100644 (file)
index d453176..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.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( 𝐃𝛗 )"
-  non associative with precedence 70
-  for @{ 'ClassDPhi }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_tau_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_tau_0.ma
new file mode 100644 (file)
index 0000000..8b21ae5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_tau_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 70
+  for @{ 'ClassDTau }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma
deleted file mode 100644 (file)
index 1278154..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_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( 𝛗 break term 76 n. break term 70 t )"
-  non associative with precedence 70
-  for @{ 'Phi $n $t }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_2.ma
new file mode 100644 (file)
index 0000000..099360c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝛕 break term 76 n. break term 70 t )"
+  non associative with precedence 70
+  for @{ 'Tau $n $t }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 738553c7de027e4165309cd8bebc1668aa9c07dc..193136433188b5857954573034cac434610a108e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -26,7 +26,7 @@ definition dfr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃n:pnat.
            let r ≝ p●𝗔◗𝗟◗q in
            ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 &
-              t1[â\8b\94râ\86\90ð\9d\9b\97n.(t1⋔(p◖𝗦))] ⇔ t2
+              t1[â\8b\94râ\86\90ð\9d\9b\95n.(t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma
index a3a3494191ad176fd4a62cea1cb261669c1fc2a4..c3f6cfa11849a560be7114edeaa35ac2fa955327 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma
@@ -15,6 +15,8 @@
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 
+(* FOCALIZED SUBSTITUTION ***************************************************)
+
 (* Constructions with subset_equivalence ************************************)
 
 lemma subset_inclusion_fsubst_bi (t1) (t2) (u1) (u2) (p):

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
new file mode 100644 (file)
index 0000000..e1be5de
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
@@ -0,0 +1,54 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/substitution/fsubst.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
+(*
+include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/prototerm_proper.ma".
+*)
+(* FOCALIZED SUBSTITUTION ***************************************************)
+
+(* Constructions with lift for preterm **************************************)
+
+lemma lift_term_fsubst_sn (f) (t) (u) (p):
+      (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u] ⊆ ↑[f](t[⋔p←u]).
+#f #t #u #p #ql * *
+[ #rl * #r #Hr #H1 #H2 destruct
+  >lift_path_append
+  /4 width=3 by in_comp_lift_path_term, or_introl, ex2_intro/
+| * #q #Hq #H1 #H0
+  @(ex2_intro … H1) @or_intror @conj // -Hq #r #H2 destruct
+  /2 width=2 by/
+]
+qed-.
+
+lemma lift_term_fsubst_dx (f) (t) (u) (p):
+      ↑[f](t[⋔p←u]) ⊆ (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u].
+#f #t #u #p #ql * #q * *
+[ #r #Hu #H1 #H2 destruct
+  @or_introl @ex2_intro
+  [|| <lift_path_append // ]
+  /2 width=3 by ex2_intro/
+| #Hq #H0 #H1 destruct
+  @or_intror @conj [ /2 width=1 by in_comp_lift_path_term/ ] -Hq #r #Hr
+  elim (lift_path_inv_append_dx … Hr) -Hr #s1 #s2 #Hs1 #_ #H1 destruct
+  lapply (lift_path_inj … Hs1) -Hs1 #H1 destruct 
+  /2 width=2 by/
+]
+qed-.
+
+lemma lift_term_fsubst (f) (t) (u) (p):
+      (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u] ⇔ ↑[f](t[⋔p←u]).
+/3 width=1 by lift_term_fsubst_sn, conj, lift_term_fsubst_dx/ qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
index 2fae75c26603af11f644ca666774478249c613bd..d7dde19bc042e144ba53168cb0d525052f073950 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
@@ -19,26 +19,26 @@ include "delayed_updating/syntax/prototerm_constructors_eq.ma".
 (* LIFT FOR PROTOTERM *******************************************************)
 
 lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
-      (ð\9d\9b\97fï¼ â§£â\9d¨nâ\9d©.â\86\91[â\87\82*[n]f]t) â\8a\86 â\86\91[f](ð\9d\9b\97n.t).
+      (ð\9d\9b\95fï¼ â§£â\9d¨nâ\9d©.â\86\91[â\87\82*[n]f]t) â\8a\86 â\86\91[f](ð\9d\9b\95n.t).
 #f #t #n #p * #q * #r #Hr #H1 #H2 destruct
 @(ex2_intro … (𝗱n◗𝗺◗r))
 /2 width=1 by in_comp_iref/
 qed-.
 
 lemma lift_iref_dx (f) (t) (n:pnat):
-      â\86\91[f](ð\9d\9b\97n.t) â\8a\86 ð\9d\9b\97f＠⧣❨n❩.↑[⇂*[n]f]t.
+      â\86\91[f](ð\9d\9b\95n.t) â\8a\86 ð\9d\9b\95f＠⧣❨n❩.↑[⇂*[n]f]t.
 #f #t #n #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
 /3 width=1 by in_comp_iref, in_comp_lift_path_term/
 qed-.
 
 lemma lift_iref (f) (t) (n:pnat):
-      (ð\9d\9b\97fï¼ â§£â\9d¨nâ\9d©.â\86\91[â\87\82*[n]f]t) â\87\94 â\86\91[f](ð\9d\9b\97n.t).
+      (ð\9d\9b\95fï¼ â§£â\9d¨nâ\9d©.â\86\91[â\87\82*[n]f]t) â\87\94 â\86\91[f](ð\9d\9b\95n.t).
 /3 width=1 by conj, lift_iref_sn, lift_iref_dx/
 qed.
 
 lemma lift_iref_uni (t) (m) (n):
-      (ð\9d\9b\97(n+m).t) â\87\94 â\86\91[ð\9d\90®â\9d¨mâ\9d©](ð\9d\9b\97n.t).
+      (ð\9d\9b\95(n+m).t) â\87\94 â\86\91[ð\9d\90®â\9d¨mâ\9d©](ð\9d\9b\95n.t).
 #t #m #n
 @(subset_eq_trans … (lift_iref …))
 <tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
index 9c4b0f3b5ac350eba4175d9fc10d603361a96d4f..5ab8d7f05a166f99d2679810d119c9b9ecaa8ce2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "delayed_updating/substitution/lift.ma".
+include "ground/relocation/tr_pap_pap.ma".
 include "ground/relocation/tr_pap_eq.ma".
 include "ground/relocation/tr_pn_eq.ma".
 include "ground/lib/stream_tls_eq.ma".
@@ -143,6 +144,139 @@ lemma lift_path_S_dx (f) (p):
 #f #p <lift_path_append //
 qed.
 
+(* Advanced inversions ******************************************************)
+
+lemma lift_path_inv_empty (f) (p):
+      (𝐞) = ↑[f]p → 𝐞 = p.
+#f * // * [ #n ] #p
+[ <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+qed-.
+
+lemma lift_path_inv_d_sn (f) (p) (q) (k):
+      (𝗱k◗q) = ↑[f]p →
+      ∃∃r,h. k = f＠⧣❨h❩ & q = ↑[⇂*[h]f]r & 𝗱h◗r = p.
+#f * [| * [ #n ] #p ] #q #k
+[ <lift_path_empty
+| <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+/2 width=5 by ex3_2_intro/
+qed-.
+
+lemma lift_path_inv_m_sn (f) (p) (q):
+      (𝗺◗q) = ↑[f]p →
+      ∃∃r. q = ↑[f]r & 𝗺◗r = p.
+#f * [| * [ #n ] #p ] #q
+[ <lift_path_empty
+| <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lift_path_inv_L_sn (f) (p) (q):
+      (𝗟◗q) = ↑[f]p →
+      ∃∃r. q = ↑[⫯f]r & 𝗟◗r = p.
+#f * [| * [ #n ] #p ] #q
+[ <lift_path_empty
+| <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lift_path_inv_A_sn (f) (p) (q):
+      (𝗔◗q) = ↑[f]p →
+      ∃∃r. q = ↑[f]r & 𝗔◗r = p.
+#f * [| * [ #n ] #p ] #q
+[ <lift_path_empty
+| <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lift_path_inv_S_sn (f) (p) (q):
+      (𝗦◗q) = ↑[f]p →
+      ∃∃r. q = ↑[f]r & 𝗦◗r = p.
+#f * [| * [ #n ] #p ] #q
+[ <lift_path_empty
+| <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lift_path_inv_append_dx (q2) (q1) (p) (f):
+      q1●q2 = ↑[f]p →
+      ∃∃p1,p2. q1 = ↑[f]p1 & q2 = ↑[↑[p1]f]p2 & p1●p2 = p.
+#q2 #q1 elim q1 -q1
+[| * [ #n1 ] #q1 #IH ] #p #f
+[ <list_append_empty_sn #H0 destruct
+  /2 width=5 by ex3_2_intro/
+| <list_append_lcons_sn #H0
+  elim (lift_path_inv_d_sn … H0) -H0 #r1 #m1 #_ #_ #H0 #_ -IH
+    elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
+    elim Hq2 -Hq2 //
+  | elim (lift_path_inv_m_sn … H)
+  | elim (lift_path_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
+    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
+    @(ex3_2_intro … (r1●𝗟◗p1)) //
+    <structure_append <Hr1 -Hr1 //
+  | elim (lift_path_inv_A_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
+    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
+    @(ex3_2_intro … (r1●𝗔◗p1)) //
+    <structure_append <Hr1 -Hr1 //
+  | elim (lift_path_inv_S_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
+    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
+    @(ex3_2_intro … (r1●𝗦◗p1)) //
+    <structure_append <Hr1 -Hr1 //
+  ]
+]
+qed-.
+
+(* Main inversions **********************************************************)
+
+theorem lift_path_inj (q:path) (p) (f):
+        ↑[f]q = ↑[f]p → q = p.
+#q elim q -q [| * [ #k ] #q #IH ] #p #f
+[ <lift_path_empty #H0
+  <(lift_path_inv_empty … H0) -H0 //
+| <lift_path_d_sn #H0
+  elim (lift_path_inv_d_sn … H0) -H0 #r #h #H0
+  <(tr_pap_inj ????? H0) -h [1,3: // ] #Hr #H0 destruct
+| <lift_path_m_sn #H0
+  elim (lift_path_inv_m_sn … H0) -H0 #r #Hr #H0 destruct
+| <lift_path_L_sn #H0
+  elim (lift_path_inv_L_sn … H0) -H0 #r #Hr #H0 destruct
+| <lift_path_A_sn #H0
+  elim (lift_path_inv_A_sn … H0) -H0 #r #Hr #H0 destruct
+| <lift_path_S_sn #H0
+  elim (lift_path_inv_S_sn … H0) -H0 #r #Hr #H0 destruct
+]
+<(IH … Hr) -r -IH //
+qed-.
+
 (* COMMENT 
 
 (* Advanced constructions with proj_rmap and stream_tls *********************)

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 6a70f61cb0284030cf8349ffce95619bc520b721..9f8238432a9500c294b2478326efdc46d5c70abb 100644 (file)
--- 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: â\88\80t,n. bdd t â\86\92 bdd (ð\9d\9b\97n.t)
+| bdd_iref: â\88\80t,n. bdd t â\86\92 bdd (ð\9d\9b\95n.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:
-      â\88\80t,p. t ϵ ð\9d\90\83ð\9d\9b\97 → p ϵ t →
+      â\88\80t,p. t ϵ ð\9d\90\83ð\9d\9b\95 → p ϵ t →
       ∨∨ ∃∃n. #n ⇔ t & 𝗱n◗𝐞 = p
-       | â\88\83â\88\83u,q,n. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & ð\9d\9b\97n.u ⇔ t & 𝗱n◗𝗺◗q = p
-       | â\88\83â\88\83u,q. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p
-       | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p
-       | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ v & @v.u ⇔ t & 𝗦◗q = p
+       | â\88\83â\88\83u,q,n. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & ð\9d\9b\95n.u ⇔ t & 𝗱n◗𝗺◗q = p
+       | â\88\83â\88\83u,q. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p
+       | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p
+       | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & 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:
-      â\88\80t,q,n. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗱n◗q ϵ t →
+      â\88\80t,q,n. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗱n◗q ϵ t →
       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
-       | â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ ɱ.u & ð\9d\9b\97n.u ⇔ t
+       | â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ ɱ.u & ð\9d\9b\95n.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:
-      â\88\80t,q,n. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗱n◗q ϵ ▵t →
+      â\88\80t,q,n. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗱n◗q ϵ ▵t →
       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
-       | â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ â\96µÉ±.u & ð\9d\9b\97n.u ⇔ t
+       | â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ â\96µÉ±.u & ð\9d\9b\95n.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:
-      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗟◗q ϵ t →
-      â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & 𝛌.u ⇔ t
+      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗟◗q ϵ t →
+      â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\95 & 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:
-      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗟◗q ϵ ▵t →
-      â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ ▵u & 𝛌.u ⇔ t.
+      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗟◗q ϵ ▵t →
+      â\88\83â\88\83u. u ϵ ð\9d\90\83ð\9d\9b\95 & 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:
-      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗔◗q ϵ t →
-      â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & @v.u ⇔ t
+      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗔◗q ϵ t →
+      â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & 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:
-      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗔◗q ϵ ▵t →
-      â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ ▵u & @v.u ⇔ t
+      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗔◗q ϵ ▵t →
+      â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & 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:
-      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗦◗q ϵ t →
-      â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ v & @v.u ⇔ t
+      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗦◗q ϵ t →
+      â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & 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:
-      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\97 → 𝗦◗q ϵ ▵t →
-      â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ ▵v & @v.u ⇔ t
+      â\88\80t,q. t ϵ ð\9d\90\83ð\9d\9b\95 → 𝗦◗q ϵ ▵t →
+      â\88\83â\88\83v,u. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & 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:
-      â\88\80l,n,p,t. t ϵ ð\9d\90\83ð\9d\9b\97 → p◖𝗱n ϵ ▵t → p◖l ϵ ▵t → 𝗱n = l.
+      â\88\80l,n,p,t. t ϵ ð\9d\90\83ð\9d\9b\95 → 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/prototerm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
index 434f1e810cb44fe31d6bc2764bfed79e637bb6fd..f026c769e0cd3442db5b644f274f3252b37dfcf5 100644 (file)
--- 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,7 @@
 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/lamda_1.ma".
 include "delayed_updating/notation/functions/at_2.ma".
 
@@ -45,7 +45,7 @@ interpretation
 
 interpretation
   "inner variable reference by depth (prototerm)"
-  'Phi n t = (prototerm_node_1_2 (label_d n) label_m t).
+  'Tau n t = (prototerm_node_1_2 (label_d n) label_m t).
 
 interpretation
   "name-free functional abstraction (prototerm)"
@@ -58,13 +58,13 @@ interpretation
 (* Basic constructions *******************************************************)
 
 lemma in_comp_iref (t) (q) (n):
-      q ϵ t â\86\92 ð\9d\97±nâ\97\97ð\9d\97ºâ\97\97q ϵ ð\9d\9b\97n.t.
+      q ϵ t â\86\92 ð\9d\97±nâ\97\97ð\9d\97ºâ\97\97q ϵ ð\9d\9b\95n.t.
 /2 width=3 by ex2_intro/ qed.
 
 (* Basic inversions *********************************************************)
 
 lemma in_comp_inv_iref (t) (p) (n):
-      p ϵ ð\9d\9b\97n.t →
+      p ϵ ð\9d\9b\95n.t →
       ∃∃q. 𝗱n◗𝗺◗q = p & q ϵ t.
 #t #p #n * #q #Hq #Hp
 /2 width=3 by ex2_intro/
@@ -80,7 +80,7 @@ elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
 qed-.
 
 lemma prototerm_in_root_inv_lcons_iref:
-      â\88\80t,p,l,n. lâ\97\97p ϵ â\96µð\9d\9b\97n.t →
+      â\88\80t,p,l,n. lâ\97\97p ϵ â\96µð\9d\9b\95n.t →
       ∧∧ 𝗱n = l & p ϵ ▵ɱ.t.
 #t #p #l #n * #q * #r #Hr
 <list_append_lcons_sn #H0 destruct -H0

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
index 88f567214877cd7c3566f502dc1a29bb2897e24a..46e945ede9ed9b0e022b9573cbc96c3d677a7162 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
@@ -20,6 +20,6 @@ include "ground/lib/subset_ext_equivalence.ma".
 (* Constructions with equivalence for prototerm *****************************)
 
 lemma iref_eq_repl (t1) (t2) (n):
-      t1 â\87\94 t2 â\86\92 ð\9d\9b\97n.t1 â\87\94 ð\9d\9b\97n.t2.
+      t1 â\87\94 t2 â\86\92 ð\9d\9b\95n.t1 â\87\94 ð\9d\9b\95n.t2.
 /2 width=1 by subset_equivalence_ext_f1_bi/
 qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
index c7bb79244876fad03c2454df4228db67e2a6e6db..309eb00246b0a93089a18aead73907caf3dab2c4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
@@ -20,6 +20,6 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 (* Constructions with prototerm constructors ********************************)
 
 lemma ppc_iref (t) (n):
-      (ð\9d\9b\97n.t) ϵ 𝐏.
+      (ð\9d\9b\95n.t) ϵ 𝐏.
 #t #n #p * #q #Hq #H0 destruct //
 qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
index c70e09e1abd0b4c306ce57785bad629d24ea1130..8cdfb5bf958f55ed7f8822974b468d164478f912 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
@@ -20,20 +20,20 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 (* Constructions with constructors ******************************************)
 
 lemma unwind2_term_iref_sn (f) (t) (n:pnat):
-      â\96¼[fâ\88\98ð\9d\90®â\9d¨nâ\9d©]t â\8a\86 â\96¼[f](ð\9d\9b\97n.t).
+      â\96¼[fâ\88\98ð\9d\90®â\9d¨nâ\9d©]t â\8a\86 â\96¼[f](ð\9d\9b\95n.t).
 #f #t #n #p * #q #Hq #H0 destruct
 @(ex2_intro … (𝗱n◗𝗺◗q))
 /2 width=1 by in_comp_iref/
 qed-.
 
 lemma unwind2_term_iref_dx (f) (t) (n:pnat):
-      â\96¼[f](ð\9d\9b\97n.t) ⊆ ▼[f∘𝐮❨n❩]t.
+      â\96¼[f](ð\9d\9b\95n.t) ⊆ ▼[f∘𝐮❨n❩]t.
 #f #t #n #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
 /2 width=1 by in_comp_unwind2_path_term/
 qed-.
 
 lemma unwind2_term_iref (f) (t) (n:pnat):
-      â\96¼[fâ\88\98ð\9d\90®â\9d¨nâ\9d©]t â\87\94 â\96¼[f](ð\9d\9b\97n.t).
+      â\96¼[fâ\88\98ð\9d\90®â\9d¨nâ\9d©]t â\87\94 â\96¼[f](ð\9d\9b\95n.t).
 /3 width=2 by conj, unwind2_term_iref_sn, unwind2_term_iref_dx/
 qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
index 522ad9455a99868fc3eb73668cbf597a6f89e857..452c913e54b0154e374b811ae3e8dd5a884e91ba 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
@@ -18,7 +18,7 @@ include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/syntax/preterm.ma".
 include "delayed_updating/syntax/prototerm_proper.ma".
 
-(* UNWIND FOR PRETERM ******************************************************)
+(* UNWIND FOR PRETERM *******************************************************)
 
 (* Constructions with fsubst ************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
index d8a44810cf3a92f9619a5fba295da00e234ea933..5c92a9af5a364189d99d17b24a6cc7554b6c6710 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
@@ -19,9 +19,9 @@ include "delayed_updating/syntax/path_proper.ma".
 include "ground/xoa/ex_4_2.ma".
 include "ground/xoa/ex_3_2.ma".
 
-(* GENERIC UNWIND FOR PATH *************************************************)
+(* GENERIC UNWIND FOR PATH **************************************************)
 
-(* Basic constructions with structure **************************************)
+(* Basic constructions with structure ***************************************)
 
 lemma structure_unwind_gen (p) (f):
       ⊗p = ⊗◆[f]p.