Nuprl Definition : pv11_p1_pvalue
pv11_p1_pvalue{i:l}(Cmd;ldrs_uid;accpts;es;e;x;f) ==
(x ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))
∨ (∃b:pv11_p1_Ballot_Num(). ∃start:E. (start ≤loc e ∧ (x ∈ snd(pv11_p1_ScoutStateFun(Cmd;accpts;f;b;es.start;e)))))
∨ ((header(e) = ``pv11_p1 p1b`` ∈ Name) ∧ (x ∈ snd(snd(snd(msgval(e))))))
∨ ((header(e) = ``pv11_p1 p2a`` ∈ Name) ∧ (x = (snd(msgval(e))) ∈ (pv11_p1_Ballot_Num() × ℤ × Cmd)))
∨ ((header(e) = ``pv11_p1 adopted`` ∈ Name) ∧ (x ∈ snd(msgval(e))))
Definitions occuring in Statement :
pv11_p1_ScoutStateFun: pv11_p1_ScoutStateFun(Cmd;accpts;mf;x;es;e),
pv11_p1_AcceptorStateFun: pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;mf;es;e),
pv11_p1_Ballot_Num: pv11_p1_Ballot_Num(),
es-info-body: msgval(e),
es-header: header(e),
eo-forward: eo.e,
es-le: e ≤loc e' ,
es-E: E,
name: Name,
l_member: (x ∈ l),
cons: [a / b],
nil: [],
pi2: snd(t),
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
product: x:A × B[x],
int: ℤ,
token: "$token",
equal: s = t ∈ T
FDL editor aliases :
pv11_p1_pvalue
Latex:
pv11\_p1\_pvalue\{i:l\}(Cmd;ldrs$_{uid}$;accpts;es;e;x;f) ==
(x \mmember{} snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e)))
\mvee{} (\mexists{}b:pv11\_p1\_Ballot\_Num()
\mexists{}start:E. (start \mleq{}loc e \mwedge{} (x \mmember{} snd(pv11\_p1\_ScoutStateFun(Cmd;accpts;f;b;es.start;e)))))
\mvee{} ((header(e) = ``pv11\_p1 p1b``) \mwedge{} (x \mmember{} snd(snd(snd(msgval(e))))))
\mvee{} ((header(e) = ``pv11\_p1 p2a``) \mwedge{} (x = (snd(msgval(e)))))
\mvee{} ((header(e) = ``pv11\_p1 adopted``) \mwedge{} (x \mmember{} snd(msgval(e))))
Date html generated:
2016_05_17-PM-04_15_37
Last ObjectModification:
2013_12_18-PM-06_19_30
Theory : paxos!synod
Home
Index