[isabelle] Help on Proof



Hello,

Can Isabelle do a proof for the following recursion:

a(0)=a(1)=a(2)=1; a(n)=((n^3 - 6 n^2 + 12 n - 7)*a(n - 3) + (-3 n^3 + 15 n^2
- 25 n + 14)*
     a(n - 2) + (3 n^3 - 12 n^2 + 15 n - 6)*a(n - 1))/(n (n - 1) (n - 2))

Prove that, for all n ≥ 1, abs(a(n)-(n+1)/3) < 2/(sqrt(3n)).

Unfortunately, I don't have the bandwidth to download the software; it would
be greatly appreciated if somebody could input this into Isabelle and email
me the output.

Thanks,
Howard




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.