Rip-ret-alistp
Recognizer for the oracle sub-field of the environment
field env
- Signature
(rip-ret-alistp lst) → *
A valid rip-ret-alistp associates canonical linear
addresses, i.e., 48-bit integers in our specification, to a list
of arbitrary values. For example, '((1 . ((-1 . 12) 5000)) (2
. (0))) means that if the oracle in the environment field is
consulted at address 1, '(-1 . 12) will be
popped out. If the oracle is consulted again at the address
1, then 5000 will be popped out.
Definitions and Theorems
Function: rip-ret-alistp
(defun rip-ret-alistp (lst)
(declare (xargs :guard t))
(let ((__function__ 'rip-ret-alistp))
(declare (ignorable __function__))
(if (atom lst)
(equal lst nil)
(and (consp (car lst))
(i48p (caar lst))
(true-listp (cdar lst))
(rip-ret-alistp (cdr lst))))))
Theorem: rip-ret-alistp-fwd-chaining-alistp
(defthm rip-ret-alistp-fwd-chaining-alistp
(implies (rip-ret-alistp x) (alistp x))
:rule-classes :forward-chaining)
