Nuprl Lemma : scout_wf
[Op:LimitedType]. [ldr:Id]. [num:
]. [b:ballot-id()]. [acceptors:Id List].
(scout(Op;ldr;num;acceptors;b) 
EClass'(Message 
Id?))
Proof not projected
Definitions occuring in Statement :
scout: scout(Op;ldr;num;acceptors;b),
ballot-id: ballot-id(),
Message: Message,
eclass: EClass(A[eo; e]),
Id: Id,
uall: [x:A]. B[x],
unit: Unit,
member: t T,
product: x:A B[x],
union: left + right,
list: type List,
int: ,
limited-type: LimitedType
Definitions :
pMsg: pMsg(P.M[P]),
so_lambda: 
x.t[x],
all: x:A. B[x],
Message: Message,
eclass: EClass(A[eo; e]),
so_lambda: x y.t[x; y],
let: let,
spreadn: spread3,
scout: scout(Op;ldr;num;acceptors;b),
member: t T,
uall: [x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
so_apply: x[s1;s2],
limited-type: LimitedType,
subtype: S 
T
Lemmas :
subtype_rel_self,
event-ordering+-subtype,
subtype_rel_dep_function,
bag_wf,
event-ordering+_inc,
es-E_wf,
mData_wf,
name_wf,
event-ordering+_wf,
limited-type_wf,
ballot-id_wf,
class1b_wf,
msgPreempted_wf,
it_wf,
msgAdopted_wf,
length_wf,
lt_int_wf,
eq_ballot_wf,
ifthenelse_wf,
append_wf,
eq_id_wf,
bnot_wf,
filter_wf,
sm-command_wf,
smr-class_wf,
unit_wf2,
Id_wf,
Message_wf,
once-class_wf
\mforall{}[Op:LimitedType]. \mforall{}[ldr:Id]. \mforall{}[num:\mBbbZ{}]. \mforall{}[b:ballot-id()]. \mforall{}[acceptors:Id List].
(scout(Op;ldr;num;acceptors;b) \mmember{} EClass'(Message \mtimes{} Id?))
Date html generated:
2012_01_23-PM-01_41_26
Last ObjectModification:
2011_12_13-PM-05_26_20
Home
Index