update in delayed_updating

+ some notation updated
+ some unused files removed

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc
deleted file mode 100644 (file)
index b568c32..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc
+++ /dev/null
@@ -1,37 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/syntax/prototerm_constructors.ma".
-include "delayed_updating/syntax/prototerm_equivalence.ma".
-include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/substitution/unwind.ma".
-include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/syntax/path_balanced.ma".
-include "delayed_updating/syntax/path_depth.ma".
-include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
-include "ground/xoa/ex_1_2.ma".
-include "ground/xoa/and_4.ma".
-
-(* DELAYED FOCUSED REDUCTION ************************************************)
-
-definition dfr (p) (q): relation2 prototerm prototerm ≝
-           λt1,t2. ∃∃b,n.
-           let r ≝ p●𝗔◗b●𝗟◗q in
-           ∧∧ ⊗b ϵ 𝐁 & ∀f. ↑❘q❘ = (↑[q]⫯f)@❨n❩ & r◖𝗱n ϵ t1 &
-              t1[⋔r←𝛗(n+❘b❘).(t1⋔(p◖𝗦))] ⇔ t2
-.
-
-interpretation
-  "focused balanced reduction with delayed updating (prototerm)"
-  'BlackRightArrowDF t1 p q t2 = (dfr p q t1 t2).

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc
deleted file mode 100644 (file)
index 0694154..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc
+++ /dev/null
@@ -1,106 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/reduction/dfr.ma".
-include "delayed_updating/reduction/ifr.ma".
-include "delayed_updating/substitution/fsubst_unwind.ma".
-include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/unwind_constructors.ma".
-include "delayed_updating/substitution/unwind_preterm_eq.ma".
-include "delayed_updating/substitution/unwind_structure_depth.ma".
-include "delayed_updating/substitution/unwind_depth.ma".
-include "delayed_updating/syntax/prototerm_proper_constructors.ma".
-include "delayed_updating/syntax/path_structure_depth.ma".
-include "ground/relocation/tr_uni_compose.ma".
-include "ground/relocation/tr_pap_pushs.ma".
-
-(* DELAYED FOCUSED REDUCTION ************************************************)
-
-lemma tr_uni_eq_repl (n1) (n2):
-      n1 = n2 → 𝐮❨n1❩ ≗ 𝐮❨n2❩.
-// qed.
-
-axiom pippo (b) (q) (n):
-      ↑❘q❘ = (↑[q]𝐢)@❨n❩ →
-      ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)@❨n+❘b❘❩.
-
-lemma unwind_rmap_tls_eq_id (p) (n):
-      ❘p❘ = ↑[p]𝐢@❨n❩ →
-      (𝐢) ≗ ⇂*[n]↑[p]𝐢.
-#p @(list_ind_rcons … p) -p
-[ #n <depth_empty #H destruct
-| #p * [ #m ] #IH #n
-  [ <depth_d_dx <unwind_rmap_pap_d_dx #H0
-    @(stream_eq_trans … (unwind_rmap_tls_d_dx …))
-    @(stream_eq_trans … (IH …)) -IH //
-  | /2 width=1 by/
-  | <depth_L_dx <unwind_rmap_L_dx
-    cases n -n [| #n ] #H0
-    [
-    | 
-    ]
-  | /2 width=1 by/
-  | /2 width=1 by/
-  ]
-]
-
-
-(*  (↑❘q❘+❘b❘=↑[b●𝗟◗q]𝐢@❨n+❘b❘❩ *)
-(* [↑[p]𝐢@❨n❩]⫯*[❘p❘]f∘⇂*[n]↑[p]𝐢) *)
-lemma unwind_rmap_tls_eq (f) (p) (n):
-      ❘p❘ = ↑[p]𝐢@❨n❩ →
-      f ≗ ⇂*[n]↑[p]f.
-#f #p #n #Hp
-@(stream_eq_canc_dx … (stream_tls_eq_repl …))
-[| @unwind_rmap_decompose | skip ]
-<tr_compose_tls <Hp
-
-@(stream_eq_canc_dx) … (unwind_rmap_decompose …)) 
-
-lemma dfr_unwind_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
-      t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐟[⊗p,⊗q] ↑[f]t2.
-#f #p #q #t1 #t2 #H0t1
-* #b #n * #Hb #Hn  #Ht1 #Ht2
-@(ex1_2_intro … (⊗b) (↑❘⊗q❘)) @and4_intro
-[ //
-| #g <unwind_rmap_structure <depth_structure
-  >tr_pushs_swap <tr_pap_pushs_le //
-| lapply (in_comp_unwind_bi f … Ht1) -Ht1 -H0t1 -Hb -Ht2
-  <unwind_path_d_empty_dx //
-| lapply (unwind_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
-  @(subset_eq_trans … Ht2) -t2
-  @(subset_eq_trans … (unwind_fsubst …))
-  [ <unwind_rmap_append <unwind_rmap_A_sn (* <unwind_rmap_append <unwind_rmap_L_sn *)
-    <structure_append <structure_A_sn <structure_append <structure_L_sn
-    <depth_append <depth_L_sn <depth_structure <depth_structure
-    @fsubst_eq_repl [ // ]
-    @(subset_eq_trans … (unwind_iref …))
-    @(subset_eq_canc_sn … (unwind_term_eq_repl_dx …))
-    [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ]
-    @(subset_eq_trans … (unwind_term_after …))
-    @(subset_eq_canc_dx … (unwind_term_after …))
-    @unwind_term_eq_repl_sn -t1
-    @(stream_eq_trans … (tr_compose_uni_dx …))
-    lapply (Hn (𝐢)) -Hn >tr_id_unfold #Hn
-    lapply (pippo … b … Hn) -Hn #Hn
-    @tr_compose_eq_repl
-    [ <unwind_rmap_pap_le //
-      <Hn <nrplus_inj_sn //
-    |
-    ]
-  | //
-  | /2 width=2 by ex_intro/
-  | //
-  ]
-]

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst.etc
deleted file mode 100644 (file)
index adbc16c..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst.etc
+++ /dev/null
@@ -1,28 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/syntax/prototerm.ma".
-include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma".
-
-(* FOCALIZED SUBSTITUTION ***************************************************)
-
-definition fsubst (p) (u): prototerm → prototerm ≝
-           λt,q.
-           ∨∨ ∃∃r. r ϵ u & p●r = q
-            | ∧∧ q ϵ t & (∀r. p●r = q → ⊥)
-.
-
-interpretation
-  "focalized substitution (prototerm)"
-  'PitchforkLeftArrow t p u = (fsubst p u t).

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_eq.etc
deleted file mode 100644 (file)
index a6681b5..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_eq.etc
+++ /dev/null
@@ -1,33 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/syntax/prototerm_equivalence.ma".
-
-(* Constructions with subset_equivalence ************************************)
-
-lemma subset_inclusion_fsubst_bi (t1) (t2) (u1) (u2) (p):
-      t1 ⊆ t2 → u1 ⊆ u2 → t1[⋔p←u1] ⊆ t2[⋔p←u2].
-#t1 #t2 #u1 #u2 #p #Ht #Hu #q * *
-[ #r #Hr #H0 destruct
-  /4 width=3 by ex2_intro, or_introl/
-| /4 width=2 by or_intror, conj/
-]
-qed.
-
-lemma fsubst_eq_repl (t1) (t2) (u1) (u2) (p):
-      t1 ⇔ t2 → u1 ⇔ u2 → t1[⋔p←u1] ⇔ t2[⋔p←u2].
-#t1 #t2 #u1 #u2 #p * #H1t #H2t * #H1u #H2u
-/3 width=5 by conj, subset_inclusion_fsubst_bi/
-qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/ifr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/ifr.etc
deleted file mode 100644 (file)
index 054aef5..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/ifr.etc
+++ /dev/null
@@ -1,36 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/substitution/unwind_prototerm.ma".
-include "delayed_updating/syntax/prototerm_equivalence.ma".
-include "delayed_updating/syntax/path_depth.ma".
-include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/syntax/path_balanced.ma".
-include "delayed_updating/notation/relations/black_rightarrow_f_4.ma".
-include "ground/xoa/ex_1_2.ma".
-include "ground/xoa/and_4.ma".
-
-(* IMMEDIATE FOCUSED REDUCTION ************************************************)
-
-definition ifr (p) (q): relation2 prototerm prototerm ≝
-           λt1,t2. ∃∃b,n.
-           let r ≝ p●𝗔◗b●𝗟◗q in
-           ∧∧ ⊗b ϵ 𝐁 & ∀f. ↑❘q❘ = (↑[q]⫯f)@❨n❩ & r◖𝗱n ϵ t1 &
-              t1[⋔r←↑[𝐮❨❘b●𝗟◗q❘❩](t1⋔(p◖𝗦))] ⇔ t2
-.
-
-interpretation
-  "focused balanced reduction with immediate updating (prototerm)"
-  'BlackRightArrowF t1 p q t2 = (ifr p q t1 t2).

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 576df6ec6fdb3aef007ed612584b132914b9654b..849c5f32dfd76fa5b3d257c2936d118dad9612fd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -28,8 +28,8 @@ include "ground/xoa/and_4.ma".
 definition dfr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃∃b,n.
            let r ≝ p●𝗔◗b●𝗟◗q in
-           â\88§â\88§ (â\8a\97b ϵ ð\9d\90\81 â\88§ ð\9d\9f\8e = â\9d\98bâ\9d\98) & â\86\91â\9d\98qâ\9d\98 = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
-              t1[â\8b\94râ\86\90ð\9d\9b\97(n+â\9d\98bâ\9d\98).(t1⋔(p◖𝗦))] ⇔ t2
+           â\88§â\88§ (â\8a\97b ϵ ð\9d\90\81 â\88§ ð\9d\9f\8e = â\99­b) & â\86\91â\99­q = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
+              t1[â\8b\94râ\86\90ð\9d\9b\97(n+â\99­b).(t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
index dd24f856863792f367b106e4354464ede5961645..2d3fdbdf596f7e405e1a29725db9c922314e6f56 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -14,11 +14,13 @@
 
 include "delayed_updating/reduction/dfr.ma".
 include "delayed_updating/reduction/ifr.ma".
+
 include "delayed_updating/unwind1/unwind_fsubst.ma".
 include "delayed_updating/unwind1/unwind_constructors.ma".
 include "delayed_updating/unwind1/unwind_preterm_eq.ma".
 include "delayed_updating/unwind1/unwind_structure_depth.ma".
 include "delayed_updating/unwind1/unwind_depth.ma".
+
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 include "delayed_updating/syntax/prototerm_proper_constructors.ma".
@@ -71,9 +73,9 @@ lemma dfr_unwind_id_bi (p) (q) (t1) (t2): t1 ϵ 𝐓 →
       t1 ➡𝐝𝐟[p,q] t2 → ▼[𝐢]t1 ➡𝐟[⊗p,⊗q] ▼[𝐢]t2.
 #p #q #t1 #t2 #H0t1
 * #b #n * #Hb #Hn #Ht1 #Ht2
-@(ex1_2_intro â\80¦ (â\8a\97b) (â\86\91â\9d\98â\8a\97qâ\9d\98)) @and4_intro
+@(ex1_2_intro â\80¦ (â\8a\97b) (â\86\91â\99­â\8a\97q)) @and4_intro
 [ //
-| //
+| (*//*)
 | lapply (in_comp_unwind_bi (𝐢) … Ht1) -Ht1 -H0t1 -Hb -Ht2
   <unwind_path_d_empty_dx <depth_structure //
 | lapply (unwind_term_eq_repl_dx (𝐢) … Ht2) -Ht2 #Ht2
@@ -85,11 +87,21 @@ lemma dfr_unwind_id_bi (p) (q) (t1) (t2): t1 ϵ 𝐓 →
     @fsubst_eq_repl [ // ]
     @(subset_eq_trans … (unwind_iref …))
 
-    elim Hb -Hb #Hb #H0 <H0 -H0 <nrplus_zero_dx <nplus_zero_dx <Hn
+    elim Hb -Hb #Hb #H0 <H0 -H0 <nrplus_zero_dx <nplus_zero_dx <nsucc_unfold
+    >Hn
     @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
     [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ]
-
+    <Hn <Hn
+(*    
+    @(subset_eq_trans … (lift_term_eq_repl_dx …))
+    [ @(unwind_term_eq_repl_sn … (tls_succ_unwind q …)) | skip ]
+*)
 (*
+    
+    @subset_eq_trans
+    [2: @unwind_term_eq_repl_dx
+    @(subset_eq_canc_sn … (unwind_term_eq_repl_dx …))
+
     @(subset_eq_canc_sn … (unwind_term_eq_repl_dx …))
     [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ]
 
@@ -116,3 +128,6 @@ Hn : ↑❘q❘ = ↑[p●𝗔◗b●𝗟◗q]𝐢@❨n❩
 ---------------------------
 ↑[𝐮❨↑❘q❘+❘b❘❩] ↑[↑[p]𝐢] t ⇔ ↑[𝐮❨↑[p●𝗔◗b●𝗟◗q]𝐢@❨n+❘b❘❩❩] t
 *)
+(*
+(↑[𝐮❨↑❘q❘❩]▼[⇂*[↑❘q❘]▼[p●𝗟◗q]𝐢](t1⋔(p◖𝗦))⇔▼[𝐮❨↑❘q❘❩∘▼[p●𝗔◗b●𝗟◗q]𝐢](t1⋔(p◖𝗦))
+*)

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index 8d0cfc52dc46aca4d628c8e85381e1a8249543e6..d2a33afc211f1bb60396108e33a1362e6a6fb5b6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -28,8 +28,8 @@ include "ground/xoa/and_4.ma".
 definition ifr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃∃b,n.
            let r ≝ p●𝗔◗b●𝗟◗q in
-           â\88§â\88§ (â\8a\97b ϵ ð\9d\90\81 â\88§ ð\9d\9f\8e = â\9d\98bâ\9d\98) & â\86\91â\9d\98qâ\9d\98 = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
-              t1[â\8b\94râ\86\90â\86\91[ð\9d\90®â\9d¨â\9d\98bâ\97\8fð\9d\97\9fâ\97\97qâ\9d\98❩](t1⋔(p◖𝗦))] ⇔ t2
+           â\88§â\88§ (â\8a\97b ϵ ð\9d\90\81 â\88§ ð\9d\9f\8e = â\99­b) & â\86\91â\99­q = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
+              t1[â\8b\94râ\86\90â\86\91[ð\9d\90®â\9d¨â\99­(bâ\97\8fð\9d\97\9fâ\97\97q)❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
index cdf24943af922c8a47c74990fb79e92acf803231..474bbcbda501f43dd5de91697dd321d58ca33c7f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/flat_1.ma".
 include "ground/arith/nat_plus.ma".
-include "ground/notation/functions/verticalbars_1.ma".
 
 (* DEPTH FOR PATH ***********************************************************)
 
@@ -33,32 +33,32 @@ match p with
 
 interpretation
   "depth (path)"
-  'VerticalBars p = (depth p).
+  'Flat p = (depth p).
 
 (* Basic constructions ******************************************************)
 
-lemma depth_empty: ð\9d\9f\8e = â\9d\98ð\9d\90\9eâ\9d\98.
+lemma depth_empty: ð\9d\9f\8e = â\99­ð\9d\90\9e.
 // qed.
 
-lemma depth_d_sn (q) (n): â\9d\98qâ\9d\98 = â\9d\98ð\9d\97±nâ\97\97qâ\9d\98.
+lemma depth_d_sn (q) (n): â\99­q = â\99­(ð\9d\97±nâ\97\97q).
 // qed.
 
-lemma depth_m_sn (q): â\9d\98qâ\9d\98 = â\9d\98ð\9d\97ºâ\97\97qâ\9d\98.
+lemma depth_m_sn (q): â\99­q = â\99­(ð\9d\97ºâ\97\97q).
 // qed.
 
-lemma depth_L_sn (q): â\86\91â\9d\98qâ\9d\98 = â\9d\98ð\9d\97\9fâ\97\97qâ\9d\98.
+lemma depth_L_sn (q): â\86\91â\99­q = â\99­(ð\9d\97\9fâ\97\97q).
 // qed.
 
-lemma depth_A_sn (q): â\9d\98qâ\9d\98 = â\9d\98ð\9d\97\94â\97\97qâ\9d\98.
+lemma depth_A_sn (q): â\99­q = â\99­(ð\9d\97\94â\97\97q).
 // qed.
 
-lemma depth_S_sn (q): â\9d\98qâ\9d\98 = â\9d\98ð\9d\97¦â\97\97qâ\9d\98.
+lemma depth_S_sn (q): â\99­q = â\99­(ð\9d\97¦â\97\97q).
 // qed.
 
 (* Main constructions *******************************************************)
 
 theorem depth_append (p1) (p2):
-        ❘p2❘+❘p1❘ = ❘p1●p2❘.
+        (♭p2)+(♭p1) = ♭(p1●p2).
 #p1 elim p1 -p1 //
 * [ #n ] #p1 #IH #p2 <list_append_lcons_sn
 [ <depth_d_sn <depth_d_sn //
@@ -72,21 +72,21 @@ qed.
 (* Constructions with list_rcons ********************************************)
 
 lemma depth_d_dx (p) (n):
-      â\9d\98pâ\9d\98 = â\9d\98pâ\97\96ð\9d\97±nâ\9d\98.
+      â\99­p = â\99­(pâ\97\96ð\9d\97±n).
 // qed.
 
 lemma depth_m_dx (p):
-      â\9d\98pâ\9d\98 = â\9d\98pâ\97\96ð\9d\97ºâ\9d\98.
+      â\99­p = â\99­(pâ\97\96ð\9d\97º).
 // qed.
 
 lemma depth_L_dx (p):
-      â\86\91â\9d\98pâ\9d\98 = â\9d\98pâ\97\96ð\9d\97\9fâ\9d\98.
+      â\86\91â\99­p = â\99­(pâ\97\96ð\9d\97\9f).
 // qed.
 
 lemma depth_A_dx (p):
-      â\9d\98pâ\9d\98 = â\9d\98pâ\97\96ð\9d\97\94â\9d\98.
+      â\99­p = â\99­(pâ\97\96ð\9d\97\94).
 // qed.
 
 lemma depth_S_dx (p):
-      â\9d\98pâ\9d\98 = â\9d\98pâ\97\96ð\9d\97¦â\9d\98.
+      â\99­p = â\99­(pâ\97\96ð\9d\97¦).
 // qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
index 700da6a46e26d3c6e5f8c6b4b3ac0be0425a571c..4648217932fcd1d310c88dc807afa8f64f622b45 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
@@ -20,7 +20,7 @@ include "delayed_updating/syntax/path_depth.ma".
 (* Constructions with depth *************************************************)
 
 lemma depth_structure (p):
-      â\9d\98pâ\9d\98 = â\9d\98â\8a\97pâ\9d\98.
+      â\99­p = â\99­â\8a\97p.
 #p elim p -p //
 * [ #n ] #p #IH //
 [ <structure_L_sn <depth_L_sn <depth_L_sn //

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
index 43e634114db60fd29c22830f179bbef666cd96b1..e5a6ea13f100fee50a70a3d77c110baffafcb45d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
@@ -63,11 +63,11 @@ lemma unwind_empty (A) (k) (f):
       k f (𝐞) = ▼{A}❨k, f, 𝐞❩.
 // qed.
 
-lemma unwind_d_empty_sn (A) (k) (n) (f):
+lemma unwind_d_empty (A) (k) (n) (f):
       ▼❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐮❨f@❨n❩❩, 𝐞❩ = ▼{A}❨k, f, 𝗱n◗𝐞❩.
 // qed.
 
-lemma unwind_d_lcons_sn (A) (k) (p) (l) (n) (f):
+lemma unwind_d_lcons (A) (k) (p) (l) (n) (f):
       ▼❨k, 𝐮❨f@❨n❩❩, l◗p❩ = ▼{A}❨k, f, 𝗱n◗l◗p❩.
 // qed.
 
@@ -93,11 +93,11 @@ lemma unwind_path_empty (f):
       (𝐞) = ▼[f]𝐞.
 // qed.
 
-lemma unwind_path_d_empty_sn (f) (n):
+lemma unwind_path_d_empty (f) (n):
       𝗱(f@❨n❩)◗𝐞 = ▼[f](𝗱n◗𝐞).
 // qed.
 
-lemma unwind_path_d_lcons_sn (f) (p) (l) (n):
+lemma unwind_path_d_lcons (f) (p) (l) (n):
       ▼[𝐮❨f@❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p).
 // qed.
 

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma
index 2a03b6831017a561d87df6584247590d426b82b7..8943b733565e233f12bf5e57561ec885b4511d1e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma
@@ -33,9 +33,9 @@ lemma unwind_eq_repl (A) (p) (k1) (k2):
 #A #p @(path_ind_unwind … p) -p [| #n #IH | #n #l0 #q #IH |*: #q #IH ]
 #k1 #k2 #Hk #f1 #f2 #Hf
 [ <unwind_empty <unwind_empty /2 width=1 by/
-| <unwind_d_empty_sn <unwind_d_empty_sn <(tr_pap_eq_repl … Hf)
+| <unwind_d_empty <unwind_d_empty <(tr_pap_eq_repl … Hf)
   /2 width=1 by stream_eq_refl/
-| <unwind_d_lcons_sn <unwind_d_lcons_sn
+| <unwind_d_lcons <unwind_d_lcons
   /5 width=1 by tr_uni_eq_repl, tr_pap_eq_repl, eq_f/ 
 | /2 width=1 by/
 | /3 width=1 by tr_push_eq_repl/
@@ -72,7 +72,7 @@ lemma unwind_path_eq_repl (p):
 lemma unwind_path_append_sn (p) (f) (q):
       q●▼[f]p = ▼❨(λg,p. proj_path g (q●p)), f, p❩.
 #p @(path_ind_unwind … p) -p // [ #n #l #p |*: #p ] #IH #f #q
-[ <unwind_d_lcons_sn <unwind_d_lcons_sn <IH -IH //
+[ <unwind_d_lcons <unwind_d_lcons <IH -IH //
 | <unwind_m_sn <unwind_m_sn //
 | <unwind_L_sn <unwind_L_sn >unwind_lcons_alt // >unwind_append_rcons_sn //
   <IH <IH -IH <list_append_rcons_sn //
@@ -104,8 +104,8 @@ lemma unwind_path_S_sn (f) (p):
 lemma unwind_path_after_id_sn (p) (f):
       ▼[𝐢]▼[f]p = ▼[f]p.
 #p @(path_ind_unwind … p) -p // [ #n | #n #l #p | #p ] #IH #f
-[ <unwind_path_d_empty_sn //
-| <unwind_path_d_lcons_sn //
+[ <unwind_path_d_empty //
+| <unwind_path_d_lcons //
 | <unwind_path_L_sn <unwind_path_L_sn //
 ]
 qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
index 27d369219a13a255fb86a6a36c450ebe5918ecbc..ed025110a54db56bbb60b7f7b96d59fc0ba0d6d7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
@@ -46,7 +46,7 @@ lemma unwind_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
 #p2 #p1 @(path_ind_unwind … p1) -p1 //
 [ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
 [ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
-| <unwind_path_d_lcons_sn <IH //
+| <unwind_path_d_lcons <IH //
 | <unwind_path_m_sn <IH //
 | <unwind_path_L_sn <IH //
 | <unwind_path_A_sn <IH //
@@ -114,9 +114,9 @@ lemma unwind_path_inv_d_sn (k) (q) (p) (f):
 #k #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
-| <unwind_path_d_empty_sn #H destruct -IH
+| <unwind_path_d_empty #H destruct -IH
   /2 width=5 by ex4_2_intro/
-| <unwind_path_d_lcons_sn #H
+| <unwind_path_d_lcons #H
   elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
   /2 width=5 by ex4_2_intro/
 | <unwind_path_m_sn #H
@@ -133,8 +133,8 @@ lemma unwind_path_inv_m_sn (q) (p) (f):
 #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
-| <unwind_path_d_empty_sn #H destruct
-| <unwind_path_d_lcons_sn #H /2 width=2 by/
+| <unwind_path_d_empty #H destruct
+| <unwind_path_d_lcons #H /2 width=2 by/
 | <unwind_path_m_sn #H /2 width=2 by/
 | <unwind_path_L_sn #H destruct
 | <unwind_path_A_sn #H destruct
@@ -148,8 +148,8 @@ lemma unwind_path_inv_L_sn (q) (p) (f):
 #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
-| <unwind_path_d_empty_sn #H destruct
-| <unwind_path_d_lcons_sn #H
+| <unwind_path_d_empty #H destruct
+| <unwind_path_d_lcons #H
   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
 | <unwind_path_m_sn #H
@@ -168,8 +168,8 @@ lemma unwind_path_inv_A_sn (q) (p) (f):
 #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
-| <unwind_path_d_empty_sn #H destruct
-| <unwind_path_d_lcons_sn #H
+| <unwind_path_d_empty #H destruct
+| <unwind_path_d_lcons #H
   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
 | <unwind_path_m_sn #H
@@ -188,8 +188,8 @@ lemma unwind_path_inv_S_sn (q) (p) (f):
 #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
-| <unwind_path_d_empty_sn #H destruct
-| <unwind_path_d_lcons_sn #H
+| <unwind_path_d_empty #H destruct
+| <unwind_path_d_lcons #H
   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
 | <unwind_path_m_sn #H

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma
index c13471e810765e89fa3ff41384172ff8da11fd30..df3423e164aa3107f8d5c2407ccc6581b315e20b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma
@@ -22,7 +22,7 @@ include "ground/arith/nat_pred_succ.ma".
 (* Basic constructions with structure and depth ****************************)
 
 lemma unwind_rmap_structure (p) (f):
-      (⫯*[â\9d\98pâ\9d\98]f) = ▼[⊗p]f.
+      (⫯*[â\99­p]f) = ▼[⊗p]f.
 #p elim p -p //
 * [ #n ] #p #IH #f //
 [ <unwind_rmap_A_sn //

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 2ec69e63f23b7b0e55cbc6ea927b3c9e871e8d44..92cb18cfac13d75ee81c0660b959b9ac473f1786 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1537,7 +1537,7 @@ let predefined_classes = [
  ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ;
  ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
  ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; "𝗔"; ] ;
- ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;
+ ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; "♭"; ] ;
  ["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁"; "Ⓑ"; ] ;
  ["c"; "𝕔"; "𝐜"; "ⓒ"; ] ;
  ["C"; "ℭ"; "∁"; "𝐂"; "ℂ"; "Ⓒ"; ] ;