---

Step * of Lemma first-25-rationals

map(λn.nth-rational(n);upto(25))
= [0;
   -1;
   1;
   (-1/2);
   -2;
   (1/2);
   (-1/3);
   2;
   (1/3);
   (-1/4);
   -3;
   (-2/3);
   (1/4);
   (-1/5);
   3;
   (-3/2);
   (2/3);
   (1/5);
   (-1/6);
   -4;
   (3/2);
   (-2/5);
   (1/6);
   (-1/7);
   4]
∈ (ℚ List)
BY
{ (Symmetry
   THEN Unfold `upto` 0
   THEN Repeat ((RecUnfold `from-upto` 0 THEN Reduce 0))
   THEN Repeat ((EqCD THEN Try (Trivial)))
   THEN (RW assert_pushupC 0 THENA Auto)
   THEN (BLemma `eqtt_to_assert` THENA Auto)
   THEN Symmetry
   THEN ShowSqEq
   THEN ((RW (AddrC [2] (TagC (mk_tag_term 2)))0 THEN ByComputeAll) ORELSE MemCD ⋅)) }

---

Latex:

---

Latex:
map(\mlambda{}n.nth-rational(n);upto(25))
=  [0;
      -1;
      1;
      (-1/2);
      -2;
      (1/2);
      (-1/3);
      2;
      (1/3);
      (-1/4);
      -3;
      (-2/3);
      (1/4);
      (-1/5);
      3;
      (-3/2);
      (2/3);
      (1/5);
      (-1/6);
      -4;
      (3/2);
      (-2/5);
      (1/6);
      (-1/7);
      4]


By

---

Latex:
(Symmetry
  THEN  Unfold  `upto`  0
  THEN  Repeat  ((RecUnfold  `from-upto`  0  THEN  Reduce  0))
  THEN  Repeat  ((EqCD  THEN  Try  (Trivial)))
  THEN  (RW  assert\_pushupC  0  THENA  Auto)
  THEN  (BLemma  `eqtt\_to\_assert`  THENA  Auto)
  THEN  Symmetry
  THEN  ShowSqEq
  THEN  ((RW  (AddrC  [2]  (TagC  (mk\_tag\_term  2)))0  THEN  ByComputeAll)  ORELSE  MemCD  \mcdot{}))

---

Home Index