---

Step * 1 2 1 of Lemma pv11_p1_append_news_iff2

.....rewrite subgoal..... 
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
⊢ (∀x∈(pv11_p1_add_if_new() pv11_p1_same_pvalue(Cmd) u L1) @ v.
     ↓∃e:E. (x ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e))))
BY
{ (All (\i. RWO "l_all_iff" i THENA CpltAuto)
   THEN Auto
   THEN BackThruSomeHyp
   THEN GenListD (-1)
   THEN D (-1)
   THEN Try (Complete (RepeatFor 2 ((GenListD 0 THEN OrRight THEN Auto))))
   THEN (RWO "pv11_p1_add_if_new_iff2" (-1) THENA Auto)
   THEN D (-1)
   THEN Try (Complete (((GenListD 0 THENA Auto) THEN OrLeft THEN Auto)))
   THEN SplitOnHypITE (-1)
   THEN Auto
   THEN (GenListD 0 THENA Auto)
   THEN (OrRight THENA Auto)
   THEN GenListD 0
   THEN OrLeft
   THEN Auto) }

---

Latex:

---

Latex:
.....rewrite  subgoal..... 
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.  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.  u  :  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd@i
21.  v  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
22.  \mforall{}L1:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List
            ((\mforall{}x\mmember{}L1  @  v.\mdownarrow{}\mexists{}e:E.  (x  \mmember{}  snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es\000C;e))))
            {}\mRightarrow{}  ((pv  \mmember{}  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))
                  \mLeftarrow{}{}\mRightarrow{}  (pv  \mmember{}  L1)  \mvee{}  (pv  \mmember{}  v)))@i
23.  L1  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
24.  (\mforall{}x\mmember{}L1  @  [u  /  v].\mdownarrow{}\mexists{}e:E.  (x  \mmember{}  snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f\000C;es;e))))@i
25.  (pv  \mmember{}  L1)  \mvee{}  (pv  \mmember{}  [u  /  v])@i
\mvdash{}  (\mforall{}x\mmember{}(pv11\_p1\_add\_if\_new()  pv11\_p1\_same\_pvalue(Cmd)  u  L1)  @  v.
          \mdownarrow{}\mexists{}e:E.  (x  \mmember{}  snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e))))


By

---

Latex:
(All  (\mbackslash{}i.  RWO  "l\_all\_iff"  i  THENA  CpltAuto)
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  GenListD  (-1)
  THEN  D  (-1)
  THEN  Try  (Complete  (RepeatFor  2  ((GenListD  0  THEN  OrRight  THEN  Auto))))
  THEN  (RWO  "pv11\_p1\_add\_if\_new\_iff2"  (-1)  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  (((GenListD  0  THENA  Auto)  THEN  OrLeft  THEN  Auto)))
  THEN  SplitOnHypITE  (-1)
  THEN  Auto
  THEN  (GenListD  0  THENA  Auto)
  THEN  (OrRight  THENA  Auto)
  THEN  GenListD  0
  THEN  OrLeft
  THEN  Auto)

---

Home Index