---

Step * of Lemma cs-ref-map3-decided

∀[V:Type]
  ∀L:ts-reachable(consensus-ts3(V)). ∀v:V.  ((COMMITED[v] ∈ L) ⇐⇒ cs-ref-map3(L) = Decided[v] ∈ consensus-state2(V))
BY
{ (InstLemma `consensus-ts3-invariant1` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (D 2 THEN Thin 3)
   THEN RepUR ``consensus-ts3 ts-type`` 2) }

1
1. [V] : Type
2. L : consensus-state3(V) List@i
3. v : V@i
4. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ L) ∨ (COMMITED[v'] ∈ L) 
   supposing (CONSIDERING[v] ∈ L) ∨ (COMMITED[v] ∈ L)
⊢ (COMMITED[v] ∈ L) ⇐⇒ cs-ref-map3(L) = Decided[v] ∈ consensus-state2(V)

---

Latex:


\mforall{}[V:Type]
    \mforall{}L:ts-reachable(consensus-ts3(V)).  \mforall{}v:V.    ((COMMITED[v]  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  cs-ref-map3(L)  =  Decided[v])


By

(InstLemma  `consensus-ts3-invariant1`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (D  2  THEN  Thin  3)
  THEN  RepUR  ``consensus-ts3  ts-type``  2)

---

Home Index