逐次可逆列変換の機械証明 a.k.a. 他人の研究の内容に熱を上げる変なやつらの祭り 基にしている論文は以下の大会の予稿 https://jssst.or.jp/files/user/taikai/2023/papers/15-R-S.pdf 現在の定式化は以下のものがある。 Coq (by chiguri) Agda (by wasabi315) 詳細は各フォルダのREADMEにて。