---

Step * 1 of Lemma pv11_p1_pmax_desc_implies


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))))
BY
{ (InstConcl [⌈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>)⌉]⋅
   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
⊢ (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>) ∈ pvals)

2
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
8. (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>) ∈ pvals)
⊢ ↑let bn,z = 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>) 
   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

3
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
8. (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>) ∈ pvals)
9. ↑let bn,z = 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>) 
    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
⊢ <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(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>)))
∈ (ℤ × Cmd)

---

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.  b  :  pv11\_p1\_Ballot\_Num()@i
5.  s  :  \mBbbZ{}@i
6.  c  :  Cmd@i
7.  (<b,  s,  c>  \mmember{}  pvals)@i
\mvdash{}  \mexists{}y:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd
      ((y  \mmember{}  pvals)
      \mwedge{}  ((\muparrow{}let  bn,z  =  y 
                in  let  s,c  =  z 
                      in  \mneg{}\msubb{}(\mexists{}zw\mmember{}pvals.let  bn',z  =  zw 
                                                      in  let  s',z  =  z 
                                                            in  (s  =\msubz{}  s')  \mwedge{}\msubb{}  (bn    <  bn'))\_b)
          c\mwedge{}  (<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  =\msubz{}  s')  then  if  pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b'  b  the\000Cn  a  else  x  fi    else  a  fi 
                                      over  list:
                                          pvals
                                      with  starting  value:
                                        <b,  s,  c>)))
                  >
                =  (snd(y)))))


By

---

Latex:
(InstConcl  [\mkleeneopen{}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  el\000Cse  x  fi    else  a  fi 
                          over  list:
                              pvals
                          with  starting  value:
                            <b,  s,  c>)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  )

---

Home Index