---

Step * of Lemma member-free-dl-meet

∀[X:Type]
  ∀as,bs:X List List. ∀x:X List.
    ((x ∈ free-dl-meet(as;bs)) ⇐⇒ ∃u,v:X List. ((u ∈ as) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List))))
BY
{ ((Intro THEN Unfold `free-dl-meet` 0)
   THEN (Assert ⌜∀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)))))⌝⋅
        THENM (RWO "-1" 0 THEN Auto)
        )
   ) }

1
.....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)))))

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}as,bs:X  List  List.  \mforall{}x:X  List.
        ((x  \mmember{}  free-dl-meet(as;bs))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}u,v:X  List.  ((u  \mmember{}  as)  \mwedge{}  (v  \mmember{}  bs)  \mwedge{}  (x  =  (u  @  v))))


By

---

Latex:
((Intro  THEN  Unfold  `free-dl-meet`  0)
  THEN  (Assert  \mkleeneopen{}\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)))))\mkleeneclose{}\mcdot{}
            THENM  (RWO  "-1"  0  THEN  Auto)
            )
  )

---

Home Index