---

Step * 1 3 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
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)
BY
{ ((InstLemma `list_accum_invariant2` [⌈pv11_p1_Ballot_Num() × ℤ × Cmd⌉;⌈⌈pv11_p1_Ballot_Num() × ℤ × Cmd⌉⌉;
    ⌈λa,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 ⌉;⌈λx.(<s, snd(snd(x))>
                                                                                             = (snd(x))
                                                                                             ∈ (ℤ × Cmd))⌉;⌈pvals⌉;
    ⌈<b, s, c>⌉]⋅
    THENA Auto
    )
   THEN All (RepUR ``so_apply``)
   THEN Auto
   THEN (DVar `a' THEN DVar `a2' THEN DVar `x' THEN DVar `x2')
   THEN All Reduce
   THEN RepeatFor 2 (AutoSplit))⋅ }

---

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
8.  (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  else  x  fi    \000Celse  a  fi 
        over  list:
            pvals
        with  starting  value:
          <b,  s,  c>)  \mmember{}  pvals)
9.  \muparrow{}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  =\msubz{}  s')  then  if  pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b'  b  then  a  \000Celse  x  fi    else  a  fi 
                              over  list:
                                  pvals
                              with  starting  value:
                                <b,  s,  c>) 
        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
\mvdash{}  <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  then  a  els\000Ce  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  =\msubz{}  s')  then  if  pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b'  b  then  a  else  x  f\000Ci    else  a  fi 
              over  list:
                  pvals
              with  starting  value:
                <b,  s,  c>)))


By

---

Latex:
((InstLemma  `list\_accum\_invariant2`  [\mkleeneopen{}pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd\mkleeneclose{};\mkleeneopen{}\mkleeneopen{}pv11\_p1\_Ballot\_Num()
                                                                                                                                                \mtimes{}  \mBbbZ{}
                                                                                                                                                \mtimes{}  Cmd\mkleeneclose{}\mkleeneclose{};
    \mkleeneopen{}\mlambda{}a,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  else  x  f\000Ci    else  a  fi  \mkleeneclose{};
    \mkleeneopen{}\mlambda{}x.(<s,  snd(snd(x))>  =  (snd(x)))\mkleeneclose{};\mkleeneopen{}pvals\mkleeneclose{};\mkleeneopen{}<b,  s,  c>\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto
  THEN  (DVar  `a'  THEN  DVar  `a2'  THEN  DVar  `x'  THEN  DVar  `x2')
  THEN  All  Reduce
  THEN  RepeatFor  2  (AutoSplit))\mcdot{}

---

Home Index