Nuprl Lemma : consensus-ts5-true-knowledge
∀[V:Type]
∀A:Id List. ∀W:{a:Id| (a ∈ A)} List List. ∀x:ts-reachable(consensus-ts5(V;A;W)).
let x1,x2 = x
in ∀a,b:{a:Id| (a ∈ A)} .
let I,z = Knowledge(x2;a)(b)
in (I ≤ Inning(x1;b))
∧ case z
of inl(p) =>
let k,v = p
in k < I
∧ (↑k ∈ dom(Estimate(x1;b)))
∧ (Estimate(x1;b)(k) = v ∈ V)
∧ (∀i:ℤ. ¬↑i ∈ dom(Estimate(x1;b)) supposing k < i ∧ i < I)
| inr(p) =>
∀i:ℤ. ¬↑i ∈ dom(Estimate(x1;b)) supposing i < I
supposing ↑b ∈ dom(Knowledge(x2;a))
Proof
Definitions occuring in Statement :
consensus-ts5: consensus-ts5(V;A;W),
cs-knowledge: Knowledge(x;a),
cs-estimate: Estimate(s;a),
cs-inning: Inning(s;a),
fpf-ap: f(x),
fpf-dom: x ∈ dom(f),
id-deq: IdDeq,
Id: Id,
l_member: (x ∈ l),
list: T List,
int-deq: IntDeq,
assert: ↑b,
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
le: A ≤ B,
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
set: {x:A| B[x]} ,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
int: ℤ,
universe: Type,
equal: s = t ∈ T,
ts-reachable: ts-reachable(ts)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
ts-reachable: ts-reachable(ts),
subtype_rel: A ⊆r B,
ts-type: ts-type(ts),
pi1: fst(t),
consensus-ts5: consensus-ts5(V;A;W),
prop: ℙ,
uimplies: b supposing a,
so_apply: x[s],
top: Top,
implies: P ⇒ Q,
and: P ∧ Q,
guard: {T},
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
assert: ↑b,
ifthenelse: if b then t else f fi ,
bfalse: ff,
exists: ∃x:A. B[x],
or: P ∨ Q,
sq_type: SQType(T),
bnot: ¬bb,
false: False,
sq_stable: SqStable(P),
not: ¬A,
le: A ≤ B,
true: True,
cs-estimate: Estimate(s;a),
cs-inning: Inning(s;a),
cs-knowledge: Knowledge(x;a),
ts-init: ts-init(ts),
pi2: snd(t),
fpf-ap: f(x),
mk_fpf: mk_fpf(L;f),
fpf-empty: ⊗,
fpf-dom: x ∈ dom(f),
cand: A c∧ B,
less_than': less_than'(a;b),
ts-rel: ts-rel(ts),
infix_ap: x f y,
consensus-rel-knowledge: consensus-rel-knowledge(V;A;W;x;y),
consensus-rel-knowledge-step: consensus-rel-knowledge-step(V;A;W;x1;x2;y1;y2;a),
consensus-rel-knowledge-inning-step: consensus-rel-knowledge-inning-step(V;A;W;x1;x2;y1;y2;a),
consensus-rel-knowledge-archive-step: consensus-rel-knowledge-archive-step(V;A;W;x1;x2;y1;y2;a),
consensus-rel-add-knowledge-step: consensus-rel-add-knowledge-step(V;A;W;x1;x2;y1;y2;a),
consensus-state5: Knowledge(ConsensusState),
decidable: Dec(P),
squash: ↓T,
Id: Id,
satisfiable_int_formula: satisfiable_int_formula(fmla),
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
exposed-bfalse: exposed-bfalse,
rev_uimplies: rev_uimplies(P;Q),
eq_id: a = b
Latex:
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List. \mforall{}x:ts-reachable(consensus-ts5(V;A;W)).
let x1,x2 = x
in \mforall{}a,b:\{a:Id| (a \mmember{} A)\} .
let I,z = Knowledge(x2;a)(b)
in (I \mleq{} Inning(x1;b))
\mwedge{} case z
of inl(p) =>
let k,v = p
in k < I
\mwedge{} (\muparrow{}k \mmember{} dom(Estimate(x1;b)))
\mwedge{} (Estimate(x1;b)(k) = v)
\mwedge{} (\mforall{}i:\mBbbZ{}. \mneg{}\muparrow{}i \mmember{} dom(Estimate(x1;b)) supposing k < i \mwedge{} i < I)
| inr(p) =>
\mforall{}i:\mBbbZ{}. \mneg{}\muparrow{}i \mmember{} dom(Estimate(x1;b)) supposing i < I
supposing \muparrow{}b \mmember{} dom(Knowledge(x2;a))
Date html generated:
2016_05_16-PM-00_23_56
Last ObjectModification:
2016_01_17-PM-04_01_58
Theory : event-ordering
Home
Index