rtmap (platform-indepent multple relocation): application and composition

diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/complement_1.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/complement_1.etc
new file mode 100644 (file)
index 0000000..a10c80f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/complement_1.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( ∁ term 70 t )"
+   non associative with precedence 70
+   for @{ 'Complement $t }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/isuniform_1.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/isuniform_1.etc
new file mode 100644 (file)
index 0000000..349f2b3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/isuniform_1.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( 𝐔 ⦃ term 46 f ⦄ )"
+   non associative with precedence 45
+   for @{ 'IsUniform $f }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/norm_1.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/norm_1.etc
new file mode 100644 (file)
index 0000000..d0f0719
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/norm_1.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox ( ∥ term 19 C ∥ )"
+  with precedence 70
+  for @{ 'Norm $C }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/runion_3.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/runion_3.etc
new file mode 100644 (file)
index 0000000..16120c0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/runion_3.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( L1 ⋓ break term 46 L2 ≡ break term 46 L )"
+   non associative with precedence 45
+   for @{ 'RUnion $L1 $L2 $L }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
index bdc740c82ff42646cbd6fb362c6ac714fa731cf3..050568754f5edc111fb8ccf948c73fc5fb34cfac 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/notation/functions/drop_1.ma".
 include "ground_2/lib/streams.ma".
 include "ground_2/lib/arith.ma".
 
@@ -23,17 +24,16 @@ definition hd (A:Type[0]): stream A → A ≝
 definition tl (A:Type[0]): stream A → stream A ≝
               λt. match t with [ seq _ t ⇒ t ].
 
-let rec tln (A:Type[0]) (i:nat) on i: stream A → stream A ≝ ?.
-cases i -i [ #t @t | #i * #_ #t @(tln … i t) ]
-qed.
+interpretation "tail (streams)" 'Drop t = (tl ? t).
 
 (* basic properties *********************************************************)
 
-lemma eq_stream_split (A) (t): (hd … t) @ (tl … t) ≐⦋A⦌ t.
-#A * //
-qed.
+lemma hd_rew (A) (a) (t): a = hd A (a@t).
+// qed.
 
-lemma tln_eq_repl (A) (i): eq_stream_repl A (λt1,t2. tln … i t1 ≐ tln … i t2).
-#A #i elim i -i //
-#i #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 by/
+lemma tl_rew (A) (a) (t): t = tl A (a@t).
+// qed.
+
+lemma eq_stream_split (A) (t): (hd … t) @ ↓t ≐⦋A⦌ t.
+#A * //
 qed.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/complement_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/complement_1.ma
deleted file mode 100644 (file)
index a10c80f..0000000
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/complement_1.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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( ∁ term 70 t )"
-   non associative with precedence 70
-   for @{ 'Complement $t }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppred_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppred_1.ma
new file mode 100644 (file)
index 0000000..7e82080
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppred_1.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( ⫱ term 46 T )"
+   non associative with precedence 46
+   for @{ 'DropPred $T }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppreds_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppreds_2.ma
new file mode 100644 (file)
index 0000000..1b10938
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppreds_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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( ⫱ * [ term 46 n ] term 46 T )"
+   non associative with precedence 46
+   for @{ 'DropPreds $n $T }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drops_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drops_2.ma
new file mode 100644 (file)
index 0000000..9b20a43
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drops_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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( ↓ * [ term 46 n ] term 46 T )"
+   non associative with precedence 46
+   for @{ 'Drops $n $T }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/norm_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/norm_1.ma
deleted file mode 100644 (file)
index d0f0719..0000000
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/norm_1.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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox ( ∥ term 19 C ∥ )"
-  with precedence 70
-  for @{ 'Norm $C }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma
deleted file mode 100644 (file)
index 349f2b3..0000000
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( 𝐔 ⦃ term 46 f ⦄ )"
-   non associative with precedence 45
-   for @{ 'IsUniform $f }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rintersection_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rintersection_3.ma
new file mode 100644 (file)
index 0000000..c680542
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rintersection_3.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( L1 ⋒ break term 46 L2 ≡ break term 46 L )"
+   non associative with precedence 45
+   for @{ 'RIntersection $L1 $L2 $L }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma
deleted file mode 100644 (file)
index 16120c0..0000000
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( L1 ⋓ break term 46 L2 ≡ break term 46 L )"
-   non associative with precedence 45
-   for @{ 'RUnion $L1 $L2 $L }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
index aaa1ba9b6551f67099861a199fdf067f9169e558..8d7dacc4ed7632a7270f33473076f238b6c20601 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
@@ -13,8 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/notation/functions/lift_1.ma".
-include "ground_2/lib/arith.ma".
-include "ground_2/lib/streams.ma".
+include "ground_2/lib/streams_tls.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
@@ -88,3 +87,11 @@ lemma iota_push: ∀R,a,b,f. a f = case_type0 R a b (↑f).
 lemma iota_next: ∀R,a,b,f. b f = case_type0 R a b (⫯f).
 #R #a #b * //
 qed.
+
+(* Specific properties ******************************************************)
+
+lemma tl_push: ∀f. f = ↓↑f.
+// qed.
+
+lemma tl_next: ∀f. ↓f = ↓⫯f.
+* // qed.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
index b599e03cc5d1cfaa88eadeb4c372b855335b0932..a9b022b4df88a995edfcc217f22b83e32046df69 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
@@ -12,82 +12,69 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/relations/rafter_3.ma".
-include "ground_2/lib/streams_hdtl.ma".
-include "ground_2/relocation/nstream_at.ma".
+include "ground_2/relocation/nstream_istot.ma".
+include "ground_2/relocation/rtmap_after.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
 let corec compose: rtmap → rtmap → rtmap ≝ ?.
 #f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2
-@(tln … (⫯n2) f1)
+@(↓*[⫯n2] f1)
 defined.
 
 interpretation "functional composition (nstream)"
    'compose f1 f2 = (compose f1 f2).
 
-coinductive after: relation3 rtmap rtmap rtmap ≝
-| after_refl: ∀f1,f2,f,g1,g2,g.
-              after f1 f2 f → g1 = ↑f1 → g2 = ↑f2 → g = ↑f → after g1 g2 g
-| after_push: ∀f1,f2,f,g1,g2,g.
-              after f1 f2 f → g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → after g1 g2 g
-| after_next: ∀f1,f2,f,g1,g.
-              after f1 f2 f → g1 = ⫯f1 → g = ⫯f → after g1 f2 g
-.
-
-interpretation "relational composition (nstream)"
-   'RAfter f1 f2 f = (after f1 f2 f).
-
 (* Basic properies on compose ***********************************************)
 
-lemma compose_unfold: ∀f1,f2,n2. f1∘(n2@f2) = f1@❴n2❵@tln … (⫯n2) f1∘f2.
-#f1 #f2 #n2 >(stream_expand … (f1∘(n2@f2))) normalize //
+lemma compose_rew: ∀f1,f2,n2. f1@❴n2❵@(↓*[⫯n2]f1)∘f2 = f1∘(n2@f2).
+#f1 #f2 #n2 <(stream_rew … (f1∘(n2@f2))) normalize //
 qed.
 
 lemma compose_next: ∀f1,f2,f. f1∘f2 = f → (⫯f1)∘f2 = ⫯f.
-* #n1 #f1 * #n2 #f2 #f >compose_unfold >compose_unfold
-#H destruct normalize //
+#f1 * #n2 #f2 #f <compose_rew <compose_rew
+* -f <tls_S1 /2 width=1 by eq_f2/
 qed.
 
 (* Basic inversion lemmas on compose ****************************************)
 
-lemma compose_inv_unfold: ∀f1,f2,f,n2,n. f1∘(n2@f2) = n@f →
-                          f1@❴n2❵ = n ∧ tln … (⫯n2) f1∘f2 = f.
-#f1 #f2 #f #n2 #n >(stream_expand … (f1∘(n2@f2))) normalize
+lemma compose_inv_rew: ∀f1,f2,f,n2,n. f1∘(n2@f2) = n@f →
+                       f1@❴n2❵ = n ∧ (↓*[⫯n2]f1)∘f2 = f.
+#f1 #f2 #f #n2 #n <(stream_rew … (f1∘(n2@f2))) normalize
 #H destruct /2 width=1 by conj/
 qed-.
 
 lemma compose_inv_O2: ∀f1,f2,f,n1,n. (n1@f1)∘(↑f2) = n@f →
-                      n = n1 ∧ f1∘f2 = f.
-#f1 #f2 #f #n1 #n >compose_unfold
+                      n1 = n ∧ f1∘f2 = f.
+#f1 #f2 #f #n1 #n <compose_rew
 #H destruct /2 width=1 by conj/
 qed-.
 
 lemma compose_inv_S2: ∀f1,f2,f,n1,n2,n. (n1@f1)∘(⫯n2@f2) = n@f →
-                      n = ⫯(n1+f1@❴n2❵) ∧ f1∘(n2@f2) = f1@❴n2❵@f.
-#f1 #f2 #f #n1 #n2 #n >compose_unfold
-#H destruct /2 width=1 by conj/
+                      ⫯(n1+f1@❴n2❵) = n ∧ f1∘(n2@f2) = f1@❴n2❵@f.
+#f1 #f2 #f #n1 #n2 #n <compose_rew
+#H destruct <tls_S1 /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_S1: ∀f1,f2,f,n1,n2,n. (⫯n1@f1)∘(n2@f2) = n@f →
-                      n = ⫯((n1@f1)@❴n2❵) ∧ (n1@f1)∘(n2@f2) = (n1@f1)@❴n2❵@f.
-#f1 #f2 #f #n1 #n2 #n >compose_unfold
-#H destruct /2 width=1 by conj/
+lemma compose_inv_S1: ∀f1,f2,f,n2,n. (⫯f1)∘(n2@f2) = n@f →
+                      ⫯(f1@❴n2❵) = n ∧ f1∘(n2@f2) = f1@❴n2❵@f.
+#f1 #f2 #f #n2 #n <compose_rew
+#H destruct <tls_S1 /2 width=1 by conj/
 qed-.
 
-(* Basic properties on after ************************************************)
+(* Specific properties ******************************************************)
 
 lemma after_O2: ∀f1,f2,f. f1 ⊚ f2 ≡ f →
                 ∀n. n@f1 ⊚ ↑f2 ≡ n@f.
-#f1 #f2 #f #Ht #n elim n -n /2 width=7 by after_refl, after_next/
+#f1 #f2 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
 qed.
 
 lemma after_S2: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f →
                 ∀n1. n1@f1 ⊚ ⫯n2@f2 ≡ ⫯(n1+n)@f.
-#f1 #f2 #f #n2 #n #Ht #n1 elim n1 -n1 /2 width=7 by after_next, after_push/
+#f1 #f2 #f #n2 #n #Hf #n1 elim n1 -n1 /2 width=7 by after_next, after_push/
 qed.
 
-lemma after_apply: ∀n2,f1,f2,f. (tln … (⫯n2) f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ≡ f1@❴n2❵@f.
+lemma after_apply: ∀n2,f1,f2,f. (↓*[⫯n2] f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ≡ f1@❴n2❵@f.
 #n2 elim n2 -n2
 [ * /2 width=1 by after_O2/
 | #n2 #IH * /3 width=1 by after_S2/
@@ -97,405 +84,67 @@ qed-.
 let corec after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f ≝ ?.
 * #n1 #f1 * #n2 #f2 * #n #f cases n1 -n1
 [ cases n2 -n2
-  [ #H cases (compose_inv_O2 … H) -H
-    /3 width=7 by after_refl, eq_f2/
-  | #n2 #H cases (compose_inv_S2 … H) -H
-    /3 width=7 by after_push/
+  [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
+  | #n2 #H cases (compose_inv_S2 … H) -H * -n /3 width=7 by after_push/
   ]
-| #n1 #H cases (compose_inv_S1 … H) -H
-  /4 width=7 by after_next, next_rew_sn/
+| #n1 >next_rew #H cases (compose_inv_S1 … H) -H * -n /3 width=7 by after_next/
 ]
 qed-.
 
 theorem after_total: ∀f2,f1. f1 ⊚ f2 ≡ f1 ∘ f2.
 /2 width=1 by after_total_aux/ qed.
 
-(* Basic inversion lemmas on after ******************************************)
-
-fact after_inv_OOx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ↑f2 →
-                        ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f.
-#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
-[ #g2 #g #Hf #H1 #H2 #H #x1 #x2 #Hx1 #Hx2 destruct
-  <(injective_push … Hx1) <(injective_push … Hx2) -x2 -x1
-  /2 width=3 by ex2_intro/
-| #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
-  elim (discr_next_push … Hx2)
-| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
-  elim (discr_next_push … Hx1)
-]
-qed-.
-
-lemma after_inv_OOx: ∀f1,f2,g. ↑f1 ⊚ ↑f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f.
-/2 width=5 by after_inv_OOx_aux/ qed-.
-
-fact after_inv_OSx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ⫯f2 →
-                        ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
-#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
-[ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
-  elim (discr_push_next … Hx2)
-| #g2 #g #Hf #H1 #H2 #H3 #x1 #x2 #Hx1 #Hx2 destruct
-  <(injective_push … Hx1) <(injective_next … Hx2) -x2 -x1
-  /2 width=3 by ex2_intro/
-| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
-  elim (discr_next_push … Hx1)
-]
-qed-.
-
-lemma after_inv_OSx: ∀f1,f2,g. ↑f1 ⊚ ⫯f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
-/2 width=5 by after_inv_OSx_aux/ qed-.
-
-fact after_inv_Sxx_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g → ∀f1. g1 = ⫯f1 →
-                        ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
-#g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1
-[ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
-  elim (discr_push_next … Hx1)
-| #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
-  elim (discr_push_next … Hx1)
-| #g #Hf #H1 #H #x1 #Hx1 destruct
-  <(injective_next … Hx1) -x1
-  /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma after_inv_Sxx: ∀f1,f2,g. ⫯f1 ⊚ f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
-/2 width=5 by after_inv_Sxx_aux/ qed-.
-
-(* Advanced inversion lemmas on after ***************************************)
-
-fact after_inv_OOO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
-                        ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ↑f → f1 ⊚ f2 ≡ f.
-#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
-#x #Hf #Hx destruct >(injective_push … Hx) -f //
-qed-.
-
-fact after_inv_OOS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
-                        ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ⫯f → ⊥.
-#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
-#x #Hf #Hx destruct elim (discr_next_push … Hx)
-qed-.
-
-fact after_inv_OSS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
-                        ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → f1 ⊚ f2 ≡ f.
-#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
-#x #Hf #Hx destruct >(injective_next … Hx) -f //
-qed-.
-
-fact after_inv_OSO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
-                        ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ↑f → ⊥.
-#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
-#x #Hf #Hx destruct elim (discr_push_next … Hx)
-qed-.
-
-fact after_inv_SxS_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g →
-                        ∀f1,f. g1 = ⫯f1 → g = ⫯f → f1 ⊚ f2 ≡ f.
-#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1
-#x #Hf #Hx destruct >(injective_next … Hx) -f //
-qed-.
-
-fact after_inv_SxO_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g →
-                        ∀f1,f. g1 = ⫯f1 → g = ↑f → ⊥.
-#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1
-#x #Hf #Hx destruct elim (discr_push_next … Hx)
-qed-.
-
-fact after_inv_OxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
-                        ∀f1,f. g1 = ↑f1 → g = ↑f →
-                        ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2.
-#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H
-[ elim (after_inv_OSO_aux … Hg … H1 … H) -g1 -g -f1 -f //
-| lapply (after_inv_OOO_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/
-]
-qed-.
+(* Specific inversion lemmas ************************************************)
 
-lemma after_inv_OxO: ∀f1,g2,f. ↑f1 ⊚ g2 ≡ ↑f →
-                     ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2.
-/2 width=5 by after_inv_OxO_aux/ qed-.
-
-fact after_inv_OxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
-                        ∀f1,f. g1 = ↑f1 → g = ⫯f →
-                        ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ⫯f2.
-#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H
-[ lapply (after_inv_OSS_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/
-| elim (after_inv_OOS_aux … Hg … H1 … H) -g1 -g -f1 -f // 
-]
-qed-.
-
-fact after_inv_xxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ↑f →
-                        ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2.
-* * [2: #m1 ] #g1 #g2 #g #Hg #f #H
-[ elim (after_inv_SxO_aux … Hg … H) -g2 -g -f //
-| elim (after_inv_OxO_aux … Hg … H) -g /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma after_inv_xxO: ∀g1,g2,f. g1 ⊚ g2 ≡ ↑f →
-                     ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2.
-/2 width=3 by after_inv_xxO_aux/ qed-.
-
-fact after_inv_xxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ⫯f →
-                        (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨
-                        ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1.
-* * [2: #m1 ] #g1 #g2 #g #Hg #f #H
-[ /4 width=5 by after_inv_SxS_aux, or_intror, ex2_intro/
-| elim (after_inv_OxS_aux … Hg … H) -g
-  /3 width=5 by or_introl, ex3_2_intro/
-]
-qed-.
-
-lemma after_inv_xxS: ∀g1,g2,f. g1 ⊚ g2 ≡ ⫯f →
-                     (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨
-                     ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1.
-/2 width=3 by after_inv_xxS_aux/ qed-.
-
-fact after_inv_Oxx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1. g1 = ↑f1 →
-                        (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ↑f2 & g = ↑f) ∨
-                        (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ⫯f2 & g = ⫯f).
-#g1 * * [2: #m2 ] #g2 #g #Hg #f1 #H
-[  elim (after_inv_OSx_aux … Hg … H) -g1
-  /3 width=5 by or_intror, ex3_2_intro/
-| elim (after_inv_OOx_aux … Hg … H) -g1
-  /3 width=5 by or_introl, ex3_2_intro/
-]
-qed-.
-
-lemma after_inv_Oxx: ∀f1,g2,g. ↑f1 ⊚ g2 ≡ g →
-                     (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ↑f2 & g = ↑f) ∨
-                     (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ⫯f2 & g = ⫯f).
-/2 width=3 by after_inv_Oxx_aux/ qed-.
-
-fact after_inv_xOx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ↑f2 →
-                        f1 ⊚ f2 ≡ f ∧ n1 = n.
+lemma after_inv_xpx: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. ↑f2 = g2 →
+                     f1 ⊚ f2 ≡ f ∧ n1 = n.
 #f1 #g2 #f #n1 elim n1 -n1
-[ #n #Hf #f2 #H2 elim (after_inv_OOx_aux … Hf … H2) -g2 [3: // |2: skip ]
-  #g #Hf #H elim (push_inv_seq_sn … H) -H destruct /2 width=1 by conj/
-| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_Sxx_aux … Hf) -Hf [3: // |2: skip ]
-  #g1 #Hg #H1 elim (next_inv_seq_sn … H1) -H1
-  #x #Hx #H destruct elim (IH … Hg) [2: // |3: skip ] -IH -Hg
+[ #n #Hf #f2 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ]
+  #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
+| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
+  #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
+  #x #Hx #H destruct elim (IH … Hg) [2,3: // ] -IH -Hg
   #H destruct /2 width=1 by conj/
 ]
 qed-.
 
-lemma after_inv_xOx: ∀f1,f2,f,n1,n. n1@f1 ⊚ ↑f2 ≡ n@f →
-                     f1 ⊚ f2 ≡ f ∧ n1 = n.
-/2 width=3 by after_inv_xOx_aux/ qed-.
-
-fact after_inv_xSx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ⫯f2 →
-                        ∃∃m. f1 ⊚ f2 ≡ m@f & n = ⫯(n1+m).
+lemma after_inv_xnx: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. ⫯f2 = g2 →
+                     ∃∃m. f1 ⊚ f2 ≡ m@f & ⫯(n1+m) = n.
 #f1 #g2 #f #n1 elim n1 -n1
-[ #n #Hf #f2 #H2 elim (after_inv_OSx_aux … Hf … H2) -g2 [3: // |2: skip ]
-  #g #Hf #H elim (next_inv_seq_sn … H) -H
+[ #n #Hf #f2 #H2 elim (after_inv_pnx … Hf … H2) -g2 [2,3: // ]
+  #g #Hf #H elim (next_inv_seq_dx … H) -H
   #x #Hx #Hg destruct /2 width=3 by ex2_intro/
-| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_Sxx_aux … Hf) -Hf [3: // |2: skip ]
-  #g #Hg #H elim (next_inv_seq_sn … H) -H
-  #x #Hx #H destruct elim (IH … Hg) -IH -Hg [3: // |2: skip ]
+| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
+  #g #Hg #H elim (next_inv_seq_dx … H) -H
+  #x #Hx #H destruct elim (IH … Hg) -IH -Hg [2,3: // ]
   #m #Hf #Hm destruct /2 width=3 by ex2_intro/
 ]
 qed-.
 
-lemma after_inv_xSx: ∀f1,f2,f,n1,n. n1@f1 ⊚ ⫯f2 ≡ n@f →
-                     ∃∃m. f1 ⊚ f2 ≡ m@f & n = ⫯(n1+m).
-/2 width=3 by after_inv_xSx_aux/ qed-.
-
-lemma after_inv_const: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡ f ∧ n2 = 0.
+lemma after_inv_const: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡ f ∧ 0 = n2.
 #f1 #f2 #f #n2 #n elim n -n
-[ #H elim (after_inv_OxO … H) -H
-  #g2 #Hf #H elim (push_inv_seq_sn … H) -H /2 width=1 by conj/
-| #n #IH #H lapply (after_inv_SxS_aux … H ????) -H /2 width=5 by/
-]
-qed-.
-
-(* Forward lemmas on application ********************************************)
-
-lemma after_at_fwd: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f →
-                    ∃∃i2. @⦃i1, f1⦄ ≡ i2 & @⦃i2, f2⦄ ≡ i.
-#f #i1 #i #H elim H -f -i1 -i
-[ #f #f2 #f1 #H elim (after_inv_xxO … H) -H
-  /2 width=3 by at_refl, ex2_intro/
-| #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_xxO … H) -H
-  #g2 #g1 #Hg #H1 #H2 destruct elim (IH … Hg) -f
-  /3 width=3 by at_S1, ex2_intro/
-| #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_xxS … H) -H *
-  [ #g2 #g1 #Hg #H2 #H1 destruct elim (IH … Hg) -f
-    /3 width=3 by at_S1, at_next, ex2_intro/
-  | #g1 #Hg #H destruct elim (IH … Hg) -f
-    /3 width=3 by at_next, ex2_intro/
-  ]
+[ #H elim (after_inv_pxp … H) -H [ |*: // ]
+  #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
+| #n #IH #H lapply (after_inv_nxn … H ????) -H /2 width=5 by/
 ]
 qed-.
 
-lemma after_at1_fwd: ∀f1,i1,i2. @⦃i1, f1⦄ ≡ i2 → ∀f2,f. f2 ⊚ f1 ≡ f →
-                     ∃∃i. @⦃i2, f2⦄ ≡ i & @⦃i1, f⦄ ≡ i.
-#f1 #i1 #i2 #H elim H -f1 -i1 -i2
-[ #f1 * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H /2 width=3 by ex2_intro/
-| #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H
-  #Hf #H destruct elim (IH … Hf) -f1 /3 width=3 by at_S1, ex2_intro/
-| #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xSx … H) -H
-  #m #Hf #Hm destruct elim (IH … Hf) -f1
-  /4 width=3 by at_plus2, at_S1, at_next, ex2_intro/
-]
-qed-.
-
-lemma after_fwd_at: ∀f1,f2,i1,i2,i. @⦃i1, f1⦄ ≡ i2 → @⦃i2, f2⦄ ≡ i →
-                    ∀f. f2 ⊚ f1 ≡ f → @⦃i1, f⦄ ≡ i.
-#f1 #f2 #i1 #i2 #i #Hi1 #Hi2 #f #Ht elim (after_at1_fwd … Hi1 … Ht) -f1
-#j #H #Hj >(at_mono … H … Hi2) -i2 //
-qed-.
-
-lemma after_fwd_at1: ∀f2,f,i1,i2,i. @⦃i1, f⦄ ≡ i → @⦃i2, f2⦄ ≡ i →
-                     ∀f1. f2 ⊚ f1 ≡ f → @⦃i1, f1⦄ ≡ i2.
-#f2 #f #i1 #i2 #i #Hi1 #Hi2 #f1 #Ht elim (after_at_fwd … Hi1 … Ht) -f
-#j1 #Hij1 #H >(at_inj … Hi2 … H) -i //
-qed-.
+(* Specific forward lemmas **************************************************)
 
-lemma after_fwd_at2: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f1,i2. @⦃i1, f1⦄ ≡ i2 →
-                     ∀f2. f2 ⊚ f1 ≡ f → @⦃i2, f2⦄ ≡ i.
-#f #i1 #i #H elim H -f -i1 -i
-[ #f #f1 #i2 #Ht1 #f2 #H elim (after_inv_xxO … H) -H
-  #g2 #g1 #_ #H1 #H2 destruct >(at_inv_OOx … Ht1) -f -g1 -i2 //
-| #f #i1 #i #_ #IH #f1 #i2 #Ht1 #f2 #H elim (after_inv_xxO … H) -H
-  #g2 #g1 #Hu #H1 #H2 destruct elim (at_inv_SOx … Ht1) -Ht1
-  /3 width=3 by at_push/
-| #f #i1 #i #_ #IH #f1 #i2 #Hf1 #f2 #H elim (after_inv_xxS … H) -H *
-  [ #g2 #g1 #Hg #H2 #H1 destruct elim (at_inv_xSx … Hf1) -Hf1
-    /3 width=3 by at_push/
-  | #g2 #Hg #H destruct /3 width=3 by at_next/
-  ]
-]
-qed-.
-
-(* Advanced forward lemmas on after *****************************************)
-
-lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → n = f1@❴n2❵.
-#f1 #f2 #f #n2 #n #H lapply (after_fwd_at … 0 … H) -H [1,4: // |2,3: skip ]
+lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → f1@❴n2❵ = n.
+#f1 #f2 #f #n2 #n #H lapply (after_fwd_at ? n2 0 … H) -H [1,2,3: // ]
 /3 width=2 by at_inv_O1, sym_eq/
 qed-.
 
-lemma after_fwd_tl: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f →
-                    tln … n2 f1 ⊚ f2 ≡ f.
+lemma after_fwd_tls: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f →
+                     (↓*[n2]f1) ⊚ f2 ≡ f.
 #f #f2 #n2 elim n2 -n2
-[ #f1 #n1 #n #H elim (after_inv_xOx … H) -H //
-| #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xSx_aux … H ??) -H [3: // |2: skip ]
+[ #f1 #n1 #n #H elim (after_inv_xpx … H) -H //
+| #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xnx … H) -H [2,3: // ]
   #m #Hm #H destruct /2 width=3 by/
 ]
 qed-.
 
-lemma after_inv_apply: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f →
-                       a = (a1@f1)@❴a2❵ ∧ tln … a2 f1 ⊚ f2 ≡ f.
-/3 width=3 by after_fwd_tl, after_fwd_hd, conj/ qed-.
-
-(* Main properties on after *************************************************)
-
-let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 →
-                        ∀f1,f2. f1 ⊚ f2 ≡ f0 →
-                        ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?.
-#f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4
-[ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
-  cases (after_inv_xxO_aux … Hg0 … H0) -g0
-  #f1 #f2 #Hf0 #H1 #H2
-  cases (after_inv_OOx_aux … Hg … H2 H3) -g2 -g3
-  #f #Hf #H /3 width=7 by after_refl/
-| #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
-  cases (after_inv_xxO_aux … Hg0 … H0) -g0
-  #f1 #f2 #Hf0 #H1 #H2
-  cases (after_inv_OSx_aux … Hg … H2 H3) -g2 -g3
-  #f #Hf #H /3 width=7 by after_push/
-| #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg
-  cases (after_inv_xxS_aux … Hg0 … H0) -g0 *
-  [ #f1 #f2 #Hf0 #H1 #H2
-    cases (after_inv_Sxx_aux … Hg … H2) -g2
-    #f #Hf #H /3 width=7 by after_push/
-  | #f1 #Hf0 #H1 /3 width=6 by after_next/
-  ]
-]
-qed-.
-
-let corec after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 →
-                        ∀f2, f3. f2 ⊚ f3 ≡ f0 →
-                        ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4 ≝ ?.
-#f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4
-[ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
-  cases (after_inv_xxO_aux … Hg0 … H0) -g0
-  #f2 #f3 #Hf0 #H2 #H3
-  cases (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
-  #f #Hf #H /3 width=7 by after_refl/
-| #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
-  cases (after_inv_xxS_aux … Hg0 … H0) -g0 *
-  [ #f2 #f3 #Hf0 #H2 #H3
-    cases (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
-    #f #Hf #H /3 width=7 by after_push/
-  | #f2 #Hf0 #H2
-    cases (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
-    #f #Hf #H /3 width=6 by after_next/
-  ]
-| #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg
-  cases (after_inv_Sxx_aux … Hg … H1) -g1
-  #f #Hg #H /3 width=6 by after_next/
-]
-qed-.
-
-(* Main inversion lemmas on after *******************************************)
-
-let corec after_mono: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g →
-                      f1 ≐ g1 → f2 ≐ g2 → f ≐ g ≝ ?.
-* #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2
-cases (after_inv_apply … Hf) -Hf #Hn #Hf
-cases (after_inv_apply … Hg) -Hg #Hm #Hg
-cases (eq_stream_inv_seq ????? H1) -H1
-cases (eq_stream_inv_seq ????? H2) -H2
-/4 width=8 by apply_eq_repl, tln_eq_repl, eq_seq/
-qed-.
-
-let corec after_inj: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g →
-                     f1 ≐ g1 → f ≐ g → f2 ≐ g2 ≝ ?.
-* #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2
-cases (after_inv_apply … Hf) -Hf #Hn #Hf
-cases (after_inv_apply … Hg) -Hg #Hm #Hg
-cases (eq_stream_inv_seq ????? H1) -H1 #Hnm1 #Hfg1
-cases (eq_stream_inv_seq ????? H2) -H2 #Hnm #Hfg
-lapply (apply_inj_aux … Hn Hm Hnm ?) -n -m
-/4 width=8 by tln_eq_repl, eq_seq/
-qed-.
-
-theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f.
-/2 width=8 by after_mono/ qed-.
-
-(* Properties on after ******************************************************)
-
-lemma after_isid_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ≐ f → 𝐈⦃f1⦄.
-#f2 #f1 #f #Ht #H2 @isid_at_total
-#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -f1
-/3 width=6 by at_inj, eq_stream_sym/
-qed.
-
-lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄.
-#f2 #f1 #f #Ht #H1 @isid_at_total
-#i2 #i #Hi2 lapply (at_total i2 f1)
-#H0 lapply (at_increasing … H0)
-#Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht)
-/3 width=7 by at_eq_repl_back, at_mono, at_id_le/
-qed.
-
-(* Inversion lemmas on after ************************************************)
-
-let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?.
-* #n1 #f1 * * [ | #n2 ] #f2 #H cases (isid_inv_seq … H) -H
-/3 width=7 by after_push, after_refl/
-qed-.
-
-let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?.
-* #n2 #f2 * *
-[ #f1 #H cases (isid_inv_seq … H) -H
-  /3 width=7 by after_refl/
-| #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/
-]
-qed-.
-
-lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f →  𝐈⦃f1⦄ → f2 ≐ f.
-/3 width=8 by isid_after_sn, after_mono/
-qed-.
-
-lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f →  𝐈⦃f2⦄ → f1 ≐ f.
-/3 width=8 by isid_after_dx, after_mono/
-qed-.
-
-axiom after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄.
+lemma after_inv_apply: ∀f1,f2,f,n1,n2,n. n1@f1 ⊚ n2@f2 ≡ n@f →
+                       (n1@f1)@❴n2❵ = n ∧ (↓*[n2]f1) ⊚ f2 ≡ f.
+/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma
index cec531469437e7689976f4a209848f8eaa7c81e9..4d979cefb1cbea4c1252f1a793db255945277d7d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma
@@ -16,7 +16,7 @@ include "ground_2/relocation/rtmap_eq.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
-(* Specific properties on eq ************************************************)
+(* Specific properties ******************************************************)
 
 fact eq_inv_seq_aux: ∀f1,f2,n1,n2. n1@f1 ≗ n2@f2 → n1 = n2 ∧ f1 ≗ f2.
 #f1 #f2 #n1 #n2 @(nat_elim2 … n1 n2) -n1 -n2

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
index 0001b90b9c06cff094db74fc2b49b3d54da71815..d2bd0837e41959f45c6ffea20ddac132992d7611 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
@@ -98,8 +98,6 @@ lemma apply_S1: ∀f,i. (⫯f)@❴i❵ = ⫯(f@❴i❵).
 qed.
 
 (* Main inversion lemmas ****************************************************)
-(*
-lemma apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. f1@❴i1❵ = j1 → f2@❴i2❵ = j2 →
-                     j1 = j2 → f1 ≗ f2 → i1 = i2.
-/2 width=6 by at_inj/ qed-.
-*)
+
+theorem apply_inj: ∀f,i1,i2,j. f@❴i1❵ = j → f@❴i2❵ = j → i1 = i2.
+/2 width=4 by at_inj/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
index 492a00e91969c184e5698a28b0b6bcc830e1f570..45a72459e732de5d92d0906fbf42a241c4803376 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
@@ -220,10 +220,10 @@ let corec after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x 
 ]
 qed-.
 
-(* Properties on minus ******************************************************)
+(* Properties on tls ********************************************************)
 
-lemma after_minus: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → 
-                   f1 ⊚ f2 ≡ f → f1-n ⊚ f2 ≡ f-n.
+lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → 
+                 f1 ⊚ f2 ≡ f → ⫱*[n]f1 ⊚ f2 ≡ ⫱*[n]f.
 #n elim n -n //
 #n #IH #f1 #f2 #f #Hf1 #Hf cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ]
 #g1 #Hg1 #H1 cases (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/
@@ -385,8 +385,8 @@ cases (after_inv_pxx … H1f … H1) -H1f * #g21 #g #H1g #H21 #H
 | cases (after_inv_pxn … H2f … H1 H) -f1 -f #g22 #H2g #H22
   @(eq_next … H21 H22) -f21 -f22
 ]
-@(after_inj_O_aux (g1-n) … (g-n)) -after_inj_O_aux
-/2 width=1 by after_minus, istot_minus, at_pxx_minus/
+@(after_inj_O_aux (⫱*[n]g1) … (⫱*[n]g)) -after_inj_O_aux
+/2 width=1 by after_tls, istot_tls, at_pxx_tls/
 qed-.
 
 fact after_inj_aux: (∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1) →

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
index 3bc16b8ecc6e954df15699fe66040a3e71fd7bdb..00ee4edb2d5c0d2d9e37bcc54e2975af503e2422 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
@@ -85,8 +85,6 @@ lemma at_inv_xnn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
 #x2 #Hg * -i2 #H destruct //
 qed-.
 
-(* --------------------------------------------------------------------------*)
-
 lemma at_inv_pxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i1 → 0 = i2 → ∃g. ↑g = f.
 #f elim (pn_split … f) * /2 width=2 by ex_intro/
 #g #H #i1 #i2 #Hf #H1 #H2 cases (at_inv_xnp … Hf … H H2)
@@ -117,8 +115,7 @@ lemma at_inv_nxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j1,j2. ⫯j1 = i1 → 
 /4 width=7 by at_inv_xnn, at_inv_npn, ex2_intro, or_intror, or_introl/
 qed-.
 
-(* --------------------------------------------------------------------------*)
-
+(* Note: the following inversion lemmas must be checked *)
 lemma at_inv_xpx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ↑g = f →
                   (0 = i1 ∧ 0 = i2) ∨
                   ∃∃j1,j2. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ⫯j2 = i2.
@@ -270,9 +267,9 @@ theorem at_inj: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀i2. @⦃i2, f⦄ ≡ i →
 #Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/
 qed-.
 
-(* Properties on minus ******************************************************)
+(* Properties on tls ********************************************************)
 
-lemma at_pxx_minus: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, f-n⦄ ≡ 0.
+lemma at_pxx_tls: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, ⫱*[n]f⦄ ≡ 0.
 #n elim n -n //
 #n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf /2 width=3 by/
 qed.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
index cfe2b37717e586fb7298d4492278f71044127973..5ad6aa83c32edb6c8c37599dad3974473f5e4f8c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/notation/relations/isidentity_1.ma".
-include "ground_2/relocation/rtmap_minus.ma".
+include "ground_2/relocation/rtmap_tls.ma".
 
 (* RELOCATION MAP ***********************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
index 07b24f9732c38bec2a9bd8e97b2708f539eeaa56..d4e80390ff447878ad9ae93bc2cb7e001644874c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
@@ -36,14 +36,14 @@ qed-.
 
 (* Properties on tl *********************************************************)
 
-lemma istot_tl: â\88\80f. ð\9d\90\93â¦\83fâ¦\84 â\86\92 ð\9d\90\93â¦\83â\86\93f⦄.
+lemma istot_tl: â\88\80f. ð\9d\90\93â¦\83fâ¦\84 â\86\92 ð\9d\90\93â¦\83⫱f⦄.
 #f cases (pn_split f) *
 #g * -f /2 width=3 by istot_inv_next, istot_inv_push/
 qed.
 
-(* Properties on minus ******************************************************)
+(* Properties on tls ********************************************************)
 
-lemma istot_minus: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃f-n⦄.
+lemma istot_tls: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃⫱*[n]f⦄.
 #n elim n -n /3 width=1 by istot_tl/
 qed.
 

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma
deleted file mode 100644 (file)
index 91f2c84..0000000
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma
+++ /dev/null
@@ -1,40 +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 "ground_2/relocation/rtmap_tl.ma".
-
-(* RELOCATION MAP ***********************************************************)
-
-let rec minus (f:rtmap) (n:nat) on n: rtmap ≝ match n with
-[ O ⇒ f | S m ⇒ ↓(minus f m) ].
-
-interpretation "minus (rtmap)" 'minus f n = (minus f n).
-
-(* Basic properties *********************************************************)
-
-lemma minus_rew_O: ∀f. f = f - 0.
-// qed.
-
-lemma minus_rew_S: ∀f,n. ↓(f - n) = f - ⫯n.
-// qed.
-
-lemma minus_eq_repl: ∀n. eq_repl (λf1,f2. f1 - n ≗ f2 - n).
-#n elim n -n /3 width=1 by tl_eq_repl/
-qed.
-
-(* Advancedd properties *****************************************************)
-
-lemma minus_xn: ∀n,f. (↓f) - n = f - ⫯n.
-#n elim n -n //
-qed.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma
index 779cc4f6f82cf26259db74996bc2165f16592487..588f0d2242cdcbd0e6e24d7bc2fa4e295935f1e5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/drop_1.ma".
+include "ground_2/notation/functions/droppred_1.ma".
 include "ground_2/relocation/rtmap_eq.ma".
 
 (* RELOCATION MAP ***********************************************************)
@@ -21,21 +21,21 @@ definition tl: rtmap → rtmap.
 @case_type0 #f @f
 defined.
 
-interpretation "tail (rtmap)" 'Drop f = (tl f).
+interpretation "tail (rtmap)" 'DropPred f = (tl f).
 
 (* Basic properties *********************************************************)
 
-lemma tl_rew: â\88\80f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = â\86\93f.
+lemma tl_rew: â\88\80f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ⫱f.
 // qed.
 
-lemma tl_push_rew: â\88\80f. f = â\86\93↑f.
+lemma tl_push_rew: â\88\80f. f = ⫱↑f.
 #f <tl_rew <iota_push //
 qed.
 
-lemma tl_next_rew: â\88\80f. f = â\86\93⫯f.
+lemma tl_next_rew: â\88\80f. f = ⫱⫯f.
 #f <tl_rew <iota_next //
 qed.
 
-lemma tl_eq_repl: eq_repl â\80¦ (λf1,f2. â\86\93f1 â\89\97 â\86\93f2).
+lemma tl_eq_repl: eq_repl â\80¦ (λf1,f2. ⫱f1 â\89\97 ⫱f2).
 #f1 #f2 * -f1 -f2 //
 qed.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma
new file mode 100644 (file)
index 0000000..d461488
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground_2/notation/functions/droppreds_2.ma".
+include "ground_2/relocation/rtmap_tl.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+let rec tls (f:rtmap) (n:nat) on n: rtmap ≝ match n with
+[ O ⇒ f | S m ⇒ ⫱(tls f m) ].
+
+interpretation "tls (rtmap)" 'DropPreds n f = (tls f n).
+
+(* Basic properties *********************************************************)
+
+lemma tls_rew_O: ∀f. f = ⫱*[0] f.
+// qed.
+
+lemma tls_rew_S: ∀f,n. ⫱ ⫱*[n] f = ⫱*[⫯n] f.
+// qed.
+
+lemma tls_eq_repl: ∀n. eq_repl (λf1,f2. ⫱*[n] f1 ≗ ⫱*[n] f2).
+#n elim n -n /3 width=1 by tl_eq_repl/
+qed.
+
+(* Advancedd properties *****************************************************)
+
+lemma tls_xn: ∀n,f. ⫱*[n] ⫱f = ⫱*[⫯n] f.
+#n elim n -n //
+qed.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml
index 3584c9e1482ba0d4fd31636974778363b4a4e641..2dbdd34444c202873bdf71c94c63f3bf9c90af7f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml
@@ -12,6 +12,9 @@
          and its timeline.
    </body>
    <table name="ground_2_sum"/>
+   <news class="alpha" date="2016 March 4.">
+         Platform-independent multiple relocation (rtmap).
+   </news>
    <news class="alpha" date="2016 January 20.">
          Multiple relocation with streams of naturals.
    </news>
@@ -19,7 +22,7 @@
          Multiple relocation with lists of booleans.
    </news>
    <news class="alpha" date="2013 November 27.">
-         Natural numbers with infinity.
+         Natural numbers with infinity (ynat).
    </news>
    <news class="alpha" date="2011 August 10.">
          Specification starts.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index d35679f25478c692cc508a652e4de494a3d0b002..699d0767be4e1683c3684b571deaa46044970619 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -23,10 +23,12 @@ table {
    class "grass"
    [ { "multiple relocation" * } {
         [ { "" * } {
-             [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ↓? )" "rtmap_minus ( ? - ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_sle ( ? ⊆ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ]
-             [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
+             [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ↓? )" "rtmap_minus ( ? - ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ]
+             [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "nstream_sand" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
+(*
              [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
                "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
+*)
              [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]
           }
         ]

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
index 8d17df7ff8daabc1b28051b450cd5135cacda97c..07fed2a507ba2d1bb940e3dfc7362b5a6748bb92 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/predecessor_1.ma".
-include "ground_2/lib/arith.ma".
 include "ground_2/ynat/ynat.ma".
 
 (* NATURAL NUMBERS WITH INFINITY ********************************************)

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
index be5bef7077887a884a6bab177c010fe523e28ea1..f08e632937ee67dd06dfb6bac7392125d1ce9389 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/successor_1.ma".
 include "ground_2/ynat/ynat_pred.ma".
 
 (* NATURAL NUMBERS WITH INFINITY ********************************************)

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index d4f38b0baead585e99570b7caff1e34cb80ce0d3..76885077939c13172fc6abd749bfe2351e17a7c4 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1505,14 +1505,14 @@ let load_predefined_virtuals () =
 let predefined_classes = [
  ["&"; "⅋"; ];
  ["|"; "∥"; ];
- ["!"; "¡"; "⫯"; "⫰"; ];
+ ["!"; "¡"; "⫯"; "⫰"; "⟟"; "⫱"; ];
  ["?"; "¿"; "⸮"; ];
  [":"; "⁝"; ];
  ["."; "•"; "◦"; ];
  ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
  ["+"; "⊞"; ];
  ["-"; "÷"; "⊢"; "⊩"; "⊟"; ];
- ["="; "≝"; "≡"; "⩬"; "≂"; "≃"; "≈"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; "⊜"; ];  
+ ["="; "â\89\9d"; "â\89¡"; "⩬"; "â\89\82"; "â\89\83"; "â\89\88"; "â\89\85"; "â\89\97"; "â\89\90"; "â\89\91"; "â\89\9a"; "â\89\99"; "â\8c\86"; "â\8a\9c"; ];  
  ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
  ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➤"; "➸"; "⇉"; "⥰"; ] ;
  ["^"; "↑"; ] ;
@@ -1520,7 +1520,7 @@ let predefined_classes = [
  ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ;
  ["⇕"; "⇳"; "⬍"; ];
  ["↔"; "⇔"; "⬄"; "⬌"; ] ; 
- ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ];
+ ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ;
  ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ];
  ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
  ["("; "❨"; "❪"; "❲"; "（"; ];
@@ -1533,7 +1533,7 @@ let predefined_classes = [
  ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
  [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ;
  ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; 
- ["â\88¨"; "â©\96"; "â\8b\93"; ] ;
+ ["â\88¨"; "â©\96"; "â\88ª"; "â\88©"; "â\8b\93"; "â\8b\92" ] ;
  ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
  ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ;
  ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;