---

Step * 1 2 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
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
BY
{ Assert ⌈(∃zw∈L'.let bn',z = zw in let s',z = z in (a3 =z s') ∧b (a1  < bn'))_b = ff⌉⋅ }

1
.....assertion..... 
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
⊢ (∃zw∈L'.let bn',z = zw in let s',z = z in (a3 =z s') ∧b (a1  < bn'))_b = ff

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)
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
18. (∃zw∈L'.let bn',z = zw in let s',z = z in (a3 =z s') ∧b (a1  < bn'))_b = ff
⊢ ↑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.  a1  :  pv11\_p1\_Ballot\_Num()@i
10.  a3  :  \mBbbZ{}@i
11.  a4  :  Cmd@i
12.  x1  :  pv11\_p1\_Ballot\_Num()@i
13.  x3  :  \mBbbZ{}@i
14.  x4  :  Cmd@i
15.  L'  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
16.  L'  @  [<x1,  x3,  x4>]  \mleq{}  pvals@i
17.  \muparrow{}\mneg{}\msubb{}(\mexists{}zw\mmember{}L'.let  bn',z  =  zw 
                              in  let  s',z  =  z 
                                    in  (a3  =\msubz{}  s')  \mwedge{}\msubb{}  (a1    <  bn'))\_b@18
\mvdash{}  \muparrow{}let  bn,z  =  if  (a3  =\msubz{}  x3)
      then  if  pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  x1  a1  then  <a1,  a3,  a4>  else  <x1,  x3,  \000Cx4>  fi 
      else  <a1,  a3,  a4>
      fi   
      in  let  s,c  =  z 
            in  \mneg{}\msubb{}(\mexists{}zw\mmember{}L'  @  [<x1,  x3,  x4>].let  bn',z  =  zw 
                                                                      in  let  s',z  =  z 
                                                                            in  (s  =\msubz{}  s')  \mwedge{}\msubb{}  (bn    <  bn'))\_b


By

---

Latex:
Assert  \mkleeneopen{}(\mexists{}zw\mmember{}L'.let  bn',z  =  zw  in  let  s',z  =  z  in  (a3  =\msubz{}  s')  \mwedge{}\msubb{}  (a1    <  bn'))\_b  =  ff\mkleeneclose{}\mcdot{}

---

Home Index