Proof of Nuprl Lemma : pv11_p1_ldr

Step * 1 2 of Lemma pv11_p1_ldr_proposal3

.....falsecase.....
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. ldrs_uid : Id ─→ ℤ@i
14. e : E@i
15. ∀e':E
      ((e' < e)
      ⇒ (∀v1:pv11_p1_Ballot_Num(). ∀v3:𝔹. ∀v4:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
            (<v1, v3, v4> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e')
            ⇒ (<s, c> ∈ v4)
            ⇒ (∃e1:E
                 ∃bnum:pv11_p1_Ballot_Num()
                  ∃active:𝔹
                   ∃proposals:(ℤ × Cmd) List
                    ((e1 <loc e')
                    ∧ <bnum, active, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e1)

                    ∧ (∀e'':E. ∀x:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).

                         ((e1 <loc e'')
                         ⇒ e'' ≤loc e'
                         ⇒ x ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e'')
                         ⇒ (<s, c> ∈ snd(snd(x)))))

                    ∧ ((<s, c> ∈ pv11_p1_propose'base(Cmd;f)(e1) ∧ (¬↑(pv11_p1_in_domain(Cmd) s proposals)))

             ∧ (<v1, v3, v4> = (pv11_p1_on_propose(Cmd) loc(e) x s) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))

if pred(e) ∈_b pv11_p1_adopted'base(Cmd;f)
  then ∃x:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
        ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
         (x ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
         ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
         ∧ (<v1, v3, v4>
           = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) x s)
           ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
if pred(e) ∈_b pv11_p1_preempted'base(Cmd;f)
  then ∃x:pv11_p1_Ballot_Num()
        ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
         (x ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
         ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
         ∧ (<v1, v3, v4>
           = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) x s)
           ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
else <v1, v3, v4> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
fi
24. ¬↑first(e)
⊢ ∃e':E
   ∃bnum:pv11_p1_Ballot_Num()
    ∃active:𝔹
     ∃proposals:(ℤ × Cmd) List
      ((e' <loc e)
      ∧ <bnum, active, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e')
      ∧ (∀e'':E. ∀x:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
           ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ x ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e'') ⇒ (<s, c> ∈ snd(snd(x)))))
      ∧ ((<s, c> ∈ pv11_p1_propose'base(Cmd;f)(e') ∧ (¬↑(pv11_p1_in_domain(Cmd) s proposals)))
        ∨ (∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
            ∃b:pv11_p1_Ballot_Num()
             (<bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e')
             ∧ (<b, s, c> ∈ pvals)
             ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.  ((<b', s, c'> ∈ pvals) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))))
BY
{ ((SplitOnHypITE (-2) THENA Auto) THEN ExRepD) }

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

                    ∧ (∀e'':E. ∀x:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).

                         ((e1 <loc e'')
                         ⇒ e'' ≤loc e'
                         ⇒ x ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e'')
                         ⇒ (<s, c> ∈ snd(snd(x)))))

                    ∧ ((<s, c> ∈ pv11_p1_propose'base(Cmd;f)(e1) ∧ (¬↑(pv11_p1_in_domain(Cmd) s proposals)))

27. <v1, v3, v4> = (pv11_p1_on_propose(Cmd) loc(e) x s1) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))

28. ¬↑first(e)
29. ↑pred(e) ∈_b pv11_p1_propose'base(Cmd;f)
⊢ ∃e':E
   ∃bnum:pv11_p1_Ballot_Num()
    ∃active:𝔹
     ∃proposals:(ℤ × Cmd) List
      ((e' <loc e)
      ∧ <bnum, active, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e')
      ∧ (∀e'':E. ∀x:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
           ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ x ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e'') ⇒ (<s, c> ∈ snd(snd(x)))))
      ∧ ((<s, c> ∈ pv11_p1_propose'base(Cmd;f)(e') ∧ (¬↑(pv11_p1_in_domain(Cmd) s proposals)))
        ∨ (∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
            ∃b:pv11_p1_Ballot_Num()
             (<bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e')
             ∧ (<b, s, c> ∈ pvals)
             ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.  ((<b', s, c'> ∈ pvals) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))))

2
.....falsecase.....
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

                    ∧ (∀e'':E. ∀x:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).

                         ((e1 <loc e'')
                         ⇒ e'' ≤loc e'
                         ⇒ x ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e'')
                         ⇒ (<s, c> ∈ snd(snd(x)))))

                    ∧ ((<s, c> ∈ pv11_p1_propose'base(Cmd;f)(e1) ∧ (¬↑(pv11_p1_in_domain(Cmd) s proposals)))

                      ∨ (∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
                          ∃b:pv11_p1_Ballot_Num()
                           (<bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
                           ∧ (<b, s, c> ∈ pvals)
                           ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.
                                ((<b', s, c'> ∈ pvals) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))))))))
