---

{ t:. A:Id List.
    ( {a:Id| (a  A)}  ~ (3 * t) + 1
     (W:{a:Id| (a  A)}  List List
          ((ws:{a:Id| (a  A)}  List
              ((ws  W)
               (||ws|| = ((2 * t) + 1))  no_repeats({a:Id| (a  A)} ;ws)))
           three-intersection(A;W)))) }

{ Proof }

---

Definitions occuring in Statement :  three-intersection: three-intersection(A;W),  Id: Id,  length: ||as||,  int_seg: {i..j},  nat: ,  all: x:A. B[x],  iff: P  Q,  implies: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  list: type List,  multiply: n * m,  add: n + m,  natural_number: $n,  int: ,  equal: s = t,  no_repeats: no_repeats(T;l),  l_member: (x  l),  equipollent:  A ~ B
Definitions :  all: x:A. B[x],  nat: ,  implies: P  Q,  and: P  Q,  member: t  T,  le: A  B,  not: A,  false: False,  prop: ,  length: ||as||,  combination: Combination(n;T),  three-intersection: three-intersection(A;W),  l_all: (xL.P[x]),  ge: i  j ,  label: ...$L... t,  ycomb: Y,  top: Top,  exists: x:A. B[x],  cand: A c B,  l_member: (x  l),  so_lambda: x.t[x],  iff: P  Q,  rev_implies: P  Q,  n-intersecting: n-intersecting(A;T;n),  so_apply: x[s],  guard: {T}
Lemmas :  combinations-n-intersecting,  le_wf,  Id_wf,  l_member_wf,  iff_wf,  length_wf1,  no_repeats_wf,  equipollent_wf,  int_seg_wf,  nat_wf,  length_nil,  length_wf_nat,  top_wf,  length_cons,  non_neg_length,  l_all_wf2,  select_wf,  iff_transitivity,  l_all_cons,  and_functionality_wrt_iff

---

\mforall{}t:\mBbbN{}.  \mforall{}A:Id  List.
    (  \{a:Id|  (a  \mmember{}  A)\}    \msim{}  \mBbbN{}(3  *  t)  +  1
    {}\mRightarrow{}  (\mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List
                ((\mforall{}ws:\{a:Id|  (a  \mmember{}  A)\}    List
                        ((ws  \mmember{}  W)  \mLeftarrow{}{}\mRightarrow{}  (||ws||  =  ((2  *  t)  +  1))  \mwedge{}  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;ws)))
                {}\mRightarrow{}  three-intersection(A;W))))


Date html generated: 2010_08_27-AM-12_50_18
Last ObjectModification: 2009_12_23-PM-03_26_42

Home Index