---

Step * 1 of Lemma tl-stream-zip


1. f : Top
2. as : stream(Top)
3. bs : stream(Top)
⊢ s-tl(let a,as' = as 
       in let b,bs' = bs 
          in <f a b, stream-zip(f;as';bs')>) ~ stream-zip(f;s-tl(as);s-tl(bs))
BY
{ ((GenConcl ⌜as = ss ∈ (Top × stream(Top))⌝⋅⋅
    THENA (Auto THEN DoSubsume THEN Auto THEN InstLemma `stream-ext` [⌜Top⌝]⋅ THEN Auto)
    )
   THEN D -2
   THEN Reduce 0
   THEN (GenConcl ⌜bs = ss ∈ (Top × stream(Top))⌝⋅⋅
         THENA (Auto THEN DoSubsume THEN Auto THEN InstLemma `stream-ext` [⌜Top⌝]⋅ THEN Auto)
         )
   THEN D -2
   THEN RepUR ``s-tl`` 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  f  :  Top
2.  as  :  stream(Top)
3.  bs  :  stream(Top)
\mvdash{}  s-tl(let  a,as'  =  as 
              in  let  b,bs'  =  bs 
                    in  <f  a  b,  stream-zip(f;as';bs')>)  \msim{}  stream-zip(f;s-tl(as);s-tl(bs))


By

---

Latex:
((GenConcl  \mkleeneopen{}as  =  ss\mkleeneclose{}\mcdot{}\mcdot{}
    THENA  (Auto  THEN  DoSubsume  THEN  Auto  THEN  InstLemma  `stream-ext`  [\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}  THEN  Auto)
    )
  THEN  D  -2
  THEN  Reduce  0
  THEN  (GenConcl  \mkleeneopen{}bs  =  ss\mkleeneclose{}\mcdot{}\mcdot{}
              THENA  (Auto  THEN  DoSubsume  THEN  Auto  THEN  InstLemma  `stream-ext`  [\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}  THEN  Auto)
              )
  THEN  D  -2
  THEN  RepUR  ``s-tl``  0
  THEN  Auto)\mcdot{}

---

Home Index