ラドーさんがず〜っと昔にビジービーバー関数の存在を証明してます