---

Step * 1 of Lemma pv11_p1_A4_C1_funC


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. accpts : bag(Id)@i
16. ldrs : bag(Id)@i
17. ldrs_uid : Id ─→ ℤ@i
18. reps : bag(Id)@i
19. i1 : Id@i
20. i2 : Id@i
21. l1 : Id@i
22. l2 : Id@i
23. b : pv11_p1_Ballot_Num()@i
24. s : ℤ@i
25. p1 : Cmd@i
26. p2 : Cmd@i
27. Inj(Id;ℤ;ldrs_uid)@i
28. pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)@i
29. pv11_p1_p2a'send(Cmd;f) i1 <l1, b, s, p1> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e1)@i
30. pv11_p1_p2a'send(Cmd;f) i2 <l2, b, s, p2> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e2)@i
⊢ p1 = p2 ∈ Cmd
BY
{ (InstLemma `pv11_p1_A4_C1` [⌈Cmd⌉;⌈f⌉;⌈es⌉;⌈e1⌉;⌈e2⌉;⌈accpts⌉;⌈ldrs⌉;⌈ldrs_uid⌉;⌈reps⌉;⌈b⌉;⌈b⌉;⌈[]⌉;⌈[]⌉;⌈i1⌉;⌈i2⌉;
   ⌈l1⌉;⌈b⌉;⌈s⌉;⌈p1⌉;⌈p2⌉]⋅
   THEN Auto
   THEN OrRight
   THEN Auto
   THEN Assert ⌈l1 = l2 ∈ Id⌉⋅
   THEN Auto
   THEN RepeatFor 2 ((FLemma `pv11_p1_bnum_p2a` [-2] THENA Auto))
   THEN ExRepD
   THEN SimpleAssertReasoning
   THEN (HypSubst' (-3) (-1) THENA Auto)
   THEN RepUR ``pv11_p1_Ballot_Num pv11_p1_mk_bnum`` (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  Cmd  :  \{T:Type|  valueall-type(T)\}  @i'
2.  f  :  pv11\_p1\_headers\_type\{i:l\}(Cmd)@i'
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))@i'
13.  e1  :  E@i
14.  e2  :  E@i
15.  accpts  :  bag(Id)@i
16.  ldrs  :  bag(Id)@i
17.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
18.  reps  :  bag(Id)@i
19.  i1  :  Id@i
20.  i2  :  Id@i
21.  l1  :  Id@i
22.  l2  :  Id@i
23.  b  :  pv11\_p1\_Ballot\_Num()@i
24.  s  :  \mBbbZ{}@i
25.  p1  :  Cmd@i
26.  p2  :  Cmd@i
27.  Inj(Id;\mBbbZ{};ldrs$_{uid}$)@i
28.  pv11\_p1\_message-constraint\{paxos-v11-part1.esh:o\}(Cmd;  accpts;  ldrs;  ldrs$_{uid}\000C$;  reps;  f;  es)@i
29.  pv11\_p1\_p2a'send(Cmd;f)  i1  <l1,  b,  s,  p1>  \mmember{}  pv11\_p1\_main(Cmd;accpts;ldrs;ldrs$_{uid\mbackslash{}\000Cff7d$;reps;f)(e1)@i
30.  pv11\_p1\_p2a'send(Cmd;f)  i2  <l2,  b,  s,  p2>  \mmember{}  pv11\_p1\_main(Cmd;accpts;ldrs;ldrs$_{uid\mbackslash{}\000Cff7d$;reps;f)(e2)@i
\mvdash{}  p1  =  p2


By

---

Latex:
(InstLemma  `pv11\_p1\_A4\_C1`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}accpts\mkleeneclose{};\mkleeneopen{}ldrs\mkleeneclose{};\mkleeneopen{}ldrs$_{uid}\mbackslash{}ff\000C24\mkleeneclose{};\mkleeneopen{}reps\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{};
  \mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}i1\mkleeneclose{};\mkleeneopen{}i2\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  OrRight
  THEN  Auto
  THEN  Assert  \mkleeneopen{}l1  =  l2\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  ((FLemma  `pv11\_p1\_bnum\_p2a`  [-2]  THENA  Auto))
  THEN  ExRepD
  THEN  SimpleAssertReasoning
  THEN  (HypSubst'  (-3)  (-1)  THENA  Auto)
  THEN  RepUR  ``pv11\_p1\_Ballot\_Num  pv11\_p1\_mk\_bnum``  (-1)
  THEN  Auto)

---

Home Index