---

Step * 1 1 of Lemma stream-map_wf


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
BY
{ (GenConcl ⌜s1 = ss ∈ (A × stream(A))⌝⋅
   THEN Auto
   THEN DoSubsume
   THEN Auto
   THEN InstLemma `stream-ext` [⌜A⌝]⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  s  :  stream(A)
5.  T  :  Type
6.  stream-map  :  stream(A)  {}\mrightarrow{}  T
7.  s1  :  stream(A)
\mvdash{}  let  a,s'  =  s1 
    in  <f  a,  stream-map  s'>  \mmember{}  B  \mtimes{}  T


By

---

Latex:
(GenConcl  \mkleeneopen{}s1  =  ss\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  DoSubsume
  THEN  Auto
  THEN  InstLemma  `stream-ext`  [\mkleeneopen{}A\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index