termination-theorem-dollar-tests

(in-package "ACL2")

(assert-equal (termination-theorem$ 'len state)
  '(if (o-p (acl2-count x))
    (if (not (consp x))
      't
      (o< (acl2-count (cdr x)) (acl2-count x)))
    'nil))

(assert-equal (car (termination-theorem$ 'cons state))
  :failed)