まずmeasureを定義。関数定義はlispと同様でdefun。アイデアとしては、まずab and b ACL2 !>(defun m (a b c) (if (and (integerp a) (integerp b) (integerp c)) (if (<= a b) 0 (if (<= b c) (cons (cons 1 1) (- a b)) (cons (cons 1 2) (- a b)))) 0))こ…

連続体濃度がアレフ２より大きくなって欲しくない理由 - くるるの数学ノートid:w2allenさんにコメント欄で質問を受けたのをこちらに持ってきます。 今の話を身近な数の世界で考えると、アレフ０は自然数の濃度、アレフ２は実数の濃度となります。そして、ア…