Nuprl Lemma : m_ping_pong_Handler

Nuprl Lemma : m_ping_pong_Handler_nlp

x0:Id. NormalLProgrammable'(Id

Message;m_ping_pong_Handler() x0)

Proof not projected

Definitions occuring in Statement : m_ping_pong_Handler: m_ping_pong_Handler(), Message: Message, normal-locally-programmable: NormalLProgrammable(A;X), Id: Id, all:

x:A. B[x], apply: f a, product: x:A

B[x]
Definitions : all:

x:A. B[x], m_ping_pong_Handler: m_ping_pong_Handler(), member: t

T, so_lambda:

x.t[x], uall:

[x:A]. B[x], implies: P

Q, so_apply: x[s]
Lemmas : parallel-class-nlp, Id_wf, Message_wf, product-valueall-type, Id-valueall-type, Message-valueall-type, valueall-type_wf, m_ping_pong_SendPing_wf, m_ping_pong_ReplyToPong_wf, m_ping_pong_SendPing_nlp, m_ping_pong_ReplyToPong_nlp

\mforall{}x0:Id. NormalLProgrammable'(Id \mtimes{} Message;m\_ping\_pong\_Handler() x0) Date html generated: 2012_02_20-PM-06_24_10 Last ObjectModification: 2012_02_02-PM-02_48_32 Home Index