---

Step * of Lemma pv11_p1_decision_from_p2a_acc

∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[accpts,ldrs:bag(Id)].
∀[ldrs_uid:Id ⟶ ℤ]. ∀[reps:bag(Id)]. ∀[e:E]. ∀[s:ℤ]. ∀[c:Cmd]. ∀[a:Id].
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ pv11_p1_decision{i:l}(Cmd;f;accpts;ldrs;ldrs_uid;reps;es;e;s;c)
  ⇒ has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
  ⇒ a ↓∈ accpts
  ⇒ (↓∃e':E
        ((e' < e)
        ∧ loc(e') ↓∈ accpts
        ∧ (s = (fst(snd(snd(msgval(e))))) ∈ ℤ)
        ∧ ((fst(snd(msgval(e)))) = (snd(snd(snd(msgval(e))))) ∈ pv11_p1_Ballot_Num())
        ∧ <loc(e), snd(snd(snd(msgval(e)))), s, c> ∈ pv11_p1_p2a'base(Cmd;f)(e'))))
BY
{ StartEmlProof }

1
1. Cmd : {T:Type| valueall-type(T)} 
2. f : pv11_p1_headers_type{i:l}(Cmd)
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))
13. accpts : bag(Id)
14. ldrs : bag(Id)
15. ldrs_uid : Id ⟶ ℤ
16. reps : bag(Id)
17. e : E
18. s : ℤ
19. c : Cmd
20. a : Id
21. Inj(Id;ℤ;ldrs_uid)@i
22. pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)@i
23. pv11_p1_decision{i:l}(Cmd;f;accpts;ldrs;ldrs_uid;reps;es;e;s;c)@i'
24. has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())@i
25. a ↓∈ accpts@i
⊢ ↓∃e':E
    ((e' < e)
    ∧ loc(e') ↓∈ accpts
    ∧ (s = (fst(snd(snd(msgval(e))))) ∈ ℤ)
    ∧ ((fst(snd(msgval(e)))) = (snd(snd(snd(msgval(e))))) ∈ pv11_p1_Ballot_Num())
    ∧ <loc(e), snd(snd(snd(msgval(e)))), s, c> ∈ pv11_p1_p2a'base(Cmd;f)(e'))

---

Latex:

---

Latex:
\mforall{}[Cmd:ValueAllType].  \mforall{}[f:pv11\_p1\_headers\_type\{i:l\}(Cmd)].  \mforall{}[es:EO+(Message(f))].
\mforall{}[accpts,ldrs:bag(Id)].  \mforall{}[ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[reps:bag(Id)].  \mforall{}[e:E].  \mforall{}[s:\mBbbZ{}]\000C.  \mforall{}[c:Cmd].  \mforall{}[a:Id].
    (Inj(Id;\mBbbZ{};ldrs$_{uid}$)
    {}\mRightarrow{}  pv11\_p1\_message-constraint\{paxos-v11-part1.esh:o\}(Cmd;  accpts;  ldrs;  ldrs$_{uid\mbackslash{}ff7\000Cd$;  reps;  f;  es)
    {}\mRightarrow{}  pv11\_p1\_decision\{i:l\}(Cmd;f;accpts;ldrs;ldrs$_{uid}$;reps;es;e;s;c)
    {}\mRightarrow{}  has-es-info-type(es;e;f;Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  pv11\_p1\_Ballot\_Num())
    {}\mRightarrow{}  a  \mdownarrow{}\mmember{}  accpts
    {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                ((e'  <  e)
                \mwedge{}  loc(e')  \mdownarrow{}\mmember{}  accpts
                \mwedge{}  (s  =  (fst(snd(snd(msgval(e))))))
                \mwedge{}  ((fst(snd(msgval(e))))  =  (snd(snd(snd(msgval(e))))))
                \mwedge{}  <loc(e),  snd(snd(snd(msgval(e)))),  s,  c>  \mmember{}  pv11\_p1\_p2a'base(Cmd;f)(e'))))


By

---

Latex:
StartEmlProof

---

Home Index