---

Step * 1 2 of Lemma rcvd-innings-nil


1. V : Type
2. A : Id List
3. L : consensus-rcv(V;A) List
4. i : ℤ
5. n : ℤ
6. filter(λr.n <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List)
7. n ≤ i
8. x : consensus-rcv(V;A)@i
9. (x ∈ L)@i
10. ↑i <z inning(x)@i
11. (x ∈ filter(λr.n <z inning(r);L))
⊢ False
BY
{ ((HypSubst' (-6) (-1) THEN Auto) THEN AutoSimpHyp Auto (-1)) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  L  :  consensus-rcv(V;A)  List
4.  i  :  \mBbbZ{}
5.  n  :  \mBbbZ{}
6.  filter(\mlambda{}r.n  <z  inning(r);L)  =  []
7.  n  \mleq{}  i
8.  x  :  consensus-rcv(V;A)@i
9.  (x  \mmember{}  L)@i
10.  \muparrow{}i  <z  inning(x)@i
11.  (x  \mmember{}  filter(\mlambda{}r.n  <z  inning(r);L))
\mvdash{}  False


By

((HypSubst'  (-6)  (-1)  THEN  Auto)  THEN  AutoSimpHyp  Auto  (-1))

---

Home Index