---

Step * 2 1 2 1 1 5 of Lemma consensus-refinement2


1. [V] : Type
2. x : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. ||y|| = ||x|| ∈ ℤ@i
5. i : ℕ||x||@i
6. ∀j:ℕ||x||. ((¬(j = i ∈ ℤ)) ⇒ (y[j] = x[j] ∈ consensus-state3(V)))@i
7. v1 : V@i
8. x[i] = CONSIDERING[v1] ∈ consensus-state3(V)@i
9. y[i] = WITHDRAWN ∈ consensus-state3(V)@i
10. x ∈ consensus-state3(V) List
11. y ∈ consensus-state3(V) List
12. v : V
13. ∀v':V. (¬(COMMITED[v'] ∈ x))
14. (CONSIDERING[v] ∈ x)
15. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
⊢ (cs-ref-map3(y) = AMBIVALENT ∈ consensus-state2(V))
∨ ((∀v':V. (¬(COMMITED[v'] ∈ y))) ∧ (CONSIDERING[v] ∈ y))
∨ (COMMITED[v] ∈ y)
BY
{ (InstHyp [⌈v1⌉] (-1)⋅
   THENA (Auto THEN OrLeft THEN Auto THEN OnMaybeHyp 8 (\h. (RevHypSubst h 0 THEN Complete (Auto))))
   ) }

1
1. [V] : Type
2. x : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. ||y|| = ||x|| ∈ ℤ@i
5. i : ℕ||x||@i
6. ∀j:ℕ||x||. ((¬(j = i ∈ ℤ)) ⇒ (y[j] = x[j] ∈ consensus-state3(V)))@i
7. v1 : V@i
8. x[i] = CONSIDERING[v1] ∈ consensus-state3(V)@i
9. y[i] = WITHDRAWN ∈ consensus-state3(V)@i
10. x ∈ consensus-state3(V) List
11. y ∈ consensus-state3(V) List
12. v : V
13. ∀v':V. (¬(COMMITED[v'] ∈ x))
14. (CONSIDERING[v] ∈ x)
15. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
16. v1 = v ∈ V
⊢ (cs-ref-map3(y) = AMBIVALENT ∈ consensus-state2(V))
∨ ((∀v':V. (¬(COMMITED[v'] ∈ y))) ∧ (CONSIDERING[v] ∈ y))
∨ (COMMITED[v] ∈ y)

---

Latex:



1.  [V]  :  Type
2.  x  :  ts-reachable(consensus-ts3(V))@i
3.  y  :  ts-reachable(consensus-ts3(V))@i
4.  ||y||  =  ||x||@i
5.  i  :  \mBbbN{}||x||@i
6.  \mforall{}j:\mBbbN{}||x||.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  (y[j]  =  x[j]))@i
7.  v1  :  V@i
8.  x[i]  =  CONSIDERING[v1]@i
9.  y[i]  =  WITHDRAWN@i
10.  x  \mmember{}  consensus-state3(V)  List
11.  y  \mmember{}  consensus-state3(V)  List
12.  v  :  V
13.  \mforall{}v':V.  (\mneg{}(COMMITED[v']  \mmember{}  x))
14.  (CONSIDERING[v]  \mmember{}  x)
15.  \mforall{}[v':V].  v'  =  v  supposing  (CONSIDERING[v']  \mmember{}  x)  \mvee{}  (COMMITED[v']  \mmember{}  x)
\mvdash{}  (cs-ref-map3(y)  =  AMBIVALENT)
\mvee{}  ((\mforall{}v':V.  (\mneg{}(COMMITED[v']  \mmember{}  y)))  \mwedge{}  (CONSIDERING[v]  \mmember{}  y))
\mvee{}  (COMMITED[v]  \mmember{}  y)


By

(InstHyp  [\mkleeneopen{}v1\mkleeneclose{}]  (-1)\mcdot{}
  THENA  (Auto  THEN  OrLeft  THEN  Auto  THEN  OnMaybeHyp  8  (\mbackslash{}h.  (RevHypSubst  h  0  THEN  Complete  (Auto))))
  )

---

Home Index