Step * 1 of Lemma l_all_eager_product-map


1. Type
2. value-type(T)
3. Type
4. Type
5. Pa A ⟶ ℙ
6. Pb B ⟶ ℙ
7. Pt T ⟶ ℙ
8. A ⟶ B ⟶ T
9. ∀a:A. ∀b:B.  (Pa[a]  Pb[b]  Pt[f b])
⊢ ∀bs:B List. ((∀a∈[].Pa[a])  (∀b∈bs.Pb[b])  (∀t∈eager-product-map(f;[];bs).Pt[t]))
BY
(Reduce THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  value-type(T)
3.  A  :  Type
4.  B  :  Type
5.  Pa  :  A  {}\mrightarrow{}  \mBbbP{}
6.  Pb  :  B  {}\mrightarrow{}  \mBbbP{}
7.  Pt  :  T  {}\mrightarrow{}  \mBbbP{}
8.  f  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  T
9.  \mforall{}a:A.  \mforall{}b:B.    (Pa[a]  {}\mRightarrow{}  Pb[b]  {}\mRightarrow{}  Pt[f  a  b])
\mvdash{}  \mforall{}bs:B  List.  ((\mforall{}a\mmember{}[].Pa[a])  {}\mRightarrow{}  (\mforall{}b\mmember{}bs.Pb[b])  {}\mRightarrow{}  (\mforall{}t\mmember{}eager-product-map(f;[];bs).Pt[t]))


By


Latex:
(Reduce  0  THEN  Auto)




Home Index