---

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

.....assertion..... 
1. [X] : Type
⊢ ∀as,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:
            as
          with starting value:
           cs))
    ⇐⇒ (x ∈ cs) ∨ (∃u,v:X List. ((u ∈ as) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List)))))
BY
{ (InductionOnList THEN Reduce 0) }

1
1. [X] : Type
⊢ ∀bs,cs:X List List. ∀x:X List.
    ((x ∈ cs) ⇐⇒ (x ∈ cs) ∨ (∃u,v:X List. ((u ∈ []) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List)))))

2
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)))))
⊢ ∀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 @ map(λb.(u @ b);bs)))
    ⇐⇒ (x ∈ cs) ∨ (∃u@0,v@0:X List. ((u@0 ∈ [u / v]) ∧ (v@0 ∈ bs) ∧ (x = (u@0 @ v@0) ∈ (X List)))))

---

Latex:

---

Latex:
.....assertion..... 
1.  [X]  :  Type
\mvdash{}  \mforall{}as,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:
                        as
                    with  starting  value:
                      cs))
        \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  cs)  \mvee{}  (\mexists{}u,v:X  List.  ((u  \mmember{}  as)  \mwedge{}  (v  \mmember{}  bs)  \mwedge{}  (x  =  (u  @  v)))))


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index