---

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


1. j : ℤ
2. 0 < j
3. ∀x,f:Base.  (λstream-map,s. let a,s' = s in <f a, stream-map s'>^j - 1 ⊥ iterate-fun-stream(f;x) ≤ iterate-fun-stream\000C(f;f x))
4. x : Base@i
5. f : Base@i
6. is-exception(λstream-map,s. let a,s' = s in <f a, stream-map s'>^j ⊥ iterate-fun-stream(f;x))
⊢ <f x, λstream-map,s. let a,s' = s in <f a, stream-map s'>^j - 1 ⊥ (fix((λiterate-fun-stream,x. x.iterate-fun-stream (f\000C x))) (f x))> 
  ≤ iterate-fun-stream(f;f x)
BY
{ (Fold `iterate-fun-stream` 0
   THEN RW (AddrC [2] (RecUnfoldC `iterate-fun-stream`)) 0
   THEN Unfold `s-cons` 0
   THEN Reduce 0
   THEN Fold `s-cons` 0
   THEN Auto
   THEN InstHyp [⌜f x⌝;⌜f⌝] 3⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}x,f:Base.
          (\mlambda{}stream-map,s.  let  a,s'  =  s  in  <f  a,  stream-map  s'>\^{}j  -  1  \mbot{}  iterate-fun-stream(f;x) 
            \mleq{}  iterate-fun-stream(f;f  x))
4.  x  :  Base@i
5.  f  :  Base@i
6.  is-exception(\mlambda{}stream-map,s.  let  a,s'  =  s  in  <f  a,  stream-map  s'>\^{}j  \mbot{}  iterate-fun-stream(f;x))
\mvdash{}  <f  x
    ,  \mlambda{}stream-map,s.  let  a,s'  =  s  in  <f  a,  stream-map  s'>\^{}j  -  1  \mbot{} 
        (fix((\mlambda{}iterate-fun-stream,x.  x.iterate-fun-stream  (f  x)))  (f  x))
    >  \mleq{}  iterate-fun-stream(f;f  x)


By

---

Latex:
(Fold  `iterate-fun-stream`  0
  THEN  RW  (AddrC  [2]  (RecUnfoldC  `iterate-fun-stream`))  0
  THEN  Unfold  `s-cons`  0
  THEN  Reduce  0
  THEN  Fold  `s-cons`  0
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}f  x\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  3\mcdot{}
  THEN  Auto)

---

Home Index