---

Step * 2 1 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. z : ℕi × V?
19. e = consensus-message(b;i;z) ∈ 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, z> ⊕ X4 = Y4 ∈ b:Id fp-> ℤ × (ℤ × V + Top)
30. Y1 = X1 ∈ ℤ
31. Y3 = X3 ∈ i:ℤ fp-> V
⊢ ∃b:{a:Id| (a ∈ A)} 
   ∃i:ℤ
    ((i ≤ (fst(let i,est,knw = consensus-accum-state(A;x b) in 
      <i, est>)))
    ∧ (((∀j:ℤ. (j < i ⇒ (¬↑j ∈ dom(snd(let i,est,knw = consensus-accum-state(A;x b) in <i, est>))))) ∧ (Y4 = b : <i, in\000Cr ⋅ > ⊕ X4 ∈ b:Id fp-> ℤ × (ℤ × V + Top)))
      ∨ (∃j:ℤ
          (j < i
          ∧ (↑j ∈ dom(snd(let i,est,knw = consensus-accum-state(A;x b) in 
            <i, est>)))
          ∧ (∀k:ℤ. (j < k ⇒ k < i ⇒ (¬↑k ∈ dom(snd(let i,est,knw = consensus-accum-state(A;x b) in <i, est>)))))
          ∧ (Y4 = b : <i, inl <j, snd(let i,est,knw = consensus-accum-state(A;x b) in <i, est>)(j)>> ⊕ X4 ∈ b:Id fp-> ℤ \000C× (ℤ × V + Top))))))
BY
{ AllHyps h.(InstHyp [⌈b⌉;⌈i⌉;⌈z⌉] h⋅ THENA Complete (Auto))  }

1
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. z : ℕi × V?
19. e = consensus-message(b;i;z) ∈ 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, z> ⊕ X4 = Y4 ∈ b:Id fp-> ℤ × (ℤ × V + Top)
30. Y1 = X1 ∈ ℤ
31. Y3 = X3 ∈ i:ℤ fp-> V
32. 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)))
⊢ ∃b:{a:Id| (a ∈ A)} 
   ∃i:ℤ
    ((i ≤ (fst(let i,est,knw = consensus-accum-state(A;x b) in 
      <i, est>)))
    ∧ (((∀j:ℤ. (j < i ⇒ (¬↑j ∈ dom(snd(let i,est,knw = consensus-accum-state(A;x b) in <i, est>))))) ∧ (Y4 = b : <i, in\000Cr ⋅ > ⊕ X4 ∈ b:Id fp-> ℤ × (ℤ × V + Top)))
      ∨ (∃j:ℤ
          (j < i
          ∧ (↑j ∈ dom(snd(let i,est,knw = consensus-accum-state(A;x b) in 
            <i, est>)))
          ∧ (∀k:ℤ. (j < k ⇒ k < i ⇒ (¬↑k ∈ dom(snd(let i,est,knw = consensus-accum-state(A;x b) in <i, est>)))))
          ∧ (Y4 = b : <i, inl <j, snd(let i,est,knw = consensus-accum-state(A;x b) in <i, est>)(j)>> ⊕ X4 ∈ b:Id fp-> ℤ \000C× (ℤ × V + Top))))))

---

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.  z  :  \mBbbN{}i  \mtimes{}  V?
19.  e  =  consensus-message(b;i;z)
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,  z>  \moplus{}  X4  =  Y4
30.  Y1  =  X1
31.  Y3  =  X3
\mvdash{}  \mexists{}b:\{a:Id|  (a  \mmember{}  A)\} 
      \mexists{}i:\mBbbZ{}
        ((i  \mleq{}  (fst(let  i,est,knw  =  consensus-accum-state(A;x  b)  in 
            <i,  est>)))
        \mwedge{}  (((\mforall{}j:\mBbbZ{}.  (j  <  i  {}\mRightarrow{}  (\mneg{}\muparrow{}j  \mmember{}  dom(snd(let  i,est,knw  =  consensus-accum-state(A;x  b)  in  <i,  est>))))\000C)  \mwedge{}  (Y4  =  b  :  <i,  inr  \mcdot{}  >  \moplus{}  X4))
            \mvee{}  (\mexists{}j:\mBbbZ{}
                    (j  <  i
                    \mwedge{}  (\muparrow{}j  \mmember{}  dom(snd(let  i,est,knw  =  consensus-accum-state(A;x  b)  in 
                        <i,  est>)))
                    \mwedge{}  (\mforall{}k:\mBbbZ{}
                              (j  <  k
                              {}\mRightarrow{}  k  <  i
                              {}\mRightarrow{}  (\mneg{}\muparrow{}k  \mmember{}  dom(snd(let  i,est,knw  =  consensus-accum-state(A;x  b)  in 
                                    <i,  est>)))))
                    \mwedge{}  (Y4  =  b  :  <i,  inl  <j,  snd(let  i,est,knw  =  consensus-accum-state(A;x  b)  in  <i,  est>)(j)>>\000C  \moplus{}  X4)))))


By

AllHyps  h.(InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto)) 

---

Home Index