---

Step * of Lemma pv11_p1_ldr_mem_adopted

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀v1,v2:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
∀p:ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num().
  ((e1 <loc e2)
  ⇒ p ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e1)
  ⇒ v1 ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e1)
  ⇒ v2 ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e2)
  ⇒ case p
      of inl(x) =>
      True
      | inr(x) =>
      case x
       of inl(x) =>
       let bnum,pvals = x 
       in let bnum1,active1,proposals1 = v1 in 
          let bnum2,active2,proposals2 = v2 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)
BY
{ (GenMemoryTrans1 3 MemoryLemmas THEN Try (Complete (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. v1 : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)@i
17. v2 : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)@i
18. p : ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num()@i
19. (e1 <loc e2)@i
20. p ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e1)@i
21. v1 ∈
     Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{pv11_p1_init_leader(Cmd) 
                                                                                               loc};... (+) ...)(e1)
22. v2 ∈
     Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{pv11_p1_init_leader(Cmd) 
                                                                                               loc};... (+) ...)(e2)
⊢ ∀a:ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num().
  ∀s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List). ∀e:E.
    (e1 ≤loc e 
    ⇒ (e <loc e2)
    ⇒ a ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e)
    ⇒ s ∈
        Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{... 
                                                                                                  loc};... (+) ...)(e)
    ⇒ (λ2v2.case a
         of inl(x) =>
         True
         | inr(x) =>
         case x
          of inl(x) =>
          let bnum,pvals = x 
          in let bnum1,active1,proposals1 = s in 
             let bnum2,active2,proposals2 = v2 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_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) a 
         s)))

2
.....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. v1 : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)@i
17. v2 : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)@i
18. p : ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num()@i
19. (e1 <loc e2)@i
20. p ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e1)@i
21. v1 ∈
     Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{pv11_p1_init_leader(Cmd) 
                                                                                               loc};... (+) ...)(e1)
22. v2 ∈
     Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{pv11_p1_init_leader(Cmd) 
                                                                                               loc};... (+) ...)(e2)
⊢ ∀a1,a2:ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num().
  ∀s1,s2:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List). ∀e,e':E.
    (e1 ≤loc e 
    ⇒ (e <loc e')
    ⇒ (e' <loc e2)
    ⇒ a1 ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e)
    ⇒ s1 ∈
        Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{... 
                                                                                                  loc};... (+) ...)(e)
    ⇒ a2 ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e')
    ⇒ s2 ∈
        Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{... 
                                                                                                  loc};... (+) ...)(e')
    ⇒ (λ2v2.case a1
         of inl(x) =>
         True
         | inr(x) =>
         case x
          of inl(x) =>
          let bnum,pvals = x 
          in let bnum1,active1,proposals1 = s1 in 
             let bnum2,active2,proposals2 = v2 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 
        s2)
    ⇒ (λ2v2.case a1
         of inl(x) =>
         True
         | inr(x) =>
         case x
          of inl(x) =>
          let bnum,pvals = x 
          in let bnum1,active1,proposals1 = s1 in 
             let bnum2,active2,proposals2 = v2 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_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e2) a2 
         s2)))

3
.....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. v1 : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)@i
17. v2 : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)@i
18. p : ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num()@i
19. (e1 <loc e2)@i
20. p ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e1)@i
21. v1 ∈
     Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{pv11_p1_init_leader(Cmd) 
                                                                                               loc};... (+) ...)(e1)
22. v2 ∈
     Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{pv11_p1_init_leader(Cmd) 
                                                                                               loc};... (+) ...)(e2)
⊢ single-valued-classrel(es;pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) ...;ℤ
                                                                                                × Cmd + ... + ...)

4
.....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. v1 : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)@i
17. v2 : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)@i
18. p : ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num()@i
19. (e1 <loc e2)@i
20. p ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e1)@i
21. v1 ∈
     Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{pv11_p1_init_leader(Cmd) 
                                                                                               loc};... (+) ...)(e1)
22. v2 ∈
     Memory-loc-class(pv11_p1_on_propose(Cmd) + pv11_p1_when_adopted(Cmd;ldrs_uid) + ...;λloc.{pv11_p1_init_leader(Cmd) 
                                                                                               loc};... (+) ...)(e2)
⊢ single-valued-bag((λloc.{pv11_p1_init_leader(Cmd) loc}) loc(e1);pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))

---

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{}v1,v2:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbB{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Cmd)  List).
\mforall{}p:\mBbbZ{}  \mtimes{}  Cmd  +  pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)  +  pv11\_p1\_Ballot\_Num().
    ((e1  <loc  e2)
    {}\mRightarrow{}  p  \mmember{}
            pv11\_p1\_propose'base(Cmd;f)  (+)  pv11\_p1\_adopted'base(Cmd;f)  (+)  pv11\_p1\_preempted'base(Cmd;f)(
            e1)
    {}\mRightarrow{}  v1  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e1)
    {}\mRightarrow{}  v2  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e2)
    {}\mRightarrow{}  case  p
            of  inl(x)  =>
            True
            |  inr(x)  =>
            case  x
              of  inl(x)  =>
              let  bnum,pvals  =  x 
              in  let  bnum1,active1,proposals1  =  v1  in 
                    let  bnum2,active2,proposals2  =  v2  in 
                    (bnum1  =  bnum)
                    {}\mRightarrow{}  (\mforall{}s:\mBbbZ{}.  \mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}c:Cmd.
                                (((<s,  c>  \mmember{}  proposals1)  \mvee{}  (<b,  s,  c>  \mmember{}  pvals))
                                {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_in\_domain(Cmd)  s  proposals2))))
              |  inr(x)  =>
              True)


By

---

Latex:
(GenMemoryTrans1  3  MemoryLemmas  THEN  Try  (Complete  (Auto)))

---

Home Index