Nuprl Definition : class2b
class2b(c) ==
(<fst(v), fst(snd(v))> where v from BaseClass(``paxos 2b``;Id 
ballot-id() 
) such that (snd(snd(v)) =
c))
Proof not projected
Definitions occuring in Statement :
ballot-id: ballot-id(),
baseclass: BaseClass(h;T),
mapfilter-class: (f[v] where v from X such that P[v]),
Id: Id,
eq_int: (i = j),
pi1: fst(t),
pi2: snd(t),
pair: <a, b>,
product: x:A B[x],
cons: [car / cdr],
nil: [],
int: ,
token: "$token"
Definitions :
mapfilter-class: (f[v] where v from X such that P[v]),
eq_int: (i = j),
pair: <a, b>,
pi1: fst(t),
pi2: snd(t),
baseclass: BaseClass(h;T),
cons: [car / cdr],
token: "$token",
nil: [],
Id: Id,
product: x:A B[x],
ballot-id: ballot-id(),
int:
class2b(c) ==
(<fst(v), fst(snd(v))> where v from BaseClass(``paxos 2b``;Id
\mtimes{} ballot-id()
\mtimes{} \mBbbZ{}) such that (snd(snd(v)) =\msubz{} c))
Date html generated:
2011_10_20-PM-04_18_46
Last ObjectModification:
2011_01_29-AM-00_24_39
Home
Index