(in-package "ACL2")

(defstub nils (*) => *)

(defaxiom nils-axiom
  (equal (nils x)
         (if (equal x 0)
             nil
           (cons nil (nils (- x 1)))))
  :rule-classes nil)

(defthm len-cons
    (equal (len (cons x y))
           (+ 1 (len y))))


(defun induct-hint (k n)
  (if (zp k)
      (list k n)
    (induct-hint (- k 1)(- n 1))))

(defthm nil-at-neg-input
  (implies (and (< x 0)
                (integerp k))
           (> (len (nils x)) k))
  :rule-classes nil
  :hints (("Goal"
           :induct (induct-hint k x))
          ("Subgoal *1/2"
           :use nils-axiom)
          ("Subgoal *1/1"
           :use nils-axiom)))


(defthm OUCH!!
    nil
    :rule-classes nil
    :hints (("Goal"
	     :use (:instance
		   nil-at-neg-input
		   (x -1)
		   (k (len (nils -1)))))))