---

Step * of Lemma member-product-map

∀[A,B,C:Type].
  ∀F:A ⟶ B ⟶ C. ∀as:A List. ∀bs:B List. ∀c:C.
    ((c ∈ product-map(F;as;bs)) ⇐⇒ ∃a:A. ((a ∈ as) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C)))))
BY
{ (Unfold `product-map` 0
   THEN InductionOnList
   THEN Reduce 0
   THEN RWW "concat-cons nil_member cons_member member_append member-map map_append_sq" 0
   THEN Auto
   THEN ExRepD
   THEN Auto) }

1
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. F : A ⟶ B ⟶ C
5. u : A
6. v : A List
7. ∀bs:B List. ∀c:C.
     ((c ∈ concat(map(λa.map(λb.(F a b);bs);v))) ⇐⇒ ∃a:A. ((a ∈ v) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C)))))
8. bs : B List
9. c : C
10. (∃y:B. ((y ∈ bs) ∧ (c = ((λb.(F u b)) y) ∈ C))) ∨ (c ∈ concat(map(λa.map(λb.(F a b);bs);v)))
⊢ ∃a:A. (((a = u ∈ A) ∨ (a ∈ v)) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C))))

2
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. F : A ⟶ B ⟶ C
5. u : A
6. v : A List
7. ∀bs:B List. ∀c:C.
     ((c ∈ concat(map(λa.map(λb.(F a b);bs);v))) ⇐⇒ ∃a:A. ((a ∈ v) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C)))))
8. bs : B List
9. c : C
10. a : A
11. (a = u ∈ A) ∨ (a ∈ v)
12. b : B
13. (b ∈ bs)
14. c = (F a b) ∈ C
⊢ (∃y:B. ((y ∈ bs) ∧ (c = ((λb.(F u b)) y) ∈ C))) ∨ (c ∈ concat(map(λa.map(λb.(F a b);bs);v)))

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].
    \mforall{}F:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C.  \mforall{}as:A  List.  \mforall{}bs:B  List.  \mforall{}c:C.
        ((c  \mmember{}  product-map(F;as;bs))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A.  ((a  \mmember{}  as)  \mwedge{}  (\mexists{}b:B.  ((b  \mmember{}  bs)  \mwedge{}  (c  =  (F  a  b))))))


By

---

Latex:
(Unfold  `product-map`  0
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  RWW  "concat-cons  nil\_member  cons\_member  member\_append  member-map  map\_append\_sq"  0
  THEN  Auto
  THEN  ExRepD
  THEN  Auto)

---

Home Index