some renaming ...

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
index ccd8857a8a7b254f69586f516d17c1496c06842a..7ba0d13eb3e641b004d6fc2598584b58015ef9d1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
@@ -17,4 +17,4 @@ include "ground_2/lib/streams.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
-definition nstream: Type[0] ≝ stream nat.
+definition rtmap: Type[0] ≝ stream nat.

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 cf5a6b6ebb038189001d91270ebd75c3f4bd7c39..ae7add375539397cb2ef84e0aab7fbadab3b4af8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
@@ -18,90 +18,90 @@ include "ground_2/relocation/nstream_at.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
-let corec compose: nstream → nstream → nstream ≝ ?.
-#t1 * #b2 #t2 @(seq … (t1@❴b2❵)) @(compose ? t2) -compose -t2
-@(tln … (⫯b2) t1)
+let corec compose: rtmap → rtmap → rtmap ≝ ?.
+#f1 * #b2 #f2 @(seq … (f1@❴b2❵)) @(compose ? f2) -compose -f2
+@(tln … (⫯b2) f1)
 qed.
 
 interpretation "functional composition (nstream)"
-   'compose t1 t2 = (compose t1 t2).
+   'compose f1 f2 = (compose f1 f2).
 
-coinductive after: relation3 nstream nstream nstream ≝
-| after_zero: ∀t1,t2,t,b1,b2,b.
-              after t1 t2 t →
+coinductive after: relation3 rtmap rtmap rtmap ≝
+| after_zero: ∀f1,f2,f,b1,b2,b.
+              after f1 f2 f →
               b1 = 0 → b2 = 0 → b = 0 →
-              after (b1@t1) (b2@t2) (b@t)
-| after_skip: ∀t1,t2,t,b1,b2,b,a2,a.
-              after t1 (a2@t2) (a@t) →
+              after (b1@f1) (b2@f2) (b@f)
+| after_skip: ∀f1,f2,f,b1,b2,b,a2,a.
+              after f1 (a2@f2) (a@f) →
               b1 = 0 → b2 = ⫯a2 → b = ⫯a →
-              after (b1@t1) (b2@t2) (b@t)
-| after_drop: ∀t1,t2,t,b1,b,a1,a.
-              after (a1@t1) t2 (a@t) →
+              after (b1@f1) (b2@f2) (b@f)
+| after_drop: ∀f1,f2,f,b1,b,a1,a.
+              after (a1@f1) f2 (a@f) →
               b1 = ⫯a1 → b = ⫯a →
-              after (b1@t1) t2 (b@t)
+              after (b1@f1) f2 (b@f)
 .
 
 interpretation "relational composition (nstream)"
-   'RAfter t1 t2 t = (after t1 t2 t).
+   'RAfter f1 f2 f = (after f1 f2 f).
 
 (* Basic properies on compose ***********************************************)
 
-lemma compose_unfold: ∀t1,t2,a2. t1∘(a2@t2) = t1@❴a2❵@tln … (⫯a2) t1∘t2.
-#t1 #t2 #a2 >(stream_expand … (t1∘(a2@t2))) normalize //
+lemma compose_unfold: ∀f1,f2,a2. f1∘(a2@f2) = f1@❴a2❵@tln … (⫯a2) f1∘f2.
+#f1 #f2 #a2 >(stream_expand … (f1∘(a2@f2))) normalize //
 qed.
 
-lemma compose_drop: ∀t1,t2,t,a1,a. (a1@t1)∘t2 = a@t → (⫯a1@t1)∘t2 = ⫯a@t.
-#t1 * #a2 #t2 #t #a1 #a >compose_unfold >compose_unfold
+lemma compose_drop: ∀f1,f2,f,a1,a. (a1@f1)∘f2 = a@f → (⫯a1@f1)∘f2 = ⫯a@f.
+#f1 * #a2 #f2 #f #a1 #a >compose_unfold >compose_unfold
 #H destruct normalize //
 qed.
 
 (* Basic inversion lemmas on compose ****************************************)
 
-lemma compose_inv_unfold: ∀t1,t2,t,a2,a. t1∘(a2@t2) = a@t →
-                          t1@❴a2❵ = a ∧ tln … (⫯a2) t1∘t2 = t.
-#t1 #t2 #t #a2 #a >(stream_expand … (t1∘(a2@t2))) normalize
+lemma compose_inv_unfold: ∀f1,f2,f,a2,a. f1∘(a2@f2) = a@f →
+                          f1@❴a2❵ = a ∧ tln … (⫯a2) f1∘f2 = f.
+#f1 #f2 #f #a2 #a >(stream_expand … (f1∘(a2@f2))) normalize
 #H destruct /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_O2: ∀t1,t2,t,a1,a. (a1@t1)∘(O@t2) = a@t →
-                      a = a1 ∧ t1∘t2 = t.
-#t1 #t2 #t #a1 #a >compose_unfold
+lemma compose_inv_O2: ∀f1,f2,f,a1,a. (a1@f1)∘(O@f2) = a@f →
+                      a = a1 ∧ f1∘f2 = f.
+#f1 #f2 #f #a1 #a >compose_unfold
 #H destruct /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_S2: ∀t1,t2,t,a1,a2,a. (a1@t1)∘(⫯a2@t2) = a@t →
-                      a = ⫯(a1+t1@❴a2❵) ∧ t1∘(a2@t2) = t1@❴a2❵@t.
-#t1 #t2 #t #a1 #a2 #a >compose_unfold
+lemma compose_inv_S2: ∀f1,f2,f,a1,a2,a. (a1@f1)∘(⫯a2@f2) = a@f →
+                      a = ⫯(a1+f1@❴a2❵) ∧ f1∘(a2@f2) = f1@❴a2❵@f.
+#f1 #f2 #f #a1 #a2 #a >compose_unfold
 #H destruct /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_S1: ∀t1,t2,t,a1,a2,a. (⫯a1@t1)∘(a2@t2) = a@t →
-                      a = ⫯((a1@t1)@❴a2❵) ∧ (a1@t1)∘(a2@t2) = (a1@t1)@❴a2❵@t.
-#t1 #t2 #t #a1 #a2 #a >compose_unfold
+lemma compose_inv_S1: ∀f1,f2,f,a1,a2,a. (⫯a1@f1)∘(a2@f2) = a@f →
+                      a = ⫯((a1@f1)@❴a2❵) ∧ (a1@f1)∘(a2@f2) = (a1@f1)@❴a2❵@f.
+#f1 #f2 #f #a1 #a2 #a >compose_unfold
 #H destruct /2 width=1 by conj/
 qed-.
 
 (* Basic properties on after ************************************************)
 
-lemma after_O2: ∀t1,t2,t. t1 ⊚ t2 ≡ t →
-                ∀b. b@t1 ⊚ O@t2 ≡ b@t.
-#t1 #t2 #t #Ht #b elim b -b /2 width=5 by after_drop, after_zero/
+lemma after_O2: ∀f1,f2,f. f1 ⊚ f2 ≡ f →
+                ∀b. b@f1 ⊚ O@f2 ≡ b@f.
+#f1 #f2 #f #Ht #b elim b -b /2 width=5 by after_drop, after_zero/
 qed.
 
-lemma after_S2: ∀t1,t2,t,b2,b. t1 ⊚ b2@t2 ≡ b@t →
-                ∀b1. b1@t1 ⊚ ⫯b2@t2 ≡ ⫯(b1+b)@t.
-#t1 #t2 #t #b2 #b #Ht #b1 elim b1 -b1 /2 width=5 by after_drop, after_skip/
+lemma after_S2: ∀f1,f2,f,b2,b. f1 ⊚ b2@f2 ≡ b@f →
+                ∀b1. b1@f1 ⊚ ⫯b2@f2 ≡ ⫯(b1+b)@f.
+#f1 #f2 #f #b2 #b #Ht #b1 elim b1 -b1 /2 width=5 by after_drop, after_skip/
 qed.
 
-lemma after_apply: ∀b2,t1,t2,t. (tln … (⫯b2) t1) ⊚ t2 ≡ t → t1 ⊚ b2@t2 ≡ t1@❴b2❵@t.
+lemma after_apply: ∀b2,f1,f2,f. (tln … (⫯b2) f1) ⊚ f2 ≡ f → f1 ⊚ b2@f2 ≡ f1@❴b2❵@f.
 #b2 elim b2 -b2
 [ * /2 width=1 by after_O2/
 | #b2 #IH * /3 width=1 by after_S2/
 ]
 qed-.
 
