---

Step * 1 1 2 1 2 1 2 1 1 2 1 1 1 2 2 1 1 1 1 3 1 1 1 3 1 1 1 2 of Lemma consensus-reachable


1. V : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)}  List@i
10. (ws ∈ W)@i
11. 0 < ||ws||
12. i : ℤ
13. x : ConsensusState
14. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ ((Inning(x;a) = i ∈ ℤ) ∧ (¬(i ∈ fpf-domain(Estimate(x;a))))))
15. v : V
16. state x may consider v in inning i
17. n : ℤ@i
18. ¬(A[n - 1] ∈ firstn(n - 1;A))
19. 0 < n@i
20. x ((λx,y. CR(in ws)[x, y] )^*) (λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi )@\000Ci
21. n - 1 < ||A|| c∧ ((A[n - 1] ∈ ws) ∧ (¬(A[n - 1] ∈ firstn(n - 1;A))))
22. z : ConsensusState@i
23. (λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi ) = z ∈ ConsensusState@i
24. (A[n - 1] ∈ ws)
25. Z : {a:Id| (a ∈ A)}  ⟶ (ℤ × j:ℤ fp-> V)@i
26. (λb.if b = A[n - 1] ∧b tt then <i, Estimate(z;b) ⊕ i : v> else z b fi ) = Z ∈ ConsensusState@i
27. (A[n - 1] ∈ ws)
28. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = A[n - 1] ∈ Id)) ⇒ ((Inning(Z;b) = Inning(z;b) ∈ ℤ) ∧ (Estimate(Z;b) = Estimate(z;b) ∈ i:ℤ fp-> V)))
29. <i, Estimate(z;A[n - 1]) ⊕ i : v> = (Z A[n - 1]) ∈ (ℤ × j:ℤ fp-> V)
30. i = Inning(z;A[n - 1]) ∈ ℤ
31. ¬(Inning(z;A[n - 1]) ∈ fpf-domain(Estimate(z;A[n - 1])))
32. w1 : {a:Id| (a ∈ A)}  List
33. (w1 ∈ W)
34. ∀b:{a:Id| (a ∈ A)} . ((b ∈ w1) ⇒ (i ≤ Inning(x;b)))
35. ∀ws':{a:Id| (a ∈ A)}  List. ((ws' ∈ W) ⇒ (¬in state x, ws' blocks w1 from archiving v in inning i))
36. ws@0 : {a:Id| (a ∈ A)}  List
37. (ws@0 ∈ W)
38. ∀a:Id. ((a ∈ A) ∈ Type)
39. b : Id@i
40. (b ∈ A)@i
41. (b ∈ ws@0)
⊢ Inning(λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi ;b) ∈ ℤ
BY
{ GenConclAtAddrType ⌜ConsensusState⌝ [2;1]⋅ }

1
.....wf..... 
1. V : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)}  List@i
10. (ws ∈ W)@i
11. 0 < ||ws||
12. i : ℤ
13. x : ConsensusState
14. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ ((Inning(x;a) = i ∈ ℤ) ∧ (¬(i ∈ fpf-domain(Estimate(x;a))))))
15. v : V
16. state x may consider v in inning i
17. n : ℤ@i
18. ¬(A[n - 1] ∈ firstn(n - 1;A))
19. 0 < n@i
20. x ((λx,y. CR(in ws)[x, y] )^*) (λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi )@\000Ci
21. n - 1 < ||A|| c∧ ((A[n - 1] ∈ ws) ∧ (¬(A[n - 1] ∈ firstn(n - 1;A))))
22. z : ConsensusState@i
23. (λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi ) = z ∈ ConsensusState@i
24. (A[n - 1] ∈ ws)
25. Z : {a:Id| (a ∈ A)}  ⟶ (ℤ × j:ℤ fp-> V)@i
26. (λb.if b = A[n - 1] ∧b tt then <i, Estimate(z;b) ⊕ i : v> else z b fi ) = Z ∈ ConsensusState@i
27. (A[n - 1] ∈ ws)
28. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = A[n - 1] ∈ Id)) ⇒ ((Inning(Z;b) = Inning(z;b) ∈ ℤ) ∧ (Estimate(Z;b) = Estimate(z;b) ∈ i:ℤ fp-> V)))
29. <i, Estimate(z;A[n - 1]) ⊕ i : v> = (Z A[n - 1]) ∈ (ℤ × j:ℤ fp-> V)
30. i = Inning(z;A[n - 1]) ∈ ℤ
31. ¬(Inning(z;A[n - 1]) ∈ fpf-domain(Estimate(z;A[n - 1])))
32. w1 : {a:Id| (a ∈ A)}  List
33. (w1 ∈ W)
34. ∀b:{a:Id| (a ∈ A)} . ((b ∈ w1) ⇒ (i ≤ Inning(x;b)))
35. ∀ws':{a:Id| (a ∈ A)}  List. ((ws' ∈ W) ⇒ (¬in state x, ws' blocks w1 from archiving v in inning i))
36. ws@0 : {a:Id| (a ∈ A)}  List
37. (ws@0 ∈ W)
38. ∀a:Id. ((a ∈ A) ∈ Type)
39. b : Id@i
40. (b ∈ A)@i
41. (b ∈ ws@0)
⊢ λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi  ∈ ConsensusState

2
.....wf..... 
1. V : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)}  List@i
10. (ws ∈ W)@i
11. 0 < ||ws||
12. i : ℤ
13. x : ConsensusState
14. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ ((Inning(x;a) = i ∈ ℤ) ∧ (¬(i ∈ fpf-domain(Estimate(x;a))))))
15. v : V
16. state x may consider v in inning i
17. n : ℤ@i
18. ¬(A[n - 1] ∈ firstn(n - 1;A))
19. 0 < n@i
20. x ((λx,y. CR(in ws)[x, y] )^*) (λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi )@\000Ci
21. n - 1 < ||A|| c∧ ((A[n - 1] ∈ ws) ∧ (¬(A[n - 1] ∈ firstn(n - 1;A))))
22. z : ConsensusState@i
23. (λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi ) = z ∈ ConsensusState@i
24. (A[n - 1] ∈ ws)
25. Z : {a:Id| (a ∈ A)}  ⟶ (ℤ × j:ℤ fp-> V)@i
26. (λb.if b = A[n - 1] ∧b tt then <i, Estimate(z;b) ⊕ i : v> else z b fi ) = Z ∈ ConsensusState@i
27. (A[n - 1] ∈ ws)
28. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = A[n - 1] ∈ Id)) ⇒ ((Inning(Z;b) = Inning(z;b) ∈ ℤ) ∧ (Estimate(Z;b) = Estimate(z;b) ∈ i:ℤ fp-> V)))
29. <i, Estimate(z;A[n - 1]) ⊕ i : v> = (Z A[n - 1]) ∈ (ℤ × j:ℤ fp-> V)
30. i = Inning(z;A[n - 1]) ∈ ℤ
31. ¬(Inning(z;A[n - 1]) ∈ fpf-domain(Estimate(z;A[n - 1])))
32. w1 : {a:Id| (a ∈ A)}  List
33. (w1 ∈ W)
34. ∀b:{a:Id| (a ∈ A)} . ((b ∈ w1) ⇒ (i ≤ Inning(x;b)))
35. ∀ws':{a:Id| (a ∈ A)}  List. ((ws' ∈ W) ⇒ (¬in state x, ws' blocks w1 from archiving v in inning i))
36. ws@0 : {a:Id| (a ∈ A)}  List
37. (ws@0 ∈ W)
38. ∀a:Id. ((a ∈ A) ∈ Type)
39. b : Id@i
40. (b ∈ A)@i
41. (b ∈ ws@0)
⊢ ConsensusState ∈ Type

3
1. V : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)}  List@i
10. (ws ∈ W)@i
11. 0 < ||ws||
12. i : ℤ
13. x : ConsensusState
14. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ ((Inning(x;a) = i ∈ ℤ) ∧ (¬(i ∈ fpf-domain(Estimate(x;a))))))
15. v : V
16. state x may consider v in inning i
17. n : ℤ@i
18. ¬(A[n - 1] ∈ firstn(n - 1;A))
19. 0 < n@i
20. x ((λx,y. CR(in ws)[x, y] )^*) (λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi )@\000Ci
21. n - 1 < ||A|| c∧ ((A[n - 1] ∈ ws) ∧ (¬(A[n - 1] ∈ firstn(n - 1;A))))
22. z : ConsensusState@i
23. (λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi ) = z ∈ ConsensusState@i
24. (A[n - 1] ∈ ws)
25. Z : {a:Id| (a ∈ A)}  ⟶ (ℤ × j:ℤ fp-> V)@i
26. (λb.if b = A[n - 1] ∧b tt then <i, Estimate(z;b) ⊕ i : v> else z b fi ) = Z ∈ ConsensusState@i
27. (A[n - 1] ∈ ws)
28. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = A[n - 1] ∈ Id)) ⇒ ((Inning(Z;b) = Inning(z;b) ∈ ℤ) ∧ (Estimate(Z;b) = Estimate(z;b) ∈ i:ℤ fp-> V)))
29. <i, Estimate(z;A[n - 1]) ⊕ i : v> = (Z A[n - 1]) ∈ (ℤ × j:ℤ fp-> V)
30. i = Inning(z;A[n - 1]) ∈ ℤ
31. ¬(Inning(z;A[n - 1]) ∈ fpf-domain(Estimate(z;A[n - 1])))
32. w1 : {a:Id| (a ∈ A)}  List
33. (w1 ∈ W)
34. ∀b:{a:Id| (a ∈ A)} . ((b ∈ w1) ⇒ (i ≤ Inning(x;b)))
35. ∀ws':{a:Id| (a ∈ A)}  List. ((ws' ∈ W) ⇒ (¬in state x, ws' blocks w1 from archiving v in inning i))
36. ws@0 : {a:Id| (a ∈ A)}  List
37. (ws@0 ∈ W)
38. ∀a:Id. ((a ∈ A) ∈ Type)
39. b : Id@i
40. (b ∈ A)@i
41. (b ∈ ws@0)
42. v1 : ConsensusState@i
43. (λa.if a ∈b firstn(n - 1;A) ∧b a ∈b ws then <i, Estimate(x;a) ⊕ i : v> else x a fi ) = v1 ∈ ConsensusState@i
⊢ Inning(v1;b) ∈ ℤ

---

Latex:

---

Latex:

1.  V  :  Type
2.  \mforall{}v1,v2:V.    Dec(v1  =  v2)@i
3.  \{\mexists{}v,v':V.  (\mneg{}(v  =  v'))\}@i
4.  A  :  Id  List@i
5.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
6.  three-intersection(A;W)@i
7.  two-intersection(A;W)
8.  one-intersection(A;W)
9.  ws  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
10.  (ws  \mmember{}  W)@i
11.  0  <  ||ws||
12.  i  :  \mBbbZ{}
13.  x  :  ConsensusState
14.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  ((a  \mmember{}  ws)  {}\mRightarrow{}  ((Inning(x;a)  =  i)  \mwedge{}  (\mneg{}(i  \mmember{}  fpf-domain(Estimate(x;a))))))
15.  v  :  V
16.  state  x  may  consider  v  in  inning  i
17.  n  :  \mBbbZ{}@i
18.  \mneg{}(A[n  -  1]  \mmember{}  firstn(n  -  1;A))
19.  0  <  n@i
20.  x 
        rel\_star(ConsensusState;  \mlambda{}x,y.  CR(in  ws)[x,  y]  ) 
        (\mlambda{}a.if  a  \mmember{}\msubb{}  firstn(n  -  1;A)  \mwedge{}\msubb{}  a  \mmember{}\msubb{}  ws  then  <i,  Estimate(x;a)  \moplus{}  i  :  v>  else  x  a  fi  )@i
21.  n  -  1  <  ||A||  c\mwedge{}  ((A[n  -  1]  \mmember{}  ws)  \mwedge{}  (\mneg{}(A[n  -  1]  \mmember{}  firstn(n  -  1;A))))
22.  z  :  ConsensusState@i
23.  (\mlambda{}a.if  a  \mmember{}\msubb{}  firstn(n  -  1;A)  \mwedge{}\msubb{}  a  \mmember{}\msubb{}  ws  then  <i,  Estimate(x;a)  \moplus{}  i  :  v>  else  x  a  fi  )  =  z@i
24.  (A[n  -  1]  \mmember{}  ws)
25.  Z  :  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  j:\mBbbZ{}  fp->  V)@i
26.  (\mlambda{}b.if  b  =  A[n  -  1]  \mwedge{}\msubb{}  tt  then  <i,  Estimate(z;b)  \moplus{}  i  :  v>  else  z  b  fi  )  =  Z@i
27.  (A[n  -  1]  \mmember{}  ws)
28.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\} 
            ((\mneg{}(b  =  A[n  -  1]))  {}\mRightarrow{}  ((Inning(Z;b)  =  Inning(z;b))  \mwedge{}  (Estimate(Z;b)  =  Estimate(z;b))))
29.  <i,  Estimate(z;A[n  -  1])  \moplus{}  i  :  v>  =  (Z  A[n  -  1])
30.  i  =  Inning(z;A[n  -  1])
31.  \mneg{}(Inning(z;A[n  -  1])  \mmember{}  fpf-domain(Estimate(z;A[n  -  1])))
32.  w1  :  \{a:Id|  (a  \mmember{}  A)\}    List
33.  (w1  \mmember{}  W)
34.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  ((b  \mmember{}  w1)  {}\mRightarrow{}  (i  \mleq{}  Inning(x;b)))
35.  \mforall{}ws':\{a:Id|  (a  \mmember{}  A)\}    List
            ((ws'  \mmember{}  W)  {}\mRightarrow{}  (\mneg{}in  state  x,  ws'  blocks  w1  from  archiving  v  in  inning  i))
36.  ws@0  :  \{a:Id|  (a  \mmember{}  A)\}    List
37.  (ws@0  \mmember{}  W)
38.  \mforall{}a:Id.  ((a  \mmember{}  A)  \mmember{}  Type)
39.  b  :  Id@i
40.  (b  \mmember{}  A)@i
41.  (b  \mmember{}  ws@0)
\mvdash{}  Inning(\mlambda{}a.if  a  \mmember{}\msubb{}  firstn(n  -  1;A)  \mwedge{}\msubb{}  a  \mmember{}\msubb{}  ws  then  <i,  Estimate(x;a)  \moplus{}  i  :  v>  else  x  a  fi  ;b)  \mmember{}  \mBbbZ{}


By

---

Latex:
GenConclAtAddrType  \mkleeneopen{}ConsensusState\mkleeneclose{}  [2;1]\mcdot{}

---

Home Index