Nuprl Definition : pv11_p1_from-p2a
pv11_p1_from-p2a{i:l}(Cmd;es;e;x) ==
(header(e) = ``pv11_p1 p2a`` ∈ Name) ∧ (x = (snd(msgval(e))) ∈ (pv11_p1_Ballot_Num() × ℤ × Cmd))
Definitions occuring in Statement :
pv11_p1_Ballot_Num: pv11_p1_Ballot_Num(),
es-info-body: msgval(e),
es-header: header(e),
name: Name,
cons: [a / b],
nil: [],
pi2: snd(t),
and: P ∧ Q,
product: x:A × B[x],
int: ℤ,
token: "$token",
equal: s = t ∈ T
FDL editor aliases :
pv11_p1_from-p2a
Latex:
pv11\_p1\_from-p2a\{i:l\}(Cmd;es;e;x) == (header(e) = ``pv11\_p1 p2a``) \mwedge{} (x = (snd(msgval(e))))
Date html generated:
2016_05_17-PM-04_15_26
Last ObjectModification:
2013_12_18-PM-06_19_22
Theory : paxos!synod
Home
Index