16. v1 : pv11_p1_Ballot_Num()@i
17. v3 : 𝔹@i
18. v4 : (ℤ × Cmd) List@i
19. s : ℤ@i
20. c : Cmd@i
21. <v1, v3, v4> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e)@i
22. (<s, c> ∈ v4)@i
23. if pred(e) ∈_b pv11_p1_adopted'base(Cmd;f)
      then ∃x:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
            ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
             (x ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
             ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
             ∧ (<v1, v3, v4>
               = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) x s)
               ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
if pred(e) ∈_b pv11_p1_preempted'base(Cmd;f)
  then ∃x:pv11_p1_Ballot_Num()
        ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
         (x ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
         ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
         ∧ (<v1, v3, v4>
           = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) x s)
           ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
else <v1, v3, v4> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
fi
24. ¬↑first(e)
25. ¬↑pred(e) ∈_b pv11_p1_propose'base(Cmd;f)
⊢ ∃e':E
   ∃bnum:pv11_p1_Ballot_Num()
    ∃active:𝔹
     ∃proposals:(ℤ × Cmd) List
      ((e' <loc e)
      ∧ <bnum, active, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e')
      ∧ (∀e'':E. ∀x:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
           ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ x ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e'') ⇒ (<s, c> ∈ snd(snd(x)))))
      ∧ ((<s, c> ∈ pv11_p1_propose'base(Cmd;f)(e') ∧ (¬↑(pv11_p1_in_domain(Cmd) s proposals)))
        ∨ (∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
            ∃b:pv11_p1_Ballot_Num()
             (<bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e')
             ∧ (<b, s, c> ∈ pvals)
             ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.  ((<b', s, c'> ∈ pvals) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))))

Latex:

