---

Step * of Lemma combine-list-member

∀[T:Type]
  ∀f:T ⟶ T ⟶ T. ∀L:T List.
    ((∀x,y:T.  ((f[x;y] = x ∈ T) ∨ (f[x;y] = y ∈ T))) ⇒ 0 < ||L|| ⇒ (combine-list(x,y.f[x;y];L) ∈ L))
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN D -3
   THEN Reduce (-1)
   THEN Try (Complete (Auto))
   THEN Thin (-1)
   THEN MoveToConcl (-3)
   THEN RepUR ``combine-list`` 0
   THEN ListInd (-2)
   THEN Reduce 0
   THEN Try ((RWO "member_singleton" 0 THEN Auto)⋅)
   THEN Auto
   THEN RenameVar `x' (-1)
   THEN (Assert (f[x;u] = x ∈ T) ∨ (f[x;u] = u ∈ T) BY
               Auto)
   THEN D -1
   THEN (HypSubst' -1 0 THENA Auto)
   THEN BLemma `cons_member`
   THEN Auto) }

1
1. [T] : Type
2. f : T ⟶ T ⟶ T
3. ∀x,y:T.  ((f[x;y] = x ∈ T) ∨ (f[x;y] = y ∈ T))
4. u : T
5. v : T List
6. ∀u:T. (accumulate (with value x and list item y): f[x;y]over list:  vwith starting value: u) ∈ [u / v])
7. x : T
8. f[x;u] = x ∈ T
⊢ (accumulate (with value x and list item y): f[x;y]over list:  vwith starting value: x) = x ∈ T)
∨ (accumulate (with value x and list item y):
    f[x;y]
   over list:
     v
   with starting value:
    x) ∈ [u / v])

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T.  \mforall{}L:T  List.
        ((\mforall{}x,y:T.    ((f[x;y]  =  x)  \mvee{}  (f[x;y]  =  y)))  {}\mRightarrow{}  0  <  ||L||  {}\mRightarrow{}  (combine-list(x,y.f[x;y];L)  \mmember{}  L))


By

---

Latex:
(RepeatFor  5  ((D  0  THENA  Auto))
  THEN  D  -3
  THEN  Reduce  (-1)
  THEN  Try  (Complete  (Auto))
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-3)
  THEN  RepUR  ``combine-list``  0
  THEN  ListInd  (-2)
  THEN  Reduce  0
  THEN  Try  ((RWO  "member\_singleton"  0  THEN  Auto)\mcdot{})
  THEN  Auto
  THEN  RenameVar  `x'  (-1)
  THEN  (Assert  (f[x;u]  =  x)  \mvee{}  (f[x;u]  =  u)  BY
                          Auto)
  THEN  D  -1
  THEN  (HypSubst'  -1  0  THENA  Auto)
  THEN  BLemma  `cons\_member`
  THEN  Auto)

---

Home Index