---

Step * of Lemma pv11_p1_valid-proposal-transitivity-forward

∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀p:ℤ × Cmd. ∀e':{e':E| e' ≤loc e } . ∀e1:{e1:E| 
                                                                                                         e1 ≤loc e' } .
    (pv11_p1_valid-proposal(Cmd;es.e1;e';p;f) ⇒ pv11_p1_valid-proposal(Cmd;es;e;p;f))
BY
{ StartEmlProof }

1
1. Cmd : {T:Type| valueall-type(T)} 
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. p : ℤ × Cmd@i
15. e' : {e':E| e' ≤loc e } @i
16. e1 : {e1:E| e1 ≤loc e' } @i
17. pv11_p1_valid-proposal(Cmd;es.e1;e';p;f)@i
⊢ pv11_p1_valid-proposal(Cmd;es;e;p;f)

---

Latex:

---

Latex:
\mforall{}[Cmd:\{T:Type|  valueall-type(T)\}  ]
    \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}p:\mBbbZ{}  \mtimes{}  Cmd.  \mforall{}e':\{e':E|  e'  \mleq{}loc  e  \}  .
    \mforall{}e1:\{e1:E|  e1  \mleq{}loc  e'  \}  .
        (pv11\_p1\_valid-proposal(Cmd;es.e1;e';p;f)  {}\mRightarrow{}  pv11\_p1\_valid-proposal(Cmd;es;e;p;f))


By

---

Latex:
StartEmlProof

---

Home Index