---

Step * 1 of Lemma pv11_p1_pmax_desc


1. Cmd : {T:Type| valueall-type(T)} @i'
2. ldrs_uid : Id ─→ ℤ@i
3. pvals : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
4. s : ℤ@i
5. c : Cmd@i
6. y1 : pv11_p1_Ballot_Num()
7. y3 : ℤ
8. y4 : Cmd
9. (<y1, y3, y4> ∈ pvals)
10. <s, c> = <y3, y4> ∈ (ℤ × Cmd)
11. (<y1, s, c> ∈ pvals)
12. b' : pv11_p1_Ballot_Num()@i
13. c' : Cmd@i
14. (<b', s, c'> ∈ pvals)@i
15. ¬↑(pv11_p1_leq_bnum(ldrs_uid) b' y1)
16. (<b', s, c'> ∈ pvals)
17. y3 = s ∈ ℤ
⊢ ↑(y1  < b')
BY
{ (MoveToConcl (-3) THEN All Thin) }

1
1. ldrs_uid : Id ─→ ℤ@i
2. y1 : pv11_p1_Ballot_Num()
3. b' : pv11_p1_Ballot_Num()@i
⊢ (¬↑(pv11_p1_leq_bnum(ldrs_uid) b' y1)) ⇒ (↑(y1  < b'))

---

Latex:

---

Latex:

1.  Cmd  :  \{T:Type|  valueall-type(T)\}  @i'
2.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
3.  pvals  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
4.  s  :  \mBbbZ{}@i
5.  c  :  Cmd@i
6.  y1  :  pv11\_p1\_Ballot\_Num()
7.  y3  :  \mBbbZ{}
8.  y4  :  Cmd
9.  (<y1,  y3,  y4>  \mmember{}  pvals)
10.  <s,  c>  =  <y3,  y4>
11.  (<y1,  s,  c>  \mmember{}  pvals)
12.  b'  :  pv11\_p1\_Ballot\_Num()@i
13.  c'  :  Cmd@i
14.  (<b',  s,  c'>  \mmember{}  pvals)@i
15.  \mneg{}\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b'  y1)
16.  (<b',  s,  c'>  \mmember{}  pvals)
17.  y3  =  s
\mvdash{}  \muparrow{}(y1    <  b')


By

---

Latex:
(MoveToConcl  (-3)  THEN  All  Thin)

---

Home Index