---

{ t:. A:Id List.
    (W:{a:Id| (a  A)}  List List
      ((ws:{a:Id| (a  A)}  List
          ((ws  W)  (||ws|| = (t + 1))  no_repeats({a:Id| (a  A)} ;ws)))
       two-intersection(A;W))) supposing 
       (no_repeats(Id;A) and 
       (||A|| = ((2 * t) + 1))) }

{ Proof }

---

Definitions occuring in Statement :  two-intersection: two-intersection(A;W),  Id: Id,  length: ||as||,  nat: ,  uimplies: b supposing a,  all: x:A. B[x],  exists: x:A. B[x],  iff: 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)
Definitions :  all: x:A. B[x],  nat: ,  uimplies: b supposing a,  exists: x:A. B[x],  and: P  Q,  iff: P  Q,  member: t  T,  implies: P  Q,  le: A  B,  not: A,  false: False,  prop: ,  cand: A c B,  rev_implies: P  Q,  top: Top,  subtype: S  T,  uall: [x:A]. B[x]
Lemmas :  no_repeats_witness,  Id_wf,  combinations-list,  le_wf,  iff_wf,  l_member_wf,  length_wf1,  no_repeats_wf,  two-intersection_wf,  nat_wf,  int_seg_wf,  decidable__equal_Id,  length_wf_nat,  top_wf,  equipollent_functionality_wrt_equipollent,  equipollent-length,  equipollent_weakening_ext-eq,  ext-eq_weakening,  equipollent-nsub,  two-intersecting-wait-set

---

\mforall{}t:\mBbbN{}.  \mforall{}A:Id  List.
    (\mexists{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List
        ((\mforall{}ws:\{a:Id|  (a  \mmember{}  A)\}    List.  ((ws  \mmember{}  W)  \mLeftarrow{}{}\mRightarrow{}  (||ws||  =  (t  +  1))  \mwedge{}  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;ws))\000C)
        \mwedge{}  two-intersection(A;W)))  supposing 
          (no\_repeats(Id;A)  and 
          (||A||  =  ((2  *  t)  +  1)))


Date html generated: 2011_08_16-AM-10_00_36
Last ObjectModification: 2011_06_18-AM-08_58_32

Home Index