---

Step * of Lemma s-sub_transitivity

∀[T:Type]. ∀[s,t,r:stream(T)].  (s-sub(T;s;t) ⇒ s-sub(T;t;r) ⇒ s-sub(T;s;r))
BY
{ (Auto THEN D -2 THEN D -1 THEN D 0 With ⌜f o f1⌝  THEN Auto THEN Reduce 0) }

1
1. T : Type
2. s : stream(T)
3. t : stream(T)
4. r : stream(T)
5. f : ℕ ⟶ ℕ
6. ∀i:ℕ. f i < f (i + 1)
7. ∀i:ℕ. (s-nth(i;t) = s-nth(f i;s) ∈ T)
8. f1 : ℕ ⟶ ℕ
9. ∀i:ℕ. f1 i < f1 (i + 1)
10. ∀i:ℕ. (s-nth(i;r) = s-nth(f1 i;t) ∈ T)
11. i : ℕ
⊢ f (f1 i) < f (f1 (i + 1))

2
1. T : Type
2. s : stream(T)
3. t : stream(T)
4. r : stream(T)
5. f : ℕ ⟶ ℕ
6. ∀i:ℕ. f i < f (i + 1)
7. ∀i:ℕ. (s-nth(i;t) = s-nth(f i;s) ∈ T)
8. f1 : ℕ ⟶ ℕ
9. ∀i:ℕ. f1 i < f1 (i + 1)
10. ∀i:ℕ. (s-nth(i;r) = s-nth(f1 i;t) ∈ T)
11. ∀i:ℕ. (f o f1) i < (f o f1) (i + 1)
12. i : ℕ
⊢ s-nth(i;r) = s-nth(f (f1 i);s) ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[s,t,r:stream(T)].    (s-sub(T;s;t)  {}\mRightarrow{}  s-sub(T;t;r)  {}\mRightarrow{}  s-sub(T;s;r))


By

---

Latex:
(Auto  THEN  D  -2  THEN  D  -1  THEN  D  0  With  \mkleeneopen{}f  o  f1\mkleeneclose{}    THEN  Auto  THEN  Reduce  0)

---

Home Index