---

Step * of Lemma pv11_p1_pmax_desc

∀Cmd:ValueAllType. ∀ldrs_uid:Id ─→ ℤ. ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ pv11_p1_pmax(Cmd;ldrs_uid) pvals)
  ⇒ (∃b:pv11_p1_Ballot_Num()
       ((<b, s, c> ∈ pvals)
       ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.  ((<b', s, c'> ∈ pvals) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b)))))))
BY
{ (Unfold `vatype` 0
   THEN Auto
   THEN RepeatFor 2 (GenListD (-1))
   THEN ExRepD
   THEN (DVar `y' THEN DVar `y2')
   THEN All Reduce
   THEN AllPushDown
   THEN (InstConcl [⌈y1⌉]⋅
         THEN Auto
         THEN SupposeNot
         THEN D (10)
         THEN (RWO "l_exists_iff" 0 THENA Auto)
         THEN InstConcl [⌈<b', s, c'>⌉]⋅
         THEN Auto)⋅) }

1
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')

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}pvals:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd\000C)  List.  \mforall{}s:\mBbbZ{}.  \mforall{}c:Cmd.
    ((<s,  c>  \mmember{}  pv11\_p1\_pmax(Cmd;ldrs$_{uid}$)  pvals)
    {}\mRightarrow{}  (\mexists{}b:pv11\_p1\_Ballot\_Num()
              ((<b,  s,  c>  \mmember{}  pvals)
              \mwedge{}  (\mforall{}b':pv11\_p1\_Ballot\_Num().  \mforall{}c':Cmd.
                        ((<b',  s,  c'>  \mmember{}  pvals)  {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b'  b))))\000C)))


By

---

Latex:
(Unfold  `vatype`  0
  THEN  Auto
  THEN  RepeatFor  2  (GenListD  (-1))
  THEN  ExRepD
  THEN  (DVar  `y'  THEN  DVar  `y2')
  THEN  All  Reduce
  THEN  AllPushDown
  THEN  (InstConcl  [\mkleeneopen{}y1\mkleeneclose{}]\mcdot{}
              THEN  Auto
              THEN  SupposeNot
              THEN  D  (10)
              THEN  (RWO  "l\_exists\_iff"  0  THENA  Auto)
              THEN  InstConcl  [\mkleeneopen{}<b',  s,  c'>\mkleeneclose{}]\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index