OAI.ThreeMachine.main_theorem