---

Step * 1 of Lemma stream-map_wf


1. A : Type
2. B : Type
3. f : A ⟶ B
4. s : stream(A)
⊢ fix((λstream-map,s. let a,s' = s in <f a, stream-map s'>)) s ∈ corec(S.B × S)
BY
{ (BLemma `fix_wf_corec_parameter` THEN Try (Complete (Auto)) THEN Isect2CD THEN Auto) }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. s : stream(A)
5. T : Type
6. stream-map : stream(A) ⟶ T
7. s1 : stream(A)
⊢ let a,s' = s1 
  in <f a, stream-map s'> ∈ B × T

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  s  :  stream(A)
\mvdash{}  fix((\mlambda{}stream-map,s.  let  a,s'  =  s  in  <f  a,  stream-map  s'>))  s  \mmember{}  corec(S.B  \mtimes{}  S)


By

---

Latex:
(BLemma  `fix\_wf\_corec\_parameter`  THEN  Try  (Complete  (Auto))  THEN  Isect2CD  THEN  Auto)

---

Home Index