---

Step * of Lemma new_23_sig_vote_with_ballot_first-assert-forward2

∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e,start:E. ∀n,r:ℤ.
  (start ≤loc e 
  ⇒ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r)
     ⇐⇒ (↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r))
         ∧ (∀e'∈[start;e).¬↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))))
BY
{ (Unfold `vatype` 0
   THEN (Intros
         THEN (RepeatFor 2 (D 0)
               THENA (Auto
                      THEN Try (OnSomeHyp(\i.(FLemma `new_23_sig_vote_with_ballot-assert-type` [i] THEN Complete (Auto))
                                )⋅)⋅
                      )
               )
         )
   THEN All (RWO "new_23_sig_vote_with_ballot_first-forward")⋅
   THEN Auto) }

1
1. Cmd : {T:Type| valueall-type(T)} @i'
2. propose : Atom List@i
3. notify : Atom List@i
4. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)@i'
5. es : EO+(Message(f))@i'
6. e : E@i
7. start : E@i
8. n : ℤ@i
9. r : ℤ@i
10. start ≤loc e @i
11. ↑(new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
∧b (∀e'∈[start;e).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))_b)@i
12. ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
⊢ (∀e'∈[start;e).¬↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))

2
1. Cmd : {T:Type| valueall-type(T)} @i'
2. propose : Atom List@i
3. notify : Atom List@i
4. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)@i'
5. es : EO+(Message(f))@i'
6. e : E@i
7. start : E@i
8. n : ℤ@i
9. r : ℤ@i
10. start ≤loc e @i
11. ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)@i
12. (∀e'∈[start;e).¬↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))@i
⊢ ↑(new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
∧b (∀e'∈[start;e).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))_b)

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}propose,notify:Atom  List.  \mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).
\mforall{}es:EO+(Message(f)).  \mforall{}e,start:E.  \mforall{}n,r:\mBbbZ{}.
    ...


By

---

Latex:
(Unfold  `vatype`  0
  THEN  (Intros
              THEN  (RepeatFor  2  (D  0)
                          THENA  (Auto
                                        THEN  Try  (OnSomeHyp(\mbackslash{}i.(FLemma  `new\_23\_sig\_vote\_with\_ballot-assert-type`  [i]
                                                                                        THEN  Complete  (Auto)
                                                                                        ))\mcdot{})\mcdot{}
                                        )
                          )
              )
  THEN  All  (RWO  "new\_23\_sig\_vote\_with\_ballot\_first-forward")\mcdot{}
  THEN  Auto)

---

Home Index