---

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


1. a : {2...}
2. x : ℤ
3. ¬x < 1
4. 0 < x
5. a^((2 * (x - 1)) + 3) * ((2 * (x - 1)) + 3)! ~ genfact(x - 1;6 * a^3;k.a^2 * ((2 * k) + 3) * ((2 * k) + 2))
⊢ a^((2 * x) + 3) * ((2 * x) + 3)! ~ (a^2 * ((2 * x) + 3) * ((2 * x) + 2))
* a^((2 * (x - 1)) + 3)
* ((2 * (x - 1)) + 3)!
BY
{ ((Subst' ((2 * x) + 3)! ~ ((2 * x) + 3) * ((2 * x) + 2) * ((2 * (x - 1)) + 3)! 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) + 3) ~ a^2 * a^((2 * (x - 1)) + 3) 0 THENM Auto)
   THEN Subst' (2 * x) + 3 ~ 2 + (2 * (x - 1)) + 3 0
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst'  ((2  *  x)  +  3)!  \msim{}  ((2  *  x)  +  3)  *  ((2  *  x)  +  2)  *  ((2  *  (x  -  1))  +  3)!  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)  +  3)  \msim{}  a\^{}2  *  a\^{}((2  *  (x  -  1))  +  3)  0  THENM  Auto)
  THEN  Subst'  (2  *  x)  +  3  \msim{}  2  +  (2  *  (x  -  1))  +  3  0
  THEN  Auto)

---

Home Index