induct

(defund fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))

(defun or-dist-induct
  (y n)
  (if (and (integerp n) (>= n 0))
    (if (= n 0)
      y
      (or-dist-induct (fl (/ y 2)) (1- n)))
    nil))

(defun log-induct
  (i j)
  (if (and (integerp i) (>= i 0) (integerp j) (>= j 0))
    (if (or (= i 0) (= j 0))
      nil
      (log-induct (fl (/ i 2)) (fl (/ j 2))))
    nil))

(defun logand-three-args-induct
  (i j k)
  (declare (xargs :measure (acl2-count (abs i))
      :hints (("Goal" :in-theory (enable abs)))))
  (if (and (integerp i) (integerp j) (integerp k))
    (if (or (= i 0) (= j 0) (= k 0) (= i -1) (= j -1) (= k -1))
      nil
      (logand-three-args-induct (fl (/ i 2))
        (fl (/ j 2))
        (fl (/ k 2))))
    nil))

(defun log-induct-allows-negatives
  (i j)
  (if (and (integerp i) (integerp j))
    (if (or (= i 0) (= j 0) (= i -1) (= j -1))
      nil
      (log-induct-allows-negatives (fl (/ i 2)) (fl (/ j 2))))
    nil))

(defun op-dist-induct
  (i j n)
  (if (and (integerp n) (>= n 0))
    (if (= n 0)
      (list i j)
      (op-dist-induct (fl (/ i 2)) (fl (/ j 2)) (1- n)))
    nil))

(defun natp-induct
  (k)
  (if (zp k)
    t
    (natp-induct (1- k))))