---

Step * 1 of Lemma combine-list-rel-or


1. [T] : Type
2. f : T ⟶ T ⟶ T
3. R : T ⟶ T ⟶ ℙ
4. ∀x,y,z:T.  (R[x;f[y;z]] ⇐⇒ R[x;y] ∨ R[x;z])
5. n : ℕ
6. u : T
7. v : T List
8. ∀L1:T List
     (||L1|| < ||v|| + 1
     ⇒ (∀a:T. R[a;combine-list(x,y.f[x;y];L1)] ⇐⇒ (∃b∈L1. R[a;b]) supposing 0 < ||L1|| ∧ Assoc(T;λx,y. f[x;y])))
9. a : T
10. 0 < ||v|| + 1 ∧ Assoc(T;λx,y. f[x;y])
11. ¬(v = [] ∈ (T List))
12. 0 < ||v||
13. R[a;combine-list(x,y.f[x;y];v)] ⇐⇒ (∃b∈v. R[a;b])
⊢ R[a;f[u;combine-list(x,y.f[x;y];v)]] ⇐⇒ R[a;u] ∨ (∃b∈v. R[a;b])
BY
{ (RWW "4 -1" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
3.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x,y,z:T.    (R[x;f[y;z]]  \mLeftarrow{}{}\mRightarrow{}  R[x;y]  \mvee{}  R[x;z])
5.  n  :  \mBbbN{}
6.  u  :  T
7.  v  :  T  List
8.  \mforall{}L1:T  List
          (||L1||  <  ||v||  +  1
          {}\mRightarrow{}  (\mforall{}a:T
                      R[a;combine-list(x,y.f[x;y];L1)]  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}L1.  R[a;b]) 
                      supposing  0  <  ||L1||  \mwedge{}  Assoc(T;\mlambda{}x,y.  f[x;y])))
9.  a  :  T
10.  0  <  ||v||  +  1  \mwedge{}  Assoc(T;\mlambda{}x,y.  f[x;y])
11.  \mneg{}(v  =  [])
12.  0  <  ||v||
13.  R[a;combine-list(x,y.f[x;y];v)]  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}v.  R[a;b])
\mvdash{}  R[a;f[u;combine-list(x,y.f[x;y];v)]]  \mLeftarrow{}{}\mRightarrow{}  R[a;u]  \mvee{}  (\mexists{}b\mmember{}v.  R[a;b])


By

---

Latex:
(RWW  "4  -1"  0  THEN  Auto)\mcdot{}

---

Home Index