---

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

∀[V:Type]. ∀[A:Id List]. ∀[t:ℕ+]. ∀[f:(V List) ─→ V]. ∀[v0:V]. ∀[L:consensus-rcv(V;A) List].
  ((snd(consensus-rcvs-to-consensus-events(f;t;v0;L))) = L ∈ (consensus-rcv(V;A) List))
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN BLemma `last_induction`
   THEN Auto
   THEN MoveToConcl (-1)
   THEN RepUR ``consensus-rcvs-to-consensus-events`` 0
   THEN Try (Complete (Auto))
   THEN (RW (AddrC [2;2;1] (LemmaC `list_accum_append`)) 0 THENA Auto)
   THEN (GenConclAtAddrType ⌈consensus-event(V;A) List × (consensus-rcv(V;A) List)⌉ [1;2;1]⋅
         THENA (Auto THEN GenConclAtAddrType ⌈𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V⌉ [2;1]⋅ THEN Auto)
         )
   THEN Thin (-1)
   THEN D -1
   THEN Reduce 0
   THEN Auto) }

1
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)

---

Latex:


\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].
    ((snd(consensus-rcvs-to-consensus-events(f;t;v0;L)))  =  L)


By

(Auto
  THEN  MoveToConcl  (-1)
  THEN  BLemma  `last\_induction`
  THEN  Auto
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``consensus-rcvs-to-consensus-events``  0
  THEN  Try  (Complete  (Auto))
  THEN  (RW  (AddrC  [2;2;1]  (LemmaC  `list\_accum\_append`))  0  THENA  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}consensus-event(V;A)  List  \mtimes{}  (consensus-rcv(V;A)  List)\mkleeneclose{}  [1;2;1]\mcdot{}
              THENA  (Auto
                            THEN  GenConclAtAddrType  \mkleeneopen{}\mBbbB{}  \mtimes{}  \mBbbZ{}  \mtimes{}  \{a:Id|  (a  \mmember{}  A)\}    List  \mtimes{}  V  List  \mtimes{}  V\mkleeneclose{}  [2;1]\mcdot{}
                            THEN  Auto)
              )
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index