(create-canonical-address-list count addr) → *
Given a canonical address
Function:
(defun create-canonical-address-list (count addr) (declare (xargs :guard (natp count))) (let ((__function__ 'create-canonical-address-list)) (declare (ignorable __function__)) (if (or (zp count) (not (canonical-address-p addr))) nil (cons addr (create-canonical-address-list (1- count) (1+ addr))))))
Theorem:
(defthm true-listp-create-canonical-address-list (true-listp (create-canonical-address-list cnt lin-addr)) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm canonical-address-listp-create-canonical-address-list (canonical-address-listp (create-canonical-address-list count addr)) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm create-canonical-address-list-1 (implies (canonical-address-p x) (equal (create-canonical-address-list 1 x) (list x))))
Theorem:
(defthm len-of-create-canonical-address-list (implies (and (canonical-address-p (+ -1 addr count)) (canonical-address-p addr) (natp count)) (equal (len (create-canonical-address-list count addr)) count)))
Theorem:
(defthm car-create-canonical-address-list (implies (and (canonical-address-p addr) (posp count)) (equal (car (create-canonical-address-list count addr)) addr)))
Theorem:
(defthm cdr-create-canonical-address-list (implies (and (canonical-address-p addr) (posp count)) (equal (cdr (create-canonical-address-list count addr)) (create-canonical-address-list (1- count) (1+ addr)))))
Theorem:
(defthm consp-of-create-canonical-address-list (implies (and (canonical-address-p addr) (natp count) (< 0 count)) (consp (create-canonical-address-list count addr))))
Theorem:
(defthm create-canonical-address-list-split (implies (and (canonical-address-p addr) (canonical-address-p (+ k addr)) (natp j) (natp k)) (equal (create-canonical-address-list (+ k j) addr) (append (create-canonical-address-list k addr) (create-canonical-address-list j (+ k addr))))))