---

Step * of Lemma combine-combine-list-right

∀[T:Type]
  ∀f:T ⟶ T ⟶ T. ∀L:T List.
    ((∀x,y,z:T.  (f[x;f[y;z]] = f[y;z] ∈ T ⇐⇒ (f[x;y] = y ∈ T) ∨ (f[x;z] = z ∈ T)))
    ⇒ 0 < ||L||
    ⇒ (∀a:T. (f[a;combine-list(x,y.f[x;y];L)] = combine-list(x,y.f[x;y];L) ∈ T ⇐⇒ (∃b∈L. f[a;b] = b ∈ T))))
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 "l_exists_single" 0 THEN Auto))
   THEN (RWO "-1" 0 THENA Auto)
   THEN RWW "l_exists_cons" 0
   THEN Auto
   THEN Try ((RWO "3" (-1) THEN Auto THEN SplitOrHyps THEN TrivialOr))
   THEN Try ((RWO "3" 0 THEN Auto THEN SplitOrHyps THEN TrivialOr)⋅)) }

---

Latex:

---

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


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  "l\_exists\_single"  0  THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  RWW  "l\_exists\_cons"  0
  THEN  Auto
  THEN  Try  ((RWO  "3"  (-1)  THEN  Auto  THEN  SplitOrHyps  THEN  TrivialOr))
  THEN  Try  ((RWO  "3"  0  THEN  Auto  THEN  SplitOrHyps  THEN  TrivialOr)\mcdot{}))

---

Home Index