Step
*
1
1
2
of Lemma
pv11_p1_A2
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. ¬↑first(e)
15. ¬↑e ∈b pv11_p1_p1a'base(Cmd;f)
16. ldrs_uid : Id ─→ ℤ@i
17. bnum1 : pv11_p1_Ballot_Num()@i
18. bnum2 : pv11_p1_Ballot_Num()@i
19. accepted1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
20. b : pv11_p1_Ballot_Num()@i
21. pv : ℤ × Cmd@i
22. loc : Id@i
23. Inj(Id;ℤ;ldrs_uid)@i
24. ¬False@i
25. <bnum1, accepted1>
= pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
26. ¬(<b, pv> ∈ accepted1)@i
27. ↑(pv11_p1_leq_bnum(ldrs_uid) bnum1 bnum2)
28. l : (pv11_p1_Ballot_Num() × ℤ × Cmd) List
29. (<b, pv> ∈ l)
30. ↑e ∈b pv11_p1_p2a'base(Cmd;f)
⊢ (<bnum2, accepted1 @ l>
= ((pv11_p1_on_p1a(Cmd;ldrs_uid) o pv11_p1_p1a'base(Cmd;f))
|| (pv11_p1_on_p2a(Cmd;ldrs_uid) o pv11_p1_p2a'base(Cmd;f))@e
pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e)))
∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
⇒ (b = bnum2 ∈ pv11_p1_Ballot_Num())
BY
{ ((RWO "classfun-res-parallel-class-right" 0 THENA Auto)
THEN Try (Complete ((ProveFunctional THEN Auto)))
THEN (RWO "classfun-res-eclass1" 0 THENA (Auto THEN ProveFunctional THEN Auto))
THEN RepUR ``pv11_p1_on_p2a`` 0
THEN (InstLemma `classfun-res-member-base` [⌈f⌉;⌈es⌉;⌈e⌉;⌈``pv11_p1 p2a``⌉]⋅ THENA Auto)
THEN (Subst ⌈Base(``pv11_p1 p2a``) ~ pv11_p1_p2a'base(Cmd;f)⌉ (-1)⋅ THENA (RepUR ``pv11_p1_p2a'base`` 0 THEN Auto))
THEN HypSubst (-1) 0) }
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. e : E@i
14. ¬↑first(e)
15. ¬↑e ∈b pv11_p1_p1a'base(Cmd;f)
16. ldrs_uid : Id ─→ ℤ@i
17. bnum1 : pv11_p1_Ballot_Num()@i
18. bnum2 : pv11_p1_Ballot_Num()@i
19. accepted1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
20. b : pv11_p1_Ballot_Num()@i
21. pv : ℤ × Cmd@i
22. loc : Id@i
23. Inj(Id;ℤ;ldrs_uid)@i
24. ¬False@i
25. <bnum1, accepted1>
= pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
26. ¬(<b, pv> ∈ accepted1)@i
27. ↑(pv11_p1_leq_bnum(ldrs_uid) bnum1 bnum2)
28. l : (pv11_p1_Ballot_Num() × ℤ × Cmd) List
29. (<b, pv> ∈ l)
30. ↑e ∈b pv11_p1_p2a'base(Cmd;f)
31. pv11_p1_p2a'base(Cmd;f)@e ~ msgval(e)
⊢ (<bnum2, accepted1 @ l>
= let loc,zg = msgval(e)
in let b,sp = zg
in let ballot_num,accepted = pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
in let ballot_num' = pv11_p1_max_bnum(ldrs_uid) b ballot_num in
let accepted' = if pv11_p1_leq_bnum(ldrs_uid) ballot_num b
then pv11_p1_add_if_new() pv11_p1_same_pvalue(Cmd) <b, sp> accepted
else accepted
fi in
<ballot_num', accepted'>
∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
⇒ (b = bnum2 ∈ pv11_p1_Ballot_Num())
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. e : E@i
14. \mneg{}\muparrow{}first(e)
15. \mneg{}\muparrow{}e \mmember{}\msubb{} pv11\_p1\_p1a'base(Cmd;f)
16. ldrs$_{uid}$ : Id {}\mrightarrow{} \mBbbZ{}@i
17. bnum1 : pv11\_p1\_Ballot\_Num()@i
18. bnum2 : pv11\_p1\_Ballot\_Num()@i
19. accepted1 : (pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List@i
20. b : pv11\_p1\_Ballot\_Num()@i
21. pv : \mBbbZ{} \mtimes{} Cmd@i
22. loc : Id@i
23. Inj(Id;\mBbbZ{};ldrs$_{uid}$)@i
24. \mneg{}False@i
25. <bnum1, accepted1> = pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;pred(e))
26. \mneg{}(<b, pv> \mmember{} accepted1)@i
27. \muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$) bnum1 bnum2)
28. l : (pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List
29. (<b, pv> \mmember{} l)
30. \muparrow{}e \mmember{}\msubb{} pv11\_p1\_p2a'base(Cmd;f)
\mvdash{} (<bnum2, accepted1 @ l>
= ((pv11\_p1\_on\_p1a(Cmd;ldrs$_{uid}$) o pv11\_p1\_p1a'base(Cmd;f))
|| (pv11\_p1\_on\_p2a(Cmd;ldrs$_{uid}$) o pv11\_p1\_p2a'base(Cmd;f))@e
pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;pred(e))))
{}\mRightarrow{} (b = bnum2)
By
Latex:
((RWO "classfun-res-parallel-class-right" 0 THENA Auto)
THEN Try (Complete ((ProveFunctional THEN Auto)))
THEN (RWO "classfun-res-eclass1" 0 THENA (Auto THEN ProveFunctional THEN Auto))
THEN RepUR ``pv11\_p1\_on\_p2a`` 0
THEN (InstLemma `classfun-res-member-base` [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}``pv11\_p1 p2a``\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (Subst \mkleeneopen{}Base(``pv11\_p1 p2a``) \msim{} pv11\_p1\_p2a'base(Cmd;f)\mkleeneclose{} (-1)\mcdot{}
THENA (RepUR ``pv11\_p1\_p2a'base`` 0 THEN Auto)
)
THEN HypSubst (-1) 0)
Home
Index