The computer programs used in the proof are in the file ada.tgz