Step
*
1
of Lemma
stream-zip_wf
1. A : Type
2. B : Type
3. C : Type
4. f : A ⟶ B ⟶ C
5. as : stream(A)
6. bs : stream(B)
7. ∀[n:ℕ]. ∀[as:primrec(n;Top;λ,T. (A × T))]. ∀[bs:primrec(n;Top;λ,T. (B × T))].
     (stream-zip(f;as;bs) ∈ primrec(n;Top;λ,T. (C × T)))
⊢ stream-zip(f;as;bs) ∈ stream(C)
BY
{ (All (RepUR ``stream corec``)
   THEN Auto
   THEN BackThruSomeHyp
   THEN OnMaybeHyp 5 (\h. (With ⌜n⌝ (D h)⋅ THEN Complete (Auto)))) }
Latex:
Latex:
1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  f  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C
5.  as  :  stream(A)
6.  bs  :  stream(B)
7.  \mforall{}[n:\mBbbN{}].  \mforall{}[as:primrec(n;Top;\mlambda{},T.  (A  \mtimes{}  T))].  \mforall{}[bs:primrec(n;Top;\mlambda{},T.  (B  \mtimes{}  T))].
          (stream-zip(f;as;bs)  \mmember{}  primrec(n;Top;\mlambda{},T.  (C  \mtimes{}  T)))
\mvdash{}  stream-zip(f;as;bs)  \mmember{}  stream(C)
By
Latex:
(All  (RepUR  ``stream  corec``)
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  OnMaybeHyp  5  (\mbackslash{}h.  (With  \mkleeneopen{}n\mkleeneclose{}  (D  h)\mcdot{}  THEN  Complete  (Auto))))
Home
Index