Nuprl Definition : matching-conversation

MatchingConversation(n;thr1;thr2) ==
  (n ≤ ||thread-messages(thr1)||)
  ∧ (n ≤ ||thread-messages(thr2)||)
  ∧ (∀p∈zip(firstn(n;thread-messages(thr1));firstn(n;thread-messages(thr2))).let m1,m2 
                                                                             in send-rcv-match(m1;m2)
                                                                                ∨ send-rcv-match(m2;m1))



Definitions occuring in Statement :  send-rcv-match: send-rcv-match(m1;m2) thread-messages: thread-messages(thr) zip: zip(as;bs) l_all: (∀x∈L.P[x]) firstn: firstn(n;as) length: ||as|| le: A ≤ B or: P ∨ Q and: P ∧ Q spread: spread def
FDL editor aliases :  matching-conversation

Latex:
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: 2015_07_23-PM-00_09_33
Last ObjectModification: 2013_10_01-PM-05_05_34

Home Index