Nuprl Lemma : consensus-rcvs-to-consensus-events-cases

[V:Type]

A:Id List.

t:

.

f:V List

V.

v0:V.

L:consensus-rcv(V;A) List.

r:consensus-rcv(V;A).
    let L2 = L @ [r] in
     let S1 = fst(consensus-rcvs-to-consensus-events(f;t;v0;L)) in
     let S2 = fst(consensus-rcvs-to-consensus-events(f;t;v0;L2)) in
     (

a:{a:Id| (a

A)}

i:

v:V
((r = Vote[a;i;v])

((

m:

w:V
(archive-condition(V;A;t;f;m;w;L2)

(S2
                 = (S1
                   @ [consensus-message(a;i + 1;inl <i, v> ) /
                      if ||filter(

x.is-inning-event(x);S1)|| + 1 <z i
then map(

x.NextInning;upto(i - ||filter(

x.is-inning-event(x);S1)||)) @ [Archive(w); NextInning]
                      else [Archive(w); NextInning]
                      fi ]))))

((

m:

.

w:V. (

archive-condition(V;A;t;f;m;w;L2)))

(S2 = (S1 @ [consensus-message(a;i + 1;inl <i, v> )]))))))

(

v:V
((r = Init[v])

((

m:

.

w:V. (archive-condition(V;A;t;f;m;w;L2)

(S2 = (S1 @ [Archive(w); NextInning]))))

((

m:

.

w:V. (

archive-condition(V;A;t;f;m;w;L2)))

(S2 = S1)))))

Proof not projected

Error : references

\mforall{}[V:Type] \mforall{}A:Id List. \mforall{}t:\mBbbN{}\msupplus{}. \mforall{}f:V List {}\mrightarrow{} V. \mforall{}v0:V. \mforall{}L:consensus-rcv(V;A) List. \mforall{}r:consensus-rcv(V;A). let L2 = L @ [r] in let S1 = fst(consensus-rcvs-to-consensus-events(f;t;v0;L)) in let S2 = fst(consensus-rcvs-to-consensus-events(f;t;v0;L2)) in (\mexists{}a:\{a:Id| (a \mmember{} A)\} \mexists{}i:\mBbbN{} \mexists{}v:V ((r = Vote[a;i;v]) \mwedge{} ((\mexists{}m:\mBbbN{} \mexists{}w:V (archive-condition(V;A;t;f;m;w;L2) \mwedge{} (S2 = (S1 @ [consensus-message(a;i + 1;inl <i, v> ) / if ||filter(\mlambda{}x.is-inning-event(x);S1)|| + 1 <z i then map(\mlambda{}x.NextInning;upto(i - ||filter(\mlambda{}x.is-inning-event(x);S1)||)) @ [Archive(w); NextInning] else [Archive(w); NextInning] fi ])))) \mvee{} ((\mforall{}m:\mBbbN{}. \mforall{}w:V. (\mneg{}archive-condition(V;A;t;f;m;w;L2))) \mwedge{} (S2 = (S1 @ [consensus-message(a;i + 1;inl <i, v> )])))))) \mvee{} (\mexists{}v:V ((r = Init[v]) \mwedge{} ((\mexists{}m:\mBbbN{} \mexists{}w:V. (archive-condition(V;A;t;f;m;w;L2) \mwedge{} (S2 = (S1 @ [Archive(w); NextInning])))) \mvee{} ((\mforall{}m:\mBbbN{}. \mforall{}w:V. (\mneg{}archive-condition(V;A;t;f;m;w;L2))) \mwedge{} (S2 = S1))))) Date html generated: 2012_02_20-PM-07_50_44 Last ObjectModification: 2010_12_16-PM-09_37_47 Home Index