---

Step * 1 2 1 1 2 of Lemma cosine-approx-lemma


1. a : {2...}
2. x : ℤ
3. ¬x < 1
4. 0 < x
5. a^((2 * (x - 1)) + 2) * ((2 * (x - 1)) + 2)! ~ genfact(x - 1;2 * a^2;k.a^2 * ((2 * k) + 2) * ((2 * k) + 1))
⊢ a^((2 * x) + 2) * ((2 * x) + 2)! ~ (a^2 * ((2 * x) + 2) * ((2 * x) + 1))
* a^((2 * (x - 1)) + 2)
* ((2 * (x - 1)) + 2)!
BY
{ ((Subst' ((2 * x) + 2)! ~ ((2 * x) + 2) * ((2 * x) + 1) * ((2 * (x - 1)) + 2)! 0
    THENA (RepeatFor 2 (((RW (AddrC [1] (LemmaC `fact_unroll`)) 0 THENA Auto)
                         THEN (OReduce 0 THENA Auto)
                         THEN EqCD
                         THEN Try (Trivial)))
           THEN Auto
           )
    )
   THEN (Subst' a^((2 * x) + 2) ~ a^2 * a^((2 * (x - 1)) + 2) 0 THENM Auto)
   THEN Subst' (2 * x) + 2 ~ 2 + (2 * (x - 1)) + 2 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \{2...\}
2.  x  :  \mBbbZ{}
3.  \mneg{}x  <  1
4.  0  <  x
5.  a\^{}((2  *  (x  -  1))  +  2)  *  ((2  *  (x  -  1))  +  2)!  \msim{}  genfact(x  -  1;2  *  a\^{}2;k.a\^{}2
*  ((2  *  k)  +  2)
*  ((2  *  k)  +  1))
\mvdash{}  a\^{}((2  *  x)  +  2)  *  ((2  *  x)  +  2)!  \msim{}  (a\^{}2  *  ((2  *  x)  +  2)  *  ((2  *  x)  +  1))
*  a\^{}((2  *  (x  -  1))  +  2)
*  ((2  *  (x  -  1))  +  2)!


By

---

Latex:
((Subst'  ((2  *  x)  +  2)!  \msim{}  ((2  *  x)  +  2)  *  ((2  *  x)  +  1)  *  ((2  *  (x  -  1))  +  2)!  0
    THENA  (RepeatFor  2  (((RW  (AddrC  [1]  (LemmaC  `fact\_unroll`))  0  THENA  Auto)
                                              THEN  (OReduce  0  THENA  Auto)
                                              THEN  EqCD
                                              THEN  Try  (Trivial)))
                  THEN  Auto
                  )
    )
  THEN  (Subst'  a\^{}((2  *  x)  +  2)  \msim{}  a\^{}2  *  a\^{}((2  *  (x  -  1))  +  2)  0  THENM  Auto)
  THEN  Subst'  (2  *  x)  +  2  \msim{}  2  +  (2  *  (x  -  1))  +  2  0
  THEN  Auto)

---

Home Index