---

Step * of Lemma round-robin-equal

∀[L:Top List]. ∀[b:ℕ]. (round-robin(L) (b + ||L||) ~ round-robin(L) b) supposing 0 < ||L||
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``round-robin`` 0
   THEN EqCD
   THEN Auto
   THEN (InstLemma `rem_invariant` [⌜b⌝;⌜1⌝;⌜||L||⌝]⋅ THENA Auto)
   THEN NthHypSq (-1)
   THEN RepeatFor 3 (EqCD)
   THEN Auto
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[b:\mBbbN{}].  (round-robin(L)  (b  +  ||L||)  \msim{}  round-robin(L)  b)  supposing  0  <  ||L||


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``round-robin``  0
  THEN  EqCD
  THEN  Auto
  THEN  (InstLemma  `rem\_invariant`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}||L||\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  3  (EqCD)
  THEN  Auto
  THEN  Auto')

---

Home Index