Nuprl Definition : paxos_C1
paxos_C1{i:l}(es;accpts) ==
all-class-value-pairs+{i:l}(es;Id 
PValue();BaseClass(pax_p2a();Id
PValue())@accpts;v1,v2.compat-pvals(snd(v1);snd(v2)))
Proof not projected
Definitions occuring in Statement :
pax_p2a: pax_p2a(),
compat-pvals: compat-pvals(bsp;bsp'),
PValue: PValue(),
all-class-value-pairs+: all-class-value-pairs+{i:l}(es;T;A;t1,t2.Q[t1; t2]),
restricted-baseclass: BaseClass(h;T)@locs,
Id: Id,
pi2: snd(t),
product: x:A B[x]
FDL editor aliases :
paxos_C1
paxos\_C1\{i:l\}(es;accpts) ==
all-class-value-pairs+\{i:l\}(es;Id \mtimes{} PValue();BaseClass(pax\_p2a();Id
\mtimes{} PValue())@accpts;v1,v2.compat-pvals(snd(v1);snd(v2)))
Date html generated:
2011_10_20-PM-11_59_53
Last ObjectModification:
2011_06_22-PM-04_24_33
Home
Index