---

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


1. [V] : Type
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. v0 : V@i
⊢ let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;[]) in if b
then archive-condition(V;A;t;f;i - 1;v;[])
else ∀v:V. (¬archive-condition(V;A;t;f;i;v;[]))
fi 
BY
{ ((RepUR ``consensus-accum-num-state`` 0 THEN Auto)
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN ExRepD
   THEN Thin (-1)
   THEN D -3
   THEN Reduce (-1)
   THEN AutoSimpHyp Auto (-1)) }

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  t  :  \mBbbN{}\msupplus{}@i
4.  f  :  (V  List)  {}\mrightarrow{}  V@i
5.  v0  :  V@i
\mvdash{}  let  b,i,as,vs,v  =  consensus-accum-num-state(t;f;v0;[])  in  if  b
then  archive-condition(V;A;t;f;i  -  1;v;[])
else  \mforall{}v:V.  (\mneg{}archive-condition(V;A;t;f;i;v;[]))
fi 


By

((RepUR  ``consensus-accum-num-state``  0  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  ExRepD
  THEN  Thin  (-1)
  THEN  D  -3
  THEN  Reduce  (-1)
  THEN  AutoSimpHyp  Auto  (-1))

---

Home Index