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


1. [X] Type
2. List
3. 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)))))
BY
((RWO  "-1" THEN Auto)
   THEN (All (RWW "member_append member_map cons_member" THENA Auto)
   THEN Reduce -1
   THEN Reduce 0
   THEN SplitOrHyps
   THEN ExRepD
   THEN Auto) }

1
1. [X] Type
2. List
3. 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 List List
6. cs List List
7. List
8. u@0 List
9. v@0 List
10. (u@0 u ∈ (X List)) ∨ (u@0 ∈ v)
11. (v@0 ∈ bs)
12. (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))))


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)))))
\mvdash{}  \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  @  map(\mlambda{}b.(u  @  b);bs)))
        \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  cs)  \mvee{}  (\mexists{}u@0,v@0:X  List.  ((u@0  \mmember{}  [u  /  v])  \mwedge{}  (v@0  \mmember{}  bs)  \mwedge{}  (x  =  (u@0  @  v@0)))))


By


Latex:
((RWO    "-1"  0  THEN  Auto)
  THEN  (All  (RWW  "member\_append  member\_map  cons\_member"  )  THENA  Auto)
  THEN  Reduce  -1
  THEN  Reduce  0
  THEN  SplitOrHyps
  THEN  ExRepD
  THEN  Auto)




Home Index