---

Step * of Lemma combine-combine-list-left

∀[T:Type]
  ∀f:T ⟶ T ⟶ T. ∀L:T List.
    (∀a:T. uiff(f[a;combine-list(x,y.f[x;y];L)] = a ∈ T;(∀b∈L.f[a;b] = a ∈ T))) supposing 
       (0 < ||L|| and 
       (∀x,y,z:T.  (f[x;f[y;z]] = x ∈ T ⇐⇒ (f[x;y] = x ∈ T) ∧ (f[x;z] = x ∈ 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_all_single" 0 THEN Auto))
   THEN (RWO "-1" 0 THENA Auto)
   THEN RWW "l_all_cons" 0
   THEN Auto
   THEN Try ((RWO "3" (-2) THEN Complete (Auto)))
   THEN Try ((RWO "3" 0 THEN Complete (Auto)))) }

---

Latex:

---

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


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\_all\_single"  0  THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  RWW  "l\_all\_cons"  0
  THEN  Auto
  THEN  Try  ((RWO  "3"  (-2)  THEN  Complete  (Auto)))
  THEN  Try  ((RWO  "3"  0  THEN  Complete  (Auto))))

---

Home Index