---

Step * 1 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 : {b:Id| (b ∈ A)} @i
6. v : V@i
⊢ (<b, v> ∈ mapfilter(λr.let a,j,v = rcvd-vote(r) in <a, v>;λr.inning(r) =z i;L)) ⇐⇒ (Vote[b;i;v] ∈ L)
BY
{ (RWO "member-mapfilter" 0
   THEN Reduce 0
   THEN Auto
   THEN AllHyps h.(DSet h THEN Reduce (h+1)) 
   THEN Reduce 0
   THEN Auto
   THEN Try ((D -2
              THEN RepUR ``rcvd-inning-eq rcv-vote?`` -1
              THEN Auto
              THEN RepeatFor 2 (D -2)
              THEN All (RepUR ``rcvd-vote``)
              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. ∃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))))@i
⊢ (Vote[b;i;v] ∈ L)

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. \\%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))))

3
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. -any : (<b, v> ∈ mapfilter(λr.let a,j,v = rcvd-vote(r) in <a, v>;λr.inning(r) =z i;L))@i
9. ∀x:consensus-rcv(V;A). ((x ∈ L) c∧ (↑inning(x) =z i) ∈ Type)
10. r : consensus-rcv(V;A)@i
11. (r ∈ L) c∧ (↑inning(r) =z i)@i
⊢ let a,j,v = rcvd-vote(r) in 
  <a, v> ∈ {b:Id| (b ∈ A)}  × V

4
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. -any : (Vote[b;i;v] ∈ L)@i
9. ∃y:consensus-rcv(V;A). ((y ∈ L) ∧ ((↑((λr.inning(r) =z i) y)) c∧ (<b, v> = ((λr.let a,j,v = rcvd-vote(r) in <a, v>) y\000C) ∈ ({b:Id| (b ∈ A)}  × V))))@i
10. ∀x:consensus-rcv(V;A). ((x ∈ L) c∧ (↑inning(x) =z i) ∈ Type)
11. r : consensus-rcv(V;A)@i
12. (r ∈ L) c∧ (↑inning(r) =z i)@i
13. (Vote[b;i;v] ∈ L)@i
⊢ let a,j,v = rcvd-vote(r) 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  :  \{b:Id|  (b  \mmember{}  A)\}  @i
6.  v  :  V@i
\mvdash{}  (<b,  v>  \mmember{}  mapfilter(\mlambda{}r.let  a,j,v  =  rcvd-vote(r)  in  <a,  v>\mlambda{}r.inning(r)  =\msubz{}  i;L))  \mLeftarrow{}{}\mRightarrow{}  (Vote[b;i;v]  \mmember{}\000C  L)


By

(RWO  "member-mapfilter"  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AllHyps  h.(DSet  h  THEN  Reduce  (h+1)) 
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((D  -2
                        THEN  RepUR  ``rcvd-inning-eq  rcv-vote?``  -1
                        THEN  Auto
                        THEN  RepeatFor  2  (D  -2)
                        THEN  All  (RepUR  ``rcvd-vote``)
                        THEN  Auto)))\mcdot{}

---

Home Index