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 = p 
                                                                             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