OAI.Tachikawa.main_theorem