---

Step * 1 of Lemma pv11_p1_append_news_iff2


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. accpts : bag(Id)@i
14. ldrs : bag(Id)@i
15. ldrs_uid : Id ─→ ℤ@i
16. reps : bag(Id)@i
17. pv : pv11_p1_Ballot_Num() × ℤ × Cmd@i
18. L1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
19. L2 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
20. Inj(Id;ℤ;ldrs_uid)@i
21. pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)@i
22. (∀x∈L1 @ L2.↓∃e:E. (x ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e))))@i
⊢ (pv ∈ pv11_p1_append_news(Cmd) pv11_p1_same_pvalue(Cmd) L1 L2) ⇐⇒ (pv ∈ L1) ∨ (pv ∈ L2)
BY
{ (MoveToConcl (-5) THEN RepUR ``pv11_p1_append_news`` 0 THEN ListInd (-3) THEN Reduce 0 THEN Auto) }

1
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. accpts : bag(Id)@i
14. ldrs : bag(Id)@i
15. ldrs_uid : Id ─→ ℤ@i
16. reps : bag(Id)@i
17. pv : pv11_p1_Ballot_Num() × ℤ × Cmd@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. u : pv11_p1_Ballot_Num() × ℤ × Cmd@i
21. v : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
22. ∀L1:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
      ((∀x∈L1 @ v.↓∃e:E. (x ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e))))
      ⇒ ((pv ∈ accumulate (with value a and list item x):
                 pv11_p1_add_if_new() pv11_p1_same_pvalue(Cmd) x a
                over list:
                  v
                with starting value:
                 L1))
         ⇐⇒ (pv ∈ L1) ∨ (pv ∈ v)))@i
23. L1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
24. (∀x∈L1 @ [u / v].↓∃e:E. (x ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e))))@i
25. (pv ∈ accumulate (with value a and list item x):
           pv11_p1_add_if_new() pv11_p1_same_pvalue(Cmd) x a
          over list:
            v
          with starting value:
           pv11_p1_add_if_new() pv11_p1_same_pvalue(Cmd) u L1))@i
⊢ (pv ∈ L1) ∨ (pv ∈ [u / v])

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. accpts : bag(Id)@i
14. ldrs : bag(Id)@i
15. ldrs_uid : Id ─→ ℤ@i
16. reps : bag(Id)@i
17. pv : pv11_p1_Ballot_Num() × ℤ × Cmd@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. u : pv11_p1_Ballot_Num() × ℤ × Cmd@i
21. v : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
22. ∀L1:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
      ((∀x∈L1 @ v.↓∃e:E. (x ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e))))
      ⇒ ((pv ∈ accumulate (with value a and list item x):
                 pv11_p1_add_if_new() pv11_p1_same_pvalue(Cmd) x a
                over list:
                  v
                with starting value:
                 L1))
         ⇐⇒ (pv ∈ L1) ∨ (pv ∈ v)))@i
23. L1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
24. (∀x∈L1 @ [u / v].↓∃e:E. (x ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e))))@i
25. (pv ∈ L1) ∨ (pv ∈ [u / v])@i
⊢ (pv ∈ accumulate (with value a and list item x):
         pv11_p1_add_if_new() pv11_p1_same_pvalue(Cmd) x a
        over list:
          v
        with starting value:
         pv11_p1_add_if_new() pv11_p1_same_pvalue(Cmd) u L1))

---

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.  accpts  :  bag(Id)@i
14.  ldrs  :  bag(Id)@i
15.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
16.  reps  :  bag(Id)@i
17.  pv  :  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd@i
18.  L1  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
19.  L2  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
20.  Inj(Id;\mBbbZ{};ldrs$_{uid}$)@i
21.  pv11\_p1\_message-constraint\{paxos-v11-part1.esh:o\}(Cmd;  accpts;  ldrs;  ldrs$_{uid}\000C$;  reps;  f;  es)@i
22.  (\mforall{}x\mmember{}L1  @  L2.\mdownarrow{}\mexists{}e:E.  (x  \mmember{}  snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e\000C))))@i
\mvdash{}  (pv  \mmember{}  pv11\_p1\_append\_news(Cmd)  pv11\_p1\_same\_pvalue(Cmd)  L1  L2)  \mLeftarrow{}{}\mRightarrow{}  (pv  \mmember{}  L1)  \mvee{}  (pv  \mmember{}  L2)


By

---

Latex:
(MoveToConcl  (-5)  THEN  RepUR  ``pv11\_p1\_append\_news``  0  THEN  ListInd  (-3)  THEN  Reduce  0  THEN  Auto)

---

Home Index