---

MatchingConversation(n;thr1;thr2) ==
  (n  ||thread-messages(thr1)||)
   (n  ||thread-messages(thr2)||)
   (pzip(firstn(n;thread-messages(thr1));firstn(n;thread-messages(thr2))).
       let m1,m2 = p in
         send-rcv-match(m1;m2)  send-rcv-match(m2;m1))

---

Definitions :  and: P  Q,  le: A  B,  length: ||as||,  l_all: (xL.P[x]),  zip: zip(as;bs),  firstn: firstn(n;as),  thread-messages: thread-messages(thr),  product: x:A  B[x],  es-E: E,  spread: spread def,  or: P  Q,  send-rcv-match: send-rcv-match(m1;m2)
FDL editor aliases :  matching-conversation

---

MatchingConversation(n;thr1;thr2)  ==
    (n  \mleq{}  ||thread-messages(thr1)||)
    \mwedge{}  (n  \mleq{}  ||thread-messages(thr2)||)
    \mwedge{}  (\mforall{}p\mmember{}zip(firstn(n;thread-messages(thr1));firstn(n;thread-messages(thr2))).
              let  m1,m2  =  p  in
                  send-rcv-match(m1;m2)  \mvee{}  send-rcv-match(m2;m1))


Date html generated: 2010_08_28-AM-02_39_44
Last ObjectModification: 2010_02_22-PM-10_49_55

Home Index