Latex:
.....falsecase..... 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. ldrs$_{uid}$ : Id {}\mrightarrow{} \mBbbZ{}@i 14. e : E@i 15. \mforall{}e':E ((e' < e) {}\mRightarrow{} (\mforall{}v1:pv11\_p1\_Ballot\_Num(). \mforall{}v3:\mBbbB{}. \mforall{}v4:(\mBbbZ{} \mtimes{} Cmd) List. \mforall{}s:\mBbbZ{}. \mforall{}c:Cmd. (<v1, v3, v4> \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e') {}\mRightarrow{} (<s, c> \mmember{} v4) {}\mRightarrow{} (\mexists{}e1:E \mexists{}bnum:pv11\_p1\_Ballot\_Num() \mexists{}active:\mBbbB{} \mexists{}proposals:(\mBbbZ{} \mtimes{} Cmd) List ((e1 <loc e') \mwedge{} <bnum, active, proposals> \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid\mbackslash{}ff7\000Cd$;f)(e1) \mwedge{} (\mforall{}e'':E. \mforall{}x:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List). ((e1 <loc e'') {}\mRightarrow{} e'' \mleq{}loc e' {}\mRightarrow{} x \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e'') {}\mRightarrow{} (<s, c> \mmember{} snd(snd(x))))) \mwedge{} ((<s, c> \mmember{} pv11\_p1\_propose'base(Cmd;f)(e1) \mwedge{} (\mneg{}\muparrow{}(pv11\_p1\_in\_domain(Cmd) s proposals))) \mvee{} (\mexists{}pvals:(pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List \mexists{}b:pv11\_p1\_Ballot\_Num() (<bnum, pvals> \mmember{} pv11\_p1\_adopted'base(Cmd;f)(e1) \mwedge{} (<b, s, c> \mmember{} pvals) \mwedge{} (\mforall{}b':pv11\_p1\_Ballot\_Num(). \mforall{}c':Cmd. ((<b', s, c'> \mmember{} pvals) {}\mRightarrow{} (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$) b' b)))))))\000C))))) 16. v1 : pv11\_p1\_Ballot\_Num()@i 17. v3 : \mBbbB{}@i 18. v4 : (\mBbbZ{} \mtimes{} Cmd) List@i 19. s : \mBbbZ{}@i 20. c : Cmd@i 21. <v1, v3, v4> \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e)@i 22. (<s, c> \mmember{} v4)@i 23. if pred(e) \mmember{}\msubb{} pv11\_p1\_propose'base(Cmd;f) then \mexists{}x:\mBbbZ{} \mtimes{} Cmd \mexists{}s:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List) (x \mmember{} pv11\_p1\_propose'base(Cmd;f)(pred(e)) \mwedge{} s \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(pred(e)) \mwedge{} (<v1, v3, v4> = (pv11\_p1\_on\_propose(Cmd) loc(e) x s))) if pred(e) \mmember{}\msubb{} pv11\_p1\_adopted'base(Cmd;f) then \mexists{}x:pv11\_p1\_Ballot\_Num() \mtimes{} ((pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List) \mexists{}s:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List) (x \mmember{} pv11\_p1\_adopted'base(Cmd;f)(pred(e)) \mwedge{} s \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(pred(e)) \mwedge{} (<v1, v3, v4> = (pv11\_p1\_when\_adopted(Cmd;ldrs$_{uid}$) loc(e) x s))) if pred(e) \mmember{}\msubb{} pv11\_p1\_preempted'base(Cmd;f) then \mexists{}x:pv11\_p1\_Ballot\_Num() \mexists{}s:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List) (x \mmember{} pv11\_p1\_preempted'base(Cmd;f)(pred(e)) \mwedge{} s \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(pred(e)) \mwedge{} (<v1, v3, v4> = (pv11\_p1\_when\_preempted(Cmd;ldrs$_{uid}$) loc(e) x s)\000C)) else <v1, v3, v4> \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(pred(e)) fi 24. \mneg{}\muparrow{}first(e) \mvdash{} \mexists{}e':E \mexists{}bnum:pv11\_p1\_Ballot\_Num() \mexists{}active:\mBbbB{} \mexists{}proposals:(\mBbbZ{} \mtimes{} Cmd) List ((e' <loc e) \mwedge{} <bnum, active, proposals> \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e') \mwedge{} (\mforall{}e'':E. \mforall{}x:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List). ((e' <loc e'') {}\mRightarrow{} e'' \mleq{}loc e {}\mRightarrow{} x \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e'') {}\mRightarrow{} (<s, c> \mmember{} snd(snd(x))))) \mwedge{} ((<s, c> \mmember{} pv11\_p1\_propose'base(Cmd;f)(e') \mwedge{} (\mneg{}\muparrow{}(pv11\_p1\_in\_domain(Cmd) s proposals))) \mvee{} (\mexists{}pvals:(pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List \mexists{}b:pv11\_p1\_Ballot\_Num() (<bnum, pvals> \mmember{} pv11\_p1\_adopted'base(Cmd;f)(e') \mwedge{} (<b, s, c> \mmember{} pvals) \mwedge{} (\mforall{}b':pv11\_p1\_Ballot\_Num(). \mforall{}c':Cmd. ((<b', s, c'> \mmember{} pvals) {}\mRightarrow{} (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$) b'\000C b)))))))) By Latex: ((SplitOnHypITE (-2) THENA Auto) THEN ExRepD) Home Index