SPINを業務へ使用してみたくなったので、SPIN初ネタを見直した。
初ネタでは証明が失敗した時の反例を数えることを予定していたが上手く行かず。。汗）
よくよく考えると反例を過不足無く出力って、補集合を出力ですか！！
「おとなの階段登る～～♪♪君はtype論理さ～～♪♪」
階数が１個上がるだな。自然数も扱ってるし。。
SPINにそこまで要求するのは酷なんでしょうね。
初ネタは反例が何個か出てきた事でOKとします。
次のねた考えます。
SPIN モデル検証 回路検証
