---

Step * of Lemma pv11_p1_decision_from_p2a

∀[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]. ∀[k:ℤ]. ∀[v:Cmd].
  ∀a:Id
    (pv11_p1_decision{i:l}(Cmd;f;accpts;ldrs;ldrs_uid;reps;es;e;k;v)
    ⇒ has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
    ⇒ a ↓∈ accpts
    ⇒ (↓∃e':E
          (e' ≤loc e 
          ∧ (k = (fst(snd(snd(msgval(e))))) ∈ ℤ)
          ∧ ((fst(snd(msgval(e)))) = (snd(snd(snd(msgval(e))))) ∈ pv11_p1_Ballot_Num())
          ∧ pv11_p1_p2a'send(Cmd;f) a <loc(e), fst(snd(msgval(e))), k, v> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f\000C)(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. k : ℤ
19. v : Cmd
20. a : Id@i
21. pv11_p1_decision{i:l}(Cmd;f;accpts;ldrs;ldrs_uid;reps;es;e;k;v)@i'
22. has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())@i
23. a ↓∈ accpts@i
⊢ ↓∃e':E
    (e' ≤loc e 
    ∧ (k = (fst(snd(snd(msgval(e))))) ∈ ℤ)
    ∧ ((fst(snd(msgval(e)))) = (snd(snd(snd(msgval(e))))) ∈ pv11_p1_Ballot_Num())
    ∧ pv11_p1_p2a'send(Cmd;f) a <loc(e), fst(snd(msgval(e))), k, v> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;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{}[k:\mBbbZ{}]\000C.  \mforall{}[v:Cmd].
    \mforall{}a:Id
        (pv11\_p1\_decision\{i:l\}(Cmd;f;accpts;ldrs;ldrs$_{uid}$;reps;es;e;k;v)
        {}\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'  \mleq{}loc  e 
                    \mwedge{}  (k  =  (fst(snd(snd(msgval(e))))))
                    \mwedge{}  ((fst(snd(msgval(e))))  =  (snd(snd(snd(msgval(e))))))
                    \mwedge{}  pv11\_p1\_p2a'send(Cmd;f)  a  <loc(e),  fst(snd(msgval(e))),  k,  v>  \mmember{}  pv11\_p1\_main(Cmd;accpts;\000Cldrs;ldrs$_{uid}$;reps;f)(
                                                                                                    e'))))


By

---

Latex:
StartEmlProof

---

Home Index