---

Step * 1 2 1 of Lemma member-free-dl-meet


1. [X] : Type
2. u : X List
3. v : X List List
4. ∀bs,cs:X List List. ∀x:X List.
     ((x ∈ accumulate (with value cs and list item a):
            cs @ map(λb.(a @ b);bs)
           over list:
             v
           with starting value:
            cs))
     ⇐⇒ (x ∈ cs) ∨ (∃u,v@0:X List. ((u ∈ v) ∧ (v@0 ∈ bs) ∧ (x = (u @ v@0) ∈ (X List)))))
5. bs : X List List
6. cs : X List List
7. x : X List
8. u@0 : X List
9. v@0 : X List
10. (u@0 = u ∈ (X List)) ∨ (u@0 ∈ v)
11. (v@0 ∈ bs)
12. x = (u@0 @ v@0) ∈ (X List)
⊢ ((x ∈ cs) ∨ (∃y:X List. ((y ∈ bs) ∧ (x = (u @ y) ∈ (X List)))))
∨ (∃u,v@0:X List. ((u ∈ v) ∧ (v@0 ∈ bs) ∧ (x = (u @ v@0) ∈ (X List))))
BY
{ (SplitOrHyps THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  u  :  X  List
3.  v  :  X  List  List
4.  \mforall{}bs,cs:X  List  List.  \mforall{}x:X  List.
          ((x  \mmember{}  accumulate  (with  value  cs  and  list  item  a):
                        cs  @  map(\mlambda{}b.(a  @  b);bs)
                      over  list:
                          v
                      with  starting  value:
                        cs))
          \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  cs)  \mvee{}  (\mexists{}u,v@0:X  List.  ((u  \mmember{}  v)  \mwedge{}  (v@0  \mmember{}  bs)  \mwedge{}  (x  =  (u  @  v@0)))))
5.  bs  :  X  List  List
6.  cs  :  X  List  List
7.  x  :  X  List
8.  u@0  :  X  List
9.  v@0  :  X  List
10.  (u@0  =  u)  \mvee{}  (u@0  \mmember{}  v)
11.  (v@0  \mmember{}  bs)
12.  x  =  (u@0  @  v@0)
\mvdash{}  ((x  \mmember{}  cs)  \mvee{}  (\mexists{}y:X  List.  ((y  \mmember{}  bs)  \mwedge{}  (x  =  (u  @  y)))))
\mvee{}  (\mexists{}u,v@0:X  List.  ((u  \mmember{}  v)  \mwedge{}  (v@0  \mmember{}  bs)  \mwedge{}  (x  =  (u  @  v@0))))


By

---

Latex:
(SplitOrHyps  THEN  Auto)

---

Home Index