---

Step * of Lemma archive-consensus-accum-num

∀[V:Type]. ∀[A:Id List]. ∀[t:ℕ+]. ∀[f:(V List) ─→ V]. ∀[v0:V]. ∀[L:consensus-rcv(V;A) List]. ∀[v:V]. ∀[i:ℤ].
  ↑(fst(consensus-accum-num-state(t;f;v0;L))) supposing archive-condition(V;A;t;f;i;v;L)
BY
{ (RepeatFor 6 ((D 0 THENA Auto)) THEN MoveToConcl (-1) THEN (BLemma `last_induction` THENA Auto)) }

1
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;[])

2
1. V : Type
2. A : Id List
3. t : ℕ+
4. f : (V List) ─→ V
5. v0 : V
⊢ ∀ys:consensus-rcv(V;A) List. ∀y:consensus-rcv(V;A).
    ((∀[v:V]. ∀[i:ℤ].  ↑(fst(consensus-accum-num-state(t;f;v0;ys))) supposing archive-condition(V;A;t;f;i;v;ys))
    ⇒ (∀[v:V]. ∀[i:ℤ].
          ↑(fst(consensus-accum-num-state(t;f;v0;ys @ [y]))) supposing archive-condition(V;A;t;f;i;v;ys @ [y])))

---

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{}[v:V].
\mforall{}[i:\mBbbZ{}].
    \muparrow{}(fst(consensus-accum-num-state(t;f;v0;L)))  supposing  archive-condition(V;A;t;f;i;v;L)


By

(RepeatFor  6  ((D  0  THENA  Auto))  THEN  MoveToConcl  (-1)  THEN  (BLemma  `last\_induction`  THENA  Auto))

---

Home Index