---

Step * of Lemma member_list_accum_l_subset

No Annotations
∀[T:Type]
  ∀f:(T List) ⟶ T ⟶ (T List). ∀L,a:T List. ∀x:T.
    ((∀a:T List. ∀x:T.  l_subset(T;a;f[a;x]))
    ⇒ ((x ∈ a) ∨ (∃z:T. ((z ∈ L) ∧ (∀l:T List. (x ∈ f[l;z])))))
    ⇒ (x ∈ accumulate (with value a and list item x):
             f[a;x]
            over list:
              L
            with starting value:
             a)))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN SplitOrHyps THEN Auto THEN ExRepD THEN Try (Complete (Auto))) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}f:(T  List)  {}\mrightarrow{}  T  {}\mrightarrow{}  (T  List).  \mforall{}L,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{}  L)  \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:
                            L
                        with  starting  value:
                          a)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  ExRepD
  THEN  Try  (Complete  (Auto)))

---

Home Index