{ 
[V:Type]
A:Id List. W:{a:Id| (a 
A)} List List. L:consensus-event(V;A) List.
x,y:{a:Id| (a A)} 
(consensus-event(V;A) List). a:{a:Id| (a A)} .
((b:{a:Id| (a A)} . i:
. z:i 
V?.
((consensus-message(b;i;z) L)
let i',est,knw = consensus-accum-state(A;x b) in
(i 
i')
case z
of inl(p) =>
let j,v = p
in (
j dom(est))
(k:
. (
k dom(est)) supposing ((k < i) and (j < k)))
(v = est(j))
| inr(a) =>
j:. j dom(est) supposing j < i))
(v:V. j:||L||.
let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;L)) in
((i fpf-domain(est)))
may consider v in inning i based on knowledge (knw)
supposing L[j] = Archive(v))
(x (ts-rel(consensus-ts6(V;A;W))^*) y)) supposing
(((y a) = ((x a) @ L)) and
(b:{a:Id| (a A)} . (y b) = (x b) supposing (b = a))) }
{ Proof }
Definitions occuring in Statement :
consensus-ts6: consensus-ts6(V;A;W),
consensus-accum-state: consensus-accum-state(A;L),
consensus-message: consensus-message(b;i;z),
archive-event: Archive(v),
consensus-event: consensus-event(V;A),
cs-knowledge-precondition: may consider v in inning i based on knowledge (s),
fpf-ap: f(x),
fpf-domain: fpf-domain(f),
fpf-dom: x dom(f),
Id: Id,
select: l[i],
firstn: firstn(n;as),
length: ||as||,
append: as @ bs,
assert: b,
int_seg: {i..j
},
nat: ,
spreadn: spread3,
uimplies: b supposing a,
uall: [x:A]. B[x],
infix_ap: x f y,
le: A B,
all: x:A. B[x],
not: A,
implies: P Q,
and: P Q,
unit: Unit,
less_than: a < b,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
spread: spread def,
product: x:A B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
union: left + right,
list: type List,
natural_number: $n,
int: ,
universe: Type,
equal: s = t,
l_member: (x l),
rel_star: R^*,
int-deq: IntDeq,
ts-rel: ts-rel(ts),
ts-type: ts-type(ts)
Definitions :
and: P Q,
btrue: tt,
false: False,
prop: 
,
member: t T,
ifthenelse: if b then t else f fi ,
le: A B,
implies: P Q,
not: A,
uimplies: b supposing a,
all: x:A. B[x],
bfalse: ff,
or: P 
Q,
subtype: S 
T,
top: Top,
ycomb: Y,
label: ...$L... t,
ge: i 
j ,
lelt: i j < k,
length: ||as||,
int_seg: {i..j},
iff: P 
Q,
rev_implies: P Q,
true: True,
squash: 
T,
lt_int: i <z j,
bnot: 
b,
le_int: i z j,
select: l[i],
guard: {T},
so_lambda: 
x.t[x],
spreadn: spread3,
cand: A c B,
assert: b,
one-consensus-event: y = x after e@a,
uall: [x:A]. B[x],
nat: ,
bool: 
,
unit: Unit,
so_apply: x[s],
sq_type: SQType(T),
it: 
Lemmas :
bool_wf,
btrue_wf,
eq_id_self,
archive-event_wf,
length_wf1,
select_wf,
nat_wf,
unit_wf,
nat_properties,
int_seg_wf,
consensus-message_wf,
not_wf,
l_member_wf,
Id_wf,
append_wf,
consensus-event_wf,
eq_id_wf,
ifthenelse_wf,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
assert-eq-id,
eqtt_to_assert,
uiff_transitivity,
iff_weakening_uiff,
bnot_wf,
assert_wf,
member_append,
le_wf,
length_append,
non_neg_length,
length_cons,
top_wf,
length_wf_nat,
length_nil,
select_append_front,
firstn_append,
select_append_back,
squash_wf,
firstn_all,
cons_member,
append-nil,
fpf_wf,
consensus-accum-state_wf,
fpf-ap_wf,
int_seg_properties,
fpf-trivial-subtype-top,
int-deq_wf,
fpf-dom_wf,
assert_elim,
fpf-join_wf,
not_functionality_wrt_iff,
bool_subtype_base,
subtype_base_sq,
fpf-single-dom,
decidable__assert,
or_functionality_wrt_uiff3,
fpf-single_wf,
fpf-join-dom2,
fpf-join-ap-sq,
append_assoc
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List. \mforall{}L:consensus-event(V;A) List.
\mforall{}x,y:\{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (consensus-event(V;A) List). \mforall{}a:\{a:Id| (a \mmember{} A)\} .
((\mforall{}b:\{a:Id| (a \mmember{} A)\} . \mforall{}i:\mBbbN{}. \mforall{}z:\mBbbN{}i \mtimes{} V?.
((consensus-message(b;i;z) \mmember{} L)
{}\mRightarrow{} let i',est,knw = consensus-accum-state(A;x b) in
(i \mleq{} i')
\mwedge{} case z
of inl(p) =>
let j,v = p
in (\muparrow{}j \mmember{} dom(est)) \mwedge{} (\mforall{}k:\mBbbZ{}. (\mneg{}\muparrow{}k \mmember{} dom(est)) supposing ((k < i) and (j < k))) \mwedge{} (v = e\000Cst(j))
| inr(a) =>
\mforall{}j:\mBbbZ{}. \mneg{}\muparrow{}j \mmember{} dom(est) supposing j < i))
{}\mRightarrow{} (\mforall{}v:V. \mforall{}j:\mBbbN{}||L||.
let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;L)) in
(\mneg{}(i \mmember{} fpf-domain(est))) \mwedge{} may consider v in inning i based on knowledge (knw)
supposing L[j] = Archive(v))
{}\mRightarrow{} (x rel\_star(ts-type(consensus-ts6(V;A;W)); ts-rel(consensus-ts6(V;A;W))) y)) supposing
(((y a) = ((x a) @ L)) and
(\mforall{}b:\{a:Id| (a \mmember{} A)\} . (y b) = (x b) supposing \mneg{}(b = a)))
Date html generated:
2011_08_16-AM-10_10_25
Last ObjectModification:
2011_06_18-AM-09_03_19
Home
Index