---

Step * 1 of Lemma cs-ref-map3-ambivalent


∀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))
BY
{ (InstLemma `consensus-ts3-invariant1` []
   THEN (RepeatFor 2 (ParallelLast')
         THEN (InstLemma `cs-ref-map3-decided` [⌈V⌉;⌈L⌉]⋅ THENA Auto)
         THEN (InstLemma `cs-ref-map3-predecided` [⌈V⌉;⌈L⌉]⋅ THENA Auto))
   THEN (D 2 THEN Thin 3)
   THEN RepUR ``consensus-ts3 ts-type`` 2
   THEN RepeatFor 2 (D 0)
   THEN Try (Complete (Auto))) }

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

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

---

Latex:



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


By

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

---

Home Index