---

Step * 2 of Lemma map-iterate-fun-stream


1. j : ℤ
2. 0 < j
3. ∀x,f:Base.  (λiterate-fun-stream,x. x.iterate-fun-stream (f x)^j - 1 ⊥ (f x) ≤ stream-map(f;iterate-fun-stream(f;x)))
4. x : Base@i
5. f : Base@i
6. is-exception(λiterate-fun-stream,x. x.iterate-fun-stream (f x)^j ⊥ (f x))
⊢ f x.λiterate-fun-stream,x. x.iterate-fun-stream (f x)^j - 1 ⊥ (f (f x)) ≤ stream-map(f;iterate-fun-stream(f;x))
BY
{ (RecUnfold `stream-map` 0
   THEN RecUnfold `iterate-fun-stream` 0
   THEN Unfold `s-cons` 0
   THEN Reduce 0
   THEN Fold `s-cons` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}x,f:Base.    (\mlambda{}iterate-fun-stream,x.  x.iterate-fun-stream  (f  x)\^{}j  -  1  \mbot{}  (f  x)  \mleq{}  stream-map(f;itera\000Cte-fun-stream(f;x)))
4.  x  :  Base@i
5.  f  :  Base@i
6.  is-exception(\mlambda{}iterate-fun-stream,x.  x.iterate-fun-stream  (f  x)\^{}j  \mbot{}  (f  x))
\mvdash{}  f  x.\mlambda{}iterate-fun-stream,x.  x.iterate-fun-stream  (f  x)\^{}j  -  1  \mbot{}  (f  (f  x))  \mleq{}  stream-map(f;iterate-fun\000C-stream(f;x))


By

---

Latex:
(RecUnfold  `stream-map`  0
  THEN  RecUnfold  `iterate-fun-stream`  0
  THEN  Unfold  `s-cons`  0
  THEN  Reduce  0
  THEN  Fold  `s-cons`  0
  THEN  Auto)

---

Home Index