Nuprl Lemma : consensus-ts3-invariant1
∀[V:Type]. ∀[L:ts-reachable(consensus-ts3(V))]. ∀[v:V].
∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ L) ∨ (COMMITED[v'] ∈ L)
supposing (CONSIDERING[v] ∈ L) ∨ (COMMITED[v] ∈ L)
Proof
Definitions occuring in Statement :
consensus-ts3: consensus-ts3(T),
cs-commited: COMMITED[v],
cs-considering: CONSIDERING[v],
consensus-state3: consensus-state3(T),
l_member: (x ∈ l),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
or: P ∨ Q,
universe: Type,
equal: s = t ∈ T,
ts-reachable: ts-reachable(ts)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
subtype_rel: A ⊆r B,
ts-reachable: ts-reachable(ts),
so_lambda: λ2x.t[x],
infix_ap: x f y,
so_apply: x[s],
ts-type: ts-type(ts),
pi1: fst(t),
consensus-ts3: consensus-ts3(T),
list: T List,
or: P ∨ Q,
ts-init: ts-init(ts),
pi2: snd(t),
nil: [],
it: ⋅,
guard: {T},
not: ¬A,
false: False,
ts-rel: ts-rel(ts),
and: P ∧ Q,
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
l_member: (x ∈ l),
cand: A c∧ B,
nat: ℕ,
int_seg: {i..j-},
ge: i ≥ j ,
lelt: i ≤ j < k,
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
top: Top,
le: A ≤ B,
squash: ↓T,
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
less_than: a < b,
sq_type: SQType(T),
less_than': less_than'(a;b),
true: True,
cs-commited: COMMITED[v],
consensus-state3: consensus-state3(T),
outl: outl(x),
isl: isl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
cs-considering: CONSIDERING[v]
Latex:
\mforall{}[V:Type]. \mforall{}[L:ts-reachable(consensus-ts3(V))]. \mforall{}[v:V].
\mforall{}[v':V]. v' = v supposing (CONSIDERING[v'] \mmember{} L) \mvee{} (COMMITED[v'] \mmember{} L)
supposing (CONSIDERING[v] \mmember{} L) \mvee{} (COMMITED[v] \mmember{} L)
Date html generated:
2016_05_16-AM-11_52_20
Last ObjectModification:
2016_01_17-PM-03_53_33
Theory : event-ordering
Home
Index