---

Step * of Lemma cs-ref-map3-predecided

∀[V:Type]
  ∀L:ts-reachable(consensus-ts3(V)). ∀v:V.
    ((∀v':V. (¬(COMMITED[v'] ∈ L))) ∧ (CONSIDERING[v] ∈ L) ⇐⇒ cs-ref-map3(L) = PREDECIDED[v] ∈ consensus-state2(V))
BY
{ (InstLemma `consensus-ts3-invariant1` []
   THEN (RepeatFor 3 (ParallelLast') THEN (InstLemma `cs-ref-map3-decided` [⌈V⌉;⌈L⌉]⋅ THENA Auto))
   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)
5. ∀v:V. ((COMMITED[v] ∈ L) ⇐⇒ cs-ref-map3(L) = Decided[v] ∈ consensus-state2(V))
⊢ (∀v':V. (¬(COMMITED[v'] ∈ L))) ∧ (CONSIDERING[v] ∈ L) ⇐⇒ cs-ref-map3(L) = PREDECIDED[v] ∈ consensus-state2(V)

---

Latex:


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


By

(InstLemma  `consensus-ts3-invariant1`  []
  THEN  (RepeatFor  3  (ParallelLast')  THEN  (InstLemma  `cs-ref-map3-decided`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (D  2  THEN  Thin  3)
  THEN  RepUR  ``consensus-ts3  ts-type``  2)

---

Home Index