---

Step * 1 of Lemma archive-consensus-accum-num


1. V : Type
2. A : Id List
3. t : ℕ+
4. f : (V List) ─→ V
5. v0 : V
⊢ ∀[v:V]. ∀[i:ℤ].  ↑(fst(consensus-accum-num-state(t;f;v0;[]))) supposing archive-condition(V;A;t;f;i;v;[])
BY
{ ((RepUR ``consensus-accum-num-state`` 0 THEN Auto)
   THEN D -1
   THEN ExRepD
   THEN Thin (-1)
   THEN D -3
   THEN Reduce (-1)
   THEN (ImpossibleEq Auto (-1) THEN Auto)⋅) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  t  :  \mBbbN{}\msupplus{}
4.  f  :  (V  List)  {}\mrightarrow{}  V
5.  v0  :  V
\mvdash{}  \mforall{}[v:V].  \mforall{}[i:\mBbbZ{}].
        \muparrow{}(fst(consensus-accum-num-state(t;f;v0;[])))  supposing  archive-condition(V;A;t;f;i;v;[])


By

((RepUR  ``consensus-accum-num-state``  0  THEN  Auto)
  THEN  D  -1
  THEN  ExRepD
  THEN  Thin  (-1)
  THEN  D  -3
  THEN  Reduce  (-1)
  THEN  (ImpossibleEq  Auto  (-1)  THEN  Auto)\mcdot{})

---

Home Index