---

Step * of Lemma pv11_p1_pmax_desc_implies

∀Cmd:ValueAllType. ∀ldrs_uid:Id ─→ ℤ. ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ.
∀c:Cmd.
  ((<b, s, c> ∈ pvals) ⇒ (∃c':Cmd. (<s, c'> ∈ pv11_p1_pmax(Cmd;ldrs_uid) pvals)))
BY
{ ((Unfold `vatype` 0 THEN Auto)
   THEN (InstConcl [⌈snd(snd(accumulate (with value a and list item x):
                              let b,s,c = a in 
                              let b',s',c' = x in 
                              if (s =z s') then if pv11_p1_leq_bnum(ldrs_uid) b' b then a else x fi  else a fi 
                             over list:
                               pvals
                             with starting value:
                              <b, s, c>)))⌉]⋅
         THENA Auto
         )
   THEN RepeatFor 2 ((GenListD 0 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. b : pv11_p1_Ballot_Num()@i
5. s : ℤ@i
6. c : Cmd@i
7. (<b, s, c> ∈ pvals)@i
⊢ ∃y:pv11_p1_Ballot_Num() × ℤ × Cmd
   ((y ∈ pvals)
   ∧ ((↑let bn,z = y 
        in let s,c = z 
           in ¬b(∃zw∈pvals.let bn',z = zw 
                           in let s',z = z 
                              in (s =z s') ∧b (bn  < bn'))_b)
     c∧ (<s
         , snd(snd(accumulate (with value a and list item x):
                    let b,s,c = a in 
                    let b',s',c' = x in 
                    if (s =z s') then if pv11_p1_leq_bnum(ldrs_uid) b' b then a else x fi  else a fi 
                   over list:
                     pvals
                   with starting value:
                    <b, s, c>)))
         >
        = (snd(y))
        ∈ (ℤ × Cmd))))

---

Latex:

---

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


By

---

Latex:
((Unfold  `vatype`  0  THEN  Auto)
  THEN  (InstConcl  [\mkleeneopen{}snd(snd(accumulate  (with  value  a  and  list  item  x):
                                                        let  b,s,c  =  a  in 
                                                        let  b',s',c'  =  x  in 
                                                        if  (s  =\msubz{}  s')
                                                        then  if  pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b'  b  then  a  e\000Clse  x  fi 
                                                        else  a
                                                        fi 
                                                      over  list:
                                                          pvals
                                                      with  starting  value:
                                                        <b,  s,  c>)))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RepeatFor  2  ((GenListD  0  THEN  Auto)))

---

Home Index