Converted from arXiv:math/0312227 by Thomas C. Hales (2003) which is licensed under the Creative Commons Attribution License v1.0.