Nuprl Lemma : RSC_Quorum

Nuprl Lemma : RSC_Quorum_nlp

Cmd:ValueAllType.

cmdeq:EqDecider(Cmd).

flrs:

.

x0:

.
NormalLProgrammable'(Id

Message;RSC_Quorum(Cmd;cmdeq;flrs) x0)

Proof not projected

Error : references

\mforall{}Cmd:ValueAllType. \mforall{}cmdeq:EqDecider(Cmd). \mforall{}flrs:\mBbbZ{}. \mforall{}x0:\mBbbZ{} \mtimes{} \mBbbZ{}. NormalLProgrammable'(Id \mtimes{} Message;RSC\_Quorum(Cmd;cmdeq;flrs) x0) Date html generated: 2012_02_20-PM-07_50_55 Last ObjectModification: 2012_02_02-PM-01_58_21 Home Index