Nuprl Lemma : ler_leader_ring_main

Nuprl Lemma : ler_leader_ring_main_nlp

client:Id.

nodes:bag(Id).

uid:Id

. NormalLProgrammable'(Id

Message;ler_leader_ring_main(client;nodes;uid))

Proof not projected

Definitions occuring in Statement : ler_leader_ring_main: ler_leader_ring_main(client;nodes;uid), Message: Message, normal-locally-programmable: NormalLProgrammable(A;X), Id: Id, all:

x:A. B[x], function: x:A

B[x], product: x:A

B[x], int:

, bag: bag(T)
Definitions : so_lambda:

x.t[x], member: t

T, ler_leader_ring_main: ler_leader_ring_main(client;nodes;uid), all:

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

Q, uall:

[x:A]. B[x]
Lemmas : bag_wf, ler_ChooseReply_nlp, ler_ProposeReply_nlp, parallel-class-nlp, ler_ChooseReply_wf, ler_ProposeReply_wf, parallel-class_wf, valueall-type_wf, Message-valueall-type, Id-valueall-type, product-valueall-type, Message_wf, Id_wf, class-at-nlp

\mforall{}client:Id. \mforall{}nodes:bag(Id). \mforall{}uid:Id {}\mrightarrow{} \mBbbZ{}. NormalLProgrammable'(Id \mtimes{} Message;ler\_leader\_ring\_main(client;nodes;uid)) Date html generated: 2012_02_20-PM-06_01_39 Last ObjectModification: 2012_02_02-PM-02_38_05 Home Index