---

Step * 2 1 3 1 2 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. x[i] = INITIAL ∈ consensus-state3(V)@i
8. y[i] = WITHDRAWN ∈ consensus-state3(V)@i
9. x ∈ consensus-state3(V) List
10. y ∈ consensus-state3(V) List
11. v : V
12. (COMMITED[v] ∈ x)
13. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
⊢ (COMMITED[v] ∈ y)
BY
{ ((RepeatFor 2 (ParallelOp -2) THEN Auto)
   THEN (Assert y[i1] = x[i1] ∈ consensus-state3(V) BY
               BackThruSomeHyp)
   THEN Auto
   THEN (D 0 THENA 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. x[i] = INITIAL ∈ consensus-state3(V)@i
8. y[i] = WITHDRAWN ∈ consensus-state3(V)@i
9. x ∈ consensus-state3(V) List
10. y ∈ consensus-state3(V) List
11. v : V
12. i1 : ℕ
13. i1 < ||x|| c∧ (COMMITED[v] = x[i1] ∈ consensus-state3(V))
14. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
15. i1 < ||y||
16. i1 = i ∈ ℤ@i
⊢ False

---

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.  x[i]  =  INITIAL@i
8.  y[i]  =  WITHDRAWN@i
9.  x  \mmember{}  consensus-state3(V)  List
10.  y  \mmember{}  consensus-state3(V)  List
11.  v  :  V
12.  (COMMITED[v]  \mmember{}  x)
13.  \mforall{}[v':V].  v'  =  v  supposing  (CONSIDERING[v']  \mmember{}  x)  \mvee{}  (COMMITED[v']  \mmember{}  x)
\mvdash{}  (COMMITED[v]  \mmember{}  y)


By

((RepeatFor  2  (ParallelOp  -2)  THEN  Auto)
  THEN  (Assert  y[i1]  =  x[i1]  BY
                          BackThruSomeHyp)
  THEN  Auto
  THEN  (D  0  THENA  Auto))

---

Home Index