---

Step * of Lemma rcos-seq-step

∀[n:ℕ]. (rcos-seq(n + 1) = (rcos-seq(n) + rcos(rcos-seq(n))))
BY
{ (Auto THEN RW (AddrC [1] UnfoldTopAbC) 0) }

1
1. n : ℕ
⊢ primrec(n + 1;(r(1570796326))/1000000000;λi,x. radd_rcos(x)) = (rcos-seq(n) + rcos(rcos-seq(n)))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (rcos-seq(n  +  1)  =  (rcos-seq(n)  +  rcos(rcos-seq(n))))


By

---

Latex:
(Auto  THEN  RW  (AddrC  [1]  UnfoldTopAbC)  0)

---

Home Index