mult - ACL2 Book

Included Books

top-with-meta ihs-definitions ihs-lemmas structures array1 @logops list-defuns list-defthms deflist defalist meta-lemmas

other

(in-package "ACL2")

other

(set-irrelevant-formals-ok t)

include-book

(include-book "arithmetic/top-with-meta" :dir :system)

include-book

(include-book "ihs/ihs-definitions" :dir :system)

include-book

(include-book "ihs/ihs-lemmas" :dir :system)

include-book

(include-book "data-structures/structures" :dir :system)

include-book

(include-book "data-structures/array1" :dir :system)

include-book

(include-book "ihs/@logops" :dir :system)

include-book

(include-book "data-structures/list-defuns" :dir :system)

include-book

(include-book "data-structures/list-defthms" :dir :system)

include-book

(include-book "data-structures/deflist" :dir :system)

include-book

(include-book "data-structures/defalist" :dir :system)

include-book

(include-book "meta-lemmas")

other

(minimal-ihs-theory)

in-theory

(in-theory (enable @logops-theory array1-lemmas meta-lemma-theory))

other

(enable-theory (definition-free-theory (theory 'list-defuns)))

other

(enable-theory (definition-free-theory (theory 'alist-defuns)))

in-theory

(in-theory (disable (force)))

in-theory

(in-theory (enable nth-update-nth))

sub1-inductionfunction

(defun sub1-induction
  (x)
  (if (zp x)
    x
    (sub1-induction (1- x))))

sub1-logcdr-inductionfunction

(defun sub1-logcdr-induction
  (m x)
  (if (zp m)
    x
    (sub1-logcdr-induction (1- m) (logcdr x))))

logcdr-logcdr-inductionfunction

(defun logcdr-logcdr-induction
  (b c)
  (declare (xargs :measure (abs (ifix b))
      :hints (("goal" :in-theory (enable logcdr)))))
  (if (or (equal b -1) (zip b))
    c
    (logcdr-logcdr-induction (logcdr b) (logcdr c))))

sub1-sub1-logcdr-inductionfunction

(defun sub1-sub1-logcdr-induction
  (a b v)
  (if (zp b)
    (or a v)
    (sub1-sub1-logcdr-induction (1- a) (1- b) (logcdr v))))

sub1-logcdr-logcdr-inductionfunction

(defun sub1-logcdr-logcdr-induction
  (m x y)
  (if (zp m)
    (or x y)
    (sub1-logcdr-logcdr-induction (1- m) (logcdr x) (logcdr y))))

sub1-sub1-inductionfunction

(defun sub1-sub1-induction
  (m n)
  (if (zp m)
    n
    (sub1-sub1-induction (1- m) (1- n))))

sub1-logcdr-logcdr-carry-inductionfunction

(defun sub1-logcdr-logcdr-carry-induction
  (m x y c)
  (if (zp m)
    (or x y c)
    (sub1-logcdr-logcdr-carry-induction (1- m)
      (logcdr x)
      (logcdr y)
      (if (or (and (equal (logcar x) 1) (equal (logcar y) 1))
          (and (equal (logcar x) 1) (equal c 1))
          (and (equal (logcar y) 1) (equal c 1)))
        1
        0))))

unsigned-byte-p-<=theorem

(defthm unsigned-byte-p-<=
  (equal (unsigned-byte-p bits i)
    (and (integerp bits)
      (>= bits 0)
      (integerp i)
      (>= i 0)
      (<= i (1- (expt 2 bits)))))
  :rule-classes :definition :hints (("goal" :in-theory (enable unsigned-byte-p))))

signed-byte-p-<=theorem

(defthm signed-byte-p-<=
  (equal (signed-byte-p bits i)
    (and (integerp bits)
      (> bits 0)
      (integerp i)
      (>= i (- (expt 2 (- bits 1))))
      (<= i (1- (expt 2 (- bits 1))))))
  :rule-classes :definition :hints (("goal" :in-theory (enable signed-byte-p))))

in-theory

(in-theory (disable unsigned-byte-p-<= signed-byte-p-<=))

ash-*2-simplifytheorem

(defthm ash-*2-simplify
  (implies (and (integerp x) (integerp n) (<= 0 n))
    (equal (ash (* 2 x) n) (* 2 (ash x n))))
  :hints (("goal" :in-theory (enable ash))))

in-theory

(in-theory (disable ash-*2-simplify))

*ark*-ifix-ashtheorem

(defthm *ark*-ifix-ash (equal (ifix (ash x y)) (ash x y)))

*ark*-open-logconstheorem

(defthm *ark*-open-logcons
  (implies (syntaxp (constant-syntaxp b))
    (equal (logcons b i)
      (let ((b (bfix b)) (i (ifix i)))
        (+ b (* 2 i)))))
  :hints (("goal" :in-theory (enable logcons))))

*ark*-sum-constantstheorem

(defthm *ark*-sum-constants
  (implies (and (syntaxp (constant-syntaxp x))
      (syntaxp (constant-syntaxp y))
      (equal sum (+ x y)))
    (equal (+ x y z) (+ sum z))))

*ark*-ash-+-postheorem

(defthm *ark*-ash-+-pos
  (implies (and (integerp x) (integerp y) (integerp m) (<= 0 m))
    (equal (ash (+ x y) m) (+ (ash x m) (ash y m))))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory)
     :induct (sub1-induction m))))

in-theory

(in-theory (disable *ark*-ash-+-pos))

logtail-+-ashtheorem

(defthm logtail-+-ash
  (implies (and (integerp n1)
      (integerp n2)
      (integerp x)
      (integerp y)
      (<= 0 n1)
      (<= n1 n2))
    (equal (logtail n1 (+ x (ash y n2)))
      (+ (logtail n1 x) (ash y (- n2 n1)))))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory logtail*)
     :induct (sub1-sub1-logcdr-induction n2 n1 x))))

