---

Step * of Lemma pv11_p1_ldr_fun_mem_adopted

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((e1 <loc e2)
  ⇒ <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)), pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
  ⇒ ((↓(<s, c> ∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))))
     ∨ (∃b:pv11_p1_Ballot_Num(). (↓(<b, s, c> ∈ pvals))))
  ⇒ (↑(pv11_p1_in_domain(Cmd) s (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))))))
BY
{ (StartEmlProof
   THEN (InstLemma `pv11_p1_ldr_mem_adopted` [⌈Cmd⌉;⌈f⌉;⌈es⌉;⌈e1⌉;⌈e2⌉;⌈ldrs_uid⌉;
         ⌈pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)⌉;⌈pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)⌉;
         ⌈inr (inl <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)), pvals>) ⌉]⋅
         THENA (Auto THEN Try ((BLemma `pv11_p1_LeaderState-classrel` THEN Auto)))
         )
   ) }

1
.....antecedent..... 
1. Cmd : {T:Type| valueall-type(T)} @i'
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. e1 : E@i
14. e2 : E@i
15. ldrs_uid : Id ─→ ℤ@i
16. pvals : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
17. s : ℤ@i
18. c : Cmd@i
19. (e1 <loc e2)@i
20. <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)), pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e1)@i
21. (↓(<s, c> ∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))))
∨ (∃b:pv11_p1_Ballot_Num(). (↓(<b, s, c> ∈ pvals)))@i
⊢ inr (inl <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)), pvals>)  ∈
   pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e1)

2
1. Cmd : {T:Type| valueall-type(T)} @i'
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. e1 : E@i
14. e2 : E@i
15. ldrs_uid : Id ─→ ℤ@i
16. pvals : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
17. s : ℤ@i
18. c : Cmd@i
19. (e1 <loc e2)@i
20. <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)), pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e1)@i
21. (↓(<s, c> ∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))))
∨ (∃b:pv11_p1_Ballot_Num(). (↓(<b, s, c> ∈ pvals)))@i
22. case inr (inl <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)), pvals>) 
 of inl(x) =>
 True
 | inr(x) =>
 case x
  of inl(x) =>
  let bnum,pvals = x 
  in let bnum1,active1,proposals1 = pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1) in 
     let bnum2,active2,proposals2 = pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2) in 
     (bnum1 = bnum ∈ pv11_p1_Ballot_Num())
     ⇒ (∀s:ℤ. ∀b:pv11_p1_Ballot_Num(). ∀c:Cmd.
           (((<s, c> ∈ proposals1) ∨ (<b, s, c> ∈ pvals)) ⇒ (↑(pv11_p1_in_domain(Cmd) s proposals2))))
  | inr(x) =>
  True
⊢ ↑(pv11_p1_in_domain(Cmd) s (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))))

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}pvals:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List.  \mforall{}s:\mBbbZ{}.  \mforall{}c:Cm\000Cd.
    ((e1  <loc  e2)
    {}\mRightarrow{}  <fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1)),  pvals>  \mmember{}  pv11\_p1\_ad\000Copted'base(Cmd;f)(e1)
    {}\mRightarrow{}  ((\mdownarrow{}(<s,  c>  \mmember{}  snd(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1)))))
          \mvee{}  (\mexists{}b:pv11\_p1\_Ballot\_Num().  (\mdownarrow{}(<b,  s,  c>  \mmember{}  pvals))))
    {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_in\_domain(Cmd)  s  (snd(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}\mbackslash{}ff2\000C4;f;es;e2)))))))


By

---

Latex:
(StartEmlProof
  THEN  (InstLemma  `pv11\_p1\_ldr\_mem\_adopted`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}ldrs$_{uid}\mbackslash{}ff\000C24\mkleeneclose{};
              \mkleeneopen{}pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1)\mkleeneclose{};\mkleeneopen{}pv11\_p1\_LeaderStateFu\000Cn(Cmd;ldrs$_{uid}$;f;es;e2)\mkleeneclose{};
              \mkleeneopen{}inr  (inl  <fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1)),  pvals>)\000C  \mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Try  ((BLemma  `pv11\_p1\_LeaderState-classrel`  THEN  Auto)))
              )
  )

---

Home Index