Step
*
1
2
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)
⊢ if first(e) then <[], []>
if pred(e) ∈b new_23_sig_vote'base(Cmd;notify;propose;f)
then new_23_sig_add_to_quorum(Cmd) <n, r> loc(e) new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e)
new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es;pred(e))
else new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es;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);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);e)))
>
∈ (Cmd List × (Id List))
BY
{ (Repeat SimpleSplit
THEN Try (Complete ((Assert ⌈False⌉⋅ THEN Auto)))
THEN (RW (SweepUpC (AddrC [3] (LemmaC `es-closed-open-interval-decomp-last`))) 0
THENA (Auto
THEN AllReduce
THEN Try (FLemma `new_23_sig_vote_with_ballot_first-assert-type` [-1])
THEN Try (BLemma `es-init-locl`)
THEN Auto
THEN ProveSingleVal)
)
THEN (RWO "mapfilter-append" 0 THENA Auto)
THEN (RWO "mapfilter-singleton" 0 THENA Auto)
THEN SimpleSplit
THEN AllReduce
THEN (RWO "-5" 0
THENA (Auto
THEN AllReduce
THEN Try (ProveSingleVal)
THEN FLemma `new_23_sig_vote_with_ballot_first-assert-type` [-1]
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. 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))
2
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)))
@ [])
, 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)))
@ [])
>
∈ (Cmd List × (Id List))
3
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)
⊢ <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))
4
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)
⊢ <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)))
@ [])
, 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)))
@ [])
>
∈ (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)
\mvdash{} if first(e) then <[], []>
if pred(e) \mmember{}\msubb{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)
then new\_23\_sig\_add\_to\_quorum(Cmd) <n, r> loc(e) new\_23\_sig\_vote'base(Cmd;notify;propose;f)@pred(e\000C)
new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n, r>es;pred(e))
else new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n, r>es;pred(e))
fi
= <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);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);e)))
>
By
Latex:
(Repeat SimpleSplit
THEN Try (Complete ((Assert \mkleeneopen{}False\mkleeneclose{}\mcdot{} THEN Auto)))
THEN (RW (SweepUpC (AddrC [3] (LemmaC `es-closed-open-interval-decomp-last`))) 0
THENA (Auto
THEN AllReduce
THEN Try (FLemma `new\_23\_sig\_vote\_with\_ballot\_first-assert-type` [-1])
THEN Try (BLemma `es-init-locl`)
THEN Auto
THEN ProveSingleVal)
)
THEN (RWO "mapfilter-append" 0 THENA Auto)
THEN (RWO "mapfilter-singleton" 0 THENA Auto)
THEN SimpleSplit
THEN AllReduce
THEN (RWO "-5" 0
THENA (Auto
THEN AllReduce
THEN Try (ProveSingleVal)
THEN FLemma `new\_23\_sig\_vote\_with\_ballot\_first-assert-type` [-1]
THEN Auto)
))
Home
Index