logcdr-logapptheorem

(defthm logcdr-logapp
  (implies (and (integerp n) (integerp x) (integerp y) (< 0 n))
    (equal (logcdr (logapp n x y)) (logapp (1- n) (logcdr x) y)))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory)
     :induct (sub1-logcdr-induction n x))))

logcdr-logheadtheorem

(defthm logcdr-loghead
  (implies (and (integerp n) (integerp x) (< 0 n))
    (equal (logcdr (loghead n x)) (loghead (1- n) (logcdr x))))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory)
     :induct (sub1-logcdr-induction n x))))

*ark*-logcar-i+j+2*ktheorem

(defthm *ark*-logcar-i+j+2*k
  (implies (and (integerp i) (integerp j) (integerp k))
    (equal (logcar (+ i j (* 2 k))) (logcar (+ i j))))
  :hints (("Goal" :use ((:instance logcar-i+2*j (i (+ i j)) (j k))))))

*ark*-logcar-+theorem

(defthm *ark*-logcar-+
  (implies (and (integerp i) (integerp j))
    (equal (logcar (+ i j)) (b-xor (logcar i) (logcar j))))
  :hints (("Goal" :in-theory (enable b-xor))))

*ark*-loghead-1theorem

(defthm *ark*-loghead-1
  (implies (integerp x) (equal (loghead 1 x) (logcar x)))
  :hints (("goal" :in-theory (enable loghead logcons))))

unsigned-byte-p-+theorem

(defthm unsigned-byte-p-+
  (implies (and (unsigned-byte-p n x) (unsigned-byte-p n y))
    (unsigned-byte-p (1+ n) (+ x y)))
  :hints (("goal" :in-theory (enable unsigned-byte-p expt))))

unsigned-byte-p-logcdr-bridgetheorem

(defthm unsigned-byte-p-logcdr-bridge
  (implies (unsigned-byte-p 9 x)
    (unsigned-byte-p 8 (logcdr x)))
  :hints (("goal" :in-theory (enable unsigned-byte-p))))

unsigned-byte-p-logcdr-bridge-2theorem

(defthm unsigned-byte-p-logcdr-bridge-2
  (implies (unsigned-byte-p 8 x)
    (unsigned-byte-p 7 (logcdr x)))
  :hints (("goal" :in-theory (enable unsigned-byte-p))))

*ark*-+*theorem

