---

Step * of Lemma no_repeats_from-upto

∀[n1,n2:ℤ].  no_repeats(ℤ;[n1, n2))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `no_repeats` 0
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN (RWO "length-from-upto" (-4) THENA Auto)
   THEN (RWO "length-from-upto" (-3) THENA Auto)
   THEN RepeatFor 2 ((SplitOnHypITE (-4) THEN Auto))
   THEN RWO "select-from-upto" (-3)
   THEN Auto
   THEN D (-4)
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[n1,n2:\mBbbZ{}].    no\_repeats(\mBbbZ{};[n1,  n2))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `no\_repeats`  0
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "length-from-upto"  (-4)  THENA  Auto)
  THEN  (RWO  "length-from-upto"  (-3)  THENA  Auto)
  THEN  RepeatFor  2  ((SplitOnHypITE  (-4)  THEN  Auto))
  THEN  RWO  "select-from-upto"  (-3)
  THEN  Auto
  THEN  D  (-4)
  THEN  Auto')

---

Home Index