Nuprl Lemma : RSC-ilf

(

[Cmd:ValueAllType].

[es:EO'].

[e:E].

v:

Cmd

Id. {v

RSC_Vote(Cmd)(e)

v

Base(``sc vote``;

Cmd

Id)(e)})

(

[z3,z2:

].

[Cmd:ValueAllType].

[es:EO'].

[e:E].

v:Cmd List

(Id List)
{v

Accum-class(

v,state.
                      if RSC_newvote(Cmd) <z2, z3> v state
                      then RSC_addvote() v state
                      else state
                      fi ;RSC_init() <[], []>;RSC_Vote(Cmd))(e)

L:(

Cmd

Id

E) List
(prior-classrel-list(es;

Cmd

Id;RSC_Vote(Cmd);L;e)

(

a,a1:

a2:Cmd

a3:Id
(<<<a, a1>, a2>, a3>

Base(``sc vote``;

Cmd

Id)(e)

(v
                     = if RSC_newvote(Cmd) <z2, z3> <<<a, a1>, a2>, a3>
                          list_accum(b,a.if RSC_newvote(Cmd) <z2, z3> a b then RSC_addvote() a b else b fi ;
                                     <[], []>;
                                     map(

p.(fst(p));L))
                       then RSC_addvote() <<<a, a1>, a2>, a3>
                            list_accum(b,a.if RSC_newvote(Cmd) <z2, z3> a b then RSC_addvote() a b else b fi ;
                                       <[], []>;
                                       map(

p.(fst(p));L))
                       else list_accum(b,a.if RSC_newvote(Cmd) <z2, z3> a b then RSC_addvote() a b else b fi ;
                                       <[], []>;
                                       map(

p.(fst(p));L))
fi ))))})

(

[Cmd:ValueAllType].

[es:EO'].

[e:E].

v:

Cmd
{v

RSC_RoundInfo(Cmd)(e)

v

Base(``sc retry``;

Cmd)(e)

(

a,a1:

a2:Cmd
((v = <<a, a1>, a2>)

(

a3:Id. <<<a, a1>, a2>, a3>

Base(``sc vote``;

Cmd

Id)(e))))})

(

[Cmd:ValueAllType].

[es:EO'].

[e:E].

v:

Cmd
{v

RSC_Proposal(Cmd)(e)

v

Base(``sc propose``;

Cmd)(e)

(

a,a1:

a2:Cmd. ((v = <a, a2>)

(

a3:Id. <<<a, a1>, a2>, a3>

Base(``sc vote``;

Cmd

Id)(e))))})

(

[Cmd:ValueAllType].

[es:EO'].

[e:E].

v:

(

List)
{v

Accum-class(

v,state.
                      if RSC_new_proposal() v state
                      then RSC_onnewpropose() v state
                      else state
                      fi ;RSC_init() <0, []>;RSC_Proposal(Cmd))(e)

L:(

Cmd

E) List
(prior-classrel-list(es;

Cmd;RSC_Proposal(Cmd);L;e)

(

a:

a1:Cmd
((<a, a1>

Base(``sc propose``;

Cmd)(e)

(

a3:

.

a5:Id. <<<a, a3>, a1>, a5>

Base(``sc vote``;

Cmd

Id)(e)))

(v
                    = if RSC_new_proposal() <a, a1>
                         list_accum(b,a.if RSC_new_proposal() a b then RSC_onnewpropose() a b else b fi ;
                                    <0, []>;
                                    map(

p.(fst(p));L))
                      then RSC_onnewpropose() <a, a1>
                           list_accum(b,a.if RSC_new_proposal() a b then RSC_onnewpropose() a b else b fi ;
                                      <0, []>;
                                      map(

p.(fst(p));L))
                      else list_accum(b,a.if RSC_new_proposal() a b then RSC_onnewpropose() a b else b fi ;
                                      <0, []>;
                                      map(

p.(fst(p));L))
fi ))))})

(

[z:

].

[clients:bag(Id)].

[Cmd:ValueAllType].

[es:EO'].

[e:E].

[i:Id].

[m:Message].
{<i, m>

RSC_Decision(Cmd;clients) z@|Loc, RSC_Decided(Cmd)|(e)

i

clients

(

a1:Cmd. (<z, a1>

Base(``sc decided``;

Cmd)(e)

(m = make-Msg(``sc notify``;

Cmd;<z, a1>))))})

(

[z:

].

[clients:bag(Id)].

[Cmd:ValueAllType].

[es:EO'].

[e:E].

[i:Id].

[m:Message].
{<i, m>

RSC_Notify(Cmd;clients) z(e)

(no RSC_Decision(Cmd;clients) z@|Loc, RSC_Decided(Cmd)| prior to e)

<i, m>

{RSC_Decision(Cmd;clients) z@|Loc, RSC_Decided(Cmd)|}(e)})

(

[Cmd:ValueAllType].

[z:

].

[es:EO'].

[e:E].

v:{x:

| x = 0}
{v

Accum-class(

v,state.
                      if RSC_round_increase() z v state
                      then RSC_incround() v state
                      else state
                      fi ;RSC_init() 0;RSC_RoundInfo(Cmd))(e)

L:(

Cmd

E) List
(prior-classrel-list(es;

Cmd;RSC_RoundInfo(Cmd);L;e)

(

a,a1:

.

a2:Cmd. ((<<..., ...>, ...>

...(...)

...)

...)))})

...

Proof not projected

Definitions occuring in Statement : RSC_main: RSC_main(Cmd;clients;cmdeq;flrs;locs), RSC_new_proposal: RSC_new_proposal(), RSC_Proposal: RSC_Proposal(Cmd), RSC_onnewpropose: RSC_onnewpropose(), RSC_Notify: RSC_Notify(Cmd;clients), RSC_Decision: RSC_Decision(Cmd;clients), RSC_incround: RSC_incround(), RSC_round_increase: RSC_round_increase(), RSC_RoundInfo: RSC_RoundInfo(Cmd), RSC_Quorum: RSC_Quorum(Cmd;cmdeq;flrs), RSC_addvote: RSC_addvote(), RSC_newvote: RSC_newvote(Cmd), RSC_init: RSC_init(), RSC_Decided: RSC_Decided(Cmd), RSC_Vote: RSC_Vote(Cmd), prior-classrel-list: prior-classrel-list(es;A;X;L;e), Accum-class: Accum-class(f;init;X), concat-lifting-loc-1: f@, make-Msg: make-Msg(hdr;typ;val), base-headers-msg-val: Base(hdr;typ), Message: Message, simple-loc-comb-1: F|Loc, X|, primed-class-opt: Prior(X)?b, no-classrel-in-interval: (no X between start and e), no-prior-classrel: (no X prior to e), classrel: v

X(e), eo-forward: eo.e, event-ordering+: EO+(Info), es-le: e

loc e' , es-loc: loc(e), es-E: E, Id: Id, map: map(f;as), length: ||as||, assert:

b, ifthenelse: if b then t else f fi , sq_or: a

b, uall:

[x:A]. B[x], guard: {T}, pi1: fst(t), pi2: snd(t), all:

x:A. B[x], exists:

x:A. B[x], iff: P

Q, not:

A, squash:

T, or: P

Q, and: P

Q, set: {x:A| B[x]} , apply: f a, lambda:

x.A[x], pair: <a, b>, product: x:A

B[x], cons: [car / cdr], nil: [], list: type List, multiply: n * m, add: n + m, natural_number: $n, int:

, token: "$token", equal: s = t, list_accum: list_accum(x,a.f[x; a];y;l), poss-maj: poss-maj(eq;L;x), deq: EqDecider(T), bag-member: x

bs, bag: bag(T), vatype: ValueAllType
Definitions : guard: {T}, hide: HIDDEN
Lemmas : RSC-ilf-hide

(\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id. \{v \mmember{} RSC\_Vote(Cmd)(e) \mLeftarrow{}{}\mRightarrow{} v \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)\}) \mwedge{} (\mforall{}[z3,z2:\mBbbZ{}]. \mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}v:Cmd List \mtimes{} (Id List) \{v \mmember{} Accum-class(\mlambda{}v,state. if RSC\_newvote(Cmd) <z2, z3> v state then RSC\_addvote() v state else state fi ;RSC\_init() <[], []>RSC\_Vote(Cmd))(e) \mLeftarrow{}{}\mRightarrow{} \mdownarrow{}\mexists{}L:(\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id \mtimes{} E) List (prior-classrel-list(es;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;RSC\_Vote(Cmd);L;e) \mwedge{} (\mexists{}a,a1:\mBbbZ{} \mexists{}a2:Cmd \mexists{}a3:Id (<<<a, a1>, a2>, a3> \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e) \mwedge{} (v = if RSC\_newvote(Cmd) <z2, z3> <<<a, a1>, a2>, a3> list\_accum(b,a.if RSC\_newvote(Cmd) <z2, z3> a b then RSC\_addvote() a b else b fi ; <[], []> map(\mlambda{}p.(fst(p));L)) then RSC\_addvote() <<<a, a1>, a2>, a3> list\_accum(b,a.if RSC\_newvote(Cmd) <z2, z3> a b then RSC\_addvote() a b else b fi ; <[], []> map(\mlambda{}p.(fst(p));L)) else list\_accum(b,a.if RSC\_newvote(Cmd) <z2, z3> a b then RSC\_addvote() a b else b fi ; <[], []> map(\mlambda{}p.(fst(p));L)) fi ))))\}) \mwedge{} (\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \{v \mmember{} RSC\_RoundInfo(Cmd)(e) \mLeftarrow{}{}\mRightarrow{} v \mmember{} Base(``sc retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e) \mdownarrow{}\mvee{} (\mexists{}a,a1:\mBbbZ{} \mexists{}a2:Cmd ((v = <<a, a1>, a2>) \mwedge{} (\mexists{}a3:Id. <<<a, a1>, a2>, a3> \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e))))\}) \mwedge{} (\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}v:\mBbbZ{} \mtimes{} Cmd \{v \mmember{} RSC\_Proposal(Cmd)(e) \mLeftarrow{}{}\mRightarrow{} v \mmember{} Base(``sc propose``;\mBbbZ{} \mtimes{} Cmd)(e) \mdownarrow{}\mvee{} (\mexists{}a,a1:\mBbbZ{} \mexists{}a2:Cmd ((v = <a, a2>) \mwedge{} (\mexists{}a3:Id. <<<a, a1>, a2>, a3> \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e))))\}) \mwedge{} (\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}v:\mBbbZ{} \mtimes{} (\mBbbZ{} List) \{v \mmember{} Accum-class(...;RSC\_init() ɘ, []>RSC\_Proposal(Cmd))(e) \mLeftarrow{}{}\mRightarrow{} \mdownarrow{}\mexists{}L:(\mBbbZ{} \mtimes{} Cmd \mtimes{} E) List (prior-classrel-list(es;\mBbbZ{} \mtimes{} Cmd;RSC\_Proposal(Cmd);L;e) \mwedge{} (\mexists{}a:\mBbbZ{} \mexists{}a1:Cmd ((<a, a1> \mmember{} Base(``sc propose``;\mBbbZ{} \mtimes{} Cmd)(e) \mdownarrow{}\mvee{} (\mexists{}a3:\mBbbZ{}. \mexists{}a5:Id. <<<a, a3>, a1>, a5> \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e))) \mwedge{} (v = if RSC\_new\_proposal() <a, a1> list\_accum(b,a.if RSC\_new\_proposal() a b then RSC\_onnewpropose() a b else b fi ; ɘ, []> map(\mlambda{}p.(fst(p));L)) then RSC\_onnewpropose() <a, a1> list\_accum(b,a.if RSC\_new\_proposal() a b then RSC\_onnewpropose() a b else b fi ; ɘ, []> map(\mlambda{}p.(fst(p));L)) else list\_accum(b,a.if RSC\_new\_proposal() a b then RSC\_onnewpropose() a b else b fi ; ɘ, []> map(\mlambda{}p.(fst(p));L)) fi ))))\}) \mwedge{} (\mforall{}[z:\mBbbZ{}]. \mforall{}[clients:bag(Id)]. \mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message]. \{<i, m> \mmember{} RSC\_Decision(Cmd;clients) z@|Loc, RSC\_Decided(Cmd)|(e) \mLeftarrow{}{}\mRightarrow{} i \mdownarrow{}\mmember{} clients \mwedge{} (\mdownarrow{}\mexists{}a1:Cmd (<z, a1> \mmember{} Base(``sc decided``;\mBbbZ{} \mtimes{} Cmd)(e) \mwedge{} (m = make-Msg(``sc notify``;\mBbbZ{} \mtimes{} Cmd;<z, a1>))))\}) \mwedge{} (\mforall{}[z:\mBbbZ{}]. \mforall{}[clients:bag(Id)]. \mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message]. \{<i, m> \mmember{} RSC\_Notify(Cmd;clients) z(e) \mLeftarrow{}{}\mRightarrow{} (no RSC\_Decision(Cmd;clients) z@|Loc, RSC\_Decided(Cmd)| prior to e) \mwedge{} <i, m> \mmember{} \{RSC\_Decision(Cmd;clients) z@|Loc, RSC\_Decided(Cmd)|\}(e)\}) \mwedge{} (\mforall{}[Cmd:ValueAllType]. \mforall{}[z:\mBbbZ{}]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}v:\{x:\mBbbZ{}| x = 0\} \{v \mmember{} Accum-class(...;RSC\_init() 0;RSC\_RoundInfo(Cmd))(e) \mLeftarrow{}{}\mRightarrow{} \mdownarrow{}\mexists{}L:(\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} E) List (prior-classrel-list(es;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd;RSC\_RoundInfo(Cmd);L;e) \mwedge{} (\mexists{}a,a1:\mBbbZ{} \mexists{}a2:Cmd ((<<a, a1>, a2> \mmember{} Base(``sc retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e) \mdownarrow{}\mvee{} (\mexists{}a6:Id. <<<a, a1>, a2>, a6> \mmember{} Base(``sc vote``;... \mtimes{} ...)(...))) \mwedge{} ...)))\}) \mwedge{} ... Date html generated: 2012_02_20-PM-04_01_26 Last ObjectModification: 2012_02_02-PM-01_59_18 Home Index