---

Step * of Lemma consensus-accum-num-archives

∀[V:Type]
  ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V. ∀v0:V. ∀L:consensus-rcv(V;A) List.
    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
BY
{ (RepeatFor 5 ((D 0 THENA Auto)) THEN (BLemma `last_induction` THENA Auto)) }

1
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 archive-condition(V;A;t;f;i - 1;v;[]) supposing ↑b

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

---

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.
        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  \muparrow{}b


By

(RepeatFor  5  ((D  0  THENA  Auto))  THEN  (BLemma  `last\_induction`  THENA  Auto))

---

Home Index