---

Step * 2 2 of Lemma l_all_eager_product-map


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]))
13. u1 : B
14. v1 : B List
15. (∀a∈[u / v].Pa[a])
16. (∀b∈[u1 / v1].Pb[b])
17. (∀b∈v1.Pb[b]) ⇒ (∀t∈eager-product-map(f;[u / v];v1).Pt[t])
⊢ (∀t∈eager-product-map(f;[u / v];[u1 / v1]).Pt[t])
BY
{ (((RWO "l_all_cons" (-3) THENA Auto) THEN D -3)
   THEN Reduce 0
   THEN (Assert (∀t∈eager-product-map(f;v;[u1 / v1]).Pt[t]) BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜eager-product-map(f;v;[u1 / v1])⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `X' (-1)
   THEN Auto) }

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])
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]))
13. u1 : B
14. v1 : B List
15. Pa[u]
16. (∀a∈v.Pa[a])
17. (∀b∈[u1 / v1].Pb[b])
18. (∀b∈v1.Pb[b]) ⇒ (∀t∈eager-product-map(f;[u / v];v1).Pt[t])
19. X : T List
20. (∀t∈X.Pt[t])
⊢ (∀t∈eager-map-append(f u;[u1 / v1];X).Pt[t])

---

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])
10.  u  :  A
11.  v  :  A  List
12.  \mforall{}bs:B  List.  ((\mforall{}a\mmember{}v.Pa[a])  {}\mRightarrow{}  (\mforall{}b\mmember{}bs.Pb[b])  {}\mRightarrow{}  (\mforall{}t\mmember{}eager-product-map(f;v;bs).Pt[t]))
13.  u1  :  B
14.  v1  :  B  List
15.  (\mforall{}a\mmember{}[u  /  v].Pa[a])
16.  (\mforall{}b\mmember{}[u1  /  v1].Pb[b])
17.  (\mforall{}b\mmember{}v1.Pb[b])  {}\mRightarrow{}  (\mforall{}t\mmember{}eager-product-map(f;[u  /  v];v1).Pt[t])
\mvdash{}  (\mforall{}t\mmember{}eager-product-map(f;[u  /  v];[u1  /  v1]).Pt[t])


By

---

Latex:
(((RWO  "l\_all\_cons"  (-3)  THENA  Auto)  THEN  D  -3)
  THEN  Reduce  0
  THEN  (Assert  (\mforall{}t\mmember{}eager-product-map(f;v;[u1  /  v1]).Pt[t])  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}eager-product-map(f;v;[u1  /  v1])\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `X'  (-1)
  THEN  Auto)

---

Home Index