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