---

Step * 1 of Lemma round-robin-onto


1. [T] : Type
2. L : T List
3. i : ℕ||L||
⊢ ∃b:ℕ. (L[i] = (round-robin(L) b) ∈ T)
BY
{ (With ⌜i⌝ (D 0)⋅ THEN Auto THEN RepUR ``round-robin`` 0 THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  i  :  \mBbbN{}||L||
\mvdash{}  \mexists{}b:\mBbbN{}.  (L[i]  =  (round-robin(L)  b))


By

---

Latex:
(With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  RepUR  ``round-robin``  0  THEN  EqCD  THEN  Auto)

---

Home Index