---

Step * 1 1 2 2 1 1 2 1 of Lemma consensus-ts4-archived-invariant


1. V : Type@i'
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. x : ConsensusState@i
6. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) x@i
7. y : ConsensusState@i
8. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) y@i
9. ∀i:ℤ. ∀v:V. ∀a:{a:Id| (a ∈ A)} .
     (by state x, a archived v in inning i
     ⇒ (∀j:ℕi. ∀v':V.  (in state x, inning j could commit v'  ⇒ (v' = v ∈ V))))@i
10. a : {a:Id| (a ∈ A)} @i
11. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = a ∈ Id)) ⇒ ((Inning(y;b) = Inning(x;b) ∈ ℤ) ∧ (Estimate(y;b) = Estimate(x;b) ∈ i:ℤ fp-> V)))@i
12. Inning(y;a) = Inning(x;a) ∈ ℤ@i
13. ¬(Inning(x;a) ∈ fpf-domain(Estimate(x;a)))@i
14. v1 : V@i
15. state x may consider v1 in inning Inning(x;a)@i
16. Estimate(y;a) = Estimate(x;a) ⊕ Inning(x;a) : v1 ∈ i:ℤ fp-> V@i
17. i : ℤ@i
18. v : V@i
19. a ∈ Id
20. by state y, a archived v in inning i@i
21. j : ℕi@i
22. v' : V@i
23. in state y, inning j could commit v' @i
24. ¬by state x, a archived v in inning i
25. Inning(x;a) = i ∈ ℤ
26. v1 = v ∈ V
27. state x may consider v in inning i
∧ (Inning(y;a) = i ∈ ℤ)
∧ (Estimate(y;a) = Estimate(x;a) ⊕ i : v ∈ i:ℤ fp-> V)
∧ (¬(i ∈ fpf-domain(Estimate(x;a))))
⊢ v' = v ∈ V
BY
{ (Thin (-2) THEN D -4 THEN SupposeNot THEN Auto THEN RepUR ``cs-precondition`` -5 THEN ExRepD) }

1
1. V : Type@i'
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. x : ConsensusState@i
6. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) x@i
7. y : ConsensusState@i
8. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) y@i
9. ∀i:ℤ. ∀v:V. ∀a:{a:Id| (a ∈ A)} .
     (by state x, a archived v in inning i
     ⇒ (∀j:ℕi. ∀v':V.  (in state x, inning j could commit v'  ⇒ (v' = v ∈ V))))@i
10. a : {a:Id| (a ∈ A)} @i
11. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = a ∈ Id)) ⇒ ((Inning(y;b) = Inning(x;b) ∈ ℤ) ∧ (Estimate(y;b) = Estimate(x;b) ∈ i:ℤ fp-> V)))@i
12. Inning(y;a) = Inning(x;a) ∈ ℤ@i
13. ¬(Inning(x;a) ∈ fpf-domain(Estimate(x;a)))@i
14. v1 : V@i
15. state x may consider v1 in inning Inning(x;a)@i
16. Estimate(y;a) = Estimate(x;a) ⊕ Inning(x;a) : v1 ∈ i:ℤ fp-> V@i
17. i : ℤ@i
18. v : V@i
19. a ∈ Id
20. by state y, a archived v in inning i@i
21. j : ℕi@i
22. v' : V@i
23. ws : {a:Id| (a ∈ A)}  List@i
24. (ws ∈ W)@i
25. ∀a:{a:Id| (a ∈ A)} 
      ((a ∈ ws) ⇒ (by state y, a archived v' in inning j ∨ in state y, a has not completed inning j))@i
26. ¬by state x, a archived v in inning i
27. Inning(x;a) = i ∈ ℤ
28. w1 : {a:Id| (a ∈ A)}  List
29. (w1 ∈ W)
30. ∀b:{a:Id| (a ∈ A)} . ((b ∈ w1) ⇒ (i ≤ Inning(x;b)))
31. ∀ws':{a:Id| (a ∈ A)}  List. ((ws' ∈ W) ⇒ (¬in state x, ws' blocks w1 from archiving v in inning i))
32. Inning(y;a) = i ∈ ℤ
33. Estimate(y;a) = Estimate(x;a) ⊕ i : v ∈ i:ℤ fp-> V
34. ¬(i ∈ fpf-domain(Estimate(x;a)))
35. ¬(v' = v ∈ V)
⊢ v' = v ∈ V

---

Latex:



1.  V  :  Type@i'
2.  \mforall{}v1,v2:V.    Dec(v1  =  v2)@i
3.  A  :  Id  List@i
4.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
5.  x  :  ConsensusState@i
6.  (\mlambda{}a.<-1,  \motimes{}>)  rel\_star(ConsensusState;  \mlambda{}x,y.  CR[x,y])  x@i
7.  y  :  ConsensusState@i
8.  (\mlambda{}a.<-1,  \motimes{}>)  rel\_star(ConsensusState;  \mlambda{}x,y.  CR[x,y])  y@i
9.  \mforall{}i:\mBbbZ{}.  \mforall{}v:V.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .
          (by  state  x,  a  archived  v  in  inning  i
          {}\mRightarrow{}  (\mforall{}j:\mBbbN{}i.  \mforall{}v':V.    (in  state  x,  inning  j  could  commit  v'    {}\mRightarrow{}  (v'  =  v))))@i
10.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
11.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\} 
            ((\mneg{}(b  =  a))  {}\mRightarrow{}  ((Inning(y;b)  =  Inning(x;b))  \mwedge{}  (Estimate(y;b)  =  Estimate(x;b))))@i
12.  Inning(y;a)  =  Inning(x;a)@i
13.  \mneg{}(Inning(x;a)  \mmember{}  fpf-domain(Estimate(x;a)))@i
14.  v1  :  V@i
15.  state  x  may  consider  v1  in  inning  Inning(x;a)@i
16.  Estimate(y;a)  =  Estimate(x;a)  \moplus{}  Inning(x;a)  :  v1@i
17.  i  :  \mBbbZ{}@i
18.  v  :  V@i
19.  a  \mmember{}  Id
20.  by  state  y,  a  archived  v  in  inning  i@i
21.  j  :  \mBbbN{}i@i
22.  v'  :  V@i
23.  in  state  y,  inning  j  could  commit  v'  @i
24.  \mneg{}by  state  x,  a  archived  v  in  inning  i
25.  Inning(x;a)  =  i
26.  v1  =  v
27.  state  x  may  consider  v  in  inning  i
\mwedge{}  (Inning(y;a)  =  i)
\mwedge{}  (Estimate(y;a)  =  Estimate(x;a)  \moplus{}  i  :  v)
\mwedge{}  (\mneg{}(i  \mmember{}  fpf-domain(Estimate(x;a))))
\mvdash{}  v'  =  v


By

(Thin  (-2)  THEN  D  -4  THEN  SupposeNot  THEN  Auto  THEN  RepUR  ``cs-precondition``  -5  THEN  ExRepD)

---

Home Index