---

Step * of Lemma archive-condition-threshold-accum

∀[V:Type]
  ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V. ∀v0:V. ∀L:consensus-rcv(V;A) List. ∀n:ℕ. ∀v:V.
    (archive-condition(V;A;t;f;n;v;L)
    ⇐⇒ let b,i,as,vs,w = accumulate (with value s and list item r):
                           consensus-accum-num((2 * t) + 1;f;s;r)
                          over list:
                            L
                          with starting value:
                           <ff, 0, [], [], v0>) in (↑b) ∧ ((n + 1) = i ∈ ℤ) ∧ (v = w ∈ V))
BY
{ (Fold `consensus-accum-num-state` 0
   THEN InstLemma `consensus-accum-num-archives` []
   THEN RepeatFor 6 (ParallelLast')
   THEN MoveToConcl (-1)
   THEN (InstLemma `archive-consensus-accum-num` [⌈V⌉;⌈A⌉;⌈t⌉;⌈f⌉;⌈v0⌉;⌈L⌉]⋅ THENA Auto)
   THEN MoveToConcl (-1)) }

1
1. [V] : Type
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. v0 : V@i
6. L : consensus-rcv(V;A) List@i
⊢ (∀[v:V]. ∀[i:ℤ].  ↑(fst(consensus-accum-num-state(t;f;v0;L))) supposing archive-condition(V;A;t;f;i;v;L))
⇒ let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;L) in archive-condition(V;A;t;f;i - 1;v;L) supposing ↑b
⇒ (∀n:ℕ. ∀v:V.
      (archive-condition(V;A;t;f;n;v;L)
      ⇐⇒ let b,i,as,vs,w = consensus-accum-num-state(t;f;v0;L) in (↑b) ∧ ((n + 1) = i ∈ ℤ) ∧ (v = w ∈ V)))

---

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.  \mforall{}n:\mBbbN{}.  \mforall{}v:V.
        (archive-condition(V;A;t;f;n;v;L)
        \mLeftarrow{}{}\mRightarrow{}  let  b,i,as,vs,w  =  accumulate  (with  value  s  and  list  item  r):
                                                      consensus-accum-num((2  *  t)  +  1;f;s;r)
                                                    over  list:
                                                        L
                                                    with  starting  value:
                                                      <ff,  0,  [],  [],  v0>)  in  (\muparrow{}b)  \mwedge{}  ((n  +  1)  =  i)  \mwedge{}  (v  =  w))


By

(Fold  `consensus-accum-num-state`  0
  THEN  InstLemma  `consensus-accum-num-archives`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  MoveToConcl  (-1)
  THEN  (InstLemma  `archive-consensus-accum-num`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}v0\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1))

---

Home Index