(every-bird-in-hole bird max-hole) → clauses
Function:
(defun every-bird-in-hole (bird max-hole) (declare (xargs :guard (and (natp bird) (natp max-hole)))) (let ((__function__ 'every-bird-in-hole)) (declare (ignorable __function__)) (b* (((when (zp bird)) nil) (bird (- bird 1))) (cons (bird-in-some-hole bird max-hole) (every-bird-in-hole bird max-hole)))))
Theorem:
(defthm lit-list-listp-of-every-bird-in-hole (b* ((clauses (every-bird-in-hole bird max-hole))) (lit-list-listp clauses)) :rule-classes :rewrite)