---

Step * 1 2 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
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
BY
{ (DVar `a' THEN DVar `a2' THEN DVar `x' THEN DVar `x2' THEN All Reduce) }

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. a1 : pv11_p1_Ballot_Num()@i
10. a3 : ℤ@i
11. a4 : Cmd@i
12. x1 : pv11_p1_Ballot_Num()@i
13. x3 : ℤ@i
14. x4 : Cmd@i
15. L' : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
16. L' @ [<x1, x3, x4>] ≤ pvals@i
17. ↑¬b(∃zw∈L'.let bn',z = zw 
               in let s',z = z 
                  in (a3 =z s') ∧b (a1  < bn'))_b@18
⊢ ↑let bn,z = if (a3 =z x3)
   then if pv11_p1_leq_bnum(ldrs_uid) x1 a1 then <a1, a3, a4> else <x1, x3, x4> fi 
   else <a1, a3, a4>
   fi  
   in let s,c = z 
      in ¬b(∃zw∈L' @ [<x1, x3, x4>].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)
9.  a  :  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd@i
10.  x  :  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd@i
11.  L'  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
12.  L'  @  [x]  \mleq{}  pvals@i
13.  \muparrow{}let  bn,z  =  a 
          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@18
\mvdash{}  \muparrow{}let  bn,z  =  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    el\000Cse  a  fi   
      in  let  s,c  =  z 
            in  \mneg{}\msubb{}(\mexists{}zw\mmember{}L'  @  [x].let  bn',z  =  zw 
                                                  in  let  s',z  =  z 
                                                        in  (s  =\msubz{}  s')  \mwedge{}\msubb{}  (bn    <  bn'))\_b


By

---

Latex:
(DVar  `a'  THEN  DVar  `a2'  THEN  DVar  `x'  THEN  DVar  `x2'  THEN  All  Reduce)

---

Home Index