---

Step * of Lemma cs-ref-map3-ambivalent

∀[V:Type]. ∀[L:ts-reachable(consensus-ts3(V))].
  uiff((∀[v:V]. (¬(COMMITED[v] ∈ L))) ∧ (∀[v:V]. (¬(CONSIDERING[v] ∈ L)));cs-ref-map3(L)
  = AMBIVALENT
  ∈ consensus-state2(V))
BY
{ RemoveUniform (Auto THEN Try ((D 2 THEN RepUR ``ts-type consensus-ts3`` 2 THEN Auto))) 
(Auto THEN Try ((D 2 THEN RepUR ``ts-type consensus-ts3`` 2 THEN Auto)))⋅ }

1
∀V:Type. ∀L:ts-reachable(consensus-ts3(V)).
  ((∀[v:V]. (¬(COMMITED[v] ∈ L))) ∧ (∀[v:V]. (¬(CONSIDERING[v] ∈ L)))
  ⇐⇒ cs-ref-map3(L) = AMBIVALENT ∈ consensus-state2(V))

---

Latex:


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


By

RemoveUniform  (Auto  THEN  Try  ((D  2  THEN  RepUR  ``ts-type  consensus-ts3``  2  THEN  Auto))) 
(Auto  THEN  Try  ((D  2  THEN  RepUR  ``ts-type  consensus-ts3``  2  THEN  Auto)))\mcdot{}

---

Home Index