Nuprl Lemma : ohc_v1_when_quorum1_wf
[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [flrs:
].
(ohc_v1_when_quorum1(Cmd;cmdeq;flrs) 
Id Cmd Id Cmd List (Id List) bag(Cmd? Cmd))
Proof not projected
Definitions occuring in Statement :
ohc_v1_when_quorum1: ohc_v1_when_quorum1(Cmd;cmdeq;flrs),
Id: Id,
uall: [x:A]. B[x],
unit: Unit,
member: t T,
function: x:A B[x],
product: x:A B[x],
union: left + right,
list: type List,
int: ,
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Definitions :
uall: [x:A]. B[x],
vatype: ValueAllType,
member: t T,
ohc_v1_when_quorum1: ohc_v1_when_quorum1(Cmd;cmdeq;flrs),
ifthenelse: if b then t else f fi ,
ohc_v1_newvote: ohc_v1_newvote(),
ohc_v1_roundout1: ohc_v1_roundout1(Cmd;cmdeq;flrs),
all: x:A. B[x],
implies: P 
Q,
btrue: tt,
bfalse: ff,
unit: Unit,
bool: 
,
uimplies: b supposing a,
uiff: uiff(P;Q),
and: P 
Q,
nat: 
,
it: 
Lemmas :
band_wf,
eqof_wf,
product-deq_wf,
int-deq_wf,
bnot_wf,
deq-member_wf,
Id_wf,
id-deq_wf,
bool_wf,
eqtt_to_assert,
ifthenelse_wf,
eq_int_wf,
length_wf,
bag_wf,
unit_wf2,
poss-maj_wf,
single-bag_wf,
it_wf,
empty-bag_wf,
uiff_transitivity,
equal_wf,
assert_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
deq_wf,
valueall-type_wf
\mforall{}[Cmd:ValueAllType]. \mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[flrs:\mBbbZ{}].
(ohc\_v1\_when\_quorum1(Cmd;cmdeq;flrs) \mmember{} \mBbbZ{} \mtimes{} \mBbbZ{}
{}\mrightarrow{} Id
{}\mrightarrow{} \mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id
{}\mrightarrow{} Cmd List \mtimes{} (Id List)
{}\mrightarrow{} bag(Cmd? \mtimes{} Cmd))
Date html generated:
2012_02_20-PM-05_21_40
Last ObjectModification:
2012_02_13-PM-01_05_33
Home
Index