A
Function:
(defun abstract-dot/dash-1*bit (tree) (declare (xargs :guard (treep tree))) (b* (((fun (fail)) (prog2$ (abstract-fail) 0)) ((unless (tree-case tree :nonleaf)) (fail)) (treess (tree-nonleaf->branches tree)) ((unless (and (consp treess) (consp (cdr treess)))) (fail))) (abstract-*bit (cadr treess))))
Theorem:
(defthm natp-of-abstract-dot/dash-1*bit (b* ((nat (abstract-dot/dash-1*bit tree))) (natp nat)) :rule-classes :rewrite)