Step
*
1
1
1
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. ldrs_uid : Id ─→ ℤ@i
16. bnum1 : pv11_p1_Ballot_Num()@i
17. bnum2 : pv11_p1_Ballot_Num()@i
18. accepted1 : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
19. b : pv11_p1_Ballot_Num()@i
20. pv : ℤ × Cmd@i
21. loc : Id@i
22. Inj(Id;ℤ;ldrs_uid)@i
23. ¬False@i
24. <bnum1, accepted1>
= pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
25. ¬(<b, pv> ∈ accepted1)@i
26. ↑(pv11_p1_leq_bnum(ldrs_uid) bnum1 bnum2)
27. l : (pv11_p1_Ballot_Num() × ℤ × Cmd) List
28. (<b, pv> ∈ l)
29. ↑e ∈b pv11_p1_p1a'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-left" 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_p1a`` 0
THEN (InstLemma `classfun-res-member-base` [⌈f⌉;⌈es⌉;⌈e⌉;⌈``pv11_p1 p1a``⌉]⋅ THENA Auto)
THEN (Subst ⌈Base(``pv11_p1 p1a``) ~ pv11_p1_p1a'base(Cmd;f)⌉ (-1)⋅ THENA (RepUR ``pv11_p1_p1a'base`` 0 THEN Auto))
THEN HypSubst (-1) 0
THEN Unfold `pv11_p1_p1a\'base` (-2)
THEN (FLemma `member-base-class` [-2] THENA Auto)
THEN (Assert ⌈has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num())⌉⋅
THENA ((RWO "has-es-info-type-is-msg-has-type" 0 THENA Auto)
THEN RepUR ``msg-has-type msg-type`` 0
THEN Fold `es-header` 0
THEN Auto)
)
THEN RepeatFor 2 (UsePairEta [1;3;1] 0)
THEN (D 0 THENA Auto)
THEN SimpEqPairs
THEN (RevHypSubst (-12) (-2) THENA Auto)
THEN (RevHypSubst (-11) (-1) THENA Auto)
THEN (InstLemma `append_cancel_nil` [⌈pv11_p1_Ballot_Num() × ℤ × Cmd⌉;⌈accepted1⌉;⌈l⌉]⋅ THENA Auto)
THEN HypSubst (-1) (-8)
THEN Auto) }
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. ldrs$_{uid}$ : Id {}\mrightarrow{} \mBbbZ{}@i
16. bnum1 : pv11\_p1\_Ballot\_Num()@i
17. bnum2 : pv11\_p1\_Ballot\_Num()@i
18. accepted1 : (pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List@i
19. b : pv11\_p1\_Ballot\_Num()@i
20. pv : \mBbbZ{} \mtimes{} Cmd@i
21. loc : Id@i
22. Inj(Id;\mBbbZ{};ldrs$_{uid}$)@i
23. \mneg{}False@i
24. <bnum1, accepted1> = pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;pred(e))
25. \mneg{}(<b, pv> \mmember{} accepted1)@i
26. \muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$) bnum1 bnum2)
27. l : (pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List
28. (<b, pv> \mmember{} l)
29. \muparrow{}e \mmember{}\msubb{} pv11\_p1\_p1a'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-left" 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\_p1a`` 0
THEN (InstLemma `classfun-res-member-base` [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}``pv11\_p1 p1a``\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (Subst \mkleeneopen{}Base(``pv11\_p1 p1a``) \msim{} pv11\_p1\_p1a'base(Cmd;f)\mkleeneclose{} (-1)\mcdot{}
THENA (RepUR ``pv11\_p1\_p1a'base`` 0 THEN Auto)
)
THEN HypSubst (-1) 0
THEN Unfold `pv11\_p1\_p1a\mbackslash{}'base` (-2)
THEN (FLemma `member-base-class` [-2] THENA Auto)
THEN (Assert \mkleeneopen{}has-es-info-type(es;e;f;Id \mtimes{} pv11\_p1\_Ballot\_Num())\mkleeneclose{}\mcdot{}
THENA ((RWO "has-es-info-type-is-msg-has-type" 0 THENA Auto)
THEN RepUR ``msg-has-type msg-type`` 0
THEN Fold `es-header` 0
THEN Auto)
)
THEN RepeatFor 2 (UsePairEta [1;3;1] 0)
THEN (D 0 THENA Auto)
THEN SimpEqPairs
THEN (RevHypSubst (-12) (-2) THENA Auto)
THEN (RevHypSubst (-11) (-1) THENA Auto)
THEN (InstLemma `append\_cancel\_nil` [\mkleeneopen{}pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd\mkleeneclose{};\mkleeneopen{}accepted1\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{} THENA Auto)
THEN HypSubst (-1) (-8)
THEN Auto)
Home
Index