---

Step * of Lemma combine-list-rel-or

∀[T:Type]
  ∀f:T ⟶ T ⟶ T. ∀R:T ⟶ T ⟶ ℙ.
    ((∀x,y,z:T.  (R[x;f[y;z]] ⇐⇒ R[x;y] ∨ R[x;z]))
    ⇒ (∀L:T List. ∀a:T.  R[a;combine-list(x,y.f[x;y];L)] ⇐⇒ (∃b∈L. R[a;b]) supposing 0 < ||L|| ∧ Assoc(T;λx,y. f[x;y])\000C))
BY
{ (((InductionOnLength THEN UnivCD) THENA Auto)
   THEN DVar `L'
   THEN All Reduce
   THEN Try (Complete (Auto))
   THEN (OldAutoBoolCase ⌜null(v)⌝⋅ THENA Auto)
   THEN Try (((HypSubst (-1) 0 THENM (Reduce 0 THEN RWO "l_exists_single" 0)) THEN Auto'))
   THEN (Assert 0 < ||v|| BY
               (DVar `v' THEN Auto' THEN D -1 THEN Auto))
   THEN (RWO "l_exists_cons" 0 THENA Auto)
   THEN ((RWO "combine-list-cons" 0 THENA (Auto THEN BLemma `combine-list-cons` THEN Auto))
         THEN (InstHyp [⌜v⌝;⌜a⌝] (-5)⋅ THENA Auto)
         )⋅) }

1
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])

---

Latex:

---

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


By

---

Latex:
(((InductionOnLength  THEN  UnivCD)  THENA  Auto)
  THEN  DVar  `L'
  THEN  All  Reduce
  THEN  Try  (Complete  (Auto))
  THEN  (OldAutoBoolCase  \mkleeneopen{}null(v)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (((HypSubst  (-1)  0  THENM  (Reduce  0  THEN  RWO  "l\_exists\_single"  0))  THEN  Auto'))
  THEN  (Assert  0  <  ||v||  BY
                          (DVar  `v'  THEN  Auto'  THEN  D  -1  THEN  Auto))
  THEN  (RWO  "l\_exists\_cons"  0  THENA  Auto)
  THEN  ((RWO  "combine-list-cons"  0  THENA  (Auto  THEN  BLemma  `combine-list-cons`  THEN  Auto))
              THEN  (InstHyp  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
              )\mcdot{})

---

Home Index