---

Step * 1 2 of Lemma member-votes-from-inning


1. [V] : Type
2. A : Id List@i
3. L : consensus-rcv(V;A) List@i
4. i : ℕ@i
5. b : Id@i
6. \\%2 : (b ∈ A)@i
7. v : V@i
8. (Vote[b;i;v] ∈ L)@i
⊢ ∃y:consensus-rcv(V;A). ((y ∈ L) ∧ ((↑inning(y) =z i) c∧ (<b, v> = let a,j,v = rcvd-vote(y) in <a, v> ∈ ({b:Id| (b ∈ A)\000C}  × V))))
BY
{ (InstConcl [⌈Vote[b;i;v]⌉]⋅ THEN Auto) }

1
1. [V] : Type
2. A : Id List@i
3. L : consensus-rcv(V;A) List@i
4. i : ℕ@i
5. b : Id@i
6. \\%2 : (b ∈ A)@i
7. v : V@i
8. (Vote[b;i;v] ∈ L)@i
9. (Vote[b;i;v] ∈ L)
⊢ ↑inning(Vote[b;i;v]) =z i

2
1. V : Type
2. A : Id List@i
3. L : consensus-rcv(V;A) List@i
4. i : ℕ@i
5. b : Id@i
6. (b ∈ A)@i
7. v : V@i
8. (Vote[b;i;v] ∈ L)@i
9. y : consensus-rcv(V;A)
10. (y ∈ L)
11. ↑inning(y) =z i
⊢ let a,j,v = rcvd-vote(y) in 
  <a, v> ∈ {b:Id| (b ∈ A)}  × V

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  L  :  consensus-rcv(V;A)  List@i
4.  i  :  \mBbbN{}@i
5.  b  :  Id@i
6.  \mbackslash{}\mbackslash{}\%2  :  (b  \mmember{}  A)@i
7.  v  :  V@i
8.  (Vote[b;i;v]  \mmember{}  L)@i
\mvdash{}  \mexists{}y:consensus-rcv(V;A)
      ((y  \mmember{}  L)  \mwedge{}  ((\muparrow{}inning(y)  =\msubz{}  i)  c\mwedge{}  (<b,  v>  =  let  a,j,v  =  rcvd-vote(y)  in  <a,  v>)))


By

(InstConcl  [\mkleeneopen{}Vote[b;i;v]\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index