---

Step * 1 of Lemma combine-list-member


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])
BY
{ (InstHyp [⌜x⌝] (-3)⋅ THENA 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
9. (accumulate (with value x and list item y):
     f[x;y]
    over list:
      v
    with starting value:
     x) ∈ [x / v])
⊢ (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:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
3.  \mforall{}x,y:T.    ((f[x;y]  =  x)  \mvee{}  (f[x;y]  =  y))
4.  u  :  T
5.  v  :  T  List
6.  \mforall{}u:T
          (accumulate  (with  value  x  and  list  item  y):
              f[x;y]
            over  list:
                v
            with  starting  value:
              u)  \mmember{}  [u  /  v])
7.  x  :  T
8.  f[x;u]  =  x
\mvdash{}  (accumulate  (with  value  x  and  list  item  y):  f[x;y]over  list:    vwith  starting  value:  x)  =  x)
\mvee{}  (accumulate  (with  value  x  and  list  item  y):
        f[x;y]
      over  list:
          v
      with  starting  value:
        x)  \mmember{}  [u  /  v])


By

---

Latex:
(InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)\mcdot{}

---

Home Index