---

Step * of Lemma consensus-state3-unequal

∀[V:Type]
  ((¬(INITIAL = WITHDRAWN ∈ consensus-state3(V)))
  ∧ (∀[v:V]
       (((¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))) ∧ (¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))))
       ∧ (¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)))
       ∧ (¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)))
       ∧ (∀[v':V]
            ((¬(CONSIDERING[v] = COMMITED[v'] ∈ consensus-state3(V)))
            ∧ (¬(CONSIDERING[v] = CONSIDERING[v'] ∈ consensus-state3(V)))
              ∧ (¬(COMMITED[v] = COMMITED[v'] ∈ consensus-state3(V))) 
              supposing ¬(v = v' ∈ V))))))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN Try (((RepUR ``consensus-state3 cs-initial cs-withdrawn`` -1 THEN RepUR ``cs-considering cs-commited`` -1)
              THEN Auto
              ))) }

---

Latex:


\mforall{}[V:Type]
    ((\mneg{}(INITIAL  =  WITHDRAWN))
    \mwedge{}  (\mforall{}[v:V]
              (((\mneg{}(COMMITED[v]  =  INITIAL))  \mwedge{}  (\mneg{}(CONSIDERING[v]  =  INITIAL)))
              \mwedge{}  (\mneg{}(COMMITED[v]  =  WITHDRAWN))
              \mwedge{}  (\mneg{}(CONSIDERING[v]  =  WITHDRAWN))
              \mwedge{}  (\mforall{}[v':V]
                        ((\mneg{}(CONSIDERING[v]  =  COMMITED[v']))
                        \mwedge{}  (\mneg{}(CONSIDERING[v]  =  CONSIDERING[v']))  \mwedge{}  (\mneg{}(COMMITED[v]  =  COMMITED[v'])) 
                            supposing  \mneg{}(v  =  v'))))))


By

(Auto
  THEN  (D  0  THENA  Auto)
  THEN  Try  (((RepUR  ``consensus-state3  cs-initial  cs-withdrawn``  -1
                          THEN  RepUR  ``cs-considering  cs-commited``  -1
                          )
                        THEN  Auto
                        )))

---

Home Index