---

Step * 1 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
⊢ (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)
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.(x ∈ pvals)⌉;⌈pvals⌉;⌈<\000Cb
                                                                                                                   , s
                                                                                                                   , c>⌉
    ]⋅
    THENA Auto
    )
   THEN All (RepUR ``so_apply``)⋅
   THEN Auto
   THEN (DVar `a' THEN DVar `a2' THEN DVar `x' THEN DVar `x2')
   THEN Reduce 0
   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
\mvdash{}  (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    e\000Clse  a  fi 
      over  list:
          pvals
      with  starting  value:
        <b,  s,  c>)  \mmember{}  pvals)


By

---

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

---

Home Index