From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 25 May 2022 18:38:32 +0000 (+0200)
Subject: update in ground and delayed_updating
X-Git-Tag: make_still_working~67
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=12d58352dbd62df65d44becc0f69fc5a7b370866;p=helm.git

update in ground and delayed_updating

+ main theorem about dfr proved!
+ ground: duplicated lemma removed
+ some refactoring
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/downarrowrightsharp_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/downarrowrightsharp_2.etc
new file mode 100644
index 000000000..171107d6b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/downarrowrightsharp_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( ↳⧣[ term 46 n ] break term 70 p )"
+  non associative with precedence 70
+  for @{ 'DownArrowRightSharp $n $p }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd.etc
new file mode 100644
index 000000000..f45fd1f69
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd.etc
@@ -0,0 +1,70 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/path_labels.ma".
+include "delayed_updating/notation/functions/downarrowrightsharp_2.ma".
+include "ground/arith/pnat_plus.ma".
+
+(* HEAD BY DEPTH FOR PATH ***************************************************)
+
+rec definition path_dhd (m) (p) on p: path ≝
+match p with
+[ list_empty     ⇒ 𝗟∗∗m
+| list_lcons l q ⇒
+  match l with
+  [ label_d n ⇒ l◗(path_dhd (m+n) q)
+  | label_m   ⇒ l◗(path_dhd m q)
+  | label_L   ⇒
+    match m with
+    [ punit   ⇒ l◗𝐞
+    | psucc o ⇒ l◗(path_dhd o q)
+    ]
+  | label_A   ⇒ l◗(path_dhd m q)
+  | label_S   ⇒ l◗(path_dhd m q)
+  ]
+].
+
+interpretation
+  "head by depth (reversed path)"
+  'DownArrowRightSharp n p = (path_dhd n p).
+
+(* basic constructions ****************************************************)
+
+lemma path_dhd_empty (n:pnat):
+      (𝗟∗∗n) = ↳⧣[n]𝐞.
+// qed.
+
+lemma path_dhd_d_sn (p) (n) (m):
+      (𝗱m◗↳⧣[n+m]p) = ↳⧣[n](𝗱m◗p).
+// qed.
+
+lemma path_dhd_m_sn (p) (n):
+      (𝗺◗↳⧣[n]p) = ↳⧣[n](𝗺◗p).
+// qed.
+
+lemma path_dhd_L_sn_unit (p):
+      (𝗟◗𝐞) = ↳⧣[𝟏](𝗟◗p).
+// qed.
+
+lemma path_dhd_L_sn_succ (p) (n):
+      (𝗟◗↳⧣[n]p) = ↳⧣[↑n](𝗟◗p).
+// qed.
+
+lemma path_dhd_A_sn (p) (n):
+      (𝗔◗↳⧣[n]p) = ↳⧣[n](𝗔◗p).
+// qed.
+
+lemma path_dhd_S_sn (p) (n):
+      (𝗦◗↳⧣[n]p) = ↳⧣[n](𝗦◗p).
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd_structure.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd_structure.etc
new file mode 100644
index 000000000..468d7167a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd_structure.etc
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/path_dhd.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_depth.ma".
+
+(* HEAD BY DEPTH FOR PATH ***************************************************)
+
+(* Constructions with structure *********************************************)
+
+lemma path_dhd_structure_L_sn (p) (q):
+      let r ≝ 𝗟◗p in 
+      ⊗r = ↳⧣[♭⊗r]((⊗r)●q).
+#p elim p -p //
+* [ #n ] #p #IH #q //
+  [ <structure_L_sn //
+  | <structure_A_sn <list_append_lcons_sn 
+    <path_head_A_sn //
+  | <structure_S_sn //
+  ]
+]
+*)
\ No newline at end of file
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 b4ccad9d3..8403b7781 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -39,11 +39,9 @@ theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
 #f #p #q #t1 #t2 #H0t1
 * #n * #H1n #Ht1 #Ht2
 @(ex_intro … (↑♭⊗q)) @and3_intro
