Step
*
1
1
of Lemma
new_23_sig_quorum_state_eq1-forward
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. start : E@i
14. n : ℤ@i
15. r : ℤ@i
16. start ≤loc e @i
17. new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es.start;e)
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
>
∈ (Cmd List × (Id List))
⊢ <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
>
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[start;e)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[start;e)))
>
∈ (Cmd List × (Id List))
BY
{ RepeatFor 2 ((EqCD THEN Try (Trivial))) }
1
.....implicit subterm.....
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. start : E@i
14. n : ℤ@i
15. r : ℤ@i
16. start ≤loc e @i
17. new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es.start;e)
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
>
∈ (Cmd List × (Id List))
⊢ Cmd = Cmd ∈ Type
2
.....subterm..... T:t
1:n
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. start : E@i
14. n : ℤ@i
15. r : ℤ@i
16. start ≤loc e @i
17. new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es.start;e)
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
>
∈ (Cmd List × (Id List))
⊢ mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e))
= mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[start;e))
∈ (Cmd List)
3
.....implicit subterm.....
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. start : E@i
14. n : ℤ@i
15. r : ℤ@i
16. start ≤loc e @i
17. new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es.start;e)
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
>
∈ (Cmd List × (Id List))
⊢ Id = Id ∈ Type
4
.....subterm..... T:t
1:n
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. start : E@i
14. n : ℤ@i
15. r : ℤ@i
16. start ≤loc e @i
17. new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es.start;e)
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
>
∈ (Cmd List × (Id List))
⊢ mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e))
= mapfilter(λe.(snd(msgval(e)));λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);[start;e))
∈ (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. e : E@i
13. start : E@i
14. n : \mBbbZ{}@i
15. r : \mBbbZ{}@i
16. start \mleq{}loc e @i
17. new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n, r>es.start;e)
= <rev(mapfilter(\mlambda{}e.(snd(fst(msgval(e))));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
, rev(mapfilter(\mlambda{}e.(snd(msgval(e)));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
>
\mvdash{} <rev(mapfilter(\mlambda{}e.(snd(fst(msgval(e))));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
, rev(mapfilter(\mlambda{}e.(snd(msgval(e)));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es.start;e;n;r);
[es-init(es.start;e);e)))
>
= <rev(mapfilter(\mlambda{}e.(snd(fst(msgval(e))));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es.start;e;n;r);
[start;e)))
, rev(mapfilter(\mlambda{}e.(snd(msgval(e)));
\mlambda{}e.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es.start;e;n;r);
[start;e)))
>
By
Latex:
RepeatFor 2 ((EqCD THEN Try (Trivial)))
Home
Index