---

Step * 2 3 of Lemma pv11_p1_ldr_state_eq


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. e : E
14. ¬↑pred(e) ∈b pv11_p1_propose'base(Cmd;f)
15. ¬↑first(e)
16. ldrs_uid : Id ─→ ℤ
17. v1 : pv11_p1_Ballot_Num()
18. v3 : 𝔹
19. v4 : (ℤ × Cmd) List
20. ↑pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
21. b1 : pv11_p1_Ballot_Num()
22. b3 : 𝔹
23. b4 : (ℤ × Cmd) List
24. <b1, b3, b4> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
25. a3 : pv11_p1_Ballot_Num()
26. a3 ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
27. <v1, v3, v4> = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) a3 <b1, b3, b4>) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd\000C) List))
⊢ ↓∃x:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
    ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
     (x ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
     ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
     ∧ (<v1, v3, v4> = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) x s) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
BY
{ (UseClassRel (-2)
   THEN Unfold `pv11_p1_adopted\'base` (-10)
   THEN (Using [`f',⌈f⌉] (FLemma `member-base-class` [-10])⋅ THENA Auto)
   THEN (HypSubst (-5) (-1) THENA Auto)
   THEN SimpleSimpHyp Auto (-1)) }

---

Latex:

---

Latex:

1.  Cmd  :  \{T:Type|  valueall-type(T)\} 
2.  f  :  pv11\_p1\_headers\_type\{i:l\}(Cmd)
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))
13.  e  :  E
14.  \mneg{}\muparrow{}pred(e)  \mmember{}\msubb{}  pv11\_p1\_propose'base(Cmd;f)
15.  \mneg{}\muparrow{}first(e)
16.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}
17.  v1  :  pv11\_p1\_Ballot\_Num()
18.  v3  :  \mBbbB{}
19.  v4  :  (\mBbbZ{}  \mtimes{}  Cmd)  List
20.  \muparrow{}pred(e)  \mmember{}\msubb{}  pv11\_p1\_adopted'base(Cmd;f)
21.  b1  :  pv11\_p1\_Ballot\_Num()
22.  b3  :  \mBbbB{}
23.  b4  :  (\mBbbZ{}  \mtimes{}  Cmd)  List
24.  <b1,  b3,  b4>  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(pred(e))
25.  a3  :  pv11\_p1\_Ballot\_Num()
26.  a3  \mmember{}  pv11\_p1\_preempted'base(Cmd;f)(pred(e))
27.  <v1,  v3,  v4>  =  (pv11\_p1\_when\_preempted(Cmd;ldrs$_{uid}$)  loc(e)  a3  <b1,  b3,  \000Cb4>)
\mvdash{}  \mdownarrow{}\mexists{}x:pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)
        \mexists{}s:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbB{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Cmd)  List)
          (x  \mmember{}  pv11\_p1\_adopted'base(Cmd;f)(pred(e))
          \mwedge{}  s  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(pred(e))
          \mwedge{}  (<v1,  v3,  v4>  =  (pv11\_p1\_when\_adopted(Cmd;ldrs$_{uid}$)  loc(e)  x  s)))


By

---

Latex:
(UseClassRel  (-2)
  THEN  Unfold  `pv11\_p1\_adopted\mbackslash{}'base`  (-10)
  THEN  (Using  [`f',\mkleeneopen{}f\mkleeneclose{}]  (FLemma  `member-base-class`  [-10])\mcdot{}  THENA  Auto)
  THEN  (HypSubst  (-5)  (-1)  THENA  Auto)
  THEN  SimpleSimpHyp  Auto  (-1))

---

Home Index