---

Step * of Lemma stream-zip_wf

∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[as:stream(A)]. ∀[bs:stream(B)].  (stream-zip(f;as;bs) ∈ stream(C))
BY
{ (Auto
   THEN (Assert ∀[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))) BY
               (InductionOnNat
                THEN (RWO "primrec-unroll" 0 THENA Auto)
                THEN AutoSplit
                THEN RecUnfold `stream-zip` 0
                THEN Auto))
   )⋅ }

1
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)

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[as:stream(A)].  \mforall{}[bs:stream(B)].
    (stream-zip(f;as;bs)  \mmember{}  stream(C))


By

---

Latex:
(Auto
  THEN  (Assert  \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)))  BY
                          (InductionOnNat
                            THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                            THEN  AutoSplit
                            THEN  RecUnfold  `stream-zip`  0
                            THEN  Auto))
  )\mcdot{}

---

Home Index