---

Step * of Lemma pv11_p1_valid-proposal-forward

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

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. e' : {e':E| e' ≤loc e } @i
15. p : ℤ × Cmd@i
16. e'@0 : E@i
17. {e'@0 c≤ e}@i
18. p ∈ pv11_p1_propose'base(Cmd;f)(e'@0)@i
19. e'@0 c≤ e
⊢ ...system_error_message... e'@0 c≤ e

2
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. e' : {e':E| e' ≤loc e } @i
15. p : ℤ × Cmd@i
16. e'@0 : E@i
17. e'@0 c≤ e@i
18. p ∈ pv11_p1_propose'base(Cmd;f)(e'@0)@i
19. e'@0 c≤ e
⊢ p ∈ pv11_p1_propose'base(Cmd;f)(e'@0)

---

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{}e':\{e':E|  e'  \mleq{}loc  e  \}  .  \mforall{}p:\mBbbZ{}  \mtimes{}  Cmd.
        (pv11\_p1\_valid-proposal(Cmd;es.e';e;p;f)  {}\mRightarrow{}  pv11\_p1\_valid-proposal(Cmd;es;e;p;f))


By

---

Latex:
(StartEmlProof  THEN  RepeatFor  3  (ParallelLast)  THEN  Auto)

---

Home Index