(defthm *ark*-+*
  (implies (and (not (zip a)) (not (equal a -1)) (not (zip b)))
    (equal (+ a b)
      (logcons (b-xor (logcar a) (logcar b))
        (+ (b-and (logcar a) (logcar b)) (logcdr a) (logcdr b)))))
  :hints (("goal" :induct (logcdr-logcdr-induction a b)
     :in-theory (e/d (logops-recursive-definitions-theory b-and b-xor)
       (bitp-compound-recognizer)))))

in-theory

(in-theory (disable *ark*-+*))

*ark*-logcdr-+1theorem

(defthm *ark*-logcdr-+1
  (implies (integerp x)
    (and (implies (equal (logcar x) 0)
        (equal (logcdr (+ 1 x)) (logcdr x)))
      (implies (equal (logcar x) 1)
        (equal (logcdr (+ 1 x)) (+ 1 (logcdr x))))
      (implies (and (equal (logcar x) 1) (integerp y))
        (equal (logcdr (+ 1 x y)) (+ 1 (logcdr x) (logcdr y))))
      (implies (and (equal (logcar x) 1) (integerp y))
        (equal (logcdr (+ 1 y x)) (+ 1 (logcdr x) (logcdr y))))))
  :hints (("goal" :in-theory (enable *ark*-+*))))

unsigned-byte-p-+-helpertheorem

(defthm unsigned-byte-p-+-helper
  (implies (and (unsigned-byte-p n x)
      (unsigned-byte-p n y)
      (unsigned-byte-p 1 c)
      (integerp n)
      (< 0 n))
    (equal (unsigned-byte-p n (+ x y c))
      (not (logbitp n (+ x y c)))))
  :rule-classes nil
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory
       *ark*-+*
       logbitp*)
     :induct (sub1-logcdr-logcdr-carry-induction n x y c))))

*ark*-unsigned-byte-p-+theorem

(defthm *ark*-unsigned-byte-p-+
  (implies (and (unsigned-byte-p n x)
      (unsigned-byte-p n y)
      (integerp n)
      (< 0 n))
    (equal (unsigned-byte-p n (+ x y))
      (not (logbitp n (+ x y)))))
  :hints (("goal" :use (:instance unsigned-byte-p-+-helper (c 0)))))

in-theory

(in-theory (disable associativity-of-logapp))

logapp-logapptheorem

(defthm logapp-logapp
  (implies (and (integerp n1)
      (integerp n2)
      (integerp a)
      (integerp b)
      (integerp c)
      (<= 0 n2)
      (<= n2 n1))
    (equal (logapp n1 (logapp n2 a b) c)
      (logapp n2 a (logapp (- n1 n2) b c))))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory)
     :induct (sub1-sub1-logcdr-induction n1 n2 a))))

equal-logapp-xtheorem

(defthm equal-logapp-x
  (implies (and (integerp n)
      (integerp x)
      (integerp y)
      (integerp z)
      (<= 0 n)
      (equal (loghead n z) (loghead n x)))
    (equal (equal (logapp n x y) z) (equal y (logtail n z))))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory)
     :induct (sub1-logcdr-logcdr-induction n x z))))

loghead-+-simpletheorem

(defthm loghead-+-simple
  (implies (and (integerp x)
      (integerp y)
      (integerp n)
      (<= 0 n)
      (equal (loghead n x) 0))
    (equal (loghead n (+ x y)) (loghead n y)))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory)
     :induct (sub1-logcdr-logcdr-induction n x y))))

logtail-+-simpletheorem

(defthm logtail-+-simple
  (implies (and (integerp x)
      (integerp y)
      (integerp n)
      (<= 0 n)
      (equal (loghead n x) 0))
    (equal (logtail n (+ x y)) (+ (logtail n x) (logtail n y))))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory)
     :induct (sub1-logcdr-logcdr-induction n x y))))

*ark*-loghead-ash-pos-rewritetheorem

(defthm *ark*-loghead-ash-pos-rewrite
  (implies (and (integerp n1)
      (integerp n2)
      (integerp x)
      (<= 0 n1)
      (<= 0 n2))
    (equal (loghead n1 (ash x n2))
      (if (<= n1 n2)
        0
        (ash (loghead (- n1 n2) x) n2))))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory)
     :induct (sub1-sub1-induction n1 n2))))

logtail-ash-pos-rewritetheorem

