---

Step * of Lemma l_all_eager_product-map

∀T:Type
  ∀A,B:Type. ∀Pa:A ⟶ ℙ. ∀Pb:B ⟶ ℙ. ∀Pt:T ⟶ ℙ. ∀f:A ⟶ B ⟶ T.
    ((∀a:A. ∀b:B.  (Pa[a] ⇒ Pb[b] ⇒ Pt[f a b]))
    ⇒ (∀as:A List. ∀bs:B List.  ((∀a∈as.Pa[a]) ⇒ (∀b∈bs.Pb[b]) ⇒ (∀t∈eager-product-map(f;as;bs).Pt[t])))) 
  supposing value-type(T)
BY
{ InductionOnList }

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

2
1. T : Type
2. value-type(T)
3. A : Type
4. B : Type
5. Pa : A ⟶ ℙ
6. Pb : B ⟶ ℙ
7. Pt : T ⟶ ℙ
8. f : A ⟶ B ⟶ T
9. ∀a:A. ∀b:B.  (Pa[a] ⇒ Pb[b] ⇒ Pt[f a b])
10. u : A
11. v : A List
12. ∀bs:B List. ((∀a∈v.Pa[a]) ⇒ (∀b∈bs.Pb[b]) ⇒ (∀t∈eager-product-map(f;v;bs).Pt[t]))
⊢ ∀bs:B List. ((∀a∈[u / v].Pa[a]) ⇒ (∀b∈bs.Pb[b]) ⇒ (∀t∈eager-product-map(f;[u / v];bs).Pt[t]))

---

Latex:

---

Latex:
\mforall{}T:Type
    \mforall{}A,B:Type.  \mforall{}Pa:A  {}\mrightarrow{}  \mBbbP{}.  \mforall{}Pb:B  {}\mrightarrow{}  \mBbbP{}.  \mforall{}Pt:T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  T.
        ((\mforall{}a:A.  \mforall{}b:B.    (Pa[a]  {}\mRightarrow{}  Pb[b]  {}\mRightarrow{}  Pt[f  a  b]))
        {}\mRightarrow{}  (\mforall{}as:A  List.  \mforall{}bs:B  List.
                    ((\mforall{}a\mmember{}as.Pa[a])  {}\mRightarrow{}  (\mforall{}b\mmember{}bs.Pb[b])  {}\mRightarrow{}  (\mforall{}t\mmember{}eager-product-map(f;as;bs).Pt[t])))) 
    supposing  value-type(T)


By

---

Latex:
InductionOnList

---

Home Index