Step * 1 of Lemma stream-zip_wf


1. Type
2. Type
3. Type
4. 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 (\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