|
|
|---|
|
|
|
|---|
(pos-fix x) is a fixing function for posp: it is the identity for positive integers, or returns 1 for any other object.
This has guard
Function:
(defun pos-fix (x) (declare (xargs :guard t)) (if (posp x) x 1))
Theorem:
(defthm posp-of-pos-fix (posp (pos-fix x)) :rule-classes :type-prescription)
Theorem:
(defthm pos-fix-when-posp (implies (posp x) (equal (pos-fix x) x)))