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


1. [T] Type
2. T ⟶ T ⟶ T
3. T ⟶ T ⟶ ℙ
4. ∀x,y,z:T.  (R[x;f[y;z]] ⇐⇒ R[x;y] ∧ R[x;z])
5. : ℕ
6. T
7. 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. 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" 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]  \mwedge{}  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{}  (\mforall{}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{}  (\mforall{}b\mmember{}v.R[a;b])
\mvdash{}  R[a;f[u;combine-list(x,y.f[x;y];v)]]  \mLeftarrow{}{}\mRightarrow{}  R[a;u]  \mwedge{}  (\mforall{}b\mmember{}v.R[a;b])


By


Latex:
(RWW  "4  -1"  0  THEN  Auto)




Home Index