Proof of Nuprl Lemma : pv11_p1_scout_from

Step * of Lemma pv11_p1_scout_from_acc

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts:bag(Id).
∀s:bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List). ∀bnum:pv11_p1_Ballot_Num().
  (s ∈ pv11_p1_ScoutState(Cmd;accpts;f) bnum(e)
  ⇒ let waitfor,pvalues = s
     in ∀p:pv11_p1_Ballot_Num() × ℤ × Cmd
          ((p ∈ pvalues)
          ⇒ (∃e':E
               ∃l:Id
                ∃r:(pv11_p1_Ballot_Num() × ℤ × Cmd) List

                 (e' ≤loc e  ∧ <l, bnum, bnum, r> ∈ pv11_p1_p1b'base(Cmd;f)(e') ∧ (p ∈ r)))))

BY
{ (MemoryInvariant1 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

⊢ single-valued-bag((λloc.{pv11_p1_init_scout(Cmd;accpts)}) loc(e);bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))

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. e : E@i
14. accpts : bag(Id)@i
15. s : bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)@i
16. bnum : pv11_p1_Ballot_Num()@i
17. s ∈ State-loc-comb(λloc.{pv11_p1_init_scout(Cmd;accpts)};pv11_p1_on_p1b(Cmd) bnum;pv11_p1_p1b'base(Cmd;f))(e)
⊢ single-valued-classrel(es;pv11_p1_p1b'base(Cmd;f);Id
× pv11_p1_Ballot_Num()
× pv11_p1_Ballot_Num()
× ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))

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. e : E@i
14. accpts : bag(Id)@i
15. s : bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)@i
16. bnum : pv11_p1_Ballot_Num()@i
17. s ∈ State-loc-comb(λloc.{pv11_p1_init_scout(Cmd;accpts)};pv11_p1_on_p1b(Cmd) bnum;pv11_p1_p1b'base(Cmd;f))(e)
⊢ ∀s:bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
    (s ↓∈ (λloc.{pv11_p1_init_scout(Cmd;accpts)}) loc(e)
    ⇒ let waitfor,pvalues = s
       in ∀p:pv11_p1_Ballot_Num() × ℤ × Cmd
            ((p ∈ pvalues)
            ⇒ (∃e':E
                 ∃l:Id
                  ∃r:(pv11_p1_Ballot_Num() × ℤ × Cmd) List

                   (e' ≤loc e  ∧ <l, bnum, bnum, r> ∈ pv11_p1_p1b'base(Cmd;f)(e') ∧ (p ∈ r)))))

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

⊢ ∀a:Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List). ∀e':E.

  ∀s:bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
    (e' ≤loc e
    ⇒ a ∈ pv11_p1_p1b'base(Cmd;f)(e')
    ⇒ if first(e')
       then s ↓∈ (λloc.{pv11_p1_init_scout(Cmd;accpts)}) loc(e')

       else s ∈ State-loc-comb(λloc.{pv11_p1_init_scout(Cmd;accpts)};pv11_p1_on_p1b(Cmd) bnum;pv11_p1_p1b'base(Cmd;f))(

                pred(e'))
       fi
    ⇒ let waitfor,pvalues = s
       in ∀p:pv11_p1_Ballot_Num() × ℤ × Cmd
            ((p ∈ pvalues)
            ⇒ (∃e':E
                 ∃l:Id
                  ∃r:(pv11_p1_Ballot_Num() × ℤ × Cmd) List

                   (e' ≤loc e  ∧ <l, bnum, bnum, r> ∈ pv11_p1_p1b'base(Cmd;f)(e') ∧ (p ∈ r))))

    ⇒ let waitfor,pvalues = pv11_p1_on_p1b(Cmd) bnum loc(e') a s
       in ∀p:pv11_p1_Ballot_Num() × ℤ × Cmd
            ((p ∈ pvalues)
            ⇒ (∃e':E
                 ∃l:Id
                  ∃r:(pv11_p1_Ballot_Num() × ℤ × Cmd) List

                   (e' ≤loc e  ∧ <l, bnum, bnum, r> ∈ pv11_p1_p1b'base(Cmd;f)(e') ∧ (p ∈ r)))))

Latex:

Latex:
\mforall{}Cmd:ValueAllType. \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd). \mforall{}es:EO+(Message(f)). \mforall{}e:E. \mforall{}accpts:bag(Id). \mforall{}s:bag(Id) \mtimes{} ((pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List). \mforall{}bnum:pv11\_p1\_Ballot\_Num(). (s \mmember{} pv11\_p1\_ScoutState(Cmd;accpts;f) bnum(e) {}\mRightarrow{} let waitfor,pvalues = s in \mforall{}p:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd ((p \mmember{} pvalues) {}\mRightarrow{} (\mexists{}e':E \mexists{}l:Id \mexists{}r:(pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List (e' \mleq{}loc e \mwedge{} <l, bnum, bnum, r> \mmember{} pv11\_p1\_p1b'base(Cmd;f)(e') \mwedge{} (p \mmember{} r))))) By Latex: (MemoryInvariant1 THEN Try (Complete (Auto))) Home Index