(defthm logtail-ash-pos-rewrite
  (implies (and (integerp n1)
      (integerp n2)
      (integerp x)
      (<= 0 n1)
      (<= 0 n2))
    (equal (logtail n1 (ash x n2))
      (if (<= n1 n2)
        (ash x (- n2 n1))
        (logtail (- n1 n2) x))))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory)
     :induct (sub1-sub1-induction n1 n2))))

loghead-*2theorem

(defthm loghead-*2
  (implies (and (integerp n) (< 0 n) (integerp x))
    (equal (equal (loghead n (* 2 x)) 0)
      (equal (loghead (1- n) x) 0)))
  :hints (("goal" :in-theory (enable loghead*))))

logcar-identitytheorem

(defthm logcar-identity
  (implies (unsigned-byte-p 1 x) (equal (logcar x) x))
  :hints (("goal" :in-theory (enable unsigned-byte-p logcar))))

unsigned-byte-p-logcartheorem

(defthm unsigned-byte-p-logcar
  (unsigned-byte-p 1 (logcar x))
  :hints (("goal" :in-theory (enable unsigned-byte-p logcar))))

logapp-1-logcar-logcdrtheorem

(defthm logapp-1-logcar-logcdr
  (implies (integerp x)
    (equal (logapp 1 (logcar x) (logcdr x)) x))
  :hints (("goal" :in-theory (enable logapp))))

unsigned-byte-p-1-theorem

(defthm unsigned-byte-p-1-
  (implies (and (integerp n) (<= 0 n) (unsigned-byte-p n x))
    (equal (unsigned-byte-p n (1- x)) (< 0 x)))
  :hints (("goal" :in-theory (enable unsigned-byte-p))))

+-ash-logapptheorem

(defthm +-ash-logapp
  (implies (and (integerp x)
      (integerp n)
      (integerp a)
      (integerp b)
      (<= 0 n))
    (equal (+ (ash x n) (logapp n a b)) (logapp n a (+ x b))))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory)
     :induct (sub1-logcdr-induction n a))))

equal-logcar-1theorem

(defthm equal-logcar-1
  (equal (equal (logcar x) 1) (not (equal (logcar x) 0)))
  :hints (("goal" :in-theory (enable logcar))))

logapp-logheadtheorem

(defthm logapp-loghead
  (implies (and (integerp n1)
      (integerp n2)
      (integerp x)
      (integerp y)
      (<= 0 n1)
      (<= n1 n2))
    (equal (logapp n1 (loghead n2 x) y) (logapp n1 x y)))
  :hints (("goal" :induct (sub1-sub1-logcdr-induction n1 n2 x)
     :in-theory (enable logops-recursive-definitions-theory))))

logtail-almost-alltheorem

(defthm logtail-almost-all
  (implies (and (unsigned-byte-p (1+ n) x) (integerp n) (<= 0 n))
    (equal (logtail n x) (logbit n x)))
  :hints (("goal" :induct (sub1-logcdr-induction n x)
     :in-theory (enable logops-recursive-definitions-theory logbit))))

equal-x-logapp-xtheorem

(defthm equal-x-logapp-x
  (implies (and (integerp x) (integerp y) (integerp n) (<= 0 n))
    (equal (equal x (logapp n x y)) (equal (logtail n x) y)))
  :hints (("goal" :induct (sub1-logcdr-induction n x)
     :in-theory (enable logops-recursive-definitions-theory))))

equal-x-loghead-xtheorem

(defthm equal-x-loghead-x
  (implies (and (integerp x) (integerp n) (<= 0 n))
    (equal (equal x (loghead n x)) (unsigned-byte-p n x)))
  :hints (("goal" :induct (sub1-logcdr-induction n x)
     :in-theory (enable logops-recursive-definitions-theory))))

equal-logbit-logbit-logcdr-bridgetheorem

(defthm equal-logbit-logbit-logcdr-bridge
  (implies (and (integerp x) (integerp n) (<= 0 n))
    (equal (equal (logbit n (logcdr x)) (logbit (1+ n) x)) t))
  :hints (("goal" :in-theory (enable logbit logbitp*))))

unsigned-byte-p-logcdrtheorem

(defthm unsigned-byte-p-logcdr
  (implies (unsigned-byte-p n x)
    (unsigned-byte-p n (logcdr x)))
  :hints (("goal" :in-theory (enable unsigned-byte-p))))

