Nuprl Lemma : RSC_VoterState-single-val

[Cmd:ValueAllType].

[es:EO'].

cmd_num:

. single-valued-classrel(es;RSC_VoterState(Cmd) cmd_num;

)

Proof not projected

Definitions occuring in Statement : RSC_VoterState: RSC_VoterState(Cmd), Message: Message, single-valued-classrel: single-valued-classrel(es;X;T), event-ordering+: EO+(Info), uall:

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

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

, vatype: ValueAllType
Definitions : uall:

[x:A]. B[x], vatype: ValueAllType, all:

x:A. B[x], single-valued-classrel: single-valued-classrel(es;X;T), RSC_VoterState: Error :RSC_VoterState, member: t

T, RSC_Retry: Error :RSC_Retry, implies: P

Q, le: A

B, name: Name, not:

A, false: False, prop:

, subtype: S

T
Lemmas : Error :Accum-class-single-val, Error :RSC_Retry_wf, single-bag_wf, Id_wf, Error :RSC_new_retry_wf, single-valued-classrel-base, classrel_wf, Message_wf, Error :RSC_VoterState_wf, es-E_wf, event-ordering+_inc, event-ordering+_wf, valueall-type_wf

\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}cmd$_{num}$:\mBbbZ{}. single-valued-classrel(es;RSC\_V\000CoterState(Cmd) cmd$_{num}$;\mBbbZ{}) Date html generated: 2012_02_20-PM-04_02_38 Last ObjectModification: 2012_02_02-PM-01_59_38 Home Index