Step
*
1
2
1
of Lemma
new_23_sig_quorum_state_eq1
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. n : ℤ@i
13. r : ℤ@i
14. e : E@i
15. ∀e1:E
((e1 < e)
⇒ (new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es;e1)
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e1);e1)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e1);e1)))
>
∈ (Cmd List × (Id List))))
16. ¬↑first(e)
17. ¬↑first(e)
18. ↑pred(e) ∈b new_23_sig_vote'base(Cmd;notify;propose;f)
19. ↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;pred(e);n;r)
⊢ (new_23_sig_add_to_quorum(Cmd) <n, r> loc(e) new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e)
<rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;pred(e));pred(e))))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;pred(e));pred(e))))
>)
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e);pred(e)))
@ [snd(fst(msgval(pred(e))))])
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e);pred(e)))
@ [snd(msgval(pred(e)))])
>
∈ (Cmd List × (Id List))
BY
{ (RepUR ``new_23_sig_add_to_quorum new_23_sig_newvote`` 0
THEN (FLemma `member-implies-classrel` [-2] THENA Auto)
THEN SquashExRepD
THEN DProdsAndUnions
THEN (FLemma `new_23_sig_vote_with_ballot-if-classrel` [-1] THENA Auto)
THEN (FLemma `new_23_sig_vote_with_ballot-assert-type` [-1] THENA 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. n : ℤ@i
13. r : ℤ@i
14. e : E@i
15. ∀e1:E
((e1 < e)
⇒ (new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es;e1)
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e1);e1)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e1);e1)))
>
∈ (Cmd List × (Id List))))
16. ¬↑first(e)
17. ¬↑first(e)
18. ↑pred(e) ∈b new_23_sig_vote'base(Cmd;notify;propose;f)
19. ↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;pred(e);n;r)
20. v5 : ℤ
21. v6 : ℤ
22. v4 : Cmd
23. v2 : Id
24. <<<v5, v6>, v4>, v2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(pred(e))
25. ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;pred(e);v5;v6)
26. has-es-info-type(es;pred(e);f;ℤ × ℤ × Cmd × Id)
⊢ if let ze,sender = new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e)
in let ni',c = ze
in (product-deq(ℤ;ℤ;IntDeq;IntDeq) <n, r> ni')
∧b (¬bsender ∈b rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;pred(e));pred(e))))))
then new_23_sig_addvote(Cmd) new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e)
<rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;pred(e));pred(e))))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;pred(e));pred(e))))
>
else <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;pred(e));pred(e))))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;pred(e));pred(e))))
>
fi
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e);pred(e)))
@ [snd(fst(msgval(pred(e))))])
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e);pred(e)))
@ [snd(msgval(pred(e)))])
>
∈ (Cmd List × (Id List))
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. n : \mBbbZ{}@i
13. r : \mBbbZ{}@i
14. e : E@i
15. \mforall{}e1:E
((e1 < e)
{}\mRightarrow{} (new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n, r>es;e1)
= <rev(mapfilter(\mlambda{}e.(snd(fst(msgval(e))));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e1);e1)))
, rev(mapfilter(\mlambda{}e.(snd(msgval(e)));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e1);e1)))
>))
16. \mneg{}\muparrow{}first(e)
17. \mneg{}\muparrow{}first(e)
18. \muparrow{}pred(e) \mmember{}\msubb{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)
19. \muparrow{}new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;pred(e);n;r)
\mvdash{} (new\_23\_sig\_add\_to\_quorum(Cmd) <n, r> loc(e) new\_23\_sig\_vote'base(Cmd;notify;propose;f)@pred(e)
<rev(mapfilter(\mlambda{}e.(snd(fst(msgval(e))));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;pred(e));pred(e))))
, rev(mapfilter(\mlambda{}e.(snd(msgval(e)));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;pred(e));pred(e))))
>)
= <rev(mapfilter(\mlambda{}e.(snd(fst(msgval(e))));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e);pred(e)))
@ [snd(fst(msgval(pred(e))))])
, rev(mapfilter(\mlambda{}e.(snd(msgval(e)));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e);pred(e)))
@ [snd(msgval(pred(e)))])
>
By
Latex:
(RepUR ``new\_23\_sig\_add\_to\_quorum new\_23\_sig\_newvote`` 0
THEN (FLemma `member-implies-classrel` [-2] THENA Auto)
THEN SquashExRepD
THEN DProdsAndUnions
THEN (FLemma `new\_23\_sig\_vote\_with\_ballot-if-classrel` [-1] THENA Auto)
THEN (FLemma `new\_23\_sig\_vote\_with\_ballot-assert-type` [-1] THENA Auto))
Home
Index