---

Step * of Lemma consensus-accum-num-property3

∀[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 if b
    then archive-condition(V;A;t;f;i - 1;v;L)
    else ∀v:V. (¬archive-condition(V;A;t;f;i;v;L))
    fi 
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 if b
then archive-condition(V;A;t;f;i - 1;v;[])
else ∀v:V. (¬archive-condition(V;A;t;f;i;v;[]))
fi 

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 if b
    then archive-condition(V;A;t;f;i - 1;v;ys)
    else ∀v:V. (¬archive-condition(V;A;t;f;i;v;ys))
    fi 
    ⇒ let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;ys @ [y]) in if b
       then archive-condition(V;A;t;f;i - 1;v;ys @ [y])
       else ∀v:V. (¬archive-condition(V;A;t;f;i;v;ys @ [y]))
       fi )

---

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  if  b
        then  archive-condition(V;A;t;f;i  -  1;v;L)
        else  \mforall{}v:V.  (\mneg{}archive-condition(V;A;t;f;i;v;L))
        fi 


By

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

---

Home Index