-let corec after_total_aux: ∀t1,t2,t. t1 ∘ t2 = t → t1 ⊚ t2 ≡ t ≝ ?.
-* #a1 #t1 * #a2 #t2 * #a #t cases a1 -a1
+let corec after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f ≝ ?.
+* #a1 #f1 * #a2 #f2 * #a #f cases a1 -a1
 [ cases a2 -a2
   [ #H cases (compose_inv_O2 … H) -H
     /3 width=1 by after_zero/
@@ -113,141 +113,141 @@ let corec after_total_aux: ∀t1,t2,t. t1 ∘ t2 = t → t1 ⊚ t2 ≡ t ≝ ?.
 ]
 qed-.
 
-theorem after_total: ∀t2,t1. t1 ⊚ t2 ≡ t1 ∘ t2.
+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_O1_aux: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u1. t1 = 0@u1 →
-                       (∃∃u2,u. u1 ⊚ u2 ≡ u & t2 = 0@u2 & t = 0@u) ∨
-                       ∃∃u2,u,b2,b. u1 ⊚ b2@u2 ≡ b@u & t2 = ⫯b2@u2 & t = ⫯b@u.
-#t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1
-[ #b2 #b #Ht #H1 #H2 #H3 #u1 #H destruct /3 width=5 by ex3_2_intro, or_introl/
-| #b2 #b #a2 #a #Ht #H1 #H2 #H3 #u1 #H destruct /3 width=7 by ex3_4_intro, or_intror/
-| #b #a1 #a #_ #H1 #H3 #u1 #H destruct
+fact after_inv_O1_aux: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1. f1 = 0@g1 →
+                       (∃∃g2,g. g1 ⊚ g2 ≡ g & f2 = 0@g2 & f = 0@g) ∨
+                       ∃∃g2,g,b2,b. g1 ⊚ b2@g2 ≡ b@g & f2 = ⫯b2@g2 & f = ⫯b@g.
+#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1
+[ #b2 #b #Ht #H1 #H2 #H3 #g1 #H destruct /3 width=5 by ex3_2_intro, or_introl/
+| #b2 #b #a2 #a #Ht #H1 #H2 #H3 #g1 #H destruct /3 width=7 by ex3_4_intro, or_intror/
+| #b #a1 #a #_ #H1 #H3 #g1 #H destruct
 ]
 qed-.
 
-fact after_inv_O1_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b1 = 0 →
-                        (∧∧ t1 ⊚ t2 ≡ t & b2 = 0 & b = 0) ∨
-                        ∃∃a2,a. t1 ⊚ a2@t2 ≡ a@t & b2 = ⫯a2 & b = ⫯a.
-#t1 #t2 #t #b1 #b2 #b #Ht #H elim (after_inv_O1_aux … Ht) -Ht [4: // |2: skip ] *
-[ #u2 #u #Hu #H1 #H2 destruct /3 width=1 by and3_intro, or_introl/
-| #u2 #u #a2 #a #Hu #H1 #H2 destruct /3 width=5 by ex3_2_intro, or_intror/
+fact after_inv_O1_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b1 = 0 →
+                        (∧∧ f1 ⊚ f2 ≡ f & b2 = 0 & b = 0) ∨
+                        ∃∃a2,a. f1 ⊚ a2@f2 ≡ a@f & b2 = ⫯a2 & b = ⫯a.
+#f1 #f2 #f #b1 #b2 #b #Ht #H elim (after_inv_O1_aux … Ht) -Ht [4: // |2: skip ] *
+[ #g2 #g #Hu #H1 #H2 destruct /3 width=1 by and3_intro, or_introl/
+| #g2 #g #a2 #a #Hu #H1 #H2 destruct /3 width=5 by ex3_2_intro, or_intror/
 ]
 qed-.
 
-lemma after_inv_O1: ∀u1,t2,t. 0@u1 ⊚ t2 ≡ t →
-                    (∃∃u2,u. u1 ⊚ u2 ≡ u & t2 = 0@u2 & t = 0@u) ∨
-                    ∃∃u2,u,b2,b. u1 ⊚ b2@u2 ≡ b@u & t2 = ⫯b2@u2 & t = ⫯b@u.
+lemma after_inv_O1: ∀g1,f2,f. 0@g1 ⊚ f2 ≡ f →
+                    (∃∃g2,g. g1 ⊚ g2 ≡ g & f2 = 0@g2 & f = 0@g) ∨
+                    ∃∃g2,g,b2,b. g1 ⊚ b2@g2 ≡ b@g & f2 = ⫯b2@g2 & f = ⫯b@g.
 /2 width=3 by after_inv_O1_aux/ qed-.
 
-fact after_inv_zero_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b1 = 0 → b2 = 0 →
-                          t1 ⊚ t2 ≡ t ∧ b = 0.
-#t1 #t2 #t #b1 #b2 #b #Ht #H1 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 *
+fact after_inv_zero_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b1 = 0 → b2 = 0 →
+                          f1 ⊚ f2 ≡ f ∧ b = 0.
+#f1 #f2 #f #b1 #b2 #b #Ht #H1 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 *
 [ /2 width=1 by conj/
 | #a1 #a2 #_ #H0 destruct
 ]
 qed-.
 
-lemma after_inv_zero: ∀u1,u2,t. 0@u1 ⊚ 0@u2 ≡ t →
-                      ∃∃u. u1 ⊚ u2 ≡ u & t = 0@u.
-#u1 #u2 #t #H elim (after_inv_O1 … H) -H *
-[ #x2 #u #Hu #H1 #H2 destruct /2 width=3 by ex2_intro/
-| #x2 #u #a2 #a #Hu #H destruct
+lemma after_inv_zero: ∀g1,g2,f. 0@g1 ⊚ 0@g2 ≡ f →
+                      ∃∃g. g1 ⊚ g2 ≡ g & f = 0@g.
+#g1 #g2 #f #H elim (after_inv_O1 … H) -H *
+[ #x2 #g #Hu #H1 #H2 destruct /2 width=3 by ex2_intro/
+| #x2 #g #a2 #a #Hu #H destruct
 ]
 qed-.
 
-fact after_inv_skip_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b1 = 0 → ∀a2. b2 = ⫯a2 →
-                          ∃∃a. t1 ⊚ a2@t2 ≡ a@t & b = ⫯a.
-#t1 #t2 #t #b1 #b2 #b #Ht #H1 #a2 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 *
+fact after_inv_skip_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b1 = 0 → ∀a2. b2 = ⫯a2 →
+                          ∃∃a. f1 ⊚ a2@f2 ≡ a@f & b = ⫯a.
+#f1 #f2 #f #b1 #b2 #b #Ht #H1 #a2 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 *
 [ #_ #H0 destruct
 | #x2 #x #H #H0 #H1 destruct /2 width=3 by ex2_intro/
 ]
 qed-.
 
-lemma after_inv_skip: ∀u1,u2,t,b2. 0@u1 ⊚ ⫯b2@u2 ≡ t →
-                      ∃∃u,b. u1 ⊚ b2@u2 ≡ b@u & t = ⫯b@u.
-#u1 #u2 * #b #t #b2 #Ht elim (after_inv_skip_aux2 … Ht) [2,4: // |3: skip ] -Ht
+lemma after_inv_skip: ∀g1,g2,f,b2. 0@g1 ⊚ ⫯b2@g2 ≡ f →
+                      ∃∃g,b. g1 ⊚ b2@g2 ≡ b@g & f = ⫯b@g.
+#g1 #g2 * #b #f #b2 #Ht elim (after_inv_skip_aux2 … Ht) [2,4: // |3: skip ] -Ht
 #a #Ht #H destruct /2 width=4 by ex2_2_intro/
 qed-.
 
-fact after_inv_S1_aux: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u1,b1. t1 = ⫯b1@u1 →
-                       ∃∃u,b. b1@u1 ⊚ t2 ≡ b@u & t = ⫯b@u.
-#t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1
-[ #b2 #b #_ #H1 #H2 #H3 #u1 #a1 #H destruct
-| #b2 #b #a2 #a #_ #H1 #H2 #H3 #u1 #a1 #H destruct
-| #b #a1 #a #Ht #H1 #H3 #u1 #x1 #H destruct /2 width=4 by ex2_2_intro/
+fact after_inv_S1_aux: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1,b1. f1 = ⫯b1@g1 →
+                       ∃∃g,b. b1@g1 ⊚ f2 ≡ b@g & f = ⫯b@g.
+#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1
+[ #b2 #b #_ #H1 #H2 #H3 #g1 #a1 #H destruct
+| #b2 #b #a2 #a #_ #H1 #H2 #H3 #g1 #a1 #H destruct
+| #b #a1 #a #Ht #H1 #H3 #g1 #x1 #H destruct /2 width=4 by ex2_2_intro/
 ]
 qed-.
 
-fact after_inv_S1_aux2: ∀t1,t2,t,b1,b. b1@t1 ⊚ t2 ≡ b@t → ∀a1. b1 = ⫯a1 →
-                        ∃∃a. a1@t1 ⊚ t2 ≡ a@t & b = ⫯a.
-#t1 #t2 #t #b1 #b #Ht #a #H elim (after_inv_S1_aux … Ht) -Ht [4: // |2,3: skip ]
-#u #x #Hu #H0 destruct /2 width=3 by ex2_intro/ 
+fact after_inv_S1_aux2: ∀f1,f2,f,b1,b. b1@f1 ⊚ f2 ≡ b@f → ∀a1. b1 = ⫯a1 →
+                        ∃∃a. a1@f1 ⊚ f2 ≡ a@f & b = ⫯a.
+#f1 #f2 #f #b1 #b #Ht #a #H elim (after_inv_S1_aux … Ht) -Ht [4: // |2,3: skip ]
+#g #x #Hu #H0 destruct /2 width=3 by ex2_intro/ 
 qed-.
 
-lemma after_inv_S1: ∀u1,t2,t,b1. ⫯b1@u1 ⊚ t2 ≡ t →
-                    ∃∃u,b. b1@u1 ⊚ t2 ≡ b@u & t = ⫯b@u.
+lemma after_inv_S1: ∀g1,f2,f,b1. ⫯b1@g1 ⊚ f2 ≡ f →
+                    ∃∃g,b. b1@g1 ⊚ f2 ≡ b@g & f = ⫯b@g.
 /2 width=3 by after_inv_S1_aux/ qed-.
 
-fact after_inv_drop_aux2: ∀t1,t2,t,a1,a. a1@t1 ⊚ t2 ≡ a@t → ∀b1,b. a1 = ⫯b1 → a = ⫯b →
-                          b1@t1 ⊚ t2 ≡ b@t.
-#t1 #t2 #t #a1 #a #Ht #b1 #b #H1 #H elim (after_inv_S1_aux2 … Ht … H1) -a1
+fact after_inv_drop_aux2: ∀f1,f2,f,a1,a. a1@f1 ⊚ f2 ≡ a@f → ∀b1,b. a1 = ⫯b1 → a = ⫯b →
+                          b1@f1 ⊚ f2 ≡ b@f.
+#f1 #f2 #f #a1 #a #Ht #b1 #b #H1 #H elim (after_inv_S1_aux2 … Ht … H1) -a1
 #x #Ht #Hx destruct //
 qed-.
 
-lemma after_inv_drop: ∀t1,t2,t,b1,b. ⫯b1@t1 ⊚ t2 ≡ ⫯b@t → b1@t1 ⊚ t2 ≡ b@t.
+lemma after_inv_drop: ∀f1,f2,f,b1,b. ⫯b1@f1 ⊚ f2 ≡ ⫯b@f → b1@f1 ⊚ f2 ≡ b@f.
 /2 width=5 by after_inv_drop_aux2/ qed-.
 
-fact after_inv_O3_aux1: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u. t = 0@u →
-                        ∃∃u1,u2. u1 ⊚ u2 ≡ u & t1 = 0@u1 & t2 = 0@u2.
-#t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1
-[ #b2 #b #Ht #H1 #H2 #H3 #u #H destruct /2 width=5 by ex3_2_intro/
-| #b2 #b #a2 #a #_ #H1 #H2 #H3 #u #H destruct
-| #b #a1 #a #_ #H1 #H3 #u #H destruct
+fact after_inv_O3_aux1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g. f = 0@g →
+                        ∃∃g1,g2. g1 ⊚ g2 ≡ g & f1 = 0@g1 & f2 = 0@g2.
+#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1
+[ #b2 #b #Ht #H1 #H2 #H3 #g #H destruct /2 width=5 by ex3_2_intro/
+| #b2 #b #a2 #a #_ #H1 #H2 #H3 #g #H destruct
+| #b #a1 #a #_ #H1 #H3 #g #H destruct
 ]
 qed-.
 
-fact after_inv_O3_aux2: ∀t1,t2,t,b1,b2,b. b1@t1 ⊚ b2@t2 ≡ b@t → b = 0 →
-                        ∧∧ t1 ⊚ t2 ≡ t & b1 = 0 & b2 = 0.
-#t1 #t2 #t #b1 #b2 #b #Ht #H1 elim (after_inv_O3_aux1 … Ht) [2: // |3: skip ] -b
-#u1 #u2 #Ht #H1 #H2 destruct /2 width=1 by and3_intro/
+fact after_inv_O3_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b = 0 →
+                        ∧∧ f1 ⊚ f2 ≡ f & b1 = 0 & b2 = 0.
+#f1 #f2 #f #b1 #b2 #b #Ht #H1 elim (after_inv_O3_aux1 … Ht) [2: // |3: skip ] -b
+#g1 #g2 #Ht #H1 #H2 destruct /2 width=1 by and3_intro/
 qed-.
 
-lemma after_inv_O3: ∀t1,t2,u. t1 ⊚ t2 ≡ 0@u →
-                    ∃∃u1,u2. u1 ⊚ u2 ≡ u & t1 = 0@u1 & t2 = 0@u2.
+lemma after_inv_O3: ∀f1,f2,g. f1 ⊚ f2 ≡ 0@g →
+                    ∃∃g1,g2. g1 ⊚ g2 ≡ g & f1 = 0@g1 & f2 = 0@g2.
 /2 width=3 by after_inv_O3_aux1/ qed-.
 
-fact after_inv_S3_aux1: ∀t1,t2,t. t1 ⊚ t2 ≡ t → ∀u,b. t = ⫯b@u →
-                        (∃∃u1,u2,b2. u1 ⊚ b2@u2 ≡ b@u & t1 = 0@u1 & t2 = ⫯b2@u2) ∨
-                        ∃∃u1,b1. b1@u1 ⊚ t2 ≡ b@u & t1 = ⫯b1@u1.
-#t1 #t2 #t * -t1 -t2 -t #t1 #t2 #t #b1
-[ #b2 #b #_ #H1 #H2 #H3 #u #a #H destruct
-| #b2 #b #a2 #a #HT #H1 #H2 #H3 #u #x #H destruct /3 width=6 by ex3_3_intro, or_introl/
-| #b #a1 #a #HT #H1 #H3 #u #x #H destruct /3 width=4 by ex2_2_intro, or_intror/
+fact after_inv_S3_aux1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g,b. f = ⫯b@g →
+                        (∃∃g1,g2,b2. g1 ⊚ b2@g2 ≡ b@g & f1 = 0@g1 & f2 = ⫯b2@g2) ∨
+                        ∃∃g1,b1. b1@g1 ⊚ f2 ≡ b@g & f1 = ⫯b1@g1.
+#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1
+[ #b2 #b #_ #H1 #H2 #H3 #g #a #H destruct
+| #b2 #b #a2 #a #HT #H1 #H2 #H3 #g #x #H destruct /3 width=6 by ex3_3_intro, or_introl/
+| #b #a1 #a #HT #H1 #H3 #g #x #H destruct /3 width=4 by ex2_2_intro, or_intror/
 ]
 qed-.
 
-fact after_inv_S3_aux2: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ a2@t2 ≡ a@t → ∀b. a = ⫯b →
-                        (∃∃b2. t1 ⊚ b2@t2 ≡ b@t & a1 = 0 & a2 = ⫯b2) ∨
-                        ∃∃b1. b1@t1 ⊚ a2@t2 ≡ b@t & a1 = ⫯b1.
-#t1 #t2 #t #a1 #a2 #a #Ht #b #H elim (after_inv_S3_aux1 … Ht) [3: // |4,5: skip ] -a *
-[ #u1 #u2 #b2 #Ht #H1 #H2 destruct /3 width=3 by ex3_intro, or_introl/
-| #u1 #b1 #Ht #H1 destruct /3 width=3 by ex2_intro, or_intror/
+fact after_inv_S3_aux2: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f → ∀b. a = ⫯b →
+                        (∃∃b2. f1 ⊚ b2@f2 ≡ b@f & a1 = 0 & a2 = ⫯b2) ∨
+                        ∃∃b1. b1@f1 ⊚ a2@f2 ≡ b@f & a1 = ⫯b1.
+#f1 #f2 #f #a1 #a2 #a #Ht #b #H elim (after_inv_S3_aux1 … Ht) [3: // |4,5: skip ] -a *
+[ #g1 #g2 #b2 #Ht #H1 #H2 destruct /3 width=3 by ex3_intro, or_introl/
+| #g1 #b1 #Ht #H1 destruct /3 width=3 by ex2_intro, or_intror/
 ]
 qed-.
 
-lemma after_inv_S3: ∀t1,t2,u,b. t1 ⊚ t2 ≡ ⫯b@u →
-                    (∃∃u1,u2,b2. u1 ⊚ b2@u2 ≡ b@u & t1 = 0@u1 & t2 = ⫯b2@u2) ∨
-                    ∃∃u1,b1. b1@u1 ⊚ t2 ≡ b@u & t1 = ⫯b1@u1.
+lemma after_inv_S3: ∀f1,f2,g,b. f1 ⊚ f2 ≡ ⫯b@g →
+                    (∃∃g1,g2,b2. g1 ⊚ b2@g2 ≡ b@g & f1 = 0@g1 & f2 = ⫯b2@g2) ∨
+                    ∃∃g1,b1. b1@g1 ⊚ f2 ≡ b@g & f1 = ⫯b1@g1.
 /2 width=3 by after_inv_S3_aux1/ qed-.
 
 (* Advanced inversion lemmas on after ***************************************)
 
-fact after_inv_O2_aux2: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ a2@t2 ≡ a@t → a2 = 0 →
-                         a1 = a ∧ t1 ⊚ t2 ≡ t.
-#t1 #t2 #t #a1 #a2 elim a1 -a1
+fact after_inv_O2_aux2: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f → a2 = 0 →
+                         a1 = a ∧ f1 ⊚ f2 ≡ f.
+#f1 #f2 #f #a1 #a2 elim a1 -a1
 [ #a #H #H2 elim (after_inv_zero_aux2 … H … H2) -a2 /2 width=1 by conj/
 | #a1 #IH #a #H #H2 elim (after_inv_S1_aux2 … H) -H [3: // |2: skip ]
   #b #H #H1 elim (IH … H) // -a2
@@ -255,24 +255,24 @@ fact after_inv_O2_aux2: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ a2@t2 ≡ a@t → a2 = 0 
 ]
 qed-.
 
-lemma after_inv_O2: ∀t1,u2,t. t1 ⊚ 0@u2 ≡ t →
-                    ∃∃u1,u,a. t1 = a@u1 & t = a@u & u1 ⊚ u2 ≡ u.
-* #a1 #t1 #t2 * #a #t #H elim (after_inv_O2_aux2 … H) -H //
+lemma after_inv_O2: ∀f1,g2,f. f1 ⊚ 0@g2 ≡ f →
+                    ∃∃g1,g,a. f1 = a@g1 & f = a@g & g1 ⊚ g2 ≡ g.
+* #a1 #f1 #f2 * #a #f #H elim (after_inv_O2_aux2 … H) -H //
 /2 width=6 by ex3_3_intro/
 qed-.
 
-lemma after_inv_const: ∀a,t1,b2,u2,t. a@t1 ⊚ b2@u2 ≡ a@t → b2 = 0.
+lemma after_inv_const: ∀a,f1,b2,g2,f. a@f1 ⊚ b2@g2 ≡ a@f → b2 = 0.
 #a elim a -a
-[ #t1 #b2 #u2 #t #H elim (after_inv_O3 … H) -H
-  #u1 #x2 #_ #_ #H destruct //
-| #a #IH #t1 #b2 #u2 #t #H elim (after_inv_S1 … H) -H
-  #x #b #Hx #H destruct >(IH … Hx) -t1 -u2 -x -b2 -b //
+[ #f1 #b2 #g2 #f #H elim (after_inv_O3 … H) -H
+  #g1 #x2 #_ #_ #H destruct //
+| #a #IH #f1 #b2 #g2 #f #H elim (after_inv_S1 … H) -H
+  #x #b #Hx #H destruct >(IH … Hx) -f1 -g2 -x -b2 -b //
 ]
 qed-.
 
-lemma after_inv_S2: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ ⫯a2@t2 ≡ a@t → ∀b. a = ⫯(a1+b) →
-                    t1 ⊚ a2@t2 ≡ b@t.
-#t1 #t2 #t #a1 elim a1 -a1
+lemma after_inv_S2: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ ⫯a2@f2 ≡ a@f → ∀b. a = ⫯(a1+b) →
+                    f1 ⊚ a2@f2 ≡ b@f.
+#f1 #f2 #f #a1 elim a1 -a1
 [ #a2 #a #Ht #b #Hb
   elim (after_inv_skip_aux2 … Ht) -Ht [3,4: // |2: skip ]
   #c #Ht #Hc destruct //
@@ -284,147 +284,147 @@ qed-.
 
 (* Forward lemmas on application ********************************************)
 
-lemma after_at_fwd: ∀t,i1,i. @⦃i1, t⦄ ≡ i → ∀t2,t1. t2 ⊚ t1 ≡ t →
-                    ∃∃i2. @⦃i1, t1⦄ ≡ i2 & @⦃i2, t2⦄ ≡ i.
-#t #i1 #i #H elim H -t -i1 -i
-[ #t #t2 #t1 #H elim (after_inv_O3 … H) -H
+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_O3 … H) -H
   /2 width=3 by at_zero, ex2_intro/
-| #t #i1 #i #_ #IH #t2 #t1 #H elim (after_inv_O3 … H) -H
-  #u2 #u1 #Hu #H1 #H2 destruct elim (IH … Hu) -t
+| #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_O3 … H) -H
+  #g2 #g1 #Hu #H1 #H2 destruct elim (IH … Hu) -f
   /3 width=3 by at_S1, ex2_intro/
-| #t #b #i1 #i #_ #IH #t2 #t1 #H elim (after_inv_S3 … H) -H *
-  [ #u2 #u1 #b2 #Hu #H1 #H2 destruct elim (IH … Hu) -t -b
+| #f #b #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_S3 … H) -H *
+  [ #g2 #g1 #b2 #Hu #H1 #H2 destruct elim (IH … Hu) -f -b
     /3 width=3 by at_S1, at_lift, ex2_intro/
-  | #u1 #b1 #Hu #H destruct elim (IH … Hu) -t -b
+  | #g1 #b1 #Hu #H destruct elim (IH … Hu) -f -b
     /3 width=3 by at_lift, ex2_intro/
   ]
 ]
 qed-.
 
-lemma after_at1_fwd: ∀t1,i1,i2. @⦃i1, t1⦄ ≡ i2 → ∀t2,t. t2 ⊚ t1 ≡ t →
-                     ∃∃i. @⦃i2, t2⦄ ≡ i & @⦃i1, t⦄ ≡ i.
-#t1 #i1 #i2 #H elim H -t1 -i1 -i2
-[ #t1 #t2 #t #H elim (after_inv_O2 … H) -H /2 width=3 by ex2_intro/
-| #t1 #i1 #i2 #_ #IH * #b2 elim b2 -b2
-  [ #t2 #t #H elim (after_inv_zero … H) -H
-    #u #Hu #H destruct elim (IH … Hu) -t1
+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 #f2 #f #H elim (after_inv_O2 … H) -H /2 width=3 by ex2_intro/
+| #f1 #i1 #i2 #_ #IH * #b2 elim b2 -b2
+  [ #f2 #f #H elim (after_inv_zero … H) -H
+    #g #Hu #H destruct elim (IH … Hu) -f1
     /3 width=3 by at_S1, at_skip, ex2_intro/
-  | -IH #b2 #IH #t2 #t #H elim (after_inv_S1 … H) -H
-    #u #b #Hu #H destruct elim (IH … Hu) -t1
+  | -IH #b2 #IH #f2 #f #H elim (after_inv_S1 … H) -H
+    #g #b #Hu #H destruct elim (IH … Hu) -f1
     /3 width=3 by at_lift, ex2_intro/
   ]
-| #t1 #b1 #i1 #i2 #_ #IH * #b2 elim b2 -b2
-  [ #t2 #t #H elim (after_inv_skip … H) -H
-    #u #a #Hu #H destruct elim (IH … Hu) -t1 -b1
+| #f1 #b1 #i1 #i2 #_ #IH * #b2 elim b2 -b2
+  [ #f2 #f #H elim (after_inv_skip … H) -H
+    #g #a #Hu #H destruct elim (IH … Hu) -f1 -b1
     /3 width=3 by at_S1, at_lift, ex2_intro/
-  | -IH #b2 #IH #t2 #t #H elim (after_inv_S1 … H) -H
-    #u #b #Hu #H destruct elim (IH … Hu) -t1 -b1
+  | -IH #b2 #IH #f2 #f #H elim (after_inv_S1 … H) -H
+    #g #b #Hu #H destruct elim (IH … Hu) -f1 -b1
     /3 width=3 by at_lift, ex2_intro/
   ]
 ]
 qed-.
 
-lemma after_fwd_at: ∀t1,t2,i1,i2,i. @⦃i1, t1⦄ ≡ i2 → @⦃i2, t2⦄ ≡ i →
-                    ∀t. t2 ⊚ t1 ≡ t → @⦃i1, t⦄ ≡ i.
-#t1 #t2 #i1 #i2 #i #Hi1 #Hi2 #t #Ht elim (after_at1_fwd … Hi1 … Ht) -t1
+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: ∀t2,t,i1,i2,i. @⦃i1, t⦄ ≡ i → @⦃i2, t2⦄ ≡ i →
-                     ∀t1. t2 ⊚ t1 ≡ t → @⦃i1, t1⦄ ≡ i2.
-#t2 #t #i1 #i2 #i #Hi1 #Hi2 #t1 #Ht elim (after_at_fwd … Hi1 … Ht) -t
+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-.
 
-lemma after_fwd_at2: ∀t,i1,i. @⦃i1, t⦄ ≡ i → ∀t1,i2. @⦃i1, t1⦄ ≡ i2 →
-                     ∀t2. t2 ⊚ t1 ≡ t → @⦃i2, t2⦄ ≡ i.
-#t #i1 #i #H elim H -t -i1 -i
-[ #t #t1 #i2 #Ht1 #t2 #H elim (after_inv_O3 … H) -H
-  #u2 #u1 #_ #H1 #H2 destruct >(at_inv_OOx … Ht1) -t -u1 -i2 //
-| #t #i1 #i #_ #IH #t1 #i2 #Ht1 #t2 #H elim (after_inv_O3 … H) -H
-  #u2 #u1 #Hu #H1 #H2 destruct elim (at_inv_SOx … Ht1) -Ht1
+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_O3 … 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_O3 … H) -H
+  #g2 #g1 #Hu #H1 #H2 destruct elim (at_inv_SOx … Ht1) -Ht1
   /3 width=3 by at_skip/
-| #t #b #i1 #i #_ #IH #t1 #i2 #Ht1 #t2 #H elim (after_inv_S3 … H) -H *
-  [ #u2 #u1 #a1 #Hu #H1 #H2 destruct elim (at_inv_xSx … Ht1) -Ht1
+| #f #b #i1 #i #_ #IH #f1 #i2 #Ht1 #f2 #H elim (after_inv_S3 … H) -H *
+  [ #g2 #g1 #a1 #Hu #H1 #H2 destruct elim (at_inv_xSx … Ht1) -Ht1
     /3 width=3 by at_skip/
-  | #u2 #a2 #Hu #H destruct /3 width=3 by at_lift/
+  | #g2 #a2 #Hu #H destruct /3 width=3 by at_lift/
   ]
 ]
 qed-.
 
 (* Advanced forward lemmas on after *****************************************)
 
-lemma after_fwd_hd: ∀t1,t2,t,a2,a. t1 ⊚ a2@t2 ≡ a@t → a = t1@❴a2❵.
-#t1 #t2 #t #a2 #a #Ht lapply (after_fwd_at … 0 … Ht) -Ht [4: // | // |2,3: skip ]
+lemma after_fwd_hd: ∀f1,f2,f,a2,a. f1 ⊚ a2@f2 ≡ a@f → a = f1@❴a2❵.
+#f1 #f2 #f #a2 #a #Ht lapply (after_fwd_at … 0 … Ht) -Ht [4: // | // |2,3: skip ]
 /3 width=2 by at_inv_O1, sym_eq/
 qed-.
 
-lemma after_fwd_tl: ∀t,t2,a2,t1,a1,a. a1@t1 ⊚ a2@t2 ≡ a@t →
-                    tln … a2 t1 ⊚ t2 ≡ t.
-#t #t2 #a2 elim a2 -a2
-[ #t1 #a1 #a #Ht elim (after_inv_O2_aux2 … Ht) -Ht //
-| #a2 #IH * #b1 #t1 #a1 #a #Ht
+lemma after_fwd_tl: ∀f,f2,a2,f1,a1,a. a1@f1 ⊚ a2@f2 ≡ a@f →
+                    tln … a2 f1 ⊚ f2 ≡ f.
+#f #f2 #a2 elim a2 -a2
+[ #f1 #a1 #a #Ht elim (after_inv_O2_aux2 … Ht) -Ht //
+| #a2 #IH * #b1 #f1 #a1 #a #Ht
   lapply (after_fwd_hd … Ht) #Ha
   lapply (after_inv_S2 … Ht … Ha) -a
   /2 width=3 by/
 ]
 qed-.
 
-lemma after_inv_apply: ∀t1,t2,t,a1,a2,a. a1@t1 ⊚ a2@t2 ≡ a@t →
-                       a = (a1@t1)@❴a2❵ ∧ tln … a2 t1 ⊚ t2 ≡ t.
+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: ∀t1,t2,t0. t1 ⊚ t2 ≡ t0 →
-                        ∀t3,t4. t0 ⊚ t3 ≡ t4 →
-                        ∀t. t2 ⊚ t3 ≡ t → t1 ⊚ t ≡ t4 ≝ ?.
-#t1 #t2 #t0 * -t1 -t2 -t0 #t1 #t2 #t0 #b1 [1,2: #b2 ] #b0
-[ #Ht0 #H1 #H2 #H0 * #b3 #t3 * #b4 #t4 #Ht4 * #b #t #Ht
+let corec after_trans1: ∀f1,f2,f0. f1 ⊚ f2 ≡ f0 →
+                        ∀f3,f4. f0 ⊚ f3 ≡ f4 →
+                        ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?.
+#f1 #f2 #f0 * -f1 -f2 -f0 #f1 #f2 #f0 #b1 [1,2: #b2 ] #b0
+[ #Ht0 #H1 #H2 #H0 * #b3 #f3 * #b4 #f4 #Ht4 * #b #f #Ht
   cases (after_inv_O1_aux2 … Ht4 H0) -Ht4 -H0 *
   [ #Ht4 #H3 #H4 cases (after_inv_zero_aux2 … Ht H2 H3) -Ht -H2 -H3
     #Ht #H /3 width=6 by after_zero/
   | #a0 #a4 #Ht4 #H3 #H4 cases (after_inv_skip_aux2 … Ht H2 … H3) -Ht -H2 -H3
     #a #Ht3 #H /3 width=6 by after_skip/
   ]
-| #a2 #a0 #Ht0 #H1 #H2 #H0 #t3 * #b4 #t4 #Ht4 cases (after_inv_S1_aux2 … Ht4 … H0) -Ht4 -H0
-  #a4 #Ht4 #H4 * #b #t #H cases (after_inv_S1_aux2 … H … H2) -H -H2
+| #a2 #a0 #Ht0 #H1 #H2 #H0 #f3 * #b4 #f4 #Ht4 cases (after_inv_S1_aux2 … Ht4 … H0) -Ht4 -H0
+  #a4 #Ht4 #H4 * #b #f #H cases (after_inv_S1_aux2 … H … H2) -H -H2
   #a #Ht3 #H /3 width=6 by after_skip/
-| #a1 #a0 #Ht0 #H1 #H0 #t3 * #b4 #t4 #Ht4 cases (after_inv_S1_aux2 … Ht4 … H0) -Ht4 -H0
-  #a4 #Ht4 #H4 * #b #t #Ht /3 width=6 by after_drop/
+| #a1 #a0 #Ht0 #H1 #H0 #f3 * #b4 #f4 #Ht4 cases (after_inv_S1_aux2 … Ht4 … H0) -Ht4 -H0
+  #a4 #Ht4 #H4 * #b #f #Ht /3 width=6 by after_drop/
 ]
 qed-.
 
-let corec after_trans2: ∀t1,t0,t4. t1 ⊚ t0 ≡ t4 →
-                        ∀t2, t3. t2 ⊚ t3 ≡ t0 →
-                        ∀t. t1 ⊚ t2 ≡ t → t ⊚ t3 ≡ t4 ≝ ?.
-#t1 #t0 #t4 * -t1 -t0 -t4 #t1 #t0 #t4 #b1 [1,2: #b0 ] #b4
-[ #Ht4 #H1 #H0 #H4 * #b2 #t2 * #b3 #t3 #Ht0 * #b #t #Ht
+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 #b1 [1,2: #b0 ] #b4
+[ #Ht4 #H1 #H0 #H4 * #b2 #f2 * #b3 #f3 #Ht0 * #b #f #Ht
   cases (after_inv_O3_aux2 … Ht0 H0) -b0
   #Ht0 #H2 #H3 cases (after_inv_zero_aux2 … Ht H1 H2) -b1 -b2
   #Ht #H /3 width=6 by after_zero/
-| #a0 #a4 #Ht4 #H1 #H0 #H4 * #b2 #t2 * #b3 #t3 #Ht0 * #b #t #Ht
+| #a0 #a4 #Ht4 #H1 #H0 #H4 * #b2 #f2 * #b3 #f3 #Ht0 * #b #f #Ht
   cases (after_inv_S3_aux2 … Ht0 … H0) -b0 *
   [ #a3 #Ht0 #H2 #H3 cases (after_inv_zero_aux2 … Ht H1 H2) -b1 -b2
     #Ht #H /3 width=6 by after_skip/
   | #a2 #Ht0 #H2 cases (after_inv_skip_aux2 … Ht H1 … H2) -b1 -b2
     #a #Ht #H /3 width=6 by after_drop/
   ]
-| #a1 #a4 #Ht4 #H1 #H4 * #b2 #t2 * #b3 #t3 #Ht0 * #b #t #Ht
+| #a1 #a4 #Ht4 #H1 #H4 * #b2 #f2 * #b3 #f3 #Ht0 * #b #f #Ht
   cases (after_inv_S1_aux2 … Ht … H1) -b1
   #a #Ht #H /3 width=6 by after_drop/
 ]
 qed-.
 
-let corec after_mono: ∀t1,t2,x. t1 ⊚ t2 ≡ x → ∀y. t1 ⊚ t2 ≡ y → x ≐ y ≝ ?.
-* #a1 #t1 * #a2 #t2 * #c #x #Hx * #d #y #Hy
+let corec after_mono: ∀f1,f2,x. f1 ⊚ f2 ≡ x → ∀y. f1 ⊚ f2 ≡ y → x ≐ y ≝ ?.
+* #a1 #f1 * #a2 #f2 * #c #x #Hx * #d #y #Hy
 cases (after_inv_apply … Hx) -Hx #Hc #Hx
 cases (after_inv_apply … Hy) -Hy #Hd #Hy
 /3 width=4 by eq_seq/
 qed-.
 
-let corec after_inj: ∀t1,x,t. t1 ⊚ x ≡ t → ∀y. t1 ⊚ y ≡ t → x ≐ y ≝ ?.
-* #a1 #t1 * #c #x * #a #t #Hx * #d #y #Hy
+let corec after_inj: ∀f1,x,f. f1 ⊚ x ≡ f → ∀y. f1 ⊚ y ≡ f → x ≐ y ≝ ?.
+* #a1 #f1 * #c #x * #a #f #Hx * #d #y #Hy
 cases (after_inv_apply … Hx) -Hx #Hc #Hx
 cases (after_inv_apply … Hy) -Hy #Hd
 cases (apply_inj_aux … Hc Hd) //
@@ -433,5 +433,5 @@ qed-.
 
 (* Main inversion lemmas on after *******************************************)
 
-theorem after_inv_total: ∀t1,t2,t. t1 ⊚ t2 ≡ t → t1 ∘ t2 ≐ t.
+theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f.
 /2 width=4 by after_mono/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma
index 4b812836b3c08558bcb03ef3f805873e3d1afe1d..a40ba30ad1de6ccd87ff640e80803494c1835012 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma
@@ -18,155 +18,155 @@ include "ground_2/relocation/nstream.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
-let rec apply (i: nat) on i: nstream → nat ≝ ?.
-* #b #t cases i -i
+let rec apply (i: nat) on i: rtmap → nat ≝ ?.
+* #b #f cases i -i
 [ @b
-| #i lapply (apply i t) -apply -i -t
+| #i lapply (apply i f) -apply -i -f
   #i @(⫯(b+i))
 ]
 qed.
 
 interpretation "functional application (nstream)"
-   'Apply t i = (apply i t).
+   'Apply f i = (apply i f).
 
-inductive at: nstream → relation nat ≝
-| at_zero: ∀t. at (0 @ t) 0 0
-| at_skip: ∀t,i1,i2. at t i1 i2 → at (0 @ t) (⫯i1) (⫯i2)
-| at_lift: ∀t,b,i1,i2. at (b @ t) i1 i2 → at (⫯b @ t) i1 (⫯i2)
+inductive at: rtmap → relation nat ≝
+| at_zero: ∀f. at (0 @ f) 0 0
+| at_skip: ∀f,i1,i2. at f i1 i2 → at (0 @ f) (⫯i1) (⫯i2)
+| at_lift: ∀f,b,i1,i2. at (b @ f) i1 i2 → at (⫯b @ f) i1 (⫯i2)
 .
 
 interpretation "relational application (nstream)"
-   'RAt i1 t i2 = (at t i1 i2).
+   'RAt i1 f i2 = (at f i1 i2).
 
 (* Basic properties on apply ************************************************)
 
-lemma apply_S1: ∀t,a,i. (⫯a@t)@❴i❵ = ⫯((a@t)@❴i❵).
-#a #t * //
+lemma apply_S1: ∀f,a,i. (⫯a@f)@❴i❵ = ⫯((a@f)@❴i❵).
+#a #f * //
 qed.
 
 (* Basic inversion lemmas on at *********************************************)
 
-fact at_inv_xOx_aux: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → ∀u. t = 0 @ u →
+fact at_inv_xOx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. f = 0@g →
                      (i1 = 0 ∧ i2 = 0) ∨
-                     ∃∃j1,j2. @⦃j1, u⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2.
-#t #i1 #i2 * -t -i1 -i2
+                     ∃∃j1,j2. @⦃j1, g⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2.
+#f #i1 #i2 * -f -i1 -i2
 [ /3 width=1 by or_introl, conj/
-| #t #i1 #i2 #Hi #u #H destruct /3 width=5 by ex3_2_intro, or_intror/
-| #t #b #i1 #i2 #_ #u #H destruct
+| #f #i1 #i2 #Hi #g #H destruct /3 width=5 by ex3_2_intro, or_intror/
+| #f #b #i1 #i2 #_ #g #H destruct
 ]
 qed-.
 
-lemma at_inv_xOx: ∀t,i1,i2. @⦃i1, 0 @ t⦄ ≡ i2 →
+lemma at_inv_xOx: ∀f,i1,i2. @⦃i1, 0@f⦄ ≡ i2 →
                   (i1 = 0 ∧ i2 = 0) ∨
-                  ∃∃j1,j2. @⦃j1, t⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2.
+                  ∃∃j1,j2. @⦃j1, f⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2.
 /2 width=3 by at_inv_xOx_aux/ qed-.
 
-lemma at_inv_OOx: ∀t,i. @⦃0, 0 @ t⦄ ≡ i → i = 0.
-#t #i #H elim (at_inv_xOx … H) -H * //
+lemma at_inv_OOx: ∀f,i. @⦃0, 0 @ f⦄ ≡ i → i = 0.
+#f #i #H elim (at_inv_xOx … H) -H * //
 #j1 #j2 #_ #H destruct
 qed-.
 
-lemma at_inv_xOO: ∀t,i. @⦃i, 0 @ t⦄ ≡ 0 → i = 0.
-#t #i #H elim (at_inv_xOx … H) -H * //
+lemma at_inv_xOO: ∀f,i. @⦃i, 0@f⦄ ≡ 0 → i = 0.
+#f #i #H elim (at_inv_xOx … H) -H * //
 #j1 #j2 #_ #_ #H destruct
 qed-.
 
-lemma at_inv_SOx: ∀t,i1,i2. @⦃⫯i1, 0 @ t⦄ ≡ i2 →
-                  ∃∃j2. @⦃i1, t⦄ ≡ j2 & i2 = ⫯j2.
-#t #i1 #i2 #H elim (at_inv_xOx … H) -H *
+lemma at_inv_SOx: ∀f,i1,i2. @⦃⫯i1, 0@f⦄ ≡ i2 →
+                  ∃∃j2. @⦃i1, f⦄ ≡ j2 & i2 = ⫯j2.
+#f #i1 #i2 #H elim (at_inv_xOx … H) -H *
 [ #H destruct
 | #j1 #j2 #Hj #H1 #H2 destruct /2 width=3 by ex2_intro/
 ]
 qed-.
 
-lemma at_inv_xOS: ∀t,i1,i2. @⦃i1, 0 @ t⦄ ≡ ⫯i2 →
-                  ∃∃j1. @⦃j1, t⦄ ≡ i2 & i1 = ⫯j1.
-#t #i1 #i2 #H elim (at_inv_xOx … H) -H *
+lemma at_inv_xOS: ∀f,i1,i2. @⦃i1, 0@f⦄ ≡ ⫯i2 →
+                  ∃∃j1. @⦃j1, f⦄ ≡ i2 & i1 = ⫯j1.
+#f #i1 #i2 #H elim (at_inv_xOx … H) -H *
 [ #_ #H destruct
 | #j1 #j2 #Hj #H1 #H2 destruct /2 width=3 by ex2_intro/
 ]
 qed-.
 
-lemma at_inv_SOS: ∀t,i1,i2. @⦃⫯i1, 0 @ t⦄ ≡ ⫯i2 → @⦃i1, t⦄ ≡ i2.
-#t #i1 #i2 #H elim (at_inv_xOx … H) -H *
+lemma at_inv_SOS: ∀f,i1,i2. @⦃⫯i1, 0@f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2.
+#f #i1 #i2 #H elim (at_inv_xOx … H) -H *
 [ #H destruct
 | #j1 #j2 #Hj #H1 #H2 destruct //
 ]
 qed-.
 
-lemma at_inv_OOS: ∀t,i. @⦃0, 0 @ t⦄ ≡ ⫯i → ⊥.
-#t #i #H elim (at_inv_xOx … H) -H *
+lemma at_inv_OOS: ∀f,i. @⦃0, 0@f⦄ ≡ ⫯i → ⊥.
+#f #i #H elim (at_inv_xOx … H) -H *
 [ #_ #H destruct
 | #j1 #j2 #_ #H destruct
 ]
 qed-.
 
-lemma at_inv_SOO: ∀t,i. @⦃⫯i, 0 @ t⦄ ≡ 0 → ⊥.
-#t #i #H elim (at_inv_xOx … H) -H *
+lemma at_inv_SOO: ∀f,i. @⦃⫯i, 0@f⦄ ≡ 0 → ⊥.
+#f #i #H elim (at_inv_xOx … H) -H *
 [ #H destruct
 | #j1 #j2 #_ #_ #H destruct
 ]
 qed-.
 
-fact at_inv_xSx_aux: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → ∀u,a. t = ⫯a @ u →
-                     ∃∃j2. @⦃i1, a@u⦄ ≡ j2 & i2 = ⫯j2.
-#t #i1 #i2 * -t -i1 -i2
-[ #t #u #a #H destruct
-| #t #i1 #i2 #_ #u #a #H destruct
-| #t #b #i1 #i2 #Hi #u #a #H destruct /2 width=3 by ex2_intro/
+fact at_inv_xSx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g,a. f = ⫯a @ g →
+                     ∃∃j2. @⦃i1, a@g⦄ ≡ j2 & i2 = ⫯j2.
+#f #i1 #i2 * -f -i1 -i2
+[ #f #g #a #H destruct
+| #f #i1 #i2 #_ #g #a #H destruct
+| #f #b #i1 #i2 #Hi #g #a #H destruct /2 width=3 by ex2_intro/
 ]
 qed-.
 
-lemma at_inv_xSx: ∀t,b,i1,i2. @⦃i1, ⫯b @ t⦄ ≡ i2 →
-                  ∃∃j2. @⦃i1, b @ t⦄ ≡ j2 & i2 = ⫯j2.
+lemma at_inv_xSx: ∀f,b,i1,i2. @⦃i1, ⫯b@f⦄ ≡ i2 →
+                  ∃∃j2. @⦃i1, b@f⦄ ≡ j2 & i2 = ⫯j2.
 /2 width=3 by at_inv_xSx_aux/ qed-.
 
-lemma at_inv_xSS: ∀t,b,i1,i2. @⦃i1, ⫯b @ t⦄ ≡ ⫯i2 → @⦃i1, b@t⦄ ≡ i2.
-#t #b #i1 #i2 #H elim (at_inv_xSx … H) -H
+lemma at_inv_xSS: ∀f,b,i1,i2. @⦃i1, ⫯b @ f⦄ ≡ ⫯i2 → @⦃i1, b@f⦄ ≡ i2.
+#f #b #i1 #i2 #H elim (at_inv_xSx … H) -H
 #j2 #Hj #H destruct //
 qed-.
 
-lemma at_inv_xSO: ∀t,b,i. @⦃i, ⫯b @ t⦄ ≡ 0 → ⊥.
-#t #b #i #H elim (at_inv_xSx … H) -H
+lemma at_inv_xSO: ∀f,b,i. @⦃i, ⫯b@f⦄ ≡ 0 → ⊥.
+#f #b #i #H elim (at_inv_xSx … H) -H
 #j2 #_ #H destruct
 qed-.
 
 (* alternative definition ***************************************************)
 
-lemma at_O1: ∀b,t. @⦃0, b @ t⦄ ≡ b.
+lemma at_O1: ∀b,f. @⦃0, b@f⦄ ≡ b.
 #b elim b -b /2 width=1 by at_lift/
 qed.
 
-lemma at_S1: ∀b,t,i1,i2. @⦃i1, t⦄ ≡ i2 → @⦃⫯i1, b@t⦄ ≡ ⫯(b+i2).
+lemma at_S1: ∀b,f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃⫯i1, b@f⦄ ≡ ⫯(b+i2).
 #b elim b -b /3 width=1 by at_skip, at_lift/
 qed.
 
-lemma at_inv_O1: ∀t,b,i2. @⦃0, b@t⦄ ≡ i2 → i2 = b.
-#t #b elim b -b /2 width=2 by at_inv_OOx/
+lemma at_inv_O1: ∀f,b,i2. @⦃0, b@f⦄ ≡ i2 → i2 = b.
+#f #b elim b -b /2 width=2 by at_inv_OOx/
 #b #IH #i2 #H elim (at_inv_xSx … H) -H
 #j2 #Hj #H destruct /3 width=1 by eq_f/
 qed-.
 
-lemma at_inv_S1: ∀t,b,j1,i2. @⦃⫯j1, b@t⦄ ≡ i2 → ∃∃j2. @⦃j1, t⦄ ≡ j2 & i2 =⫯(b+j2).
-#t #b elim b -b /2 width=1 by at_inv_SOx/
+lemma at_inv_S1: ∀f,b,j1,i2. @⦃⫯j1, b@f⦄ ≡ i2 → ∃∃j2. @⦃j1, f⦄ ≡ j2 & i2 =⫯(b+j2).
+#f #b elim b -b /2 width=1 by at_inv_SOx/
 #b #IH #j1 #i2 #H elim (at_inv_xSx … H) -H
 #j2 #Hj #H destruct elim (IH … Hj) -IH -Hj
 #i2 #Hi #H destruct /2 width=3 by ex2_intro/
 qed-.
 
-lemma at_total: ∀i,t. @⦃i, t⦄ ≡ t@❴i❵.
+lemma at_total: ∀i,f. @⦃i, f⦄ ≡ f@❴i❵.
 #i elim i -i
 [ * // | #i #IH * /3 width=1 by at_S1/ ]
 qed.
 
 (* Advanced forward lemmas on at ********************************************)
 
-lemma at_increasing: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → i1 ≤ i2.
-#t #i1 #i2 #H elim H -t -i1 -i2 /2 width=1 by le_S_S, le_S/
+lemma at_increasing: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → i1 ≤ i2.
+#f #i1 #i2 #H elim H -f -i1 -i2 /2 width=1 by le_S_S, le_S/
 qed-.
 
-lemma at_increasing_plus: ∀t,b,i1,i2. @⦃i1, b@t⦄ ≡ i2 → i1 + b ≤ i2.
-#t #b *
+lemma at_increasing_plus: ∀f,b,i1,i2. @⦃i1, b@f⦄ ≡ i2 → i1 + b ≤ i2.
+#f #b *
 [ #i2 #H >(at_inv_O1 … H) -i2 //
 | #i1 #i2 #H elim (at_inv_S1 … H) -H
   #j1 #Ht #H destruct
@@ -174,15 +174,15 @@ lemma at_increasing_plus: ∀t,b,i1,i2. @⦃i1, b@t⦄ ≡ i2 → i1 + b ≤ i2.
 ]
 qed-.
 
-lemma at_increasing_strict: ∀t,b,i1,i2. @⦃i1, ⫯b @ t⦄ ≡ i2 →
-                            i1 < i2 ∧ @⦃i1, b@t⦄ ≡ ⫰i2.
-#t #b #i1 #i2 #H elim (at_inv_xSx … H) -H
+lemma at_increasing_strict: ∀f,b,i1,i2. @⦃i1, ⫯b @ f⦄ ≡ i2 →
+                            i1 < i2 ∧ @⦃i1, b@f⦄ ≡ ⫰i2.
+#f #b #i1 #i2 #H elim (at_inv_xSx … H) -H
 #j2 #Hj #H destruct /4 width=2 by conj, at_increasing, le_S_S/
 qed-.
 
-lemma at_fwd_id: ∀t,b,i. @⦃i, b@t⦄ ≡ i → b = 0.
-#t #b *
-[ #H <(at_inv_O1 … H) -t -b //
+lemma at_fwd_id: ∀f,b,i. @⦃i, b@f⦄ ≡ i → b = 0.
+#f #b *
+[ #H <(at_inv_O1 … H) -f -b //
 | #i #H elim (at_inv_S1 … H) -H
   #j #H #H0 destruct lapply (at_increasing … H) -H
   #H lapply (eq_minus_O … H) -H //
@@ -191,92 +191,92 @@ qed.
 
 (* Main properties on at ****************************************************)
 
-lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀t. @⦃i2, t⦄ ≡ i2 → @⦃i1, t⦄ ≡ i1.
+lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @⦃i2, f⦄ ≡ i2 → @⦃i1, f⦄ ≡ i1.
 #i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ]
-* #b #t #H lapply (at_fwd_id … H)
+* #b #f #H lapply (at_fwd_id … H)
 #H0 destruct /4 width=1 by at_S1, at_inv_SOS/
 qed-.
 
-let corec at_ext: ∀t1,t2. (∀i,i1,i2. @⦃i, t1⦄ ≡ i1 → @⦃i, t2⦄ ≡ i2 → i1 = i2) → t1 ≐ t2 ≝ ?.
-* #b1 #t1 * #b2 #t2 #Hi lapply (Hi 0 b1 b2 ? ?) //
-#H lapply (at_ext t1 t2 ?) /2 width=1 by eq_seq/ -at_ext
+let corec at_ext: ∀f1,f2. (∀i,i1,i2. @⦃i, f1⦄ ≡ i1 → @⦃i, f2⦄ ≡ i2 → i1 = i2) → f1 ≐ f2 ≝ ?.
+* #b1 #f1 * #b2 #f2 #Hi lapply (Hi 0 b1 b2 ? ?) //
+#H lapply (at_ext f1 f2 ?) /2 width=1 by eq_seq/ -at_ext
 #j #j1 #j2 #H1 #H2 @(injective_plus_r … b2) /4 width=5 by at_S1, injective_S/ (**) (* full auto fails *)
 qed-.
 
-theorem at_monotonic: ∀i1,i2. i1 < i2 → ∀t1,t2. t1 ≐ t2 → ∀j1,j2. @⦃i1, t1⦄ ≡ j1 → @⦃i2, t2⦄ ≡ j2 → j1 < j2.
+theorem at_monotonic: ∀i1,i2. i1 < i2 → ∀f1,f2. f1 ≐ f2 → ∀j1,j2. @⦃i1, f1⦄ ≡ j1 → @⦃i2, f2⦄ ≡ j2 → j1 < j2.
 #i1 #i2 #H @(lt_elim … H) -i1 -i2
-[ #i2 * #b1 #t1 * #b2 #t2 #H elim (eq_stream_inv_seq ????? H) -H
+[ #i2 * #b1 #f1 * #b2 #f2 #H elim (eq_stream_inv_seq ????? H) -H
   #H #Ht #j1 #j2 #H1 #H2 destruct
   >(at_inv_O1 … H1) elim (at_inv_S1 … H2) -H2 -j1 //
-| #i1 #i2 #IH * #b1 #t1 * #b2 #t2 #H elim (eq_stream_inv_seq ????? H) -H
+| #i1 #i2 #IH * #b1 #f1 * #b2 #f2 #H elim (eq_stream_inv_seq ????? H) -H
   #H #Ht #j1 #j2 #H1 #H2 destruct
   elim (at_inv_S1 … H2) elim (at_inv_S1 … H1) -H1 -H2
   #x1 #Hx1 #H1 #x2 #Hx2 #H2 destruct /4 width=5 by lt_S_S, monotonic_lt_plus_r/
 ]
 qed-.
 
-theorem at_inv_monotonic: ∀t1,i1,j1. @⦃i1, t1⦄ ≡ j1 → ∀t2,i2,j2. @⦃i2, t2⦄ ≡ j2 → t1 ≐ t2 → j2 < j1 → i2 < i1.
-#t1 #i1 #j1 #H elim H -t1 -i1 -j1
-[ #t1 #t2 #i2 #j2 #_ #_ #H elim (lt_le_false … H) //
-| #t1 #i1 #j1 #_ #IH * #b2 #t2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht
+theorem at_inv_monotonic: ∀f1,i1,j1. @⦃i1, f1⦄ ≡ j1 → ∀f2,i2,j2. @⦃i2, f2⦄ ≡ j2 → f1 ≐ f2 → j2 < j1 → i2 < i1.
+#f1 #i1 #j1 #H elim H -f1 -i1 -j1
+[ #f1 #f2 #i2 #j2 #_ #_ #H elim (lt_le_false … H) //
+| #f1 #i1 #j1 #_ #IH * #b2 #f2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht
   #H0 #Ht destruct elim (at_inv_xOx … H) -H *
   [ #H1 #H2 destruct //
   | #x2 #y2 #Hxy #H1 #H2 destruct /4 width=5 by lt_S_S_to_lt, lt_S_S/
   ]
-| #t1 #b1 #i1 #j1 #_ #IH * #b2 #t2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht
+| #f1 #b1 #i1 #j1 #_ #IH * #b2 #f2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht
   #H0 #Ht destruct elim (at_inv_xSx … H) -H
   #y2 #Hy #H destruct /3 width=5 by eq_seq, lt_S_S_to_lt/
 ]
 qed-.
 
-theorem at_mono: ∀t1,t2. t1 ≐ t2 → ∀i,i1. @⦃i, t1⦄ ≡ i1 → ∀i2. @⦃i, t2⦄ ≡ i2 → i2 = i1.
-#t1 #t2 #Ht #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
+theorem at_mono: ∀f1,f2. f1 ≐ f2 → ∀i,i1. @⦃i, f1⦄ ≡ i1 → ∀i2. @⦃i, f2⦄ ≡ i2 → i2 = i1.
+#f1 #f2 #Ht #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
 #Hi elim (lt_le_false i i) /3 width=8 by at_inv_monotonic, eq_stream_sym/
 qed-.
 
-theorem at_inj: ∀t1,t2. t1 ≐ t2 → ∀i1,i. @⦃i1, t1⦄ ≡ i → ∀i2. @⦃i2, t2⦄ ≡ i → i1 = i2.
-#t1 #t2 #Ht #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
+theorem at_inj: ∀f1,f2. f1 ≐ f2 → ∀i1,i. @⦃i1, f1⦄ ≡ i → ∀i2. @⦃i2, f2⦄ ≡ i → i1 = i2.
+#f1 #f2 #Ht #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
 #Hi elim (lt_le_false i i) /3 width=8 by at_monotonic, eq_stream_sym/
 qed-.
 
-lemma at_inv_total: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → i2 = t@❴i1❵.
+lemma at_inv_total: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → i2 = f@❴i1❵.
 /2 width=6 by at_mono/ qed-.
 
-lemma at_repl_back: ∀i1,i2. eq_stream_repl_back ? (λt. @⦃i1, t⦄ ≡ i2).
-#i1 #i2 #t1 #t2 #Ht #H1 lapply (at_total i1 t2)
-#H2 <(at_mono … Ht … H1 … H2) -t1 -i2 //
+lemma at_repl_back: ∀i1,i2. eq_stream_repl_back ? (λf. @⦃i1, f⦄ ≡ i2).
+#i1 #i2 #f1 #f2 #Ht #H1 lapply (at_total i1 f2)
+#H2 <(at_mono … Ht … H1 … H2) -f1 -i2 //
 qed-.
 
-lemma at_repl_fwd: ∀i1,i2. eq_stream_repl_fwd ? (λt. @⦃i1, t⦄ ≡ i2).
+lemma at_repl_fwd: ∀i1,i2. eq_stream_repl_fwd ? (λf. @⦃i1, f⦄ ≡ i2).
 #i1 #i2 @eq_stream_repl_sym /2 width=3 by at_repl_back/
 qed-.
 
 (* Advanced properties on at ************************************************)
 
 (* Note: see also: trace_at/at_dec *)
-lemma at_dec: ∀t,i1,i2. Decidable (@⦃i1, t⦄ ≡ i2).
-#t #i1 #i2 lapply (at_total i1 t)
-#Ht elim (eq_nat_dec i2 (t@❴i1❵))
+lemma at_dec: ∀f,i1,i2. Decidable (@⦃i1, f⦄ ≡ i2).
+#f #i1 #i2 lapply (at_total i1 f)
+#Ht elim (eq_nat_dec i2 (f@❴i1❵))
 [ #H destruct /2 width=1 by or_introl/
 | /4 width=6 by at_mono, or_intror/
 ]
 qed-.
 
-lemma is_at_dec_le: ∀t,i2,i. (∀i1. i1 + i ≤ i2 → @⦃i1, t⦄ ≡ i2 → ⊥) → Decidable (∃i1. @⦃i1, t⦄ ≡ i2).
-#t #i2 #i elim i -i
+lemma is_at_dec_le: ∀f,i2,i. (∀i1. i1 + i ≤ i2 → @⦃i1, f⦄ ≡ i2 → ⊥) → Decidable (∃i1. @⦃i1, f⦄ ≡ i2).
+#f #i2 #i elim i -i
 [ #Ht @or_intror * /3 width=3 by at_increasing/
-| #i #IH #Ht elim (at_dec t (i2-i) i2) /3 width=2 by ex_intro, or_introl/
+| #i #IH #Ht elim (at_dec f (i2-i) i2) /3 width=2 by ex_intro, or_introl/
   #Hi2 @IH -IH #i1 #H #Hi elim (le_to_or_lt_eq … H) -H /2 width=3 by/
   #H destruct -Ht /2 width=1 by/
 ]
 qed-.
 
 (* Note: see also: trace_at/is_at_dec *)
-lemma is_at_dec: ∀t,i2. Decidable (∃i1. @⦃i1, t⦄ ≡ i2).
-#t #i2 @(is_at_dec_le ? ? (⫯i2)) /2 width=4 by lt_le_false/
+lemma is_at_dec: ∀f,i2. Decidable (∃i1. @⦃i1, f⦄ ≡ i2).
+#f #i2 @(is_at_dec_le ? ? (⫯i2)) /2 width=4 by lt_le_false/
 qed-.
 
 (* Advanced properties on apply *********************************************)
 
-fact apply_inj_aux: ∀t1,t2. t1 ≐ t2 → ∀i,i1,i2. i = t1@❴i1❵ → i = t2@❴i2❵ → i1 = i2.
+fact apply_inj_aux: ∀f1,f2. f1 ≐ f2 → ∀i,i1,i2. i = f1@❴i1❵ → i = f2@❴i2❵ → i1 = i2.
 /2 width=6 by at_inj/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma
index d76d129407de9cfdfa75f442e5b30ae5a9dbce37..5e3d1e3b222184f1c49bed19fd952b4b83dab37e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma
@@ -19,15 +19,15 @@ include "ground_2/relocation/nstream_after.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
-let corec id: nstream ≝ ↑id.
+let corec id: rtmap ≝ ↑id.
 
 interpretation "identity (nstream)"
    'Identity = (id).
 
-definition isid: predicate nstream ≝ λt. t ≐ 𝐈𝐝.
+definition isid: predicate rtmap ≝ λf. f ≐ 𝐈𝐝.
 
 interpretation "test for identity (trace)"
-   'IsIdentity t = (isid t).
+   'IsIdentity f = (isid f).
 
 (* Basic properties on id ***************************************************)
 
@@ -40,30 +40,30 @@ qed.
 lemma isid_id: 𝐈⦃𝐈𝐝⦄.
 // qed.
 
-lemma isid_push: ∀t. 𝐈⦃t⦄ → 𝐈⦃↑t⦄.
-#t #H normalize >id_unfold /2 width=1 by eq_seq/
+lemma isid_push: ∀f. 𝐈⦃f⦄ → 𝐈⦃↑f⦄.
+#f #H normalize >id_unfold /2 width=1 by eq_seq/
 qed.
 
 (* Basic inversion lemmas on isid *******************************************)
 
-lemma isid_inv_seq: ∀t,a.  𝐈⦃a@t⦄ → 𝐈⦃t⦄ ∧ a = 0.
-#t #a normalize >id_unfold in ⊢ (???%→?);
+lemma isid_inv_seq: ∀f,a.  𝐈⦃a@f⦄ → 𝐈⦃f⦄ ∧ a = 0.
+#f #a normalize >id_unfold in ⊢ (???%→?);
 #H elim (eq_stream_inv_seq ????? H) -H /2 width=1 by conj/
 qed-.
 
-lemma isid_inv_push: ∀t. 𝐈⦃↑t⦄ → 𝐈⦃t⦄.
-* #a #t #H elim (isid_inv_seq … H) -H //
+lemma isid_inv_push: ∀f. 𝐈⦃↑f⦄ → 𝐈⦃f⦄.
+* #a #f #H elim (isid_inv_seq … H) -H //
 qed-.
 
-lemma isid_inv_next: ∀t. 𝐈⦃⫯t⦄ → ⊥.
-* #a #t #H elim (isid_inv_seq … H) -H
+lemma isid_inv_next: ∀f. 𝐈⦃⫯f⦄ → ⊥.
+* #a #f #H elim (isid_inv_seq … H) -H
 #_ #H destruct
 qed-.
 
 (* inversion lemmas on at ***************************************************)
 
-let corec id_inv_at: ∀t. (∀i. @⦃i, t⦄ ≡ i) → t ≐ 𝐈𝐝 ≝ ?.
-* #a #t #Ht lapply (Ht 0)
+let corec id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → f ≐ 𝐈𝐝 ≝ ?.
+* #a #f #Ht lapply (Ht 0)
 #H lapply (at_inv_O1 … H) -H
 #H0 >id_unfold @eq_seq
 [ cases H0 -a //
@@ -73,15 +73,15 @@ let corec id_inv_at: ∀t. (∀i. @⦃i, t⦄ ≡ i) → t ≐ 𝐈𝐝 ≝ ?.
 ]
 qed-.
 
-lemma isid_inv_at: ∀i,t. 𝐈⦃t⦄ → @⦃i, t⦄ ≡ i.
+lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i.
 #i elim i -i
-[ * #a #t #H elim (isid_inv_seq … H) -H //
-| #i #IH * #a #t #H elim (isid_inv_seq … H) -H
+[ * #a #f #H elim (isid_inv_seq … H) -H //
+| #i #IH * #a #f #H elim (isid_inv_seq … H) -H
   /3 width=1 by at_S1/
 ]
 qed-.
 
-lemma isid_inv_at_mono: ∀t,i1,i2. 𝐈⦃t⦄ → @⦃i1, t⦄ ≡ i2 → i1 = i2.
+lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ i2 → i1 = i2.
 /3 width=6 by isid_inv_at, at_mono/ qed-.
 
 (* Properties on at *********************************************************)
@@ -89,57 +89,57 @@ lemma isid_inv_at_mono: ∀t,i1,i2. 𝐈⦃t⦄ → @⦃i1, t⦄ ≡ i2 → i1 =
 lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i.
 /2 width=1 by isid_inv_at/ qed.
 
-lemma isid_at: ∀t. (∀i. @⦃i, t⦄ ≡ i) → 𝐈⦃t⦄.
+lemma isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄.
 /2 width=1 by id_inv_at/ qed.
 
-lemma isid_at_total: ∀t. (∀i1,i2. @⦃i1, t⦄ ≡ i2 → i1 = i2) → 𝐈⦃t⦄.
-#t #Ht @isid_at
-#i lapply (at_total i t)
+lemma isid_at_total: ∀f. (∀i1,i2. @⦃i1, f⦄ ≡ i2 → i1 = i2) → 𝐈⦃f⦄.
+#f #Ht @isid_at
+#i lapply (at_total i f)
 #H >(Ht … H) in ⊢ (???%); -Ht //
 qed.
 
 (* Properties on after ******************************************************)
 
-lemma after_isid_dx: ∀t2,t1,t. t2 ⊚ t1 ≡ t → t2 ≐ t → 𝐈⦃t1⦄.
-#t2 #t1 #t #Ht #H2 @isid_at_total
-#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -t1
+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: ∀t2,t1,t. t2 ⊚ t1 ≡ t → t1 ≐ t → 𝐈⦃t2⦄.
-#t2 #t1 #t #Ht #H1 @isid_at_total
-#i2 #i #Hi2 lapply (at_total i2 t1)
+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 … (t1@❴i2❵) … H0 … Ht)
+#Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht)
 /3 width=7 by at_repl_back, at_mono, at_id_le/
 qed.
 
 (* Inversion lemmas on after ************************************************)
 
-let corec isid_after_sn: ∀t1,t2. 𝐈⦃t1⦄ → t1 ⊚ t2 ≡ t2 ≝ ?.
-* #a1 #t1 * * [ | #a2 ] #t2 #H cases (isid_inv_seq … H) -H
+let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?.
+* #a1 #f1 * * [ | #a2 ] #f2 #H cases (isid_inv_seq … H) -H
 #Ht1 #H1
 [ @(after_zero … H1) -H1 /2 width=1 by/
 | @(after_skip … H1) -H1 /2 width=5 by/
 ]
 qed-.
 
-let corec isid_after_dx: ∀t2,t1. 𝐈⦃t2⦄ → t1 ⊚ t2 ≡ t1 ≝ ?.
-* #a2 #t2 * *
-[ #t1 #H cases (isid_inv_seq … H) -H
+let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?.
+* #a2 #f2 * *
+[ #f1 #H cases (isid_inv_seq … H) -H
   #Ht2 #H2 @(after_zero … H2) -H2 /2 width=1 by/
-| #a1 #t1 #H @(after_drop … a1 a1) /2 width=5 by/
+| #a1 #f1 #H @(after_drop … a1 a1) /2 width=5 by/
 ]
 qed-.
 
-lemma after_isid_inv_sn: ∀t1,t2,t. t1 ⊚ t2 ≡ t →  𝐈⦃t1⦄ → t2 ≐ t.
+lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f →  𝐈⦃f1⦄ → f2 ≐ f.
 /3 width=4 by isid_after_sn, after_mono/
 qed-.
 
-lemma after_isid_inv_dx: ∀t1,t2,t. t1 ⊚ t2 ≡ t →  𝐈⦃t2⦄ → t1 ≐ t.
+lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f →  𝐈⦃f2⦄ → f1 ≐ f.
 /3 width=4 by isid_after_dx, after_mono/
 qed-.
 (*
-lemma after_inv_isid3: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.
+lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.
 qed-.
 *)

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma
index 07a96e4d570826180da25c2fcdf7d96f8bf424ed..e98d8bee1f98515be0b45362e7b3f5d5f9330038 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma
@@ -17,45 +17,53 @@ include "ground_2/relocation/nstream_at.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
-definition push: nstream → nstream ≝ λt. 0@t.
+definition push: rtmap → rtmap ≝ λf. 0@f.
 
-interpretation "push (nstream)" 'Lift t = (push t).
+interpretation "push (nstream)" 'Lift f = (push f).
 
-definition next: nstream → nstream.
-* #a #t @(⫯a@t)
+definition next: rtmap → rtmap.
+* #a #f @(⫯a@f)
 qed.
 
-interpretation "next (nstream)" 'Successor t = (next t).
+interpretation "next (nstream)" 'Successor f = (next f).
 
 (* Basic properties on push *************************************************)
 
-lemma push_at_O: ∀t. @⦃0, ↑t⦄ ≡ 0.
+lemma push_at_O: ∀f. @⦃0, ↑f⦄ ≡ 0.
 // qed.
 
-lemma push_at_S: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → @⦃⫯i1, ↑t⦄ ≡ ⫯i2.
+lemma push_at_S: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃⫯i1, ↑f⦄ ≡ ⫯i2.
 /2 width=1 by at_S1/ qed.
 
 (* Basic inversion lemmas on push *******************************************)
 
-lemma push_inv_at_S: ∀t,i1,i2. @⦃⫯i1, ↑t⦄ ≡ ⫯i2 → @⦃i1, t⦄ ≡ i2.
+lemma push_inv_at_S: ∀f,i1,i2. @⦃⫯i1, ↑f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2.
 /2 width=1 by at_inv_SOS/ qed-.
 
 lemma injective_push: injective ? ? push.
-#t1 #t2 normalize #H destruct //
+#f1 #f2 normalize #H destruct //
+qed-.
+
+lemma discr_push_next: ∀f1,f2. ↑f1 = ⫯f2 → ⊥.
+#f1 * #n2 #f2 normalize #H destruct
+qed-.
+
+lemma discr_next_push: ∀f1,f2. ⫯f1 = ↑f2 → ⊥.
+* #n1 #f1 #f2 normalize #H destruct
 qed-.
 
 (* Basic properties on next *************************************************)
 
-lemma next_at: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → @⦃i1, ⫯t⦄ ≡ ⫯i2.
+lemma next_at: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃i1, ⫯f⦄ ≡ ⫯i2.
 * /2 width=1 by at_lift/
 qed.
 
 (* Basic inversion lemmas on next *******************************************)
 
-lemma next_inv_at: ∀t,i1,i2. @⦃i1, ⫯t⦄ ≡ ⫯i2 → @⦃i1, t⦄ ≡ i2.
+lemma next_inv_at: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2.
 * /2 width=1 by at_inv_xSS/
 qed-.
 
 lemma injective_next: injective ? ? next.
-* #a1 #t1 * #a2 #t2 normalize #H destruct //
+* #a1 #f1 * #a2 #f2 normalize #H destruct //
 qed-.