---

Step * 1 of Lemma member_list_accum_l_subset


1. [T] : Type
2. f : (T List) ⟶ T ⟶ (T List)
3. u : T
4. v : T List
5. ∀a:T List. ∀x:T.
     ((∀a:T List. ∀x:T.  l_subset(T;a;f[a;x]))
     ⇒ ((x ∈ a) ∨ (∃z:T. ((z ∈ v) ∧ (∀l:T List. (x ∈ f[l;z])))))
     ⇒ (x ∈ accumulate (with value a and list item x):
              f[a;x]
             over list:
               v
             with starting value:
              a)))
6. a : T List
7. x : T
8. ∀a:T List. ∀x:T.  l_subset(T;a;f[a;x])
9. z : T
10. (z ∈ [u / v])
11. ∀l:T List. (x ∈ f[l;z])
⊢ (x ∈ accumulate (with value a and list item x):
        f[a;x]
       over list:
         v
       with starting value:
        f[a;u]))
BY
{ ((BHyp (-7) THEN Auto)
   THEN GenListD (-2)
   THEN D (-2)
   THEN Try (Complete ((OrRight THEN Auto)))
   THEN (OrLeft THENA Auto)
   THEN (RevHypSubst' (-2) 0 THENA Auto)
   THEN BHyp (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  (T  List)  {}\mrightarrow{}  T  {}\mrightarrow{}  (T  List)
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}a:T  List.  \mforall{}x:T.
          ((\mforall{}a:T  List.  \mforall{}x:T.    l\_subset(T;a;f[a;x]))
          {}\mRightarrow{}  ((x  \mmember{}  a)  \mvee{}  (\mexists{}z:T.  ((z  \mmember{}  v)  \mwedge{}  (\mforall{}l:T  List.  (x  \mmember{}  f[l;z])))))
          {}\mRightarrow{}  (x  \mmember{}  accumulate  (with  value  a  and  list  item  x):
                            f[a;x]
                          over  list:
                              v
                          with  starting  value:
                            a)))
6.  a  :  T  List
7.  x  :  T
8.  \mforall{}a:T  List.  \mforall{}x:T.    l\_subset(T;a;f[a;x])
9.  z  :  T
10.  (z  \mmember{}  [u  /  v])
11.  \mforall{}l:T  List.  (x  \mmember{}  f[l;z])
\mvdash{}  (x  \mmember{}  accumulate  (with  value  a  and  list  item  x):
                f[a;x]
              over  list:
                  v
              with  starting  value:
                f[a;u]))


By

---

Latex:
((BHyp  (-7)  THEN  Auto)
  THEN  GenListD  (-2)
  THEN  D  (-2)
  THEN  Try  (Complete  ((OrRight  THEN  Auto)))
  THEN  (OrLeft  THENA  Auto)
  THEN  (RevHypSubst'  (-2)  0  THENA  Auto)
  THEN  BHyp  (-1)
  THEN  Auto)

---

Home Index