---

Step * of Lemma map-iterate-fun-stream

∀[f,x:Top].  (iterate-fun-stream(f;f x) ~ stream-map(f;iterate-fun-stream(f;x)))
BY
{ (Auto
   THEN SqequalSqle
   THEN SqLeTopToBase
   THEN Repeat (UnfoldAtAddr [1] 0)
   THEN OneFixpointLeast
   THEN Repeat (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN Auto
   THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)
   THEN Reduce 0
   THEN All (RepUR ``cons``)) }

1
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. (λ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))

2
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))

3
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. (λ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)

4
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)

---

Latex:

---

Latex:
\mforall{}[f,x:Top].    (iterate-fun-stream(f;f  x)  \msim{}  stream-map(f;iterate-fun-stream(f;x)))


By

---

Latex:
(Auto
  THEN  SqequalSqle
  THEN  SqLeTopToBase
  THEN  Repeat  (UnfoldAtAddr  [1]  0)
  THEN  OneFixpointLeast
  THEN  Repeat  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  Auto
  THEN  (RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  All  (RepUR  ``cons``))

---

Home Index