---

Step * 1 of Lemma pi2-consensus-rcvs-to-consensus-events


1. V : Type
2. A : Id List
3. t : ℕ+
4. f : (V List) ─→ V
5. v0 : V
6. ys : consensus-rcv(V;A) List@i
7. y : consensus-rcv(V;A)@i
8. v1 : consensus-event(V;A) List@i
9. v2 : consensus-rcv(V;A) List@i
10. v2 = ys ∈ (consensus-rcv(V;A) List)@i
⊢ (snd(let b,i,as,vs,v = accumulate (with value s and list item r):
                          consensus-accum-num((2 * t) + 1;f;s;r)
                         over list:
                           v2 @ [y]
                         with starting value:
                          <ff, 0, [], [], v0>) in <v1
                                                   @ if rcv-vote?(y)
                                                     then let a,i,v = rcvd-vote(y) in 
                                                          [consensus-message(a;i + 1;inl <i, v>)]
                                                     else []
                                                     fi 
                                                   @ if b
                                                     then if null(as)
                                                          then [Archive(v); NextInning]
                                                          else map(λn.NextInning;upto(i - 1 
                                                                   - ||filter(λx.is-inning-event(x);v1)||))
                                                               @ [Archive(v); NextInning]
                                                          fi 
                                                     else []
                                                     fi 
                                                  , v2 @ [y]
                                                  >))
= (ys @ [y])
∈ (consensus-rcv(V;A) List)
BY
{ ((GenConclAtAddrType ⌈𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V⌉ [2;1;1]⋅ THEN Auto)
   THEN RepeatFor 4 (D -2)
   THEN Reduce 0
   THEN Auto) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  t  :  \mBbbN{}\msupplus{}
4.  f  :  (V  List)  {}\mrightarrow{}  V
5.  v0  :  V
6.  ys  :  consensus-rcv(V;A)  List@i
7.  y  :  consensus-rcv(V;A)@i
8.  v1  :  consensus-event(V;A)  List@i
9.  v2  :  consensus-rcv(V;A)  List@i
10.  v2  =  ys@i
\mvdash{}  (snd(let  b,i,as,vs,v  =  accumulate  (with  value  s  and  list  item  r):
                                                    consensus-accum-num((2  *  t)  +  1;f;s;r)
                                                  over  list:
                                                      v2  @  [y]
                                                  with  starting  value:
                                                    <ff,  0,  [],  [],  v0>)  in  <v1
                                                                                                      @  if  rcv-vote?(y)
                                                                                                          then  let  a,i,v  =  rcvd-vote(y)  in 
                                                                                                                    [consensus-message(a;i  +  1;inl  <i,  v>)]
                                                                                                          else  []
                                                                                                          fi 
                                                                                                      @  if  b
                                                                                                          then  if  null(as)
                                                                                                                    then  [Archive(v);  NextInning]
                                                                                                                    else  map(\mlambda{}n.NextInning;upto(i  -  1 
                                                                                                                                      -  ||filter(\mlambda{}x.is-inning-event(x);
                                                                                                                                                            v1)||))
                                                                                                                              @  [Archive(v);  NextInning]
                                                                                                                    fi 
                                                                                                          else  []
                                                                                                          fi 
                                                                                                    ,  v2  @  [y]
                                                                                                    >))
=  (ys  @  [y])


By

((GenConclAtAddrType  \mkleeneopen{}\mBbbB{}  \mtimes{}  \mBbbZ{}  \mtimes{}  \{a:Id|  (a  \mmember{}  A)\}    List  \mtimes{}  V  List  \mtimes{}  V\mkleeneclose{}  [2;1;1]\mcdot{}  THEN  Auto)
  THEN  RepeatFor  4  (D  -2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index