全域性を証明するために尺度を導入します 関数が再帰的に呼び出されるたびに尺度が減少することを示すことによって いつかは再帰が終わることを証明します 無限下降法的な何か？ sizeはリストを作るために必要なconsの数でした 以下のような公理を使って全域…