Nuprl Definition : one-consensus-event
y = x after e@a ==
(∀b:{a:Id| (a ∈ A)} . ((¬(b = a ∈ Id)) ⇒ ((y b) = (x b) ∈ (consensus-event(V;A) List))))
∧ ((y a) = ((x a) @ [e]) ∈ (consensus-event(V;A) List))
Definitions occuring in Statement :
consensus-event: consensus-event(V;A),
Id: Id,
l_member: (x ∈ l),
append: as @ bs,
cons: [a / b],
nil: [],
list: T List,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
one-consensus-event
y = x after e@a == (\mforall{}b:\{a:Id| (a \mmember{} A)\} . ((\mneg{}(b = a)) {}\mRightarrow{} ((y b) = (x b)))) \mwedge{} ((y a) = ((x a) @ [e]))
Date html generated:
2015_07_17-AM-11_45_12
Last ObjectModification:
2012_02_25-AM-11_48_00
Home
Index