unsigned-byte-p-1-logbittheorem

(defthm unsigned-byte-p-1-logbit
  (unsigned-byte-p 1 (logbit n x))
  :hints (("goal" :in-theory (enable logbit))))

unsigned-byte-p-1-b-xortheorem

(defthm unsigned-byte-p-1-b-xor
  (unsigned-byte-p 1 (b-xor x y))
  :hints (("goal" :in-theory (enable b-xor))))

ash-0-arg2theorem

(defthm ash-0-arg2
  (implies (integerp x) (equal (ash x 0) x))
  :hints (("goal" :in-theory (enable ash))))

other

(defstobj st
  (f1 :type (unsigned-byte 8) :initially 0)
  (f2 :type (unsigned-byte 8) :initially 0)
  (f1save :type (unsigned-byte 8) :initially 0)
  (a :type (unsigned-byte 8) :initially 0)
  (low :type (unsigned-byte 8) :initially 0)
  (cflg :type (unsigned-byte 1) :initially 0)
  (zflg :type (unsigned-byte 1) :initially 0)
  (x :type (unsigned-byte 8) :initially 0))

f1-lineartheorem

(defthm f1-linear
  (implies (stp st)
    (and (<= 0 (nth 0 st)) (<= (nth 0 st) 255)))
  :rule-classes (:linear :rewrite)
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero) '(stp f1p)))))

f1-typetheorem

(defthm f1-type
  (implies (stp st)
    (and (integerp (nth 0 st)) (unsigned-byte-p 8 (nth 0 st))))
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero)
       '(signed-byte-p-<= unsigned-byte-p-<= f1p))
     :expand (stp st)))
  :rule-classes (:rewrite :type-prescription))

f1-update-type-helpertheorem