-[ -H0t1 -H1n -Ht1 -Ht2
-  >list_append_rcons_sn <reverse_append
-  >nsucc_unfold >depth_reverse >depth_L_dx >reverse_lcons
+[ -H0t1 -Ht1 -Ht2
   >structure_L_sn >structure_reverse
-  <path_head_structure //
+  >H1n >path_head_structure_depth <H1n -H1n //
 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1
   <unwind2_path_d_dx <depth_structure
   >list_append_rcons_sn in H1n; <reverse_append #H1n
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma
index 32138ee12..c561797c1 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path_head.ma".
-include "delayed_updating/syntax/path_depth_labels.ma".
 include "delayed_updating/syntax/path_height_labels.ma".
+include "delayed_updating/syntax/path_depth_labels.ma".
 
 (* HEAD FOR PATH ************************************************************)
 
@@ -32,4 +32,4 @@ cases l [ #m ]
 | <path_head_A_sn <height_A_sn <depth_A_sn //
 | <path_head_S_sn <height_S_sn <depth_S_sn //
 ]
-qed.
+qed-. (**) (* gets in the way with auto *)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_structure.ma
index c97fbfb2e..e1605752c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_structure.ma
@@ -12,26 +12,28 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/syntax/path_head.ma".
-include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/syntax/path_depth.ma".
+include "delayed_updating/syntax/path_head_depth.ma".
+include "delayed_updating/syntax/path_structure_labels.ma".
 
 (* HEAD FOR PATH ************************************************************)
 
 (* Constructions with structure *********************************************)
 
-axiom path_head_structure (p) (q):
-      ⊗p = ↳[♭⊗p]((⊗p)●q).
-(*
-#p elim p -p
-[ #q <path_head_zero //
-| * [ #n ] #p #IH #q
-  [ <structure_d_sn //
-  | <structure_m_sn //
-  | <structure_L_sn
-  | <structure_A_sn <list_append_lcons_sn 
-    <path_head_A_sn //
-  | <structure_S_sn //
-  ]
+lemma path_head_structure_height (p) (m):
+      ⊗↳[m]p = ↳[m+♯↳[m]p]⊗p.
+#p elim p -p //
+#l #p #IH #m @(nat_ind_succ … m) -m //
+#m #_ cases l [ #n ]
+[ <height_d_sn <structure_d_sn //
+| <structure_m_sn //
+| <structure_L_sn //
+| <height_A_sn <structure_A_sn <nplus_succ_sn <path_head_A_sn //
+| <height_S_sn <structure_S_sn <nplus_succ_sn <path_head_S_sn //
 ]
-*)
\ No newline at end of file
+qed.
+
+lemma path_head_structure_depth (p) (m):
+      ⊗↳[m]p = ↳[♭↳[m]p]⊗p.
+#p #m
+<path_head_depth //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_labels.ma
new file mode 100644
index 000000000..0dcc367cd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_labels.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/path_structure.ma".
+include "delayed_updating/syntax/path_labels.ma".
+
+(* STRUCTURE FOR PATH *******************************************************)
+
+(* Constructions with labels ************************************************)
+
+lemma structure_labels_L (n):
+      (𝗟∗∗n) = ⊗(𝗟∗∗n).
+#n @(nat_ind_succ … n) -n //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
deleted file mode 100644
index 985b3ae26..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
+++ /dev/null
@@ -1,51 +0,0 @@
-include "ground/relocation/tr_uni_pap.ma".
-include "ground/relocation/tr_compose_pap.ma".
-include "ground/notation/functions/applysucc_2.ma".
-include "ground/arith/nat_lt.ma".
-include "ground/arith/nat_plus_rplus.ma".
-include "ground/arith/nat_pred_succ.ma".
-
-lemma nlt_npsucc_bi (n1) (n2):
-      n1 < n2 → npsucc n1 < npsucc n2.
-#n1 #n2 #Hn elim Hn -n2 //
-#n2 #_ #IH /2 width=1 by plt_succ_dx_trans/
-qed.
-
-definition tr_nap (f) (l:nat): nat ≝
-           ↓(f＠⧣❨↑l❩).
-
-interpretation
-  "functional non-negative application (total relocation maps)"
-  'ApplySucc f l = (tr_nap f l).
-
-lemma tr_nap_unfold (f) (l):
-      ↓(f＠⧣❨↑l❩) = f@↑❨l❩.
-// qed.
-
-lemma tr_compose_nap (f2) (f1) (l):
-      f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩.
-#f2 #f1 #l
-<tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
-<tr_compose_pap <npsucc_pred //
-qed.
-
-lemma tr_uni_nap (n) (m):
-      m + n = 𝐮❨n❩@↑❨m❩.
-#n #m
-<tr_nap_unfold
-<tr_uni_pap <nrplus_npsucc_sn //
-qed.
-
-lemma tr_nap_push (f):
-      ∀l. ↑(f@↑❨l❩) = (⫯f)@↑❨↑l❩.
-#f #l
-<tr_nap_unfold <tr_nap_unfold
-<tr_pap_push <pnpred_psucc //
-qed.
-
-lemma tr_nap_pushs_lt (f) (n) (m):
-      m < n → m = (⫯*[n]f)@↑❨m❩.
-#f #n #m #Hmn
-<tr_nap_unfold <tr_pap_pushs_le
-/2 width=1 by nlt_npsucc_bi/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
index b7fc5664c..cd21acf66 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
@@ -14,8 +14,8 @@
 
 include "delayed_updating/unwind/unwind2_rmap_labels.ma".
 include "delayed_updating/unwind/unwind2_rmap_eq.ma".
-include "delayed_updating/unwind/xap.ma".
 include "delayed_updating/syntax/path_head_depth.ma".
+include "ground/relocation/xap.ma".
 include "ground/lib/stream_eq_eq.ma".
 include "ground/arith/nat_le_plus.ma".
 
@@ -93,7 +93,8 @@ lemma unwind2_rmap_append_pap_closed (f) (p) (q) (n:pnat):
       ♭p = ninj (▶[f](p●q)＠⧣❨n❩).
 #f #p #q #n #Hn
 >tr_xap_ninj >Hn in ⊢ (??%?);
->(unwind2_rmap_head_append_xap_closed … Hn) -Hn //
+>(unwind2_rmap_head_append_xap_closed … Hn) -Hn
+<path_head_depth //
 qed.
 
 lemma tls_unwind2_rmap_plus_closed (f) (p) (q) (n) (k):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/xap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/xap.ma
deleted file mode 100644
index f10ced5d6..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/xap.ma
+++ /dev/null
@@ -1,55 +0,0 @@
-include "delayed_updating/unwind/nap.ma".
-include "ground/notation/functions/apply_2.ma".
-include "ground/relocation/tr_compose_pn.ma".
-
-definition tr_xap (f) (l:nat): nat ≝
-           (⫯f)@↑❨l❩.
-
-interpretation
-  "functional extended application (total relocation maps)"
-  'Apply f l = (tr_xap f l).
-
-lemma tr_xap_unfold (f) (l):
-      (⫯f)@↑❨l❩ = f＠❨l❩.
-// qed.
-
-lemma tr_xap_zero (f):
-      (𝟎) = f＠❨𝟎❩.
-// qed.
-
-lemma tr_xap_ninj (f) (p):
-      ninj (f＠⧣❨p❩) = f＠❨ninj p❩.
-// qed.
-
-lemma tr_compose_xap (f2) (f1) (l):
-      f2＠❨f1＠❨l❩❩ = (f2∘f1)＠❨l❩.
-#f2 #f1 #l
-<tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
->tr_compose_nap >tr_compose_push_bi //
-qed.
-
-lemma tr_uni_xap_succ (n) (m):
-      ↑m + n = 𝐮❨n❩＠❨↑m❩.
-#n #m
-<tr_xap_unfold
-<tr_nap_push <tr_uni_nap //
-qed.
-
-lemma tr_uni_xap (n) (m):
-      𝐮❨n❩＠❨m❩ ≤ m+n.
-#n #m @(nat_ind_succ … m) -m //
-qed.
-
-lemma tr_xap_push (f) (l):
-      ↑(f＠❨l❩) = (⫯f)＠❨↑l❩.
-#f #l
-<tr_xap_unfold <tr_xap_unfold
-<tr_nap_push //
-qed.
-
-lemma tr_xap_pushs_le (f) (n) (m):
-      m ≤ n → m = (⫯*[n]f)＠❨m❩.
-#f #n #m #Hmn
-<tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
-/2 width=1 by nlt_succ_dx/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_succ.ma
index 3c280acb0..d7dfaa1aa 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_succ.ma
@@ -26,9 +26,6 @@ qed.
 lemma nrplus_succ_shift (p) (n): ↑p + n = p + ↑n.
 // qed.
 
-lemma nrplus_succ_sn (p) (n): ↑(p+n) = ↑p + n.
-// qed.
-
 lemma nrplus_unit_sn (n): ↑n = 𝟏 + n.
 #n @(nat_ind_succ … n) -n //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
new file mode 100644
index 000000000..985b3ae26
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
@@ -0,0 +1,51 @@
+include "ground/relocation/tr_uni_pap.ma".
+include "ground/relocation/tr_compose_pap.ma".
+include "ground/notation/functions/applysucc_2.ma".
+include "ground/arith/nat_lt.ma".
+include "ground/arith/nat_plus_rplus.ma".
+include "ground/arith/nat_pred_succ.ma".
+
+lemma nlt_npsucc_bi (n1) (n2):
+      n1 < n2 → npsucc n1 < npsucc n2.
+#n1 #n2 #Hn elim Hn -n2 //
+#n2 #_ #IH /2 width=1 by plt_succ_dx_trans/
+qed.
+
+definition tr_nap (f) (l:nat): nat ≝
+           ↓(f＠⧣❨↑l❩).
+
+interpretation
+  "functional non-negative application (total relocation maps)"
+  'ApplySucc f l = (tr_nap f l).
+
+lemma tr_nap_unfold (f) (l):
+      ↓(f＠⧣❨↑l❩) = f@↑❨l❩.
+// qed.
+
+lemma tr_compose_nap (f2) (f1) (l):
+      f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩.
+#f2 #f1 #l
+<tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
+<tr_compose_pap <npsucc_pred //
+qed.
+
+lemma tr_uni_nap (n) (m):
+      m + n = 𝐮❨n❩@↑❨m❩.
+#n #m
+<tr_nap_unfold
+<tr_uni_pap <nrplus_npsucc_sn //
+qed.
+
+lemma tr_nap_push (f):
+      ∀l. ↑(f@↑❨l❩) = (⫯f)@↑❨↑l❩.
+#f #l
+<tr_nap_unfold <tr_nap_unfold
+<tr_pap_push <pnpred_psucc //
+qed.
+
+lemma tr_nap_pushs_lt (f) (n) (m):
+      m < n → m = (⫯*[n]f)@↑❨m❩.
+#f #n #m #Hmn
+<tr_nap_unfold <tr_pap_pushs_le
+/2 width=1 by nlt_npsucc_bi/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
new file mode 100644
index 000000000..18bcec6a9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
@@ -0,0 +1,55 @@
+include "ground/relocation/nap.ma".
+include "ground/notation/functions/apply_2.ma".
+include "ground/relocation/tr_compose_pn.ma".
+
+definition tr_xap (f) (l:nat): nat ≝
+           (⫯f)@↑❨l❩.
+
+interpretation
+  "functional extended application (total relocation maps)"
+  'Apply f l = (tr_xap f l).
+
+lemma tr_xap_unfold (f) (l):
+      (⫯f)@↑❨l❩ = f＠❨l❩.
+// qed.
+
+lemma tr_xap_zero (f):
+      (𝟎) = f＠❨𝟎❩.
+// qed.
+
+lemma tr_xap_ninj (f) (p):
+      ninj (f＠⧣❨p❩) = f＠❨ninj p❩.
+// qed.
+
+lemma tr_compose_xap (f2) (f1) (l):
+      f2＠❨f1＠❨l❩❩ = (f2∘f1)＠❨l❩.
+#f2 #f1 #l
+<tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
+>tr_compose_nap >tr_compose_push_bi //
+qed.
+
+lemma tr_uni_xap_succ (n) (m):
+      ↑m + n = 𝐮❨n❩＠❨↑m❩.
+#n #m
+<tr_xap_unfold
+<tr_nap_push <tr_uni_nap //
+qed.
+
+lemma tr_uni_xap (n) (m):
+      𝐮❨n❩＠❨m❩ ≤ m+n.
+#n #m @(nat_ind_succ … m) -m //
+qed.
+
+lemma tr_xap_push (f) (l):
+      ↑(f＠❨l❩) = (⫯f)＠❨↑l❩.
+#f #l
+<tr_xap_unfold <tr_xap_unfold
+<tr_nap_push //
+qed.
+
+lemma tr_xap_pushs_le (f) (n) (m):
+      m ≤ n → m = (⫯*[n]f)＠❨m❩.
+#f #n #m #Hmn
+<tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
+/2 width=1 by nlt_succ_dx/
+qed-.