被三整除

如果一个号码,个别号码加起来能被三整除,它能被三整除
e.g.
111|3, 1+1+1|3

证明方法
100a+10b+c=3k
99a+9b+(a+b+c)=3k
(99a+9b)|3
so (a+b+c)|3

这个证法巧妙，
关键在于要如何把前提100a+10b+c=3k和结论a+b+c=3k‘关联起来。
但是更巧妙的是如何发现a+b+c=3k‘这个结论的。

这个关键在于观察能被三整除的数，得出结论
111，120.

这个观察能被自动化吗？
data mining就是搞这个的。
我们要看的是，当这些数字被apply一个function f
f(111)=f(120)..他们的数是有关系r的，这里的关系是相等。

我们要怎样找到function f和关系r呢？
简单方法是用daikon的方法，
弄template来一个个试。

还有没有更好的方法呢？