(defthm f1-update-type-helper
  (implies (stp st) (iff (stp (update-nth 0 v st)) (f1p v)))
  :hints (("goal" :expand (:free (x) (stp x))
     :in-theory (set-difference-theories (current-theory 'ground-zero)
       '(nth update-nth))))
  :rule-classes nil)

f1-update-typetheorem

(defthm f1-update-type
  (implies (stp st)
    (iff (stp (update-nth 0 v st)) (unsigned-byte-p 8 v)))
  :hints (("goal" :in-theory (union-theories '(unsigned-byte-p signed-byte-p f1p)
       (current-theory 'ground-zero))
     :use f1-update-type-helper)))

f2-lineartheorem

(defthm f2-linear
  (implies (stp st)
    (and (<= 0 (nth 1 st)) (<= (nth 1 st) 255)))
  :rule-classes (:linear :rewrite)
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero) '(stp f2p)))))

f2-typetheorem

(defthm f2-type
  (implies (stp st)
    (and (integerp (nth 1 st)) (unsigned-byte-p 8 (nth 1 st))))
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero)
       '(signed-byte-p-<= unsigned-byte-p-<= f2p))
     :expand (stp st)))
  :rule-classes (:rewrite :type-prescription))

f2-update-type-helpertheorem

(defthm f2-update-type-helper
  (implies (stp st) (iff (stp (update-nth 1 v st)) (f2p v)))
  :hints (("goal" :expand (:free (x) (stp x))
     :in-theory (set-difference-theories (current-theory 'ground-zero)
       '(nth update-nth))))
  :rule-classes nil)

f2-update-typetheorem

(defthm f2-update-type
  (implies (stp st)
    (iff (stp (update-nth 1 v st)) (unsigned-byte-p 8 v)))
  :hints (("goal" :in-theory (union-theories '(unsigned-byte-p signed-byte-p f2p)
       (current-theory 'ground-zero))
     :use f2-update-type-helper)))

f1save-lineartheorem

(defthm f1save-linear
  (implies (stp st)
    (and (<= 0 (nth 2 st)) (<= (nth 2 st) 255)))
  :rule-classes (:linear :rewrite)
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero)
       '(stp f1savep)))))

f1save-typetheorem

(defthm f1save-type
  (implies (stp st)
    (and (integerp (nth 2 st)) (unsigned-byte-p 8 (nth 2 st))))
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero)
       '(signed-byte-p-<= unsigned-byte-p-<= f1savep))
     :expand (stp st)))
  :rule-classes (:rewrite :type-prescription))

f1save-update-type-helpertheorem

(defthm f1save-update-type-helper
  (implies (stp st)
    (iff (stp (update-nth 2 v st)) (f1savep v)))
  :hints (("goal" :expand (:free (x) (stp x))
     :in-theory (set-difference-theories (current-theory 'ground-zero)
       '(nth update-nth))))
  :rule-classes nil)

f1save-update-typetheorem

(defthm f1save-update-type
  (implies (stp st)
    (iff (stp (update-nth 2 v st)) (unsigned-byte-p 8 v)))
  :hints (("goal" :in-theory (union-theories '(unsigned-byte-p signed-byte-p f1savep)
       (current-theory 'ground-zero))
     :use f1save-update-type-helper)))

a-lineartheorem

(defthm a-linear
  (implies (stp st)
    (and (<= 0 (nth 3 st)) (<= (nth 3 st) 255)))
  :rule-classes (:linear :rewrite)
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero) '(stp ap)))))

a-typetheorem

(defthm a-type
  (implies (stp st)
    (and (integerp (nth 3 st)) (unsigned-byte-p 8 (nth 3 st))))
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero)
       '(signed-byte-p-<= unsigned-byte-p-<= ap))
     :expand (stp st)))
  :rule-classes (:rewrite :type-prescription))

a-update-type-helpertheorem

(defthm a-update-type-helper
  (implies (stp st) (iff (stp (update-nth 3 v st)) (ap v)))
  :hints (("goal" :expand (:free (x) (stp x))
     :in-theory (set-difference-theories (current-theory 'ground-zero)
       '(nth update-nth))))
  :rule-classes nil)

a-update-typetheorem

(defthm a-update-type
  (implies (stp st)
    (iff (stp (update-nth 3 v st)) (unsigned-byte-p 8 v)))
  :hints (("goal" :in-theory (union-theories '(unsigned-byte-p signed-byte-p ap)
       (current-theory 'ground-zero))
     :use a-update-type-helper)))

low-lineartheorem

(defthm low-linear
  (implies (stp st)
    (and (<= 0 (nth 4 st)) (<= (nth 4 st) 255)))
  :rule-classes (:linear :rewrite)
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero) '(stp lowp)))))

low-typetheorem

(defthm low-type
  (implies (stp st)
    (and (integerp (nth 4 st)) (unsigned-byte-p 8 (nth 4 st))))
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero)
       '(signed-byte-p-<= unsigned-byte-p-<= lowp))
     :expand (stp st)))
  :rule-classes (:rewrite :type-prescription))

low-update-type-helpertheorem

(defthm low-update-type-helper
  (implies (stp st) (iff (stp (update-nth 4 v st)) (lowp v)))
  :hints (("goal" :expand (:free (x) (stp x))
     :in-theory (set-difference-theories (current-theory 'ground-zero)
       '(nth update-nth))))
  :rule-classes nil)

low-update-typetheorem

(defthm low-update-type
  (implies (stp st)
    (iff (stp (update-nth 4 v st)) (unsigned-byte-p 8 v)))
  :hints (("goal" :in-theory (union-theories '(unsigned-byte-p signed-byte-p lowp)
       (current-theory 'ground-zero))
     :use low-update-type-helper)))

cflg-lineartheorem

(defthm cflg-linear
  (implies (stp st) (and (<= 0 (nth 5 st)) (<= (nth 5 st) 1)))
  :rule-classes (:linear :rewrite)
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero) '(stp cflgp)))))

cflg-typetheorem

(defthm cflg-type
  (implies (stp st)
    (and (integerp (nth 5 st)) (unsigned-byte-p 1 (nth 5 st))))
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero)
       '(signed-byte-p-<= unsigned-byte-p-<= cflgp))
     :expand (stp st)))
  :rule-classes (:rewrite :type-prescription))

cflg-update-type-helpertheorem

(defthm cflg-update-type-helper
  (implies (stp st) (iff (stp (update-nth 5 v st)) (cflgp v)))
  :hints (("goal" :expand (:free (x) (stp x))
     :in-theory (set-difference-theories (current-theory 'ground-zero)
       '(nth update-nth))))
  :rule-classes nil)

cflg-update-typetheorem

(defthm cflg-update-type
  (implies (stp st)
    (iff (stp (update-nth 5 v st)) (unsigned-byte-p 1 v)))
  :hints (("goal" :in-theory (union-theories '(unsigned-byte-p signed-byte-p cflgp)
       (current-theory 'ground-zero))
     :use cflg-update-type-helper)))

zflg-lineartheorem

(defthm zflg-linear
  (implies (stp st) (and (<= 0 (nth 6 st)) (<= (nth 6 st) 1)))
  :rule-classes (:linear :rewrite)
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero) '(stp zflgp)))))

zflg-typetheorem

(defthm zflg-type
  (implies (stp st)
    (and (integerp (nth 6 st)) (unsigned-byte-p 1 (nth 6 st))))
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero)
       '(signed-byte-p-<= unsigned-byte-p-<= zflgp))
     :expand (stp st)))
  :rule-classes (:rewrite :type-prescription))

zflg-update-type-helpertheorem

(defthm zflg-update-type-helper
  (implies (stp st) (iff (stp (update-nth 6 v st)) (zflgp v)))
  :hints (("goal" :expand (:free (x) (stp x))
     :in-theory (set-difference-theories (current-theory 'ground-zero)
       '(nth update-nth))))
  :rule-classes nil)

zflg-update-typetheorem

(defthm zflg-update-type
  (implies (stp st)
    (iff (stp (update-nth 6 v st)) (unsigned-byte-p 1 v)))
  :hints (("goal" :in-theory (union-theories '(unsigned-byte-p signed-byte-p zflgp)
       (current-theory 'ground-zero))
     :use zflg-update-type-helper)))

x-lineartheorem

(defthm x-linear
  (implies (stp st)
    (and (<= 0 (nth 7 st)) (<= (nth 7 st) 255)))
  :rule-classes (:linear :rewrite)
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero) '(stp xp)))))

x-typetheorem

(defthm x-type
  (implies (stp st)
    (and (integerp (nth 7 st)) (unsigned-byte-p 8 (nth 7 st))))
  :hints (("goal" :in-theory (union-theories (current-theory 'ground-zero)
       '(signed-byte-p-<= unsigned-byte-p-<= xp))
     :expand (stp st)))
  :rule-classes (:rewrite :type-prescription))

x-update-type-helpertheorem

(defthm x-update-type-helper
  (implies (stp st) (iff (stp (update-nth 7 v st)) (xp v)))
  :hints (("goal" :expand (:free (x) (stp x))
     :in-theory (set-difference-theories (current-theory 'ground-zero)
       '(nth update-nth))))
  :rule-classes nil)

x-update-typetheorem

(defthm x-update-type
  (implies (stp st)
    (iff (stp (update-nth 7 v st)) (unsigned-byte-p 8 v)))
  :hints (("goal" :in-theory (union-theories '(unsigned-byte-p signed-byte-p xp)
       (current-theory 'ground-zero))
     :use x-update-type-helper)))

line1function

(defun line1
  (st)
  (declare (xargs :stobjs st))
  (let ((st (update-x 8 st)))
    st))

line2function

(defun line2
  (st)
  (declare (xargs :stobjs st))
  (let ((st (update-a 0 st)))
    st))

local

(local (in-theory (enable unsigned-byte-p logbitp)))

line3function

(defun line3
  (st)
  (declare (xargs :stobjs st
      :guard-hints (("goal" :in-theory (enable logapp loghead logcar stp)))))
  (let ((temp (cflg st)))
    (let ((st (update-cflg (logcar (f1 st)) st)))
      (let ((st (update-f1 (logapp 7 (logcdr (f1 st)) temp) st)))
        st))))

line5function

(defun line5
  (st)
  (declare (xargs :stobjs st))
  (let ((st (update-cflg 0 st)))
    st))

line6function

(defun line6
  (st)
  (declare (xargs :stobjs st
      :guard-hints (("goal" :in-theory (enable logapp loghead logcar logbit)))))
  (let ((temp (+ (a st) (f2 st) (cflg st))))
    (let ((st (update-a (loghead 8 temp) st)))
      (let ((st (update-cflg (logbit 8 temp) st)))
        st))))

line7function

(defun line7
  (st)
  (declare (xargs :stobjs st
      :guard-hints (("goal" :in-theory (enable logapp loghead logcar)))))
  (let ((temp (cflg st)))
    (let ((st (update-cflg (logcar (a st)) st)))
      (let ((st (update-a (logapp 7 (logcdr (a st)) temp) st)))
        st))))

line8function

(defun line8
  (st)
  (declare (xargs :stobjs st
      :guard-hints (("goal" :in-theory (enable logapp loghead logcar)))))
  (let ((temp (cflg st)))
    (let ((st (update-cflg (logcar (low st)) st)))
      (let ((st (update-low (logapp 7 (logcdr (low st)) temp) st)))
        st))))

line9function

(defun line9
  (st)
  (declare (xargs :stobjs st
      :guard-hints (("goal" :in-theory (enable logapp loghead logcar)))))
  (let ((temp (loghead 8 (1- (x st)))))
    (let ((st (update-zflg (if (equal temp 0)
             1
             0)
           st)))
      (let ((st (update-x temp st)))
        st))))

multloopfunction

(defun multloop
  (st)
  (declare (xargs :stobjs st
      :measure (nfix (x st))
      :hints (("goal" :in-theory (enable unsigned-byte-p nfix)))))
  (if (and (integerp (x st)) (< 0 (x st)))
    (let ((st (line3 st)))
      (let ((st (if (equal (cflg st) 1)
             (let ((st (line5 st)))
               (line6 st))
             st)))
        (let ((st (line7 st)))
          (let ((st (line8 st)))
            (let ((st (line9 st)))
              (if (equal (zflg st) 0)
                (multloop st)
                st))))))
    st))

multprogfunction

(defun multprog
  (st)
  (declare (xargs :stobjs st))
  (let ((st (line1 st)))
    (let ((st (line2 st)))
      (multloop st))))

resultfunction

(defun result
  (st)
  (declare (xargs :stobjs st))
  (logapp 8 (low st) (a st)))

in-theory

(in-theory (disable stp))

ash-*-casesplit-v1theorem

(defthm ash-*-casesplit-v1
  (implies (and (equal (logcar x) 0)
      (integerp x)
      (integerp y)
      (integerp n)
      (<= 0 n))
    (equal (ash (* y x) n) (ash (* y (logcdr x)) (1+ n))))
  :hints (("goal" :in-theory (enable ash-*2-simplify ash*))))

ash-*-casesplit-v2theorem

(defthm ash-*-casesplit-v2
  (implies (and (equal (logcar x) 1)
      (integerp x)
      (integerp y)
      (integerp n)
      (<= 0 n))
    (equal (ash (* y x) n)
      (+ (ash y n) (ash (* y (logcdr x)) (1+ n)))))
  :hints (("goal" :in-theory (enable *ark*-ash-+-pos ash-*2-simplify ash*))))

*-logcar-casesplittheorem

(defthm *-logcar-casesplit
  (implies (and (integerp x) (integerp y))
    (equal (* (logcar x) y)
      (if (equal (logcar x) 0)
        0
        y)))
  :hints (("goal" :in-theory (enable logcar))))

+-reconstruct-bridgetheorem

(defthm +-reconstruct-bridge
  (implies (and (equal (logcdr (+ x y)) z) (integerp x) (integerp y))
    (equal (logapp 1 (b-xor (logcar x) (logcar y)) z) (+ x y)))
  :hints (("goal" :in-theory (enable logapp*))))

result-update-nththeorem

(defthm result-update-nth
  (implies (stp st)
    (equal (result (update-nth 3 0 st)) (low st))))

local

(local (in-theory (disable unsigned-byte-p logbitp)))

loop-workstheorem

(defthm loop-works
  (implies (and (stp st) (<= (x st) 8))
    (equal (result (multloop st))
      (+ (logtail (x st) (result st))
        (ash (* (loghead (x st) (f1 st)) (f2 st)) (- 8 (x st))))))
  :hints (("goal" :in-theory (enable logtail* logbitp* ash*))))

prog-workstheorem

(defthm prog-works
  (implies (stp st)
    (equal (result (multprog st)) (* (f1 st) (f2 st))))
  :hints (("goal" :in-theory (disable multloop result))))