Step
*
1
2
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)
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)))
@ [])
, 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))
BY
{ ((InstLemma `pair-eta` [⌜new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e)⌝]⋅
THENA (GenConclAtAddr [2] THEN Auto THEN ProveSingleVal)
)
THEN HypSubst (-1) 0
THEN Thin (-1)
THEN Reduce 0
THEN (InstLemma `pair-eta` [⌜fst(new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e))⌝]⋅
THENA (GenConclAtAddr [2;1] THEN Auto THEN ProveSingleVal)
)
THEN HypSubst (-1) 0
THEN Thin (-1)
THEN Reduce 0) }
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 (product-deq(ℤ;ℤ;IntDeq;IntDeq) <n, r> (fst(fst(new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e)))))
∧b (¬bsnd(new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e)) ∈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)
<<fst(fst(new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e)))
, snd(fst(new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e)))
>
, snd(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)))
@ [])
, 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)
17. \mneg{}\muparrow{}first(e)
18. \muparrow{}pred(e) \mmember{}\msubb{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)
19. \mneg{}\muparrow{}new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;pred(e);n;r)
20. v5 : \mBbbZ{}
21. v6 : \mBbbZ{}
22. v4 : Cmd
23. v2 : Id
24. <<<v5, v6>, v4>, v2> \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(pred(e))
25. \muparrow{}new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;pred(e);v5;v6)
26. has-es-info-type(es;pred(e);f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
\mvdash{} if let ze,sender = new\_23\_sig\_vote'base(Cmd;notify;propose;f)@pred(e)
in let ni',c = ze
in (product-deq(\mBbbZ{};\mBbbZ{};IntDeq;IntDeq) <n, r> ni')
\mwedge{}\msubb{} (\mneg{}\msubb{}sender \mmember{}\msubb{}
rev(mapfilter(\mlambda{}e.(snd(msgval(e)));
...;
[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(\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))))
>
else <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))))
>
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);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)))
@ [])
>
By
Latex:
((InstLemma `pair-eta` [\mkleeneopen{}new\_23\_sig\_vote'base(Cmd;notify;propose;f)@pred(e)\mkleeneclose{}]\mcdot{}
THENA (GenConclAtAddr [2] THEN Auto THEN ProveSingleVal)
)
THEN HypSubst (-1) 0
THEN Thin (-1)
THEN Reduce 0
THEN (InstLemma `pair-eta` [\mkleeneopen{}fst(new\_23\_sig\_vote'base(Cmd;notify;propose;f)@pred(e))\mkleeneclose{}]\mcdot{}
THENA (GenConclAtAddr [2;1] THEN Auto THEN ProveSingleVal)
)
THEN HypSubst (-1) 0
THEN Thin (-1)
THEN Reduce 0)
Home
Index