---

Step * 4 1 2 of Lemma pv11_p1_scout_from_acc


1. Cmd : {T:Type| valueall-type(T)} @i'
2. f : pv11_p1_headers_type{i:l}(Cmd)@i'
3. (f [decision]) = (ℤ × Cmd) ∈ Type
4. (f [propose]) = (ℤ × Cmd) ∈ Type
5. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
6. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
7. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
8. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
9. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
10. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
11. f ∈ Name ─→ Type
12. es : EO+(Message(f))@i'
13. e : E@i
14. accpts : bag(Id)@i
15. s : bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)@i
16. bnum : pv11_p1_Ballot_Num()@i
17. s ∈ State-loc-comb(λloc.{pv11_p1_init_scout(Cmd;accpts)};pv11_p1_on_p1b(Cmd) bnum;pv11_p1_p1b'base(Cmd;f))(e)
18. a1 : Id@i
19. a3 : pv11_p1_Ballot_Num()@i
20. a5 : pv11_p1_Ballot_Num()@i
21. a6 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
22. e' : E@i
23. s2 : bag(Id)@i
24. s3 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
25. e' ≤loc e @i
26. <a1, a3, a5, a6> ∈ pv11_p1_p1b'base(Cmd;f)(e')@i
27. if first(e')
then <s2, s3> ↓∈ {pv11_p1_init_scout(Cmd;accpts)}
else <s2, s3> ∈ State-loc-comb(λloc.{pv11_p1_init_scout(Cmd;accpts)};pv11_p1_on_p1b(Cmd) bnum;pv11_p1_p1b'base(Cmd;f))(
                pred(e'))
fi @i
28. ∀p:pv11_p1_Ballot_Num() × ℤ × Cmd
      ((p ∈ s3)
      ⇒ (∃e':E
           ∃l:Id
            ∃r:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
             (e' ≤loc e  ∧ <l, bnum, bnum, r> ∈ pv11_p1_p1b'base(Cmd;f)(e') ∧ (p ∈ r))))@i
29. bnum = a3 ∈ pv11_p1_Ballot_Num()
30. bnum = a5 ∈ pv11_p1_Ballot_Num()
31. p : pv11_p1_Ballot_Num() × ℤ × Cmd@i
32. (p ∈ accumulate (with value a and list item x):
          if (∃zzc∈a.pv11_p1_same_pvalue(Cmd) x zzc)_b then a else a @ [x] fi 
         over list:
           a6
         with starting value:
          s3))@i
33. (p ∈ a6)
⊢ ∃e':E
   ∃l:Id
    ∃r:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. (e' ≤loc e  ∧ <l, bnum, bnum, r> ∈ pv11_p1_p1b'base(Cmd;f)(e') ∧ (p ∈ r))
BY
{ (InstConcl [⌈e'⌉;⌈a1⌉;⌈a6⌉]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Cmd  :  \{T:Type|  valueall-type(T)\}  @i'
2.  f  :  pv11\_p1\_headers\_type\{i:l\}(Cmd)@i'
3.  (f  [decision])  =  (\mBbbZ{}  \mtimes{}  Cmd)
4.  (f  [propose])  =  (\mBbbZ{}  \mtimes{}  Cmd)
5.  (f  ``pv11\_p1  adopted``)  =  (pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List))
6.  (f  ``pv11\_p1  preempted``)  =  pv11\_p1\_Ballot\_Num()
7.  (f  ``pv11\_p1  p2b``)  =  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  pv11\_p1\_Ballot\_Num())
8.  (f  ``pv11\_p1  p2a``)  =  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
9.  (f  ``pv11\_p1  p1b``)
=  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List))
10.  (f  ``pv11\_p1  p1a``)  =  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num())
11.  f  \mmember{}  Name  {}\mrightarrow{}  Type
12.  es  :  EO+(Message(f))@i'
13.  e  :  E@i
14.  accpts  :  bag(Id)@i
15.  s  :  bag(Id)  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)@i
16.  bnum  :  pv11\_p1\_Ballot\_Num()@i
17.  s  \mmember{}  State-loc-comb(\mlambda{}loc.\{pv11\_p1\_init\_scout(Cmd;accpts)\};pv11\_p1\_on\_p1b(Cmd) 
                                                                                                                          bnum;pv11\_p1\_p1b'base(Cmd;f))(e)
18.  a1  :  Id@i
19.  a3  :  pv11\_p1\_Ballot\_Num()@i
20.  a5  :  pv11\_p1\_Ballot\_Num()@i
21.  a6  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
22.  e'  :  E@i
23.  s2  :  bag(Id)@i
24.  s3  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
25.  e'  \mleq{}loc  e  @i
26.  <a1,  a3,  a5,  a6>  \mmember{}  pv11\_p1\_p1b'base(Cmd;f)(e')@i
27.  if  first(e')
then  <s2,  s3>  \mdownarrow{}\mmember{}  \{pv11\_p1\_init\_scout(Cmd;accpts)\}
else  <s2,  s3>  \mmember{}  State-loc-comb(\mlambda{}loc.\{pv11\_p1\_init\_scout(Cmd;accpts)\};pv11\_p1\_on\_p1b(Cmd) 
                                                                                                                                          bnum;pv11\_p1\_p1b'base(Cmd;f))(
                                pred(e'))
fi  @i
28.  \mforall{}p:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd
            ((p  \mmember{}  s3)
            {}\mRightarrow{}  (\mexists{}e':E
                      \mexists{}l:Id
                        \mexists{}r:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List
                          (e'  \mleq{}loc  e    \mwedge{}  <l,  bnum,  bnum,  r>  \mmember{}  pv11\_p1\_p1b'base(Cmd;f)(e')  \mwedge{}  (p  \mmember{}  r))))@i
29.  bnum  =  a3
30.  bnum  =  a5
31.  p  :  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd@i
32.  (p  \mmember{}  accumulate  (with  value  a  and  list  item  x):
                    if  (\mexists{}zzc\mmember{}a.pv11\_p1\_same\_pvalue(Cmd)  x  zzc)\_b  then  a  else  a  @  [x]  fi 
                  over  list:
                      a6
                  with  starting  value:
                    s3))@i
33.  (p  \mmember{}  a6)
\mvdash{}  \mexists{}e':E
      \mexists{}l:Id
        \mexists{}r:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List
          (e'  \mleq{}loc  e    \mwedge{}  <l,  bnum,  bnum,  r>  \mmember{}  pv11\_p1\_p1b'base(Cmd;f)(e')  \mwedge{}  (p  \mmember{}  r))


By

---

Latex:
(InstConcl  [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a6\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index