List of type prescription rules for the shallowly embedded predicates for the relations called by the definition being lifted.
(lift-thm-type-prescriptions-for-called-preds rels state) → rules
We need the fact that they are booleans in the proofs of the lifting theorems.
Function:
(defun lift-thm-type-prescriptions-for-called-preds (rels state) (declare (xargs :stobjs (state))) (declare (xargs :guard (string-listp rels))) (let ((__function__ 'lift-thm-type-prescriptions-for-called-preds)) (declare (ignorable __function__)) (b* (((when (endp rels)) nil) (rel (car rels)) (pred-name (name-to-symbol rel state)) (rule (cons ':t (cons pred-name 'nil))) (rules (lift-thm-type-prescriptions-for-called-preds (cdr rels) state))) (cons rule rules))))
Theorem:
(defthm true-listp-of-lift-thm-type-prescriptions-for-called-preds (b* ((rules (lift-thm-type-prescriptions-for-called-preds rels state))) (true-listp rules)) :rule-classes :rewrite)