---

Step * 1 2 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)
⊢ ↑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
BY
{ ((InstLemma `list_accum_invariant3` [⌈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,L. (↑let bn,z = x in let s,c = z in ¬b(∃zw∈L.let bn',z = zw in let s',z = z in (s =z s') ∧b (bn  < bn'))_b)⌉;⌈pv\000Cals⌉
    ;⌈<b, s, c>⌉]⋅
    THENA Auto
    )
   THEN All (RepUR ``so_apply``)
   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
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. a : pv11_p1_Ballot_Num() × ℤ × Cmd@i
10. x : pv11_p1_Ballot_Num() × ℤ × Cmd@i
11. L' : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
12. L' @ [x] ≤ pvals@i
13. ↑let bn,z = a 
     in let s,c = z 
        in ¬b(∃zw∈L'.let bn',z = zw 
                     in let s',z = z 
                        in (s =z s') ∧b (bn  < bn'))_b@18
⊢ ↑let bn,z = 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  
   in let s,c = z 
      in ¬b(∃zw∈L' @ [x].let bn',z = zw 
                         in let s',z = z 
                            in (s =z s') ∧b (bn  < bn'))_b

---

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)
\mvdash{}  \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  e\000Clse  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


By

---

Latex:
((InstLemma  `list\_accum\_invariant3`  [\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,L.  (\muparrow{}let  bn,z  =  x 
                      in  let  s,c  =  z 
                            in  \mneg{}\msubb{}(\mexists{}zw\mmember{}L.let  bn',z  =  zw 
                                                    in  let  s',z  =  z 
                                                          in  (s  =\msubz{}  s')  \mwedge{}\msubb{}  (bn    <  bn'))\_b)\mkleeneclose{};\mkleeneopen{}pvals\mkleeneclose{};\mkleeneopen{}<b,  s,  c>\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto)

---

Home Index