---

Step * of Lemma convolution_wf

∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C ⟶ C]. ∀[c0:C]. ∀[L1:A List]. ∀[L2:B List].  (convolution(a,b,c.f[a;b;c];c0;L1;L2) ∈ C)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C  {}\mrightarrow{}  C].  \mforall{}[c0:C].  \mforall{}[L1:A  List].  \mforall{}[L2:B  List].
    (convolution(a,b,c.f[a;b;c];c0;L1;L2)  \mmember{}  C)


By

---

Latex:
ProveWfLemma

---

Home Index