---

Step * of Lemma three-cs-vote-invariant

∀V:Type. ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V. ∀s:ts-type(three-consensus-ts(V;A;t;f)).
  ((ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s)
  ⇒ (∀a:{a:Id| (a ∈ A)} . ∀n:ℕ. ∀b:{a:Id| (a ∈ A)} . ∀v1:V.
        ((Vote[b;n;v1] ∈ s a) ⇒ (∃L:consensus-rcv(V;A) List. (L ≤ s b ∧ archive-condition(V;A;t;f;n;v1;L))))))
BY
{ ((RepeatFor 4 ((D 0 THENA Auto))
    THEN (BLemma `ts-reachable-induction2`
          THENA (Auto THEN DVar `s' THEN AllHyps h.(RepUR ``ts-type three-consensus-ts`` h THEN Auto) )
          )
    THEN Try (((Unfold `ts-init` 0 THEN RepUR ``three-consensus-ts`` 0) THEN Auto)))
   THEN RepeatFor 2 (((D 0 THENA Auto) THEN D -1 THEN Thin (-1) THEN RepUR ``ts-type three-consensus-ts`` -1))
   THEN RepUR ``ts-rel three-consensus-ts`` 0
   THEN Auto
   THEN ExRepD) }

1
1. V : Type@i'
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. s : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
6. y : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
7. ∀a:{a:Id| (a ∈ A)} . ∀n:ℕ. ∀b:{a:Id| (a ∈ A)} . ∀v1:V.
     ((Vote[b;n;v1] ∈ s a) ⇒ (∃L:consensus-rcv(V;A) List. (L ≤ s b ∧ archive-condition(V;A;t;f;n;v1;L))))@i
8. a1 : {a:Id| (a ∈ A)} @i
9. e : consensus-rcv(V;A)@i
10. ∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀v:V.
      ((e = Vote[b;i;v] ∈ consensus-rcv(V;A))
      ⇒ ((∃L:consensus-rcv(V;A) List. (L ≤ s b ∧ archive-condition(V;A;t;f;i;v;L))) ∧ (¬(e ∈ s a1))))@i
11. ∀b:{a:Id| (a ∈ A)} . ((¬(b = a1 ∈ Id)) ⇒ ((y b) = (s b) ∈ (consensus-rcv(V;A) List)))@i
12. (y a1) = ((s a1) @ [e]) ∈ (consensus-rcv(V;A) List)@i
13. a : {a:Id| (a ∈ A)} @i
14. n : ℕ@i
15. b : {a:Id| (a ∈ A)} @i
16. v1 : V@i
17. (Vote[b;n;v1] ∈ y a)@i
⊢ ∃L:consensus-rcv(V;A) List. (L ≤ y b ∧ archive-condition(V;A;t;f;n;v1;L))

---

Latex:


\mforall{}V:Type.  \mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.  \mforall{}f:(V  List)  {}\mrightarrow{}  V.  \mforall{}s:ts-type(three-consensus-ts(V;A;t;f)).
    ((ts-init(three-consensus-ts(V;A;t;f))  (ts-rel(three-consensus-ts(V;A;t;f))\^{}*)  s)
    {}\mRightarrow{}  (\mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}n:\mBbbN{}.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}v1:V.
                ((Vote[b;n;v1]  \mmember{}  s  a)
                {}\mRightarrow{}  (\mexists{}L:consensus-rcv(V;A)  List.  (L  \mleq{}  s  b  \mwedge{}  archive-condition(V;A;t;f;n;v1;L))))))


By

((RepeatFor  4  ((D  0  THENA  Auto))
    THEN  (BLemma  `ts-reachable-induction2`
                THENA  (Auto
                              THEN  DVar  `s'
                              THEN  AllHyps  h.(RepUR  ``ts-type  three-consensus-ts``  h  THEN  Auto)  )
                )
    THEN  Try  (((Unfold  `ts-init`  0  THEN  RepUR  ``three-consensus-ts``  0)  THEN  Auto)))
  THEN  RepeatFor  2  (((D  0  THENA  Auto)
                                        THEN  D  -1
                                        THEN  Thin  (-1)
                                        THEN  RepUR  ``ts-type  three-consensus-ts``  -1))
  THEN  RepUR  ``ts-rel  three-consensus-ts``  0
  THEN  Auto
  THEN  ExRepD)

---

Home Index