---

Step * 2 1 1 1 1 1 2 1 of Lemma consensus-refinement5


1. V : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
6. x : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
7. y : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
8. a : {a:Id| (a ∈ A)} @i
9. e : consensus-event(V;A)@i
10. ∀v:V
      ((e = Archive(v) ∈ consensus-event(V;A))
      ⇒ let i,est,knw = consensus-accum-state(A;x a) in 
         (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw))@i
11. ∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
      ((e = consensus-message(b;i;z) ∈ consensus-event(V;A))
      ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
         (i ≤ i')
         ∧ case z
            of inl(p) =>
            let j,v = p 
            in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (j < k ⇒ k < i ⇒ (¬↑k ∈ dom(est)))) ∧ (v = est(j) ∈ V)
            | inr(a) =>
            ∀j:ℤ. (j < i ⇒ (¬↑j ∈ dom(est))))@i
12. ∀b:{a:Id| (a ∈ A)} . ((¬(b = a ∈ Id)) ⇒ ((y b) = (x b) ∈ (consensus-event(V;A) List)))@i
13. (y a) = ((x a) @ [e]) ∈ (consensus-event(V;A) List)@i
14. x ∈ ts-reachable(consensus-ts6(V;A;W))
15. y ∈ ts-reachable(consensus-ts6(V;A;W))
16. b : {a:Id| (a ∈ A)} 
17. i : ℕ
18. y1 : Unit
19. e = consensus-message(b;i;inr y1 ) ∈ consensus-event(V;A)
20. X1 : ℤ@i
21. X3 : j:ℤ fp-> V@i
22. X4 : b:Id fp-> ℤ × (ℤ × V + Top)@i
23. consensus-accum-state(A;x a) = <X1, X3, X4> ∈ (ℤ × j:ℤ fp-> V × b:Id fp-> ℤ × (ℤ × V + Top))@i
24. Y1 : ℤ@i
25. Y3 : j:ℤ fp-> V@i
26. Y4 : b:Id fp-> ℤ × (ℤ × V + Top)@i
27. X1 = Y1 ∈ ℤ
28. X3 = Y3 ∈ j:ℤ fp-> V
29. b : <i, inr y1 > ⊕ X4 = Y4 ∈ b:Id fp-> ℤ × (ℤ × V + Top)
30. Y1 = X1 ∈ ℤ
31. Y3 = X3 ∈ i:ℤ fp-> V
32. Z1 : ℤ@i
33. Z3 : j:ℤ fp-> V@i
34. Z4 : b:Id fp-> ℤ × (ℤ × V + Top)@i
35. consensus-accum-state(A;x b) = <Z1, Z3, Z4> ∈ (ℤ × j:ℤ fp-> V × b:Id fp-> ℤ × (ℤ × V + Top))@i
36. i ≤ Z1@i
37. ∀j:ℤ. (j < i ⇒ (¬↑j ∈ dom(Z3)))@i
38. i ≤ Z1
39. ∀j:ℤ. (j < i ⇒ (¬↑j ∈ dom(Z3)))
⊢ Y4 = b : <i, inr ⋅ > ⊕ X4 ∈ b:Id fp-> ℤ × (ℤ × V + Top)
BY
{ (DVar `y1' THEN All (Fold `it`) THEN Auto) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
4.  1  <  ||W||@i
5.  two-intersection(A;W)@i
6.  x  :  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-event(V;A)  List)@i
7.  y  :  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-event(V;A)  List)@i
8.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
9.  e  :  consensus-event(V;A)@i
10.  \mforall{}v:V
            ((e  =  Archive(v))
            {}\mRightarrow{}  let  i,est,knw  =  consensus-accum-state(A;x  a)  in 
                  (\mneg{}(i  \mmember{}  fpf-domain(est)))  \mwedge{}  may  consider  v  in  inning  i  based  on  knowledge  (knw))@i
11.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbN{}.  \mforall{}z:\mBbbN{}i  \mtimes{}  V?.
            ((e  =  consensus-message(b;i;z))
            {}\mRightarrow{}  let  i',est,knw  =  consensus-accum-state(A;x  b)  in 
                  (i  \mleq{}  i')
                  \mwedge{}  case  z
                        of  inl(p)  =>
                        let  j,v  =  p 
                        in  (\muparrow{}j  \mmember{}  dom(est))  \mwedge{}  (\mforall{}k:\mBbbZ{}.  (j  <  k  {}\mRightarrow{}  k  <  i  {}\mRightarrow{}  (\mneg{}\muparrow{}k  \mmember{}  dom(est))))  \mwedge{}  (v  =  est(j))
                        |  inr(a)  =>
                        \mforall{}j:\mBbbZ{}.  (j  <  i  {}\mRightarrow{}  (\mneg{}\muparrow{}j  \mmember{}  dom(est))))@i
12.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  ((\mneg{}(b  =  a))  {}\mRightarrow{}  ((y  b)  =  (x  b)))@i
13.  (y  a)  =  ((x  a)  @  [e])@i
14.  x  \mmember{}  ts-reachable(consensus-ts6(V;A;W))
15.  y  \mmember{}  ts-reachable(consensus-ts6(V;A;W))
16.  b  :  \{a:Id|  (a  \mmember{}  A)\} 
17.  i  :  \mBbbN{}
18.  y1  :  Unit
19.  e  =  consensus-message(b;i;inr  y1  )
20.  X1  :  \mBbbZ{}@i
21.  X3  :  j:\mBbbZ{}  fp->  V@i
22.  X4  :  b:Id  fp->  \mBbbZ{}  \mtimes{}  (\mBbbZ{}  \mtimes{}  V  +  Top)@i
23.  consensus-accum-state(A;x  a)  =  <X1,  X3,  X4>@i
24.  Y1  :  \mBbbZ{}@i
25.  Y3  :  j:\mBbbZ{}  fp->  V@i
26.  Y4  :  b:Id  fp->  \mBbbZ{}  \mtimes{}  (\mBbbZ{}  \mtimes{}  V  +  Top)@i
27.  X1  =  Y1
28.  X3  =  Y3
29.  b  :  <i,  inr  y1  >  \moplus{}  X4  =  Y4
30.  Y1  =  X1
31.  Y3  =  X3
32.  Z1  :  \mBbbZ{}@i
33.  Z3  :  j:\mBbbZ{}  fp->  V@i
34.  Z4  :  b:Id  fp->  \mBbbZ{}  \mtimes{}  (\mBbbZ{}  \mtimes{}  V  +  Top)@i
35.  consensus-accum-state(A;x  b)  =  <Z1,  Z3,  Z4>@i
36.  i  \mleq{}  Z1@i
37.  \mforall{}j:\mBbbZ{}.  (j  <  i  {}\mRightarrow{}  (\mneg{}\muparrow{}j  \mmember{}  dom(Z3)))@i
38.  i  \mleq{}  Z1
39.  \mforall{}j:\mBbbZ{}.  (j  <  i  {}\mRightarrow{}  (\mneg{}\muparrow{}j  \mmember{}  dom(Z3)))
\mvdash{}  Y4  =  b  :  <i,  inr  \mcdot{}  >  \moplus{}  X4


By

(DVar  `y1'  THEN  All  (Fold  `it`)  THEN  Auto)

---

Home Index