Step
*
1
2
4
1
1
1
of Lemma
pv11_p1_A4_C1
1. Cmd : {T:Type| valueall-type(T)} @i'
2. f : pv11_p1_headers_type{i:l}(Cmd)@i'
3. es : EO+(Message(f))@i'
4. (f [decision]) = (ℤ × Cmd) ∈ Type
5. (f [propose]) = (ℤ × Cmd) ∈ Type
6. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
7. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
8. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
9. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
10. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
11. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
12. f ∈ Name ⟶ Type
13. e1 : E@i
14. accpts : bag(Id)@i
15. ldrs : bag(Id)@i
16. ldrs_uid : Id ⟶ ℤ@i
17. reps : bag(Id)@i
18. Inj(Id;ℤ;ldrs_uid)@i
19. pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)@i
20. e2 : E@i
21. ∀e3:E
      ((e3 < e2)
      
⇒ (∀e1:E. ∀bnum1,bnum2:pv11_p1_Ballot_Num(). ∀accepted1,accepted2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
          ∀i1,i2,l:Id. ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀p1,p2:Cmd.
            (((<bnum1, accepted1> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e1)
            ∧ <bnum2, accepted2> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e3)
            ∧ (<b, s, p1> ∈ accepted1)
            ∧ (<b, s, p2> ∈ accepted2))
            ∨ (pv11_p1_p2a'send(Cmd;f) i1 <l, b, s, p1> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e1)
              ∧ pv11_p1_p2a'send(Cmd;f) i2 <l, b, s, p2> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e3)))
            
⇒ (p1 = p2 ∈ Cmd))))
22. bnum1 : pv11_p1_Ballot_Num()@i
23. bnum2 : pv11_p1_Ballot_Num()@i
24. accepted1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
25. accepted2 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
26. i1 : Id@i
27. i2 : Id@i
28. l : Id@i
29. b : pv11_p1_Ballot_Num()@i
30. s : ℤ@i
31. p1 : Cmd@i
32. p2 : Cmd@i
33. loc(e1) ↓∈ ldrs
34. i1 ↓∈ accpts
35. 0 = 0 ∈ ℤ
36. ff = pv11_p1_init_active()
37. l = loc(e1) ∈ Id
38. header(e1) = ``pv11_p1 adopted`` ∈ Name
39. has-es-info-type(es;e1;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
40. (fst(msgval(e1))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))) ∈ pv11_p1_Ballot_Num()
41. (<s, p1> ↓∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))
∧ (¬(∃p2:Cmd
      ∃b:pv11_p1_Ballot_Num()
       ((<b, s, p2> ∈ snd(msgval(e1)))
       ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.
            ((<b', s, c'> ∈ snd(msgval(e1))) 
⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))))
∨ (∃v2:pv11_p1_Ballot_Num()
    (<v2, s, p1> ↓∈ snd(msgval(e1))
    ∧ (¬(∃z5:pv11_p1_Ballot_Num(). ∃z8:Cmd. ((↑(v2  < z5)) ∧ (<z5, s, z8> ∈ snd(msgval(e1))))))))
42. b = (fst(msgval(e1))) ∈ pv11_p1_Ballot_Num()
43. loc(e2) ↓∈ ldrs
44. i2 ↓∈ accpts
45. 0 = 0 ∈ ℤ
46. ff = pv11_p1_init_active()
47. l = loc(e2) ∈ Id
48. header(e2) = ``pv11_p1 adopted`` ∈ Name
49. has-es-info-type(es;e2;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
50. (fst(msgval(e1))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))) ∈ pv11_p1_Ballot_Num()
51. (<s, p2> ↓∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))
∧ (¬(∃p2:Cmd
      ∃b:pv11_p1_Ballot_Num()
       ((<b, s, p2> ∈ snd(msgval(e1)))
       ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.
            ((<b', s, c'> ∈ snd(msgval(e1))) 
⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))))
∨ (∃v2:pv11_p1_Ballot_Num()
    (<v2, s, p2> ↓∈ snd(msgval(e1))
    ∧ (¬(∃z5:pv11_p1_Ballot_Num(). ∃z8:Cmd. ((↑(v2  < z5)) ∧ (<z5, s, z8> ∈ snd(msgval(e1))))))))
52. b = (fst(msgval(e1))) ∈ pv11_p1_Ballot_Num()
53. loc(e1) = loc(e2) ∈ Id
54. (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))
= (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))
∈ pv11_p1_Ballot_Num()
55. <b, snd(msgval(e1))> ∈ pv11_p1_adopted'base(Cmd;f)(e1) ∧ <b, snd(msgval(e1))> ∈ pv11_p1_adopted'base(Cmd;f)(e2)
56. (snd(msgval(e1))) = (snd(msgval(e1))) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
57. msgval(e1) = msgval(e2) ∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
⊢ p1 = p2 ∈ Cmd
BY
{ (MoveToHyp 0 41 THEN MoveToHyp 0 50 THEN SplitOrHyps THEN ExRepD) }
1
1. Cmd : {T:Type| valueall-type(T)} @i'
2. f : pv11_p1_headers_type{i:l}(Cmd)@i'
3. es : EO+(Message(f))@i'
4. (f [decision]) = (ℤ × Cmd) ∈ Type
5. (f [propose]) = (ℤ × Cmd) ∈ Type
6. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
7. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
8. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
9. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
10. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
11. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
12. f ∈ Name ⟶ Type
13. e1 : E@i
14. accpts : bag(Id)@i
15. ldrs : bag(Id)@i
16. ldrs_uid : Id ⟶ ℤ@i
17. reps : bag(Id)@i
18. Inj(Id;ℤ;ldrs_uid)@i
19. pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)@i
20. e2 : E@i
21. ∀e3:E
      ((e3 < e2)
      
⇒ (∀e1:E. ∀bnum1,bnum2:pv11_p1_Ballot_Num(). ∀accepted1,accepted2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
          ∀i1,i2,l:Id. ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀p1,p2:Cmd.
            (((<bnum1, accepted1> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e1)
            ∧ <bnum2, accepted2> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e3)
            ∧ (<b, s, p1> ∈ accepted1)
            ∧ (<b, s, p2> ∈ accepted2))
            ∨ (pv11_p1_p2a'send(Cmd;f) i1 <l, b, s, p1> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e1)
              ∧ pv11_p1_p2a'send(Cmd;f) i2 <l, b, s, p2> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e3)))
            
⇒ (p1 = p2 ∈ Cmd))))
22. bnum1 : pv11_p1_Ballot_Num()@i
23. bnum2 : pv11_p1_Ballot_Num()@i
24. accepted1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
25. accepted2 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
26. i1 : Id@i
27. i2 : Id@i
28. l : Id@i
29. b : pv11_p1_Ballot_Num()@i
30. s : ℤ@i
31. p1 : Cmd@i
32. p2 : Cmd@i
33. loc(e1) ↓∈ ldrs
34. i1 ↓∈ accpts
35. 0 = 0 ∈ ℤ
36. ff = pv11_p1_init_active()
37. l = loc(e1) ∈ Id
38. header(e1) = ``pv11_p1 adopted`` ∈ Name
39. has-es-info-type(es;e1;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
40. (fst(msgval(e1))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))) ∈ pv11_p1_Ballot_Num()
41. b = (fst(msgval(e1))) ∈ pv11_p1_Ballot_Num()
42. loc(e2) ↓∈ ldrs
43. i2 ↓∈ accpts
44. 0 = 0 ∈ ℤ
45. ff = pv11_p1_init_active()
46. l = loc(e2) ∈ Id
47. header(e2) = ``pv11_p1 adopted`` ∈ Name
48. has-es-info-type(es;e2;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
49. (fst(msgval(e1))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))) ∈ pv11_p1_Ballot_Num()
50. b = (fst(msgval(e1))) ∈ pv11_p1_Ballot_Num()
51. loc(e1) = loc(e2) ∈ Id
52. (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))
= (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))
∈ pv11_p1_Ballot_Num()
53. <b, snd(msgval(e1))> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
54. <b, snd(msgval(e1))> ∈ pv11_p1_adopted'base(Cmd;f)(e2)
55. (snd(msgval(e1))) = (snd(msgval(e1))) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
56. msgval(e1) = msgval(e2) ∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
57. <s, p1> ↓∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))
58. ¬(∃p2:Cmd
       ∃b:pv11_p1_Ballot_Num()
        ((<b, s, p2> ∈ snd(msgval(e1)))
        ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.
             ((<b', s, c'> ∈ snd(msgval(e1))) 
⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))
59. <s, p2> ↓∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))
60. ¬(∃p2:Cmd
       ∃b:pv11_p1_Ballot_Num()
        ((<b, s, p2> ∈ snd(msgval(e1)))
        ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.
             ((<b', s, c'> ∈ snd(msgval(e1))) 
⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))
⊢ p1 = p2 ∈ Cmd
2
1. Cmd : {T:Type| valueall-type(T)} @i'
2. f : pv11_p1_headers_type{i:l}(Cmd)@i'
3. es : EO+(Message(f))@i'
4. (f [decision]) = (ℤ × Cmd) ∈ Type
5. (f [propose]) = (ℤ × Cmd) ∈ Type
6. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
7. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
8. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
9. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
10. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
11. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
12. f ∈ Name ⟶ Type
13. e1 : E@i
14. accpts : bag(Id)@i
15. ldrs : bag(Id)@i
16. ldrs_uid : Id ⟶ ℤ@i
17. reps : bag(Id)@i
18. Inj(Id;ℤ;ldrs_uid)@i
19. pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)@i
20. e2 : E@i
21. ∀e3:E
      ((e3 < e2)
      
⇒ (∀e1:E. ∀bnum1,bnum2:pv11_p1_Ballot_Num(). ∀accepted1,accepted2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
          ∀i1,i2,l:Id. ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀p1,p2:Cmd.
            (((<bnum1, accepted1> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e1)
            ∧ <bnum2, accepted2> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e3)
            ∧ (<b, s, p1> ∈ accepted1)
            ∧ (<b, s, p2> ∈ accepted2))
            ∨ (pv11_p1_p2a'send(Cmd;f) i1 <l, b, s, p1> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e1)
              ∧ pv11_p1_p2a'send(Cmd;f) i2 <l, b, s, p2> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e3)))
            
⇒ (p1 = p2 ∈ Cmd))))
22. bnum1 : pv11_p1_Ballot_Num()@i
23. bnum2 : pv11_p1_Ballot_Num()@i
24. accepted1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
25. accepted2 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
26. i1 : Id@i
27. i2 : Id@i
28. l : Id@i
29. b : pv11_p1_Ballot_Num()@i
30. s : ℤ@i
31. p1 : Cmd@i
32. p2 : Cmd@i
33. loc(e1) ↓∈ ldrs
34. i1 ↓∈ accpts
35. 0 = 0 ∈ ℤ
36. ff = pv11_p1_init_active()
37. l = loc(e1) ∈ Id
38. header(e1) = ``pv11_p1 adopted`` ∈ Name
39. has-es-info-type(es;e1;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
40. (fst(msgval(e1))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))) ∈ pv11_p1_Ballot_Num()
41. b = (fst(msgval(e1))) ∈ pv11_p1_Ballot_Num()
42. loc(e2) ↓∈ ldrs
43. i2 ↓∈ accpts
44. 0 = 0 ∈ ℤ
45. ff = pv11_p1_init_active()
46. l = loc(e2) ∈ Id
47. header(e2) = ``pv11_p1 adopted`` ∈ Name
48. has-es-info-type(es;e2;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
49. (fst(msgval(e1))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))) ∈ pv11_p1_Ballot_Num()
50. b = (fst(msgval(e1))) ∈ pv11_p1_Ballot_Num()
51. loc(e1) = loc(e2) ∈ Id
52. (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))
= (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))
∈ pv11_p1_Ballot_Num()
53. <b, snd(msgval(e1))> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
54. <b, snd(msgval(e1))> ∈ pv11_p1_adopted'base(Cmd;f)(e2)
55. (snd(msgval(e1))) = (snd(msgval(e1))) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
56. msgval(e1) = msgval(e2) ∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
57. v2 : pv11_p1_Ballot_Num()
58. <v2, s, p1> ↓∈ snd(msgval(e1))
59. ¬(∃z5:pv11_p1_Ballot_Num(). ∃z8:Cmd. ((↑(v2  < z5)) ∧ (<z5, s, z8> ∈ snd(msgval(e1)))))
60. <s, p2> ↓∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))
61. ¬(∃p2:Cmd
       ∃b:pv11_p1_Ballot_Num()
        ((<b, s, p2> ∈ snd(msgval(e1)))
        ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.
             ((<b', s, c'> ∈ snd(msgval(e1))) 
⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))
⊢ p1 = p2 ∈ Cmd
3
1. Cmd : {T:Type| valueall-type(T)} @i'
2. f : pv11_p1_headers_type{i:l}(Cmd)@i'
3. es : EO+(Message(f))@i'
4. (f [decision]) = (ℤ × Cmd) ∈ Type
5. (f [propose]) = (ℤ × Cmd) ∈ Type
6. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
7. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
8. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
9. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
10. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
11. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
12. f ∈ Name ⟶ Type
13. e1 : E@i
14. accpts : bag(Id)@i
15. ldrs : bag(Id)@i
16. ldrs_uid : Id ⟶ ℤ@i
17. reps : bag(Id)@i
18. Inj(Id;ℤ;ldrs_uid)@i
19. pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)@i
20. e2 : E@i
21. ∀e3:E
      ((e3 < e2)
      
⇒ (∀e1:E. ∀bnum1,bnum2:pv11_p1_Ballot_Num(). ∀accepted1,accepted2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
          ∀i1,i2,l:Id. ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀p1,p2:Cmd.
            (((<bnum1, accepted1> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e1)
            ∧ <bnum2, accepted2> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e3)
            ∧ (<b, s, p1> ∈ accepted1)
            ∧ (<b, s, p2> ∈ accepted2))
            ∨ (pv11_p1_p2a'send(Cmd;f) i1 <l, b, s, p1> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e1)
              ∧ pv11_p1_p2a'send(Cmd;f) i2 <l, b, s, p2> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e3)))
            
⇒ (p1 = p2 ∈ Cmd))))
22. bnum1 : pv11_p1_Ballot_Num()@i
23. bnum2 : pv11_p1_Ballot_Num()@i
24. accepted1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
25. accepted2 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
26. i1 : Id@i
27. i2 : Id@i
28. l : Id@i
29. b : pv11_p1_Ballot_Num()@i
30. s : ℤ@i
31. p1 : Cmd@i
32. p2 : Cmd@i
33. loc(e1) ↓∈ ldrs
34. i1 ↓∈ accpts
35. 0 = 0 ∈ ℤ
36. ff = pv11_p1_init_active()
37. l = loc(e1) ∈ Id
38. header(e1) = ``pv11_p1 adopted`` ∈ Name
39. has-es-info-type(es;e1;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
40. (fst(msgval(e1))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))) ∈ pv11_p1_Ballot_Num()
41. b = (fst(msgval(e1))) ∈ pv11_p1_Ballot_Num()
42. loc(e2) ↓∈ ldrs
43. i2 ↓∈ accpts
44. 0 = 0 ∈ ℤ
45. ff = pv11_p1_init_active()
46. l = loc(e2) ∈ Id
47. header(e2) = ``pv11_p1 adopted`` ∈ Name
48. has-es-info-type(es;e2;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
49. (fst(msgval(e1))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))) ∈ pv11_p1_Ballot_Num()
50. b = (fst(msgval(e1))) ∈ pv11_p1_Ballot_Num()
51. loc(e1) = loc(e2) ∈ Id
52. (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))
= (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))
∈ pv11_p1_Ballot_Num()
53. <b, snd(msgval(e1))> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
54. <b, snd(msgval(e1))> ∈ pv11_p1_adopted'base(Cmd;f)(e2)
55. (snd(msgval(e1))) = (snd(msgval(e1))) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
56. msgval(e1) = msgval(e2) ∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
57. <s, p1> ↓∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))
58. ¬(∃p2:Cmd
       ∃b:pv11_p1_Ballot_Num()
        ((<b, s, p2> ∈ snd(msgval(e1)))
        ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.
             ((<b', s, c'> ∈ snd(msgval(e1))) 
⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))
59. v2 : pv11_p1_Ballot_Num()
60. <v2, s, p2> ↓∈ snd(msgval(e1))
61. ¬(∃z5:pv11_p1_Ballot_Num(). ∃z8:Cmd. ((↑(v2  < z5)) ∧ (<z5, s, z8> ∈ snd(msgval(e1)))))
⊢ p1 = p2 ∈ Cmd
4
1. Cmd : {T:Type| valueall-type(T)} @i'
2. f : pv11_p1_headers_type{i:l}(Cmd)@i'
3. es : EO+(Message(f))@i'
4. (f [decision]) = (ℤ × Cmd) ∈ Type
5. (f [propose]) = (ℤ × Cmd) ∈ Type
6. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
7. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
8. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
9. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
10. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
11. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
12. f ∈ Name ⟶ Type
13. e1 : E@i
14. accpts : bag(Id)@i
15. ldrs : bag(Id)@i
16. ldrs_uid : Id ⟶ ℤ@i
17. reps : bag(Id)@i
18. Inj(Id;ℤ;ldrs_uid)@i
19. pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)@i
20. e2 : E@i
21. ∀e3:E
      ((e3 < e2)
      
⇒ (∀e1:E. ∀bnum1,bnum2:pv11_p1_Ballot_Num(). ∀accepted1,accepted2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
          ∀i1,i2,l:Id. ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀p1,p2:Cmd.
            (((<bnum1, accepted1> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e1)
            ∧ <bnum2, accepted2> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e3)
            ∧ (<b, s, p1> ∈ accepted1)
            ∧ (<b, s, p2> ∈ accepted2))
            ∨ (pv11_p1_p2a'send(Cmd;f) i1 <l, b, s, p1> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e1)
              ∧ pv11_p1_p2a'send(Cmd;f) i2 <l, b, s, p2> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e3)))
            
⇒ (p1 = p2 ∈ Cmd))))
22. bnum1 : pv11_p1_Ballot_Num()@i
23. bnum2 : pv11_p1_Ballot_Num()@i
24. accepted1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
25. accepted2 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
26. i1 : Id@i
27. i2 : Id@i
28. l : Id@i
29. b : pv11_p1_Ballot_Num()@i
30. s : ℤ@i
31. p1 : Cmd@i
32. p2 : Cmd@i
33. loc(e1) ↓∈ ldrs
34. i1 ↓∈ accpts
35. 0 = 0 ∈ ℤ
36. ff = pv11_p1_init_active()
37. l = loc(e1) ∈ Id
38. header(e1) = ``pv11_p1 adopted`` ∈ Name
39. has-es-info-type(es;e1;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
40. (fst(msgval(e1))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))) ∈ pv11_p1_Ballot_Num()
41. b = (fst(msgval(e1))) ∈ pv11_p1_Ballot_Num()
42. loc(e2) ↓∈ ldrs
43. i2 ↓∈ accpts
44. 0 = 0 ∈ ℤ
45. ff = pv11_p1_init_active()
46. l = loc(e2) ∈ Id
47. header(e2) = ``pv11_p1 adopted`` ∈ Name
48. has-es-info-type(es;e2;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
49. (fst(msgval(e1))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))) ∈ pv11_p1_Ballot_Num()
50. b = (fst(msgval(e1))) ∈ pv11_p1_Ballot_Num()
51. loc(e1) = loc(e2) ∈ Id
52. (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))
= (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))
∈ pv11_p1_Ballot_Num()
53. <b, snd(msgval(e1))> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
54. <b, snd(msgval(e1))> ∈ pv11_p1_adopted'base(Cmd;f)(e2)
55. (snd(msgval(e1))) = (snd(msgval(e1))) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
56. msgval(e1) = msgval(e2) ∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
57. v3 : pv11_p1_Ballot_Num()
58. <v3, s, p1> ↓∈ snd(msgval(e1))
59. ¬(∃z5:pv11_p1_Ballot_Num(). ∃z8:Cmd. ((↑(v3  < z5)) ∧ (<z5, s, z8> ∈ snd(msgval(e1)))))
60. v2 : pv11_p1_Ballot_Num()
61. <v2, s, p2> ↓∈ snd(msgval(e1))
62. ¬(∃z5:pv11_p1_Ballot_Num(). ∃z8:Cmd. ((↑(v2  < z5)) ∧ (<z5, s, z8> ∈ snd(msgval(e1)))))
⊢ p1 = p2 ∈ Cmd
Latex:
Latex:
1.  Cmd  :  \{T:Type|  valueall-type(T)\}  @i'
2.  f  :  pv11\_p1\_headers\_type\{i:l\}(Cmd)@i'
3.  es  :  EO+(Message(f))@i'
4.  (f  [decision])  =  (\mBbbZ{}  \mtimes{}  Cmd)
5.  (f  [propose])  =  (\mBbbZ{}  \mtimes{}  Cmd)
6.  (f  ``pv11\_p1  adopted``)  =  (pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List))
7.  (f  ``pv11\_p1  preempted``)  =  pv11\_p1\_Ballot\_Num()
8.  (f  ``pv11\_p1  p2b``)  =  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  pv11\_p1\_Ballot\_Num())
9.  (f  ``pv11\_p1  p2a``)  =  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
10.  (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))
11.  (f  ``pv11\_p1  p1a``)  =  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num())
12.  f  \mmember{}  Name  {}\mrightarrow{}  Type
13.  e1  :  E@i
14.  accpts  :  bag(Id)@i
15.  ldrs  :  bag(Id)@i
16.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
17.  reps  :  bag(Id)@i
18.  Inj(Id;\mBbbZ{};ldrs$_{uid}$)@i
19.  pv11\_p1\_message-constraint\{paxos-v11-part1.esh:o\}(Cmd;  accpts;  ldrs;  ldrs$_{uid}\000C$;  reps;  f;  es)@i
20.  e2  :  E@i
21.  \mforall{}e3:E
            ((e3  <  e2)
            {}\mRightarrow{}  (\mforall{}e1:E.  \mforall{}bnum1,bnum2:pv11\_p1\_Ballot\_Num().  \mforall{}accepted1,accepted2:(pv11\_p1\_Ballot\_Num()
                                                                                                                                                  \mtimes{}  \mBbbZ{}
                                                                                                                                                  \mtimes{}  Cmd)  List.  \mforall{}i1,i2,l:Id.
                    \mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}s:\mBbbZ{}.  \mforall{}p1,p2:Cmd.
                        (((<bnum1,  accepted1>  \mmember{}  pv11\_p1\_AcceptorState(Cmd;ldrs$_{uid}$;f)(e1\000C)
                        \mwedge{}  <bnum2,  accepted2>  \mmember{}  pv11\_p1\_AcceptorState(Cmd;ldrs$_{uid}$;f)(e3)
                        \mwedge{}  (<b,  s,  p1>  \mmember{}  accepted1)
                        \mwedge{}  (<b,  s,  p2>  \mmember{}  accepted2))
                        \mvee{}  (pv11\_p1\_p2a'send(Cmd;f)  i1  <l,  b,  s,  p1>  \mmember{}  pv11\_p1\_main(Cmd;accpts;ldrs;ldrs$\mbackslash{}ff5\000Cf{uid}$;reps;f)(e1)
                            \mwedge{}  pv11\_p1\_p2a'send(Cmd;f)  i2  <l,  b,  s,  p2>  \mmember{}  pv11\_p1\_main(Cmd;accpts;ldrs;ldrs$\mbackslash{}ff\000C5f{uid}$;reps;f)(e3)))
                        {}\mRightarrow{}  (p1  =  p2))))
22.  bnum1  :  pv11\_p1\_Ballot\_Num()@i
23.  bnum2  :  pv11\_p1\_Ballot\_Num()@i
24.  accepted1  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
25.  accepted2  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
26.  i1  :  Id@i
27.  i2  :  Id@i
28.  l  :  Id@i
29.  b  :  pv11\_p1\_Ballot\_Num()@i
30.  s  :  \mBbbZ{}@i
31.  p1  :  Cmd@i
32.  p2  :  Cmd@i
33.  loc(e1)  \mdownarrow{}\mmember{}  ldrs
34.  i1  \mdownarrow{}\mmember{}  accpts
35.  0  =  0
36.  ff  =  pv11\_p1\_init\_active()
37.  l  =  loc(e1)
38.  header(e1)  =  ``pv11\_p1  adopted``
39.  has-es-info-type(es;e1;f;pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List))
40.  (fst(msgval(e1)))  =  (fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1)))
41.  (<s,  p1>  \mdownarrow{}\mmember{}  snd(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1)))
\mwedge{}  (\mneg{}(\mexists{}p2:Cmd
            \mexists{}b:pv11\_p1\_Ballot\_Num()
              ((<b,  s,  p2>  \mmember{}  snd(msgval(e1)))
              \mwedge{}  (\mforall{}b':pv11\_p1\_Ballot\_Num().  \mforall{}c':Cmd.
                        ((<b',  s,  c'>  \mmember{}  snd(msgval(e1)))  {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$\000C)  b'  b))))))))
\mvee{}  (\mexists{}v2:pv11\_p1\_Ballot\_Num()
        (<v2,  s,  p1>  \mdownarrow{}\mmember{}  snd(msgval(e1))
        \mwedge{}  (\mneg{}(\mexists{}z5:pv11\_p1\_Ballot\_Num().  \mexists{}z8:Cmd.  ((\muparrow{}(v2    <  z5))  \mwedge{}  (<z5,  s,  z8>  \mmember{}  snd(msgval(e1))))))))
42.  b  =  (fst(msgval(e1)))
43.  loc(e2)  \mdownarrow{}\mmember{}  ldrs
44.  i2  \mdownarrow{}\mmember{}  accpts
45.  0  =  0
46.  ff  =  pv11\_p1\_init\_active()
47.  l  =  loc(e2)
48.  header(e2)  =  ``pv11\_p1  adopted``
49.  has-es-info-type(es;e2;f;pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List))
50.  (fst(msgval(e1)))  =  (fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e2)))
51.  (<s,  p2>  \mdownarrow{}\mmember{}  snd(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e2)))
\mwedge{}  (\mneg{}(\mexists{}p2:Cmd
            \mexists{}b:pv11\_p1\_Ballot\_Num()
              ((<b,  s,  p2>  \mmember{}  snd(msgval(e1)))
              \mwedge{}  (\mforall{}b':pv11\_p1\_Ballot\_Num().  \mforall{}c':Cmd.
                        ((<b',  s,  c'>  \mmember{}  snd(msgval(e1)))  {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$\000C)  b'  b))))))))
\mvee{}  (\mexists{}v2:pv11\_p1\_Ballot\_Num()
        (<v2,  s,  p2>  \mdownarrow{}\mmember{}  snd(msgval(e1))
        \mwedge{}  (\mneg{}(\mexists{}z5:pv11\_p1\_Ballot\_Num().  \mexists{}z8:Cmd.  ((\muparrow{}(v2    <  z5))  \mwedge{}  (<z5,  s,  z8>  \mmember{}  snd(msgval(e1))))))))
52.  b  =  (fst(msgval(e1)))
53.  loc(e1)  =  loc(e2)
54.  (fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1)))
=  (fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e2)))
55.  <b,  snd(msgval(e1))>  \mmember{}  pv11\_p1\_adopted'base(Cmd;f)(e1)
\mwedge{}  <b,  snd(msgval(e1))>  \mmember{}  pv11\_p1\_adopted'base(Cmd;f)(e2)
56.  (snd(msgval(e1)))  =  (snd(msgval(e1)))
57.  msgval(e1)  =  msgval(e2)
\mvdash{}  p1  =  p2
By
Latex:
(MoveToHyp  0  41  THEN  MoveToHyp  0  50  THEN  SplitOrHyps  THEN  ExRepD)
Home
Index