Step
*
2
of Lemma
new_23_sig_replica_state_from_proposal
1. Cmd : {T:Type| valueall-type(T)} @i'
2. notify : Atom List@i
3. propose : Atom List@i
4. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)@i'
5. (f propose) = (ℤ × Cmd) ∈ Type
6. (f notify) = (ℤ × Cmd) ∈ Type
7. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
8. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
9. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
10. f ∈ Name ─→ Type
11. es : EO+(Message(f))@i'
12. e : E@i
13. slots : set-sig{i:l}(ℤ)@i'
14. s : set-sig-set(slots)@i
15. s ∈
Memory-loc-class(new_23_sig_update_replica(Cmd;slots);λloc.{set-sig-empty(slots)};...)(e)
16. a1 : ℤ@i
17. a2 : Cmd@i
18. e' : E@i
19. s1 : set-sig-set(slots)@i
20. (e' <loc e)@i
21. <a1, a2> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')@i
22. s1 ∈
Memory-loc-class(new_23_sig_update_replica(Cmd;slots);λloc.{set-sig-empty(slots)};...)(e')@i
23. ∀n:ℤ
((↑(set-sig-member(slots) n s1))
⇒ (∃e':E
∃c:Cmd
((e' <loc e)
∧ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
∧ (¬↑(set-sig-member(slots) n
let x,y = new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) es e'
in x)))))@i
24. n : ℤ@i
25. n = a1 ∈ ℤ
⊢ ∃e':E
∃c:Cmd
((e' <loc e)
∧ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
∧ (¬↑(set-sig-member(slots) n let x,y = new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) es e' in x)))
BY
{ ((Decide ⌈↑(set-sig-member(slots) n s1)⌉⋅ THENA Auto)
THEN Try (Complete ((BackThruSomeHyp THEN Auto)))
THEN (Assert ⌈∀e':Top
(let x,y = new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) es e'
in x ~ new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))⌉⋅
THENA (RepUR ``new_23_sig_ReplicaStateFun classfun sv-bag-only hd pi1`` 0 THEN Auto)
)
THEN (RWO "-1" 0 THENA Auto)
THEN InstConcl [⌈e'⌉;⌈a2⌉]⋅
THEN Auto) }
1
1. Cmd : {T:Type| valueall-type(T)} @i'
2. notify : Atom List@i
3. propose : Atom List@i
4. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)@i'
5. (f propose) = (ℤ × Cmd) ∈ Type
6. (f notify) = (ℤ × Cmd) ∈ Type
7. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
8. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
9. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
10. f ∈ Name ─→ Type
11. es : EO+(Message(f))@i'
12. e : E@i
13. slots : set-sig{i:l}(ℤ)@i'
14. s : set-sig-set(slots)@i
15. s ∈
Memory-loc-class(new_23_sig_update_replica(Cmd;slots);λloc.{set-sig-empty(slots)};...)(e)
16. a1 : ℤ@i
17. a2 : Cmd@i
18. e' : E@i
19. s1 : set-sig-set(slots)@i
20. (e' <loc e)@i
21. <a1, a2> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')@i
22. s1 ∈
Memory-loc-class(new_23_sig_update_replica(Cmd;slots);λloc.{set-sig-empty(slots)};...)(e')@i
23. ∀n:ℤ
((↑(set-sig-member(slots) n s1))
⇒ (∃e':E
∃c:Cmd
((e' <loc e)
∧ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
∧ (¬↑(set-sig-member(slots) n
let x,y = new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) es e'
in x)))))@i
24. n : ℤ@i
25. n = a1 ∈ ℤ
26. ¬↑(set-sig-member(slots) n s1)
27. ∀e':Top
(let x,y = new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) es e'
in x ~ new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
28. (e' <loc e)
29. <n, a2> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
⊢ ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
Latex:
Latex:
1. Cmd : \{T:Type| valueall-type(T)\} @i'
2. notify : Atom List@i
3. propose : Atom List@i
4. f : new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)@i'
5. (f propose) = (\mBbbZ{} \mtimes{} Cmd)
6. (f notify) = (\mBbbZ{} \mtimes{} Cmd)
7. (f ``new\_23\_sig decided``) = (\mBbbZ{} \mtimes{} Cmd)
8. (f ``new\_23\_sig retry``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
9. (f ``new\_23\_sig vote``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
10. f \mmember{} Name {}\mrightarrow{} Type
11. es : EO+(Message(f))@i'
12. e : E@i
13. slots : set-sig\{i:l\}(\mBbbZ{})@i'
14. s : set-sig-set(slots)@i
15. s \mmember{}
Memory-loc-class(new\_23\_sig\_update\_replica(Cmd;slots);\mlambda{}loc.\{set-sig-empty(slots)\};...)(e)
16. a1 : \mBbbZ{}@i
17. a2 : Cmd@i
18. e' : E@i
19. s1 : set-sig-set(slots)@i
20. (e' <loc e)@i
21. <a1, a2> \mmember{} new\_23\_sig\_Proposal(Cmd;notify;propose;f)(e')@i
22. s1 \mmember{}
Memory-loc-class(new\_23\_sig\_update\_replica(Cmd;slots);\mlambda{}loc.\{set-sig-empty(slots)\};...)(e')@i
23. \mforall{}n:\mBbbZ{}
((\muparrow{}(set-sig-member(slots) n s1))
{}\mRightarrow{} (\mexists{}e':E
\mexists{}c:Cmd
((e' <loc e)
\mwedge{} <n, c> \mmember{} new\_23\_sig\_Proposal(Cmd;notify;propose;f)(e')
\mwedge{} (\mneg{}\muparrow{}(set-sig-member(slots) n
let x,y = new\_23\_sig\_ReplicaState(Cmd;notify;propose;slots;f) es e'
in x)))))@i
24. n : \mBbbZ{}@i
25. n = a1
\mvdash{} \mexists{}e':E
\mexists{}c:Cmd
((e' <loc e)
\mwedge{} <n, c> \mmember{} new\_23\_sig\_Proposal(Cmd;notify;propose;f)(e')
\mwedge{} (\mneg{}\muparrow{}(set-sig-member(slots) n
let x,y = new\_23\_sig\_ReplicaState(Cmd;notify;propose;slots;f) es e'
in x)))
By
Latex:
((Decide \mkleeneopen{}\muparrow{}(set-sig-member(slots) n s1)\mkleeneclose{}\mcdot{} THENA Auto)
THEN Try (Complete ((BackThruSomeHyp THEN Auto)))
THEN (Assert \mkleeneopen{}\mforall{}e':Top
(let x,y = new\_23\_sig\_ReplicaState(Cmd;notify;propose;slots;f) es e'
in x \msim{} new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))\mkleeneclose{}\mcdot{}
THENA (RepUR ``new\_23\_sig\_ReplicaStateFun classfun sv-bag-only hd pi1`` 0 THEN Auto)
)
THEN (RWO "-1" 0 THENA Auto)
THEN InstConcl [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index