#|
 Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.
 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.
 NO WARRANTY
 Yuan Yu PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS IS"
 WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT
 LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
 SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
 ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
 IN NO EVENT WILL Yuan Yu BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS,
 LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT
 OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS
 OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD
 PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR
 FOR ANY CLAIM BY ANY OTHER PARTY.
|#
; ---------------------------------------------------------------------------
; Date:      Jan, 1991
; Modified:  Sep 4, 1992.
; File:      mc20-2.events
; ---------------------------------------------------------------------------
;
;-------------------------------------------------------------------------
;                       PROVING PHASE
;
; we establish basic theory for program proving based upon our MC68020
; specification.
;-------------------------------------------------------------------------
;
; load and compile the spec.

Event: Start with the library "mc20-1" using the compiled version.

Event: For efficiency, compile those definitions not yet compiled.

; a segment of the memory is ROM, iff it is pc-readable(read-only).

Definition: rom-addrp (addr, mem, n) = pc-read-memp (addr, mem, n)

; a segment of the memory is RAM, iff it is writable(random).

Definition: ram-addrp (addr, mem, n) = write-memp (addr, mem, n)

; x is an element of lst wrt numberp.

Definition: n-member (x, lst) = if lst ≃ nil then f

else (fix (x) = fix (car (lst))) ∨ n-member (x, cdr (lst)) endif

; mod-eq returns t iff x and y are the "same" bit-vector.  It is often
; used as an induction hint to many lemmas.

Definition: mod-eq (n, x, y) = if n ≃ 0 then t

else (bcar (x) = bcar (y)) ∧ mod-eq (n − 1, bcdr (x), bcdr (y)) endif

; mod32-eq is equivalent to mod-eq with n = 32. But we define it as follows.

Definition: mod32-eq (x, y) = (head (x, 32) = head (y, 32))

; the equivalence is given by this lemma.
; (prove-lemma mod-eq-lemma (rewrite)
;      (equal (mod-eq 32 x y)
;             (mod32-eq x y)))
; the negation of a bit-vector.

Definition: neg (n, x) = sub (n, x, 0)

; {x, x+1, ..., x+(m-1)} and {y} are disjoint.  We assume all the numbers are
; modulo 2^32.

Definition: disjoint0 (x, m, y) = if m ≃ 0 then t

else (¬ mod32-eq (add (32, x, m − 1), y)) ∧ disjoint0 (x, m − 1, y) endif

; {x, x+1, ..., x+(m-1)} and {y, y+1, ..., y+(n-1)} are disjoint.

Definition: disjoint (x, m, y, n) = if n ≃ 0 then t

else disjoint0 (x, m, add (32, y, n − 1)) ∧ disjoint (x, m, y, n − 1) endif

;                 BIT VECTOR AS LIST OF BIT
; A lower level layer.  This is part of my old spec that specifies the
; microprocessor at a relatively lower level.

Definition: bit (bv) = if bv ≃ nil then b0

elseif b0p (car (bv)) then b0

else b1 endif

Definition: vec (bv) = if bv ≃ nil then nil

else cdr (bv) endif

Definition: fix-bv (bv) = if bv ≃ nil then nil

else cons (bit (bv), fix-bv (vec (bv))) endif

Definition: bv-len (bv) = if bv ≃ nil then 0

else 1 + bv-len (vec (bv)) endif

Definition: bv-not (bv) = if bv ≃ nil then nil

else cons (b-not (bit (bv)), bv-not (vec (bv))) endif

Definition: bv-head (bv, n) = if n ≃ 0 then nil

else cons (bit (bv), bv-head (vec (bv), n − 1)) endif

Definition: bv-tail (bv, n) = if n ≃ 0 then fix-bv (bv)

else bv-tail (vec (bv), n − 1) endif Definition: bv-bitn (bv, n) = if n ≃ 0 then bit (bv)

else bv-bitn (vec (bv), n − 1) endif

Definition: bv-mbit (bv) = if bv ≃ nil then b0

elseif vec (bv) ≃ nil then bit (bv)

else bv-mbit (vec (bv)) endif

Definition: bv-adder (c, x, y) = if x ≃ nil then nil

else cons (b-eor (b-eor (bit (x), bit (y)), c),

bv-adder (b-or (b-and (bit (x), bit (y)),

b-or (b-and (bit (x), c), b-and (bit (y), c))), vec (x), vec (y))) endif

; conversion functions.

Definition: bv-to-nat (bv) = if bv ≃ nil then 0

else bit (bv) + (2 ∗ bv-to-nat (vec (bv))) endif

Definition: bv-sized-to-nat (bv, size) = if size ≃ 0 then 0

else bit (bv) + (2 ∗ bv-sized-to-nat (vec (bv), size − 1)) endif

Definition: nat-to-bv (n) = if n ≃ 0 then nil

else cons (n mod 2, nat-to-bv (n ÷ 2)) endif

Definition: nat-to-bv-sized (n, size) = if size ≃ 0 then nil

else cons (n mod 2, nat-to-bv-sized (n ÷ 2, size − 1)) endif

;               LISTP

Theorem: bv-len-listp (bv-len (x) = 0) = (x ≃ nil)

Theorem: bv-head-listp listp (bv-head (x, n)) = (n ≄ 0)

Theorem: bv-adder-listp listp (bv-adder (c, x, y)) = listp (x)

;               BV-LEN

Theorem: bv-head-len bv-len (bv-head (x, n)) = fix (n)

Theorem: nat-to-bv-sized-len bv-len (nat-to-bv-sized (x, n)) = fix (n)

Theorem: bv-adder-len bv-len (bv-adder (c, x, y)) = bv-len (x)

;                 CONVERSION THEOREMS
; nat-to-bv-sized only considers the first k binary digits of natural number n.

Theorem: nat-to-bv-sized-la0 nat-to-bv-sized (n mod exp (2, k), k) = nat-to-bv-sized (n, k)

; rewrite nat-to-bv-sized into nat-to-bv.

Theorem: nat-to-bv-sized-head nat-to-bv-sized (m, n) = bv-head (nat-to-bv (m), n)

; rewrite bv-sized-to-nat into bv-to-nat.

Theorem: bv-sized-to-nat-head bv-sized-to-nat (x, n) = bv-to-nat (bv-head (x, n))

Theorem: bv-to-nat-to-bv bv-head (nat-to-bv (bv-to-nat (x)), n) = bv-head (x, n)

Theorem: nat-to-bv-to-nat bv-to-nat (nat-to-bv (n)) = fix (n)

Theorem: bv-head-nat bv-to-nat (bv-head (x, n)) = if bv-to-nat (x) < exp (2, n) then bv-to-nat (x)

else bv-to-nat (x) mod exp (2, n) endif

Theorem: bv-to-nat-to-bv-sized nat-to-bv-sized (bv-to-nat (x), n) = bv-head (x, n)

Theorem: nat-to-bv-sized-to-nat bv-to-nat (nat-to-bv-sized (m, n)) = if m < exp (2, n) then fix (m)

else m mod exp (2, n) endif

Theorem: bv-sized-to-nat-to-bv-sized nat-to-bv-sized (bv-sized-to-nat (x, n), n) = bv-head (x, n)

Theorem: nat-to-bv-sized-sized-to-nat bv-sized-to-nat (nat-to-bv-sized (m, n), n) = if m < exp (2, n) then fix (m)

else m mod exp (2, n) endif

Event: Disable bv-sized-to-nat-head.

Event: Disable nat-to-bv-sized-head.

;            BV-BITN and BV-NOT

Theorem: bv-bitn-not bv-bitn (bv-not (x), i) = if i < bv-len (x) then b-not (bv-bitn (x, i))

else b0 endif

Theorem: bv-to-nat-rangep nat-rangep (bv-to-nat (x), bv-len (x))

;            BV-ADDER
; a bridge function.

Definition: bv-adder&carry (c, x, y) = if x ≃ nil then cons (fix-bit (c), nil)

else cons (b-eor (c, b-eor (bit (x), bit (y))),

bv-adder&carry (b-or (b-and (bit (x), bit (y)),

b-or (b-and (bit (x), c),

b-and (bit (y), c))),

vec (x),

vec (y))) endif

Theorem: bv-adder&carry-len bv-len (bv-adder&carry (c, x, y)) = (1 + bv-len (x))

Theorem: fix-bv-adder&carry fix-bv (bv-adder&carry (c, x, y)) = bv-adder&carry (c, x, y)

; the relation between bv-adder&carry and bv-adder.  We have successfully
; constructed the bridge!

Theorem: bv-adder-bridge bv-adder (c, x, y) = bv-head (bv-adder&carry (c, x, y), bv-len (x))

;                  lifting lemmas

Theorem: bv-not-lognot bv-to-nat (bv-not (x)) = lognot (bv-len (x), bv-to-nat (x))

Theorem: bv-bitn-bitn bv-bitn (x, n) = bitn (bv-to-nat (x), n)

Theorem: bv-mbit-bitn bv-mbit (x) = if bv-len (x) = 0 then 0

else bitn (bv-to-nat (x), bv-len (x) − 1) endif

Theorem: bv-adder&carry-nat (bv-len (x) = bv-len (y)) → (bv-to-nat (bv-adder&carry (c, x, y))

= (fix-bit (c) + bv-to-nat (x) + bv-to-nat (y)))

Theorem: bv-adder-nat ((bv-len (x) = bv-len (y)) ∧ bitp (c)) → (bv-to-nat (bv-adder (c, x, y))

= adder (bv-len (x), c, bv-to-nat (x), bv-to-nat (y)))

;                    EVENP
; add-evenp states that the sum of two even numbers is still even.

Theorem: add-evenp (evenp (x) ∧ evenp (y)) → evenp (add (n, x, y))

Event: Disable evenp.

;                     LOGNOT

Theorem: lognot-0 (x ∉ N) → ((lognot (x, y) = lognot (0, y)) ∧ (lognot (y, x) = lognot (y, 0)))

Theorem: lognot-nat-rangep nat-rangep (lognot (n, x), n)

Theorem: lognot-lognot lognot (n, lognot (n, x)) = head (x, n)

Theorem: lognot-cancel (nat-rangep (x, n) ∧ nat-rangep (y, n)) → ((lognot (n, x) = lognot (n, y)) = (fix (x) = fix (y)))

; the integer interpretation of lognot.

Theorem: lognot-int (nat-rangep (x, n) ∧ (n ≄ 0)) → (nat-to-int (lognot (n, x), n) = iplus (-1, ineg (nat-to-int (x, n))))

Theorem: adder-lognot bitp (c) → (lognot (n, adder (n, c, x, y))

= adder (n, b-not (c), lognot (n, x), lognot (n, y)))

Event: Disable lognot.

;               BASICS ABOUT HEAD & TAIL

Theorem: head-0 head (0, n) = 0

Theorem: tail-0 tail (0, n) = 0

Theorem: head-of-0 head (x, 0) = 0

Theorem: tail-of-0 tail (x, 0) = fix (x)

Theorem: head-lessp head (x, n) < exp (2, n)

Theorem: tail-lessp (tail (x, n) < y) = (x < (exp (2, n) ∗ y))

Theorem: head-leq x ≮ head (x, n)

Theorem: tail-leq x ≮ tail (x, n)

Theorem: tail-equal-0 (tail (x, n) = 0) = nat-rangep (x, n)

Theorem: head-lemma nat-rangep (x, n) → (head (x, n) = fix (x))

Theorem: tail-lemma nat-rangep (x, n) → (tail (x, n) = 0)

Theorem: replace-0 (replace (0, x, y) = fix (y)) ∧ (replace (n, x, 0) = head (x, n)) ∧ ((nat-rangep (x, n) ∧ nat-rangep (y, n))

→ (replace (n, x, y) = fix (x)))

Theorem: app-0 (app (n, x, 0) = head (x, n)) ∧ (app (n, 0, y) = (y ∗ exp (2, n))) ∧ (app (0, x, y) = fix (y))

;                THEOREMS ABOUT SHIFT AND ROTATE
; the key events are LSL-UINT, LSR-UINT, ASL-INT, and ASR-INT.
; ASL-INT and ASR-INT are pretty hard.  It took me a few days to get the
; proofs.  It would be a good challenge to other provers.

Theorem: lsl-uint uint-rangep (x, n − cnt) → (nat-to-uint (lsl (n, x, cnt)) = (nat-to-uint (x) ∗ exp (2, cnt)))

Theorem: lsr-uint nat-to-uint (lsr (x, cnt)) = (nat-to-uint (x) ÷ exp (2, cnt))

; two lemmas for asl-int.

Theorem: remainder-diff-la (((x mod z) = 0) ∧ (y < z)) → (((x − y) mod z)

= if x ≤ y then 0 elseif y ≃ 0 then 0 else z − y endif)

Theorem: asl-int-crock1 (x < exp (2, (n − s) − 1)) → (head (x ∗ exp (2, s), n) = (x ∗ exp (2, s)))

Theorem: asl-int-crock2 (((exp (2, s) ∗ (exp (2, n) − x)) ≤ exp (2, n − 1)) ∧ (x < exp (2, n))) → (head (x ∗ exp (2, s), n)

= (exp (2, n) − (exp (2, s) ∗ (exp (2, n) − x))))

Theorem: asl-int (nat-rangep (x, n) ∧ int-rangep (nat-to-int (x, n), n − s)) → (nat-to-int (asl (n, x, s), n) = itimes (nat-to-int (x, n), exp (2, s)))

Event: Disable asl-int-crock1.

Event: Disable asl-int-crock2.

Theorem: quotient-diff-la (((x mod z) = 0) ∧ (y < z)) → (((x − y) ÷ z)

= if y ≃ 0 then x ÷ z else (x ÷ z) − 1 endif)

Theorem: remainder-diff ((x mod z) = 0) → (((x − y) mod z)

= if (x ≤ y) ∨ ((y mod z) = 0) then 0 else z − (y mod z) endif)

Theorem: quotient-diff ((x mod z) = 0) → (((x − y) ÷ z)

= if (y mod z) = 0 then (x ÷ z) − (y ÷ z) else ((x ÷ z) − (y ÷ z)) − 1 endif)

Theorem: quotient-exp-lessp (cnt ≤ n) → (((x ÷ exp (2, cnt)) < exp (2, n − cnt)) = (x < exp (2, n)))

Theorem: lessp-times-exp-1s ((m + n) = fix (k)) → (((x + (exp (2, m) ∗ (exp (2, n) − 1))) < exp (2, k − 1))

= if n ≃ 0 then x < exp (2, (m + n) − 1)

else f endif)

Theorem: lessp-app-1s ((m + n) = fix (k)) → ((app (m, x, exp (2, n) − 1) < exp (2, k − 1))

= if n ≃ 0 then head (x, m) < exp (2, (m + n) − 1) else f endif)

Theorem: times-sub1 ((y − 1) ∗ x) = ((x ∗ y) − x)

Theorem: difference-app-1s ((m + n) = fix (k)) → ((exp (2, k) − app (m, x, exp (2, n) − 1)) = (exp (2, m) − head (x, m)))

Event: Disable times-sub1.

Theorem: asr-int-crock ((x < exp (2, n)) ∧ (x ≮ exp (2, n − 1)) ∧ (cnt ≤ n)) → ((app (n − cnt, x ÷ exp (2, cnt), exp (2, cnt) − 1) < exp (2, n − 1))

= f)

Theorem: asr-int nat-rangep (x, n) → (nat-to-int (asr (n, x, i), n)

= if negativep (nat-to-int (x, n))

then if iremainder (nat-to-int (x, n), exp (2, i)) = 0 then iquotient (nat-to-int (x, n), exp (2, i)) else iplus (-1, iquotient (nat-to-int (x, n), exp (2, i))) endif

else iquotient (nat-to-int (x, n), exp (2, i)) endif)

Event: Disable asr-int-crock.

Event: Disable quotient-exp-lessp.

Event: Disable remainder-diff.

Event: Disable quotient-diff.

Theorem: lsl-0 lsl (n, x, 0) = head (x, n)

Theorem: lsl-nat-rangep nat-rangep (lsl (n, x, cnt), n)

Theorem: lsl-lsl lsl (n, lsl (n, x, cnt1 ), cnt2 ) = lsl (n, x, cnt1 + cnt2 )

Theorem: lsr-0 lsr (x, 0) = fix (x)

Theorem: lsr-nat-rangep nat-rangep (x, n) → nat-rangep (lsr (x, cnt), n)

Theorem: lsr-lsr lsr (lsr (x, cnt1 ), cnt2 ) = lsr (x, cnt1 + cnt2 )

Theorem: asl-0 asl (n, x, 0) = head (x, n)

Theorem: asl-nat-rangep nat-rangep (asl (n, x, cnt), n)

Theorem: asl-asl asl (n, asl (n, x, cnt1 ), cnt2 ) = asl (n, x, cnt1 + cnt2 )

Theorem: asr-0 nat-rangep (x, n) → (asr (n, x, 0) = fix (x))

Theorem: asr-nat-rangep nat-rangep (x, n) → nat-rangep (asr (n, x, cnt), n)

; unproved!  Not useful yet.
; (prove-lemma asr-asr (rewrite)
;     (implies (and (nat-rangep x n)
;                   (not (zerop n)))
;              (equal (asr n (asr n x cnt1) cnt2)
;                     (asr n x (plus cnt1 cnt2)))))
; the integer interpretation of ext.

Theorem: mbit-means-lessp nat-rangep (x, n) → (bitn (x, n − 1)

= if x < exp (2, n − 1) then 0 else 1 endif)

Theorem: exp2-lessp (i < j ) → (exp (2, i) < exp (2, j ))

; note that ext-lemma takes care of the other aspects about ext.

Theorem: ext-int (nat-rangep (x, n) ∧ (n < size)) → (nat-to-int (ext (n, x, size), size) = nat-to-int (x, n))

Event: Disable exp2-lessp.

;                      INTEGERS!
; functions with a postfix `end' will eventually be disabled.  We use them
; to ``tell'' the prover that something unexpected happens.  They can
; somehow force the prover to stop proving and print out some information.

Definition: adder-int-end (n, c, x, y) = nat-to-int ((fix-bit (c) + int-to-nat (x, n) + int-to-nat (y, n))

mod exp (2, n), n)

Theorem: plus-to-iplus (integerp (x) ∧ integerp (y) ∧ int-rangep (x, n) ∧ int-rangep (y, n)) → (adder-int-end (n, c, x, y)

= if int-rangep (iplus (x, iplus (y, fix-bit (c))), n) then iplus (x, iplus (y, fix-bit (c))) elseif negativep (x) then iplus (x, iplus (y, iplus (fix-bit (c), exp (2, n)))) else iplus (x, iplus (y, iplus (fix-bit (c), − exp (2, n)))) endif)

Event: Disable plus-to-iplus.

Theorem: iplus-with-carry-negativep (integerp (x) ∧ integerp (y) ∧ bitp (z) ∧ negativep (x) ∧ negativep (y)) → negativep (iplus (x, iplus (y, z)))

Theorem: iplus-with-carry-non-negativep (integerp (x) ∧ integerp (y) ∧ bitp (z) ∧ (¬ negativep (x)) ∧ (¬ negativep (y))) → (¬ negativep (iplus (x, iplus (y, z))))

; two lemmas for addx-v.  They will be disabled right after we use them.

Theorem: addx-v-crock1 (integerp (x) ∧ integerp (y) ∧ bitp (z) ∧ int-rangep (x, n) ∧ int-rangep (y, n)) → (¬ negativep (iplus (x, iplus (y, iplus (z, exp (2, n))))))

Theorem: addx-v-crock2 (integerp (x) ∧ integerp (y) ∧ bitp (z) ∧ (n ≄ 0) ∧ int-rangep (x, n) ∧ int-rangep (y, n)) → negativep (iplus (x, iplus (y, iplus (z, − exp (2, n)))))

; two lemmas for BMI of add.  They will be disabled right after we
; use them.

Theorem: add-bmi-crock1 (integerp (x) ∧ integerp (y) ∧ int-rangep (x, n) ∧ int-rangep (y, n)) → (¬ negativep (iplus (x, iplus (y, exp (2, n)))))

Theorem: add-bmi-crock2 (integerp (x) ∧ integerp (y) ∧ int-rangep (x, n) ∧ int-rangep (y, n)) → negativep (iplus (x, iplus (y, − exp (2, n))))

; two lemmas for BMI of sub.  They will be disabled right after we
; use them.

Theorem: ilessp-crock1 (integerp (x) ∧ integerp (y) ∧ int-rangep (x, n) ∧ int-rangep (y, n)) → (¬ ilessp (iplus (y, exp (2, n)), x))

Theorem: ilessp-crock2 (integerp (x) ∧ integerp (y) ∧ int-rangep (x, n) ∧ int-rangep (y, n)) → ilessp (iplus (y, − exp (2, n)), x)

; the addition of two opposite sign integers will never overflow, provided
; the two integers are in "good" range.

Theorem: iplus-int-rangep1 (integerp (x) ∧ integerp (y) ∧ bitp (z) ∧ int-rangep (x, n) ∧ int-rangep (y, n) ∧ (¬ negativep (x)) ∧ negativep (y)) → int-rangep (iplus (x, iplus (y, z)), n)

Theorem: iplus-int-rangep2 (integerp (x) ∧ integerp (y) ∧ bitp (z) ∧ int-rangep (x, n) ∧ int-rangep (y, n) ∧ negativep (x) ∧ (¬ negativep (y))) → int-rangep (iplus (x, iplus (y, z)), n)

Theorem: idifference-int-rangep1 (int-rangep (x, n) ∧ int-rangep (y, n) ∧ (¬ ilessp (x, y)) ∧ (¬ negativep (y))) → int-rangep (idifference (y, x), n)

Theorem: idifference-int-rangep2 (integerp (x) ∧ integerp (y) ∧ int-rangep (x, n) ∧ int-rangep (y, n) ∧ (¬ ilessp (y, x)) ∧ negativep (y)) → int-rangep (idifference (y, x), n)

; two lemmas about uint-rangep and int-rangep. We introduce them before any
; lemmas about uint-rangep and int-rangep.

Theorem: uint-rangep-la (x < exp (2, n)) → uint-rangep (x, n)

Theorem: int-rangep-la ((x ∈ N) ∧ (x < exp (2, n − 1))) → int-rangep (x, n)

;                NAT-TO-UINT & UINT-TO-NAT

Theorem: nat-to-uint-to-nat uint-to-nat (nat-to-uint (x)) = fix (x)

Theorem: uint-to-nat-to-uint nat-to-uint (uint-to-nat (x)) = fix (x)

Theorem: uint-to-nat-rangep (x < exp (2, n)) → nat-rangep (uint-to-nat (x), n)

Theorem: nat-to-uint-rangep nat-rangep (x, n) → uint-rangep (nat-to-uint (x), n)

;                NAT-TO-INT & INT-TO-NAT

Theorem: nat-to-int-0 nat-to-int (0, n) = 0

Theorem: int-to-nat-0 int-to-nat (0, n) = 0

; nat-to-int always returns an integer, provided the input is a "good"
; natural number.

Theorem: nat-to-int-integerp integerp (nat-to-int (x, n)) = nat-rangep (x, n)

; nat-to-int always returns a "good" integer.

Theorem: nat-to-int-rangep int-rangep (nat-to-int (x, n), n)

; int-to-nat always returns a "good" natural number, provided the input
; is a "good" integer.

Theorem: int-to-nat-rangep (integerp (x) ∧ int-rangep (x, n)) → nat-rangep (int-to-nat (x, n), n)

Theorem: nat-to-int-to-nat nat-rangep (x, n) → (int-to-nat (nat-to-int (x, n), n) = fix (x))

Theorem: int-to-nat-to-int (integerp (x) ∧ int-rangep (x, n)) → (nat-to-int (int-to-nat (x, n), n) = fix-int (x))

Theorem: int-to-nat=0 (int-rangep (x, n) ∧ integerp (x)) → ((int-to-nat (x, n) = 0) = (x = 0))

; /x/ = /y/ --> x = y.

Theorem: nat-to-int= (nat-rangep (x, n) ∧ nat-rangep (y, n)) → ((nat-to-int (x, n) = nat-to-int (y, n)) = (fix (x) = fix (y)))

; nat-to-int and int-to-nat are disabled.

Event: Disable nat-to-int.

Event: Disable int-to-nat.

; theorems about int-rangep.

Theorem: abs-lessp-int-rangep (int-rangep (x, n) ∧ (abs (y) < abs (x))) → int-rangep (y, n)

; 0 is always in "good" integer range.

Theorem: int-rangep-of-0 int-rangep (0, n) Theorem: sub1-int-rangep int-rangep (x, n) → int-rangep (x − 1, n) Theorem: difference-int-rangep int-rangep (x, n) → int-rangep (x − y, n) Theorem: quotient-int-rangep int-rangep (x, n) → int-rangep (x ÷ y, n) Theorem: remainder-int-rangep (int-rangep (y, n) ∧ (y ≄ 0)) → int-rangep (x mod y, n)

; iquotient is almost always in the integer range.

Theorem: iquotient-int-rangep int-rangep (x, n) → (int-rangep (iquotient (x, y), n)

= if y = -1 then x ≠ (− exp (2, n − 1))

else t endif)

; iremainder is almost always in the integer range.

Theorem: iremainder-int-rangep (int-rangep (y, n) ∧ integerp (y) ∧ (y ≠ 0)) → int-rangep (iremainder (x, y), n)

; lemmas about integerp.

Theorem: integerp-fix-int integerp (x) → (fix-int (x) = x)

Theorem: fix-int-integerp integerp (fix-int (x))

Theorem: minus-integerp integerp (− x) = (x ≄ 0)

Theorem: integerp-minus0 integerp (x) → (x ≠ (− 0))

Theorem: negativep-guts0 (integerp (x) ∧ negativep (x)) → (negative-guts (x) ≠ 0)

Theorem: numberp-integerp (x ∈ N) → integerp (x)

Theorem: iplus-integerp integerp (iplus (x, y))

Theorem: ineg-integerp integerp (ineg (x))

Theorem: idifference-integerp integerp (idifference (x, y))

Theorem: itimes-integerp integerp (itimes (x, y))

Theorem: iremainder-integerp integerp (iremainder (x, y))

Theorem: iquotient-integerp integerp (iquotient (x, y))

; theorems about iplus, idifference, and ineg.

Theorem: iplus-commutativity iplus (x, y) = iplus (y, x)

Theorem: iplus-commutativity1 iplus (x, iplus (y, z)) = iplus (y, iplus (x, z))

Theorem: iplus-associativity iplus (iplus (x, y), z) = iplus (x, iplus (y, z))

Theorem: ineg-iplus ineg (iplus (x, y)) = iplus (ineg (x), ineg (y))

Theorem: iplus-0 izerop (x) → ((iplus (x, y) = fix-int (y)) ∧ (iplus (y, x) = fix-int (y)))

Theorem: iplus-1–1 iplus (1, iplus (-1, x)) = fix-int (x)

Theorem: idifference-x-x idifference (x, x) = 0

Theorem: idifference-negativep negativep (idifference (x, y)) = ilessp (x, y)

; lemmas about ilessp.

Theorem: ilessp-reflex ¬ ilessp (x, x)

Theorem: ilessp-entails-ileq ilessp (x, y) → (¬ ilessp (y, x))

; lemmas about itimes.

Theorem: itimes-0 itimes (0, x) = 0

Theorem: itimes-equal-0 (itimes (x, y) = 0) = (izerop (x) ∨ izerop (y))

Theorem: itimes-commutativity itimes (x, y) = itimes (y, x)

Theorem: itimes-associativity itimes (itimes (x, y), z) = itimes (x, itimes (y, z))

Theorem: itimes-equal-cancellation (¬ izerop (x)) → ((itimes (x, y) = itimes (x, z)) = (fix-int (y) = fix-int (z)))

Theorem: itimes-sign (integerp (x) ∧ integerp (y)) → (negativep (itimes (x, y))

= (((x ∈ N) ∧ (x ≠ 0) ∧ negativep (y)) ∨ (negativep (x) ∧ (y ∈ N) ∧ (y ≠ 0))))

; lemmas about iremainder and iquotient.

Theorem: iremainder-wrt-1 iremainder (x, 1) = 0 Theorem: iquotient-wrt-1 iquotient (x, 1) = fix-int (x)

Theorem: iremainder-wrt–1 iremainder (x, -1) = 0

Theorem: iquotient-wrt–1 iquotient (x, -1) = ineg (x)

Event: Disable iplus.

Event: Disable itimes.

Event: Disable iremainder.

Event: Disable iquotient.

Event: Disable integerp.

; unsigned interpretation of mulu.

Theorem: times-lessp 1 ((x < x1 ) ∧ (y < y1 )) → ((x ∗ y) < (x1 ∗ y1 ))

; three instances of mulu-nat.

Theorem: mulu 1632-nat (nat-rangep (x, 16) ∧ nat-rangep (y, 16)) → (nat-to-uint (mulu (32, x, y, 16))

= (nat-to-uint (x) ∗ nat-to-uint (y)))

Theorem: mulu 3264-nat (nat-rangep (x, 32) ∧ nat-rangep (y, 32)) → (nat-to-uint (mulu (64, x, y, 32))

= (nat-to-uint (x) ∗ nat-to-uint (y)))

Theorem: mulu 3232-nat uint-rangep (nat-to-uint (x) ∗ nat-to-uint (y), 32) → (nat-to-uint (mulu (32, x, y, 32))

= (nat-to-uint (x) ∗ nat-to-uint (y)))

; signed interpretation of muls.

Theorem: exp2-lessp-crock ((i ≄ 0) ∧ if k < i then f

else t endif) → (exp (2, i − 1) < exp (2, k))

Theorem: head-int-crock (integerp (x) ∧ int-rangep (x, n) ∧ (n ≤ j )) → (head (int-to-nat (x, j ), n) = int-to-nat (x, n))

Event: Disable exp2-lessp-crock.

Theorem: times-lessp 2 ((x ≤ x1 ) ∧ (y ≤ y1 ) ∧ (x1 ≄ 0) ∧ (y1 ≄ 0)) → ((x ∗ y) < (2 ∗ x1 ∗ y1 ))

Theorem: times-lessp 3 ((x ≤ exp (2, n − 1)) ∧ (y ≤ exp (2, n − 1)) ∧ (n ≄ 0)) → (((x ∗ y) < exp (2, (n + n) − 1)) = t)

Theorem: times-lessp 4 ((x ≤ exp (2, n − 1)) ∧ (y ≤ exp (2, n − 1)) ∧ (n ≄ 0)) → ((exp (2, (n + n) − 1) < (x ∗ y)) = f)

Theorem: muls-crock (int-rangep (x, n) ∧ int-rangep (y, n) ∧ (n ≄ 0)) → int-rangep (itimes (x, y), n + n)

; three instances of muls-int.

Theorem: muls 1632-int (nat-rangep (x, 16) ∧ nat-rangep (y, 16)) → (nat-to-int (muls (32, x, y, 16), 32)

= itimes (nat-to-int (x, 16), nat-to-int (y, 16)))

Theorem: muls 3264-int (nat-rangep (x, 32) ∧ nat-rangep (y, 32)) → (nat-to-int (muls (64, x, y, 32), 64)

= itimes (nat-to-int (x, 32), nat-to-int (y, 32)))

Theorem: muls 3232-int int-rangep (itimes (nat-to-int (x, 32), nat-to-int (y, 32)), 32) → (nat-to-int (muls (32, x, y, 32), 32)

= itimes (nat-to-int (x, 32), nat-to-int (y, 32)))

Event: Disable times-lessp 1.

Event: Disable times-lessp 2.

Event: Disable times-lessp 3.

Event: Disable times-lessp 4.

Event: Disable muls-crock.

; signed interpretation of irem.
; notice that we only consider the case that the divisor and the result
; have the same boundary n.  Since it is enough to cover the situations
; in the DIVS instructions.

Theorem: irem-int (nat-rangep (x, n) ∧ (nat-to-int (x, n) ≠ 0)) → (nat-to-int (irem (n, x, n, y, j ), n)

= iremainder (nat-to-int (y, j ), nat-to-int (x, n)))

; signed interpretation of iquot.
; notice that we only consider the case that the length of the result
; is at most the length of the dividend.  Since it is enough to cover
; the situations in DIVS instruction.

Theorem: iquot-int (int-rangep (iquotient (nat-to-int (y, j ), nat-to-int (x, i)), n) ∧ (n ≤ j )) → (nat-to-int (iquot (n, x, i, y, j ), n)

= iquotient (nat-to-int (y, j ), nat-to-int (x, i)))

Event: Disable head-int-crock.

; unsigned interpratation of rem.

Theorem: rem-nat nat-rangep (x, n) → (nat-to-uint (rem (n, x, y))

= if nat-to-uint (x) = 0 then nat-to-uint (y) mod exp (2, n) else nat-to-uint (y) mod nat-to-uint (x) endif)

; unsigned interpretation of quot.

Theorem: quot-nat nat-rangep (y, n) → (nat-to-uint (quot (n, x, y)) = (nat-to-uint (y) ÷ nat-to-uint (x)))

Event: Disable int-rangep.

; the only correct execution of DIV is when NO overflow occurs.  We
; need to pass the guard in the specification.  The following few
; lemmas are introduced for this purpose.

Theorem: divu-overflow divu-v (n, x, y) = if uint-rangep (nat-to-uint (y) ÷ nat-to-uint (x), n) then 0

else 1 endif

Theorem: divs-overflow divs-v (n, x, i, y, j ) = if int-rangep (iquotient (nat-to-int (y, j ), nat-to-int (x, i)), n) then 0

else 1 endif

Theorem: divs 3232-overflow divs-v (32, x, 32, y, 32) = if (nat-to-int (y, 32) = -2147483648)

∧ (nat-to-int (x, 32) = -1) then 1 else 0 endif

Event: Disable divu-v.

Event: Disable divs-v.

;          UNSIGNED INTERPRETATION OF ADDITION AND SUBTRACTION
;

Theorem: add-nat-la (nat-rangep (x, n) ∧ nat-rangep (y, n)) → (add (n, x, y)

= if (x + y) < exp (2, n) then x + y else (x + y) − exp (2, n) endif)

Theorem: sub-nat-la (nat-rangep (x, n) ∧ nat-rangep (y, n)) → (sub (n, x, y)

= if y < x then (y + exp (2, n)) − x else y − x endif)

Theorem: adder-nat-la (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c)) → (adder (n, c, x, y)

= if (c + x + y) < exp (2, n) then c + x + y else (c + x + y) − exp (2, n) endif)

Theorem: subtracter-nat-la (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c)) → (subtracter (n, c, x, y)

= if y < (c + x) then (y + exp (2, n)) − (c + x) else y − (c + x) endif)

Theorem: plus-numberp (y ∉ N) → ((x + y) = fix (x))

; unsigned interpretation of adder.

Theorem: adder-uint (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c)) → (nat-to-uint (adder (n, c, x, y))

= if (c + nat-to-uint (x) + nat-to-uint (y)) < exp (2, n) then c + nat-to-uint (x) + nat-to-uint (y) else (c + nat-to-uint (x) + nat-to-uint (y))

− exp (2, n) endif)

; unsigned interpretation of subtracter.

Theorem: subtracter-uint (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c)) → (nat-to-uint (subtracter (n, c, x, y))

= if nat-to-uint (y) < (c + nat-to-uint (x)) then (nat-to-uint (y) + exp (2, n)) − (c + nat-to-uint (x))

else nat-to-uint (y) − (c + nat-to-uint (x)) endif)

; unsigned interpretation of add.

Theorem: add-uint (nat-rangep (x, n) ∧ nat-rangep (y, n)) → (nat-to-uint (add (n, x, y))

= if (nat-to-uint (x) + nat-to-uint (y)) < exp (2, n) then nat-to-uint (x) + nat-to-uint (y) else (nat-to-uint (x) + nat-to-uint (y)) − exp (2, n) endif)

; unsigned interpretation of sub.

Theorem: sub-uint (nat-rangep (x, n) ∧ nat-rangep (y, n)) → (nat-to-uint (add (n, x, neg (n, y)))

= if nat-to-uint (x) < nat-to-uint (y) then (nat-to-uint (x) + exp (2, n)) − nat-to-uint (y) else nat-to-uint (x) − nat-to-uint (y) endif)

Event: Disable plus-numberp.

Event: Disable add-nat-la.

Event: Disable sub-nat-la.

Event: Disable adder-nat-la.

Event: Disable subtracter-nat-la.

;                  THEOREMS OF ADDER
;

Theorem: adder-shift-carry adder (n, c, x, adder (n, d, y, z)) = adder (n, d, x, adder (n, c, y, z))

Theorem: adder-commutativity adder (n, c, x, y) = adder (n, c, y, x)

Theorem: adder-associativity adder (n, d, adder (n, c, x, y), z) = adder (n, c, x, adder (n, d, y, z))

; another commutativity theorem about adder.

Theorem: adder-commutativity1 adder (n, c, x, adder (n, d, y, z)) = adder (n, c, y, adder (n, d, x, z))

;               THEOREMS ABOUT ADD AND SUB
;
; trivial!

Theorem: add-of-0 add (0, x, y) = 0

; x + 0 = x!

Theorem: add-0 (add (n, x, 0) = head (x, n)) ∧ (add (n, 0, x) = head (x, n))

; x - 0 = x!

Theorem: sub-0 sub (n, 0, x) = head (x, n)

; x - x = 0!

Theorem: sub-x-x sub (n, x, x) = 0

; commutativity of addition : x + y = y + x.

Theorem: add-commutativity add (n, x, y) = add (n, y, x)

; associativity of addition: (x + y) + z = x + (y + z).

Theorem: add-associativity add (n, add (n, x, y), z) = add (n, x, add (n, y, z))

; another commutativity of addition: x + (y + z) = y + (x + z).

Theorem: add-commutativity1 add (n, x, add (n, y, z)) = add (n, y, add (n, x, z)) Theorem: remainder-leq x ≮ (x mod y) Theorem: add-leq (x + y) ≮ add (n, x, y) Theorem: sub-leq-la (x ≤ y) → ((y − x) ≮ sub (n, x, y)) Event: Disable remainder-leq.

; addition and subtraction are always in "good" range.

Theorem: adder-nat-rangep nat-rangep (adder (n, c, x, y), n) Theorem: subtracter-nat-rangep nat-rangep (subtracter (n, c, y, x), n)

Theorem: add-nat-rangep nat-rangep (add (n, x, y), n) Theorem: sub-nat-rangep nat-rangep (sub (n, x, y), n) Theorem: adder-head (adder (n, c, head (x, n), y) = adder (n, c, x, y)) ∧ (adder (n, c, x, head (y, n)) = adder (n, c, x, y)) Theorem: add-head (add (n, head (x, n), y) = add (n, x, y)) ∧ (add (n, x, head (y, n)) = add (n, x, y))

; x + y = x - z <==> y + z = 0.

Theorem: add-sub-cancel (nat-rangep (y, n) ∧ nat-rangep (z, n)) → ((add (n, x, y) = sub (n, z, x)) = (add (n, y, z) = 0))

; x - y = 0 <==> x = y.

Theorem: sub-equal-0 (nat-rangep (x, n) ∧ nat-rangep (y, n)) → ((sub (n, x, y) = 0) = (fix (x) = fix (y)))

; a bridge from add to adder.

Theorem: add-adder add (n, x, y) = adder (n, 0, x, y) Theorem: plus-add1-sub1 (y ≄ 0) → ((1 + (x + (y − 1))) = (x + y))

; a bridge from sub to adder.

Theorem: sub-adder sub (n, y, x) = adder (n, 1, x, lognot (n, y)) Theorem: add-neg-adder add (n, x, neg (n, y)) = adder (n, 1, x, lognot (n, y))

; plus-add1-sub1 is a very ``dangerous'' event.  To use it,  you need
; to enable it first.

Event: Disable plus-add1-sub1.

Event: Disable add.

Event: Disable sub.

; (x + y) -z = x + (y - z).

Theorem: add-sub sub (n, z, add (n, x, y)) = add (n, x, sub (n, z, y))

; (x - y) + z = x + (z - y).

Theorem: sub-add add (n, sub (n, y, x), z) = add (n, x, sub (n, y, z))

; (x - y) - z = x - (y + z).

Theorem: sub-sub sub (n, z, sub (n, y, x)) = sub (n, add (n, y, z), x)

; x - (y - z) = x + (z - y).

Theorem: sub-sub1 sub (n, sub (n, z, y), x) = add (n, x, sub (n, y, z))

; another commutativity of addition: x + (y - z) = y + (x - z).

Theorem: add-commutativity2 add (n, x, sub (n, z, y)) = add (n, y, sub (n, z, x))

; x + y = x <==> y = 0.

Theorem: add-cancel0 (add (n, x, y) = x) = ((x ∈ N) ∧ nat-rangep (x, n) ∧ (head (y, n) = 0))

; x - y = x <==> y = 0.

Theorem: sub-cancel0 (nat-rangep (x, n) ∧ nat-rangep (y, n)) → ((sub (n, y, x) = x) = ((x ∈ N) ∧ (y ≃ 0))) Theorem: adder-cancel (adder (n, c, x, y) = adder (n, c, x, z)) = (head (y, n) = head (z, n))

; x + y = x + z <==> y = z.

Theorem: add-cancel (add (n, x, y) = add (n, x, z)) = (head (y, n) = head (z, n))

; x - y = x - z <==> y = z.

Theorem: sub-cancel (nat-rangep (y, n) ∧ nat-rangep (z, n)) → ((sub (n, y, x) = sub (n, z, x)) = (fix (y) = fix (z)))

Event: Disable add-adder.

Event: Disable sub-adder.

; x + (y - y) = x!

Theorem: addy-y nat-rangep (x, n) → (add (n, x, sub (n, y, y)) = fix (x))

; y + (x - y) = x!

Theorem: addy-y1 nat-rangep (x, n) → (add (n, y, sub (n, y, x)) = fix (x))

;           INTEGER INTERPRETATION OF ADDITION AND SUBTRACTION
; a bridge for adder-int.

Theorem: adder-int-bridge (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c)) → (nat-to-int (adder (n, c, x, y), n)

= adder-int-end (n, c, nat-to-int (x, n), nat-to-int (y, n)))

Event: Disable adder-int-end.

Event: Disable adder.

; integer interpretation of adder.

Theorem: adder-int (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c)) → (nat-to-int (adder (n, c, x, y), n)

= if int-rangep (iplus (nat-to-int (x, n), iplus (nat-to-int (y, n), c)),

n)

then iplus (nat-to-int (x, n), iplus (nat-to-int (y, n), c))

elseif negativep (nat-to-int (x, n))

then iplus (nat-to-int (x, n),

iplus (nat-to-int (y, n), iplus (c, exp (2, n))))

else iplus (nat-to-int (x, n), iplus (nat-to-int (y, n), iplus (c, − exp (2, n)))) endif)

; integer interpretation of subtracter.

Theorem: subtracter-int (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c) ∧ (n ≄ 0)) → (nat-to-int (subtracter (n, c, x, y), n)

= if int-rangep (idifference (nat-to-int (y, n),

iplus (nat-to-int (x, n), c)),

n)

then idifference (nat-to-int (y, n), iplus (nat-to-int (x, n), c)) elseif negativep (nat-to-int (y, n)) then idifference (iplus (nat-to-int (y, n), exp (2, n)),

iplus (nat-to-int (x, n), c))

else idifference (iplus (nat-to-int (y, n), − exp (2, n)), iplus (nat-to-int (x, n), c)) endif)

Event: Disable subtracter.

; integer interpretation of add.

Theorem: add-int (nat-rangep (x, n) ∧ nat-rangep (y, n)) → (nat-to-int (add (n, x, y), n)

= if int-rangep (iplus (nat-to-int (x, n), nat-to-int (y, n)), n) then iplus (nat-to-int (x, n), nat-to-int (y, n)) elseif negativep (nat-to-int (x, n)) then iplus (nat-to-int (x, n), iplus (nat-to-int (y, n), exp (2, n))) else iplus (nat-to-int (x, n),

iplus (nat-to-int (y, n), − exp (2, n))) endif)

; integer interpretation of sub.

Theorem: sub-int (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (nat-to-int (add (n, x, neg (n, y)), n)

= if int-rangep (idifference (nat-to-int (x, n), nat-to-int (y, n)), n) then idifference (nat-to-int (x, n), nat-to-int (y, n)) elseif negativep (nat-to-int (x, n)) then idifference (iplus (nat-to-int (x, n), exp (2, n)),

nat-to-int (y, n))

else idifference (iplus (nat-to-int (x, n), − exp (2, n)), nat-to-int (y, n)) endif)

Event: Disable add-neg-adder.

;            THEOREMS ABOUT HEAD, TAIL, APP, AND REPLACE
;

Theorem: head-head head (head (x, m), n) = if n < m then head (x, n)

else head (x, m) endif

Theorem: tail-tail tail (tail (x, m), n) = tail (x, m + n)

Theorem: head-plus-cancel0 (head (i + j , n) = head (i, n)) = (head (j , n) = 0)

Theorem: head-plus-cancel (head (x + y, n) = head (x + z, n)) = (head (y, n) = head (z, n))

Theorem: head-plus-head head (x + head (y, n), n) = head (x + y, n)

Theorem: remainder-plus-times-exp2-1 (j ≤ i) → (((x + (y ∗ exp (2, i))) mod exp (2, j )) = (x mod exp (2, j )))

Theorem: remainder2-plus-times-exp2 (i ≄ 0) → (((x + (y ∗ exp (2, i))) mod 2) = (x mod 2))

Theorem: remainder-plus-times-exp2-2 ((x < exp (2, i)) ∧ (i ≤ j )) → (((x + (y ∗ exp (2, i))) mod exp (2, j ))

= if i < j then x + ((y mod exp (2, j − i)) ∗ exp (2, i)) else fix (x) endif)

Theorem: quotient-plus-times-exp2-1 (j < i) → (((x + (y ∗ exp (2, i))) ÷ exp (2, j ))

= ((x ÷ exp (2, j )) + (y ∗ exp (2, i − j ))))

Theorem: exp2-leq (i ≤ j ) → (exp (2, j ) ≮ exp (2, i))

Theorem: quotient-plus-times-exp2-2 ((i ≤ j ) ∧ (x < exp (2, i))) → (((x + (y ∗ exp (2, i))) ÷ exp (2, j )) = (y ÷ exp (2, j − i)))

Theorem: remainder-quotient-exp2 ((x mod exp (2, i)) ÷ exp (2, j )) = if j < i then (x ÷ exp (2, j )) mod exp (2, i − j )

else 0 endif Event: Disable exp2-leq.

Theorem: head-replace head (replace (m, x, y), n) = if m < n then replace (m, x, head (y, n))

else head (x, n) endif

Theorem: tail-head tail (head (x, m), n) = head (tail (x, n), m − n)

Theorem: tail-app tail (app (i, x, y), j ) = if j < i then app (i − j , tail (x, j ), y)

else tail (y, j − i) endif

Theorem: tail-replace tail (replace (i, x, y), j ) = if j < i then replace (i − j , tail (x, j ), tail (y, j ))

else tail (y, j ) endif

Theorem: replace-reflex replace (n, x, x) = fix (x)

Theorem: replace-head (n ≤ m) → (replace (n, head (x, m), x) = fix (x))

Theorem: replace-associativity replace (n, x, replace (n, y, z)) = replace (n, replace (n, x, y), z)

Theorem: replace-leq1 (j ≤ i) → (replace (i, x, replace (j , y, z)) = replace (i, x, z))

Theorem: replace-leq (i ≤ j ) → (replace (i, replace (j , x, y), z) = replace (i, x, z))

Theorem: head-app (i ≤ j ) → (head (app (j , x, y), i) = head (x, i))

; a few basic lemmas about bcar and bcdr.  They are useful in induction
; proofs with bcar and bcdr disabled.

Theorem: bcar-nonnumberp (x ∉ N) → (bcar (x) = 0)

Theorem: bcdr-nonnumberp (x ∉ N) → (bcdr (x) = 0)

Theorem: bcar-1 (bcar (2 ∗ x) = 0) ∧ (bcar (1 + (2 ∗ x)) = 1)

Theorem: bcdr-1 (bcdr (2 ∗ x) = fix (x)) ∧ (bcdr (1 + (2 ∗ x)) = fix (x))

Theorem: bcar-2 bcar (x + (2 ∗ y)) = bcar (x)

Theorem: bcdr-2 bcdr (x + (2 ∗ y)) = (bcdr (x) + y)

; the first "bit" of head.

Theorem: bcar-head bcar (head (x, n)) = if n ≃ 0 then 0

else bcar (x) endif

; the first "bit" of app.

Theorem: bcar-app bcar (app (n, x, y)) = if n ≃ 0 then bcar (y)

else bcar (x) endif

; the first "bit" of replace.

Theorem: bcar-replace bcar (replace (n, x, y)) = if n ≃ 0 then bcar (y)

else bcar (x) endif

Theorem: bcar-lessp bcar (x) < 2

Theorem: bcdr-lessp (bcdr (x) < y) = (x < (2 ∗ y))

Theorem: app-associativity app (n1 , x, app (n2 , y, z)) = app (n1 + n2 , app (n1 , x, y), z)

Theorem: app-head-tail app (n, head (x, n), tail (x, n)) = fix (x)

Theorem: head-app-head-tail app (m, head (x, m), head (tail (x, m), n)) = head (x, m + n)

Event: Disable head.

Event: Disable tail.

Event: Disable bcar.

Event: Disable bcdr.

Theorem: app-nat-rangep (m ≤ n) → (nat-rangep (app (m, x, y), n) = nat-rangep (y, n − m))

Theorem: replace-nat-rangep (m ≤ n) → (nat-rangep (replace (m, x, y), n) = nat-rangep (y, n))

Event: Disable app.

Event: Disable replace.

;                     BITN

Theorem: bitn-0 (bitn (0, n) = 0) ∧ ((x ∉ N) → (bitn (x, i) = 0))

Theorem: bitn-0-1 bitn (x, n) < 2

Theorem: bitn-head bitn (head (x, i), j ) = if j < i then bitn (x, j )

else 0 endif

Theorem: bitn-tail bitn (tail (x, i), j ) = bitn (x, i + j )

Theorem: bitn-app bitn (app (n, x, y), k) = if k < n then bitn (x, k)

else bitn (y, k − n) endif

Theorem: bitn-replace bitn (replace (n, x, y), k) = if k < n then bitn (x, k)

else bitn (y, k) endif Event: Disable bitn.

Theorem: bitn-lognot nat-rangep (x, n) → (bitn (lognot (n, x), i)

= if i < n then b-not (bitn (x, i)) else 0 endif)

;               LOGAND, LOGOR, AND LOGEOR.

Theorem: logor-equal-0 (logor (x, y) = 0) = ((x ≃ 0) ∧ (y ≃ 0))

Theorem: logeor-equal-0 (logeor (x, y) = 0) = (fix (x) = fix (y))

Theorem: logand-commutativity logand (x, y) = logand (y, x)

Theorem: logor-commutativity logor (x, y) = logor (y, x)

Theorem: logeor-commutativity logeor (x, y) = logeor (y, x)

Theorem: logand-logor logand (x, logor (y, z)) = logor (logand (x, y), logand (x, z))

Theorem: logand-logeor logand (x, logeor (y, z)) = logeor (logand (x, y), logand (x, z))

Theorem: logand-uint-la nat-to-uint (logand (exp (2, i) − 1, y)) = (nat-to-uint (y) mod exp (2, i))

Theorem: logand-uint (exp (2, log (2, 1 + x)) = (1 + x)) → (nat-to-uint (logand (x, y)) = (nat-to-uint (y) mod (1 + x)))

;            HEAD WITH READ/WRITE AND READM/WRITEM

Theorem: head-readp (n ≤ k) → (readp (head (x, k), n, map) = readp (x, n, map))

Theorem: head-pc-readp (n ≤ k) → (pc-readp (head (x, k), n, map) = pc-readp (x, n, map))

Theorem: head-writep (n ≤ k) → (writep (head (x, k), n, map) = writep (x, n, map))

Theorem: head-read (n ≤ k) → (read (head (x, k), n, bt) = read (x, n, bt))

Theorem: head-pc-read (n ≤ k) → (pc-read (head (x, k), n, bt) = pc-read (x, n, bt))

Theorem: head-write (n ≤ k) → (write (value, head (x, k), n, bt) = write (value, x, n, bt))

Theorem: head-byte-readp byte-readp (head (x, 32), mem) = byte-readp (x, mem)

Theorem: head-pc-byte-readp pc-byte-readp (head (x, 32), mem) = pc-byte-readp (x, mem)

Theorem: head-byte-writep byte-writep (head (x, 32), mem) = byte-writep (x, mem)

Theorem: head-byte-read byte-read (head (x, 32), mem) = byte-read (x, mem)

Theorem: head-byte-pc-read pc-byte-read (head (x, 32), mem) = pc-byte-read (x, mem)

Theorem: head-byte-write byte-write (value, head (x, 32), mem) = byte-write (value, x, mem)

Theorem: head-read-memp read-memp (head (x, 32), mem, k) = read-memp (x, mem, k)

Theorem: head-pc-read-memp pc-read-memp (head (x, 32), mem, k) = pc-read-memp (x, mem, k)

Theorem: head-write-memp write-memp (head (x, 32), mem, k) = write-memp (x, mem, k)

Theorem: head-read-mem read-mem (head (x, 32), mem, k) = read-mem (x, mem, k)

Theorem: head-pc-read-mem pc-read-mem (head (x, 32), mem, k) = pc-read-mem (x, mem, k)

Theorem: head-write-mem write-mem (value, head (x, 32), mem, k) = write-mem (value, x, mem, k)

Theorem: head-readm-mem readm-mem (opsz, head (x, 32), mem, n) = readm-mem (opsz, x, mem, n)

;                  NAT-RANGEP

Theorem: nat-rangep-of-0 nat-rangep (0, n)

Theorem: nat-rangep-ub nat-rangep (exp (2, k) − 1, n) = (n ≮ k)

Theorem: nat-rangep-0 nat-rangep (x, 0) = (x ≃ 0)

Theorem: nat-plus-rangep nat-rangep (x, k) → (nat-rangep (x, k + j ) ∧ nat-rangep (x, j + k))

Theorem: sub1-nat-rangep nat-rangep (x, n) → nat-rangep (x − 1, n)

Theorem: sub1-times2-nat-rangep nat-rangep ((2 ∗ x) − 1, 1 + n) = nat-rangep (x − 1, n)

Theorem: difference-nat-rangep nat-rangep (x, n) → nat-rangep (x − y, n)

Theorem: quotient-nat-rangep nat-rangep (x, n) → nat-rangep (x ÷ y, n)

Theorem: times-exp2-nat-rangep nat-rangep (x ∗ exp (2, i), n) = nat-rangep (x, n − i)

Theorem: logand-nat-rangep (nat-rangep (x, n) ∨ nat-rangep (y, n)) → nat-rangep (logand (x, y), n)

Theorem: logor-nat-rangep nat-rangep (logor (x, y), n) = (nat-rangep (x, n) ∧ nat-rangep (y, n))

Theorem: logeor-nat-rangep (nat-rangep (x, n) ∧ nat-rangep (y, n)) → nat-rangep (logeor (x, y), n)

Theorem: head-nat-rangep (m ≤ n) → nat-rangep (head (x, m), n)

Theorem: tail-nat-rangep nat-rangep (tail (x, m), n) = nat-rangep (x, m + n)

Theorem: read-rn-nat-rangep nat-rangep (read-rn (n, rn, rfile), n) Theorem: byte-read-nat-rangep (8 ≤ n) → nat-rangep (byte-read (x, mem), n) Theorem: pc-byte-read-nat-rangep nat-rangep (pc-byte-read (x, mem), 8) Event: Disable nat-rangep.

Theorem: mulu-nat-rangep nat-rangep (mulu (n, x, y, i), n) Theorem: muls-nat-rangep nat-rangep (muls (n, x, y, i), n) Theorem: quot-nat-rangep nat-rangep (quot (n, x, y), n) Theorem: rem-nat-rangep nat-rangep (rem (n, x, y), n) Theorem: iquot-nat-rangep nat-rangep (iquot (n, x, i, y, j ), n) Theorem: irem-nat-rangep nat-rangep (irem (n, x, i, y, j ), n) Theorem: neg-nat-rangep nat-rangep (neg (n, x), n)

;                         EXT

Theorem: ext-0 ext (n, 0, size) = 0 Theorem: ext-lemma (size ≤ n) → (ext (n, x, size) = head (x, size)) Theorem: head-ext ((i ≤ j ) ∧ (j ≤ k)) → (head (ext (j , x, k), i) = head (x, i)) Theorem: ext-nat-rangep nat-rangep (ext (n, x, size), size) Event: Disable ext.

;                      CVZNX-FLAGS

Theorem: set-cvznx-c ccr-c (set-cvznx (cvznx (c, v, z, n, x), ccr)) = fix-bit (c) Theorem: set-cvznx-v ccr-v (set-cvznx (cvznx (c, v, z, n, x), ccr)) = fix-bit (v) Theorem: set-cvznx-z ccr-z (set-cvznx (cvznx (c, v, z, n, x), ccr)) = fix-bit (z) Theorem: set-cvznx-n ccr-n (set-cvznx (cvznx (c, v, z, n, x), ccr)) = fix-bit (n) Theorem: set-cvznx-x ccr-x (set-cvznx (cvznx (c, v, z, n, x), ccr)) = fix-bit (x)

; the new cvznx-flags replaces the old ones.

Theorem: set-set-cvznx1 set-cvznx (x, set-cvznx (y, ccr)) = set-cvznx (x, ccr) Theorem: set-cvznx-ccr set-cvznx (ccr, ccr) = fix (ccr) Theorem: set-set-cvznx2 set-cvznx (set-cvznx (x, ccr), ccr) = set-cvznx (x, ccr) Theorem: set-cvznx-nat-rangep nat-rangep (set-cvznx (x, ccr), 8) = nat-rangep (ccr, 8) Event: Disable ccr-c.

Event: Disable ccr-v.

Event: Disable ccr-z.

Event: Disable ccr-n.

Event: Disable ccr-x.

Event: Disable cvznx.

Event: Disable set-cvznx.

;                       MC ACCESSORS

Theorem: mc-status-rewrite mc-status (mc-state (status, rfile, pc, ccr, mem)) = status

Theorem: mc-rfile-rewrite mc-rfile (mc-state (status, rfile, pc, ccr, mem)) = rfile

Theorem: mc-pc-rewrite nat-rangep (pc, 32) → (mc-pc (mc-state (status, rfile, pc, ccr, mem)) = fix (pc))

Theorem: mc-ccr-rewrite nat-rangep (ccr, 8) → (mc-ccr (mc-state (status, rfile, pc, ccr, mem)) = fix (ccr))

Theorem: mc-mem-rewrite mc-mem (mc-state (status, rfile, pc, ccr, mem)) = mem

; lemmas about those mc accessors.

Theorem: mc-pc-rangep nat-rangep (mc-pc (s), 32)

Theorem: mc-ccr-rangep nat-rangep (mc-ccr (s), 8)

Event: Disable mc-status.

Event: Disable mc-rfile.

Event: Disable mc-pc.

Event: Disable mc-ccr.

Event: Disable mc-mem.

Event: Disable mc-state.

;           THE BASIC GET-NTH/PUT-NTH RELATIONS
;

Theorem: get-nth-0 (i ∉ N) → (get-nth (i, lst) = get-nth (0, lst))

Theorem: put-nth-0 (i ∉ N) → (put-nth (v, i, lst) = put-nth (v, 0, lst))

Event: Disable get-nth-0.

Event: Disable put-nth-0.

Theorem: get-nth-nil (get-nth (n, nil) = 0) ∧ (get-nth (n, 0) = 0)

Theorem: get-put get-nth (n, put-nth (value, m, lst)) = if fix (m) = fix (n) then value

else get-nth (n, lst) endif

Theorem: put-put put-nth (value1 , n, put-nth (value, n, lst)) = put-nth (value1 , n, lst)

Theorem: put-get (n < len (lst)) → (put-nth (get-nth (n, lst), n, lst) = lst)

Theorem: put-nth-len len (put-nth (value, n, lst)) = if n < len (lst) then len (lst)

else 1 + n endif

;            THE BASIC READ-RN/WRITE-RN RELATIONS
;

Theorem: head-read-rn (n1 ≤ n2 ) → (head (read-rn (n2 , rn, rfile), n1 ) = read-rn (n1 , rn, rfile))

; stop proving.

Definition: read-write-rn-end (n2 , rn, n1 , value, rm, rfile) = read-rn (n2 , rn, write-rn (n1 , value, rm, rfile))

Theorem: read-write-rn read-rn (n2 , rn, write-rn (n1 , value, rm, rfile)) = if fix (rm) = fix (rn)

then if n2 ≤ n1 then head (value, n2 )

else replace (n1 , value, read-rn (n2 , rn, rfile)) endif else read-rn (n2 , rn, rfile) endif Theorem: write-write-rn (n1 ≤ n2 ) → (write-rn (n2 , v2 , rn, write-rn (n1 , v1 , rn, rfile))

= write-rn (n2 , v2 , rn, rfile))

Theorem: write-rn-len len (write-rn (oplen, value, rn, rfile)) = if rn < len (rfile) then len (rfile)

else 1 + rn endif

Event: Disable read-rn.

Event: Disable write-rn.

;             THE BASIC READM-RN/WRITEM-RN EVENTS
;

Theorem: readm-rn-len len (readm-rn (oplen, rnlst, rfile)) = len (rnlst)

Definition: get-vlst (oplen, value, rn, rnlst, vlst) = if rnlst ≃ nil then value

elseif fix (rn) = fix (car (rnlst))

then get-vlst (oplen, head (car (vlst), oplen), rn, cdr (rnlst), cdr (vlst))

else get-vlst (oplen, value, rn, cdr (rnlst), cdr (vlst)) endif

; we deliberately put on the hypothesis (numberp value) to restrict the use
; of this lemma.  The dead loop situation is thereby avoided.

Theorem: get-vlst-member (value ∈ N) → (get-vlst (oplen, value, rn, rnlst, vlst)

= if n-member (rn, rnlst) then get-vlst (oplen, nil, rn, rnlst, vlst) else value endif)

; stop proving.

Definition: read-writem-rn-end (n1 , rn, n2 , vlst, rnlst, rfile) = read-rn (n1 , rn, writem-rn (n2 , vlst, rnlst, rfile))

Theorem: read-writem-rn read-rn (n1 , rn, writem-rn (n2 , vlst, rnlst, rfile)) = if n-member (rn, rnlst) then if (n1 ≤ n2 ) ∧ (n2 ≤ 32)

then get-vlst (n1 , 0, rn, rnlst, vlst)

else read-writem-rn-end (n1 , rn, n2 , vlst, rnlst, rfile) endif else read-rn (n1 , rn, rfile) endif

Event: Disable read-writem-rn-end.

Theorem: readm-write-rn (¬ n-member (rn, rnlst)) → (readm-rn (n1 , rnlst, write-rn (n2 , value, rn, rfile))

= readm-rn (n1 , rnlst, rfile))

Theorem: read-rn-0 (rn ∉ N) → (read-rn (oplen, rn, rfile) = read-rn (oplen, 0, rfile))

Theorem: get-vlst-readm-rn (n1 ≤ n2 ) → (get-vlst (n1 , 0, rn, rnlst, readm-rn (n2 , rnlst, rfile))

= if n-member (rn, rnlst) then read-rn (n1 , rn, rfile) else 0 endif)

Event: Disable read-rn-0.

Event: Disable get-vlst-member.

Event: Disable get-vlst.

;           THE BASIC READ-MEM/WRITE-MEM EVENTS
;

Theorem: pc-readp->readp pc-readp (x, n, map) → readp (x, n, map)

Theorem: writep->readp writep (x, n, map) → readp (x, n, map)

; a read right after a write at the same location returns the new value
; just writen.  But a read right after a write at a different location
; has the same effect as a read made on the original binary tree.

Definition: modn-eq (n, x, y) = if n ≃ 0 then t

else (bitn (x, n − 1) = bitn (y, n − 1)) ∧ modn-eq (n − 1, x, y) endif Theorem: read-write read (y, n, write (value, x, n, bt)) = if modn-eq (n, x, y) then value

else read (y, n, bt) endif

; pc should always be able to go through the memory.

Theorem: pc-read-write (writep (x, n, map) ∧ pc-readp (y, n, map)) → (pc-read (y, n, write (value, x, n, bt)) = pc-read (y, n, bt))

; write twice at the same location is equivalent to the second write on
; the original binary tree.

Theorem: write-write-la write (v2 , y, n, write (v1 , x, n, bt)) = if ¬ modn-eq (n, x, y) then write (v1 , x, n, write (v2 , y, n, bt))

else write (v2 , y, n, bt) endif

Theorem: write-write write (v2 , x, n, write (v1 , x, n, bt)) = write (v2 , x, n, bt)

Event: Disable pc-read.

Theorem: plus-times-equal ((a < k) ∧ (b < k)) → (((a + (i ∗ k)) = (b + (j ∗ k)))

= ((fix (a) = fix (b)) ∧ (fix (i) = fix (j ))))

Theorem: app-cancel (app (n, x, y) = app (n, x1 , y1 )) = ((head (x, n) = head (x1 , n)) ∧ (fix (y) = fix (y1 )))

Event: Disable plus-times-equal.

Theorem: head-app-cancel (head (x, n) = app (n, x1 , y1 )) = ((head (x, n) = head (x1 , n)) ∧ (y1 ≃ 0))

Theorem: head-recursion head (x, 1 + n) = app (n, head (x, n), bitn (x, n))

Theorem: modn-eq-equal modn-eq (n, x, y) = (head (x, n) = head (y, n))

Theorem: ext-equal ((n ≤ size) ∧ (n ≄ 0)) → ((ext (n, x, size) = ext (n, y, size)) = (head (x, n) = head (y, n)))

Theorem: ext-equal-0 ((n ≤ size) ∧ (n ≄ 0)) → ((ext (n, x, size) = 0) = (head (x, n) = 0))

Event: Disable head-recursion.

;               BYTE-READ/BYTE-WRITE
;
; pc-byte-readp --> byte-readp.

Theorem: pc-byte-readp->byte-readp pc-byte-readp (x, mem) → byte-readp (x, mem)

; byte-writep --> byte-readp.

Theorem: byte-writep->readp byte-writep (x, mem) → byte-readp (x, mem)

Theorem: byte-read-write byte-read (x, byte-write (v, y, mem)) = if mod32-eq (x, y)

then if nat-rangep (v, 8) then fix (v) else head (v, 8) endif else byte-read (x, mem) endif

Theorem: byte-write-write-la byte-write (v2 , y, byte-write (v1 , x, mem)) = if ¬ mod32-eq (x, y) then byte-write (v1 , x, byte-write (v2 , y, mem))

else byte-write (v2 , y, mem) endif

Theorem: byte-write-write byte-write (v2 , x, byte-write (v1 , x, mem)) = byte-write (v2 , x, mem)

Theorem: pc-byte-read-write (byte-writep (x, mem) ∧ pc-byte-readp (y, mem)) → (pc-byte-read (y, byte-write (value, x, mem)) = pc-byte-read (y, mem))

; write on memory does not change the properties of the memory.

Theorem: byte-write-maintain-pc-byte-readp pc-byte-readp (x, byte-write (value, y, mem)) = pc-byte-readp (x, mem)

Theorem: byte-write-maintain-byte-readp byte-readp (x, byte-write (value, y, mem)) = byte-readp (x, mem)

Theorem: byte-write-maintain-byte-writep byte-writep (x, byte-write (value, y, mem)) = byte-writep (x, mem)

; a lemma useful to deal with read-mem/write-mem.

Theorem: byte-write-app (8 ≤ n) → (byte-write (app (n, x, y), addr, mem) = byte-write (x, addr, mem))

Event: Disable pc-byte-readp.

Event: Disable byte-readp.

Event: Disable byte-writep.

Event: Disable pc-byte-read.

Event: Disable byte-read.

Event: Disable byte-write.

;             THE BASIC READ-MEM/WRITE-MEM EVENTS

Definition: mem-induct0 (k, n) = if k ≃ 0 then 0

else mem-induct0 (k − 1, n − 8) endif

Theorem: pc-read-mem-nat-rangep (n = (8 ∗ k)) → nat-rangep (pc-read-mem (x, mem, k), n)

Theorem: read-mem-nat-rangep ((8 ∗ k) ≤ n) → nat-rangep (read-mem (x, mem, k), n)

; write on memory does not change the properties of the memory. i.e. RAM is
; still RAM, ROM is still ROM, and UNAVAILABLE is still unavailable.

Theorem: write-mem-maintain-pc-byte-readp pc-byte-readp (addr, write-mem (value, x, mem, k)) = pc-byte-readp (addr, mem)

Theorem: write-mem-maintain-byte-readp byte-readp (addr, write-mem (value, x, mem, k)) = byte-readp (addr, mem)

Theorem: write-mem-maintain-byte-writep byte-writep (addr, write-mem (value, x, mem, k)) = byte-writep (addr, mem)

Theorem: byte-write-maintain-pc-read-memp pc-read-memp (addr, byte-write (value, x, mem), n) = pc-read-memp (addr, mem, n)

Theorem: byte-write-maintain-read-memp read-memp (addr, byte-write (value, x, mem), n) = read-memp (addr, mem, n)

Theorem: byte-write-maintain-write-memp write-memp (addr, byte-write (value, x, mem), n) = write-memp (addr, mem, n)

Theorem: write-mem-maintain-pc-read-memp pc-read-memp (addr, write-mem (value, x, mem, m), n) = pc-read-memp (addr, mem, n)

Theorem: write-mem-maintain-read-memp read-memp (addr, write-mem (value, x, mem, m), n) = read-memp (addr, mem, n)

Theorem: write-mem-maintain-write-memp write-memp (addr, write-mem (value, x, mem, m), n) = write-memp (addr, mem, n)

; if it is pc-readable, then it must be readable.

Theorem: pc-read-memp->read-memp pc-read-memp (x, mem, n) → read-memp (x, mem, n)

; if it is writeable, then it must be readable.

Theorem: write-memp->read-memp write-memp (x, mem, n) → read-memp (x, mem, n)

; program segments are never changed as the memory are changed.

Theorem: pc-byte-read-write-mem (write-memp (x, mem, n) ∧ pc-byte-readp (y, mem)) → (pc-byte-read (y, write-mem (value, x, mem, n)) = pc-byte-read (y, mem))

Theorem: pc-read-mem-byte-write (byte-writep (x, mem) ∧ pc-read-memp (y, mem, n)) → (pc-read-mem (y, byte-write (value, x, mem), n) = pc-read-mem (y, mem, n))

Theorem: pc-read-mem-write-mem (write-memp (x, mem, m) ∧ pc-read-memp (y, mem, n)) → (pc-read-mem (y, write-mem (value, x, mem, m), n) = pc-read-mem (y, mem, n))

; a byte-read vs a multi-write.
; stop proving.

Definition: byte-read-write-mem-end (x, value, y, mem, k) = byte-read (x, write-mem (value, y, mem, k))

Theorem: byte-read-write-mem byte-read (x, write-mem (value, y, mem, k)) = if disjoint (x, 1, y, k) then byte-read (x, mem)

else byte-read-write-mem-end (x, value, y, mem, k) endif

; a multi-read vs a byte-write.
; stop proving.

Definition: read-mem-byte-write-end (x, n, value, y, mem) = read-mem (x, byte-write (value, y, mem), n)

Theorem: read-mem-byte-write read-mem (x, byte-write (value, y, mem), n) = if disjoint0 (x, n, y) then read-mem (x, mem, n)

else read-mem-byte-write-end (x, n, value, y, mem) endif

; a multi-read vs a multi-write.
; stop proving.

Definition: read-write-mem-end (x, value, y, mem, m, n) = read-mem (x, write-mem (value, y, mem, m), n)

Theorem: read-write-mem1 read-mem (x, write-mem (value, y, mem, k), n) = if disjoint (x, n, y, k) then read-mem (x, mem, n)

else read-write-mem-end (x, value, y, mem, k, n) endif

Theorem: head-sub1-lessp ((head (x, n) − 1) < x) = (x ≄ 0)

Theorem: byte-read-write-mem-lemma (nat-rangep (y, 32) ∧ (n ≤ y)) → (byte-read (add (32, x, y), write-mem (value, x, mem, n))

= byte-read (add (32, x, y), mem))

Theorem: read-write-mem2 uint-rangep (n, 32) → (read-mem (x, write-mem (value, x, mem, n), n) = head (value, 8 ∗ n))

Event: Disable read-write-mem-end.

Event: Disable read-mem-byte-write-end.

Event: Disable byte-read-write-mem-end.

; write to the same location twice, only the second counts.

Theorem: write-mem-byte-write write-mem (v2 , y, byte-write (v1 , x, mem), n) = if disjoint0 (y, n, x) then byte-write (v1 , x, write-mem (v2 , y, mem, n))

else write-mem (v2 , y, mem, n) endif

Definition: write-write-induct (v1 , v2 , n) = if n ≃ 0 then t

else write-write-induct (tail (v1 , b), tail (v2 , b), n − 1) endif

Theorem: write-write-mem write-mem (v2 , x, write-mem (v1 , x, mem, n), n) = write-mem (v2 , x, mem, n)

;                LEMMAS ABOUT BITP

Theorem: bitp-fix-bit bitp (x) → (fix-bit (x) = x)

Theorem: fix-bit-bitp bitp (fix-bit (b))

Theorem: bitn-bitp bitp (bitn (x, n))

Theorem: add-c-bitp bitp (add-c (n, x, y))

Theorem: add-v-bitp bitp (add-v (n, x, y))

Theorem: add-z-bitp bitp (add-z (n, x, y))

Theorem: add-n-bitp bitp (add-n (n, x, y))

Theorem: addx-c-bitp bitp (addx-c (n, x, s, d))

Theorem: addx-v-bitp bitp (addx-v (n, x, s, d))

Theorem: addx-z-bitp bitp (addx-z (n, z, x, s, d))

Theorem: addx-n-bitp bitp (addx-n (n, x, s, d))

Theorem: sub-c-bitp bitp (sub-c (n, x, y))

Theorem: sub-v-bitp bitp (sub-v (n, x, y))

Theorem: sub-z-bitp bitp (sub-z (n, x, y))

Theorem: sub-n-bitp bitp (sub-n (n, x, y))

Theorem: subx-c-bitp bitp (subx-c (n, x, s, d))

Theorem: subx-v-bitp bitp (subx-v (n, x, s, d))

Theorem: subx-z-bitp bitp (subx-z (n, z, x, s, d))

Theorem: subx-n-bitp bitp (subx-n (n, x, s, d))

Theorem: and-z-bitp bitp (and-z (n, s, d))

Theorem: and-n-bitp bitp (and-n (n, s, d))

Theorem: mulu-v-bitp bitp (mulu-v (n, s, d, i))

Theorem: mulu-z-bitp bitp (mulu-z (n, s, d, i))

Theorem: mulu-n-bitp bitp (mulu-n (n, s, d, i))

Theorem: muls-v-bitp bitp (muls-v (n, s, d, i))

Theorem: muls-z-bitp bitp (muls-z (n, s, d, i))

Theorem: muls-n-bitp bitp (muls-n (n, s, d, i))

Theorem: or-z-bitp bitp (or-z (n, s, d))

Theorem: or-n-bitp bitp (or-n (n, s, d))

Theorem: divs-z-bitp bitp (divs-z (n, s, i, d, j ))

Theorem: divs-n-bitp bitp (divs-n (n, s, i, d, j ))

Theorem: divu-z-bitp bitp (divu-z (n, s, d))

Theorem: divu-n-bitp bitp (divu-n (n, s, d))

Theorem: rol-c-bitp bitp (rol-c (len, x, cnt))

Theorem: rol-z-bitp bitp (rol-z (len, x, cnt))

Theorem: rol-n-bitp bitp (rol-n (len, x, cnt))

Theorem: ror-c-bitp bitp (ror-c (len, x, cnt))

Theorem: ror-z-bitp bitp (ror-z (len, x, cnt))

Theorem: ror-n-bitp bitp (ror-n (len, x, cnt))

Theorem: lsl-c-bitp bitp (lsl-c (len, x, cnt))

Theorem: lsl-z-bitp bitp (lsl-z (len, x, cnt))

Theorem: lsl-n-bitp bitp (lsl-n (len, x, cnt))

Theorem: lsr-c-bitp bitp (lsr-c (len, x, cnt))

Theorem: lsr-z-bitp bitp (lsr-z (len, x, cnt))

Theorem: lsr-n-bitp bitp (lsr-n (len, x, cnt))

Theorem: asl-c-bitp bitp (asl-c (len, x, cnt))

Theorem: asl-v-bitp bitp (asl-v (len, x, cnt))

Theorem: asl-z-bitp bitp (asl-z (len, x, cnt))

Theorem: asl-n-bitp bitp (asl-n (len, x, cnt))

Theorem: asr-c-bitp bitp (asr-c (len, x, cnt))

Theorem: asr-z-bitp bitp (asr-z (len, x, cnt))

Theorem: asr-n-bitp bitp (asr-n (len, x, cnt))

Theorem: roxl-c-bitp bitp (roxl-c (len, opd, cnt, x))

Theorem: roxl-z-bitp bitp (roxl-z (len, opd, cnt, x))

Theorem: roxl-n-bitp bitp (roxl-n (len, opd, cnt, x))

Theorem: roxr-c-bitp bitp (roxr-c (len, opd, cnt, x))

Theorem: roxr-z-bitp bitp (roxr-z (len, opd, cnt, x))

Theorem: roxr-n-bitp bitp (roxr-n (len, opd, cnt, x))

Theorem: move-z-bitp bitp (move-z (oplen, sopd))

Theorem: move-n-bitp bitp (move-n (oplen, sopd))

Theorem: ext-z-bitp bitp (ext-z (oplen, opd, size))

Theorem: ext-n-bitp bitp (ext-n (oplen, opd, size))

Theorem: swap-z-bitp bitp (swap-z (opd))

Theorem: swap-n-bitp bitp (swap-n (opd))

Theorem: not-z-bitp bitp (not-z (oplen, opd))

Theorem: not-n-bitp bitp (not-n (oplen, opd))

Theorem: eor-z-bitp bitp (eor-z (n, s, d))

Theorem: eor-n-bitp bitp (eor-n (n, s, d))

;                          NEG
; after replacing sub by add and neg.  We can completely get rid of sub.

Theorem: neg-head neg (n, head (x, n)) = neg (n, x)

Theorem: neg-neg neg (n, neg (n, x)) = head (x, n)

Theorem: neg-cancel add (n, x, neg (n, x)) = 0

Theorem: neg-add neg (n, add (n, x, y)) = add (n, neg (n, x), neg (n, y))

Theorem: sub-neg sub (n, y, x) = add (n, x, neg (n, y))

Event: Disable neg.

; x - y = 0 <==> x = y.

Theorem: add-neg-0 (nat-rangep (x, n) ∧ nat-rangep (y, n)) → ((add (n, y, neg (n, x)) = 0) = (fix (x) = fix (y)))

; y + (x - y) = x.

Theorem: add-neg-cancel (add (n, y, add (n, x, neg (n, y))) = head (x, n)) ∧ (add (n, y, add (n, neg (n, y), x)) = head (x, n))

Theorem: sub-leq-1 (neg (n, x) ≤ y) → (((y − neg (n, x)) ≮ add (n, y, x))

∧ ((y − neg (n, x)) ≮ add (n, x, y)))

Theorem: sub-leq-2 (x ≤ y) → (((y − x) ≮ add (n, y, neg (n, x)))

∧ ((y − x) ≮ add (n, neg (n, x), y)))

Definition: add-fringe (n, x) = if listp (x) ∧ (car (x) = 'add) ∧ (cadr (x) = n)

then append (add-fringe (n, caddr (x)), add-fringe (n, cadddr (x))) else cons (x, nil) endif

Definition: add-tree (n, l) = if l ≃ nil then ''0

elseif cdr (l) ≃ nil then list ('head, car (l), n)

elseif cddr (l) ≃ nil then list ('add, n, car (l), cadr (l)) else list ('add, n, car (l), add-tree (n, cdr (l))) endif Theorem: numberp-eval$-add (car (x) = 'add) → (eval$ (t, x, a) ∈ N)

Theorem: numberp-eval$-add-tree eval$ (t, add-tree (n, l), a) ∈ N

Theorem: add-equal-cancel-1 (add (n, a, b) = add (n, c, add (n, a, d))) = (head (b, n) = add (n, c, d))

Theorem: eval$-add-member (e ∈ x) → (eval$ (t, add-tree (n, x), a)

= add (eval$ (t, n, a), eval$ (t, e, a), eval$ (t, add-tree (n, delete (e, x)), a)))

Theorem: add-tree-nat-rangep nat-rangep (eval$ (t, add-tree (n, x), a), eval$ (t, n, a))

Theorem: add-tree-append eval$ (t, add-tree (n, append (x, y)), a) = add (eval$ (t, n, a), eval$ (t, add-tree (n, x), a), eval$ (t, add-tree (n, y), a))

Theorem: add-tree-add-fringe eval$ (t, add-tree (n, add-fringe (n, x)), a) = head (eval$ (t, x, a), eval$ (t, n, a))

Definition: add-tree-delete-cond (n, x, y) = list ('and,

list ('numberp, x), list ('and,

          list ('nat-rangep, x, n),

list ('equal, add-tree (n, delete (x, y)), ''0)))

Theorem: add-tree-delete-equal (x ∈ y) → (eval$ (t, add-tree-delete-cond (n, x, y), a)

= (eval$ (t, add-tree (n, y), a) = eval$ (t, x, a)))

Theorem: add-tree-bagdiff (subbagp (x, y) ∧ subbagp (x, z)) → ((eval$ (t, add-tree (n, bagdiff (y, x)), a)

= eval$ (t, add-tree (n, bagdiff (z, x)), a))

= (eval$ (t, add-tree (n, y), a) = eval$ (t, add-tree (n, z), a)))

Definition: cancel-equal-add (x) = if listp (x) ∧ (car (x) = 'equal)

then if listp (cadr (x)) ∧ (caadr (x) = 'add) ∧ listp (caddr (x)) ∧ (caaddr (x) = 'add)

then if cadadr (x) = cadaddr (x)

then list ('equal,

add-tree (cadadr (x),

bagdiff (add-fringe (cadadr (x), cadr (x)),

bagint (add-fringe (cadadr (x),

cadr (x)),

add-fringe (cadadr (x),

caddr (x))))),

add-tree (cadadr (x),

bagdiff (add-fringe (cadadr (x), caddr (x)), bagint (add-fringe (cadadr (x),

cadr (x)),

add-fringe (cadadr (x),

caddr (x))))))

else x endif elseif listp (cadr (x))

∧ (caadr (x) = 'add)

∧ (caddr (x) ∈ add-fringe (cadadr (x), cadr (x))) then add-tree-delete-cond (cadadr (x),

caddr (x),

add-fringe (cadadr (x), cadr (x)))

elseif listp (caddr (x))

∧ (caaddr (x) = 'add)

∧ (cadr (x) ∈ add-fringe (cadaddr (x), caddr (x))) then add-tree-delete-cond (cadaddr (x),

cadr (x),

add-fringe (cadaddr (x), caddr (x)))

else x endif else x endif

Theorem: correctness-of-cancel-equal-add eval$ (t, x, a) = eval$ (t, cancel-equal-add (x), a)

Theorem: add-tree-delete (x ∈ y) → (eval$ (t, add-tree (n, delete (x, y)), a)

= sub (eval$ (t, n, a), eval$ (t, x, a), eval$ (t, add-tree (n, y), a)))

Definition: cancel-add-neg (x) = if listp (x)

∧ (car (x) = 'add) ∧ listp (cdr (x)) ∧ listp (cddr (x)) then if listp (caddr (x))

∧ listp (cdaddr (x)) ∧ listp (cddaddr (x)) ∧ (caaddr (x) = 'neg) ∧ (cadaddr (x) = cadr (x)) ∧ (caddaddr (x) ∈ add-fringe (cadr (x), cadddr (x)))

then add-tree (cadr (x),

delete (caddaddr (x), add-fringe (cadr (x), cadddr (x))))

elseif list ('neg, cadr (x), caddr (x))

∈ add-fringe (cadr (x), cadddr (x)) then add-tree (cadr (x),

delete (list ('neg, cadr (x), caddr (x)),

add-fringe (cadr (x), cadddr (x))))

else x endif else x endif

Theorem: correctness-of-cancel-add-neg eval$ (t, x, a) = eval$ (t, cancel-add-neg (x), a)

Event: For efficiency, compile those definitions not yet compiled.

;                  CONDITION CODES
; this section considers the various condition codes in Bcc and Scc
; instructions. The condition codes are specified as follows:
;  CC  carry clear       ~C                 LS  low or same     C+Z
;  CS  carry set         C                  LT  less than       N*~V+~N*V
;  EQ  equal             Z                  MI  minus           N
;  F   never true        0                  NE  not equal       ~Z
;  GE  greater or equal  N*V+~N*~V          PL  plus            ~N
;  GT  greater than      N*V*~Z+~N*~V*~Z    T   always true     1
;  HI  high              ~C*~Z              VC  overflow clear  ~V
;  LE  less or equal     Z+N*~V+~N*V        VS  overflow set    V
;                           BHI/BLS
; two bridge lemmas.
; the relation between add-c and addx-c.

Theorem: add-addx-c add-c (n, x, y) = addx-c (n, 0, x, y)

; the relation between sub-c and subx-c.

Theorem: sub-subx-c sub-c (n, x, y) = subx-c (n, 0, x, y)

; two lemmas for addx-c and subx-c.

Theorem: addx-c-la (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c) ∧ (n ≄ 0)) → (addx-c (n, c, x, y)

= if (c + x + y) < exp (2, n) then 0 else 1 endif)

Theorem: subx-c-la (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c) ∧ (n ≄ 0)) → (subx-c (n, c, x, y)

= if y < (c + x) then 1 else 0 endif)

Event: Disable addx-c.

Event: Disable add-c.

Event: Disable subx-c.

Event: Disable sub-c.

Event: Disable mbit-means-lessp.

Theorem: sub-z-la (nat-rangep (x, n) ∧ nat-rangep (y, n)) → (sub-z (n, x, y)

= if fix (x) = fix (y) then 1 else 0 endif)

Definition: between-ileq (x, y, z) = (ileq (x, y) ∧ ileq (y, z))

Theorem: sub-bhi-int (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0) ∧ (¬ negativep (nat-to-int (x, n)))) → (bhi (sub-c (n, x, y), sub-z (n, x, y))

= if between-ileq (0, nat-to-int (y, n), nat-to-int (x, n)) then 0 else 1 endif)

Theorem: sub-bhi-0 (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (nat-to-uint (x) ≮ nat-to-uint (y)) ∧ (n ≄ 0)) → (bhi (sub-c (n, x, y), sub-z (n, x, y)) = 0)

Theorem: sub-bhi-1 (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (nat-to-uint (x) < nat-to-uint (y)) ∧ (n ≄ 0)) → (bhi (sub-c (n, x, y), sub-z (n, x, y)) = 1)

Theorem: sub-bls (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (bls (sub-c (n, x, y), sub-z (n, x, y))

= if nat-to-uint (x) < nat-to-uint (y) then 0 else 1 endif)

; the trivial relation between bls and bhi.

Theorem: bls-bhi bls (c, z) = b-not (bhi (c, z))

Event: Disable bhi.

Event: Disable bls.

;                          BEQ/BNE
; the z-flag of move.
; the unsigned integer interpretation.

Theorem: move-beq-uint nat-rangep (x, n) → (beq (move-z (n, x))

= if nat-to-uint (x) = 0 then 1 else 0 endif)

; the signed integer interpretation.

Theorem: move-beq-int-0 (nat-rangep (x, n) ∧ (nat-to-int (x, n) ≠ 0)) → (beq (move-z (n, x)) = 0)

Theorem: move-beq-int-1 (nat-rangep (x, n) ∧ (nat-to-int (x, n) = 0)) → (beq (move-z (n, x)) = 1)

; zero testing on a sign-extended bit vector is equivalent to
; testing on the original value.

Theorem: move-beq-ext (nat-rangep (x, n) ∧ (n ≤ size) ∧ (n ≄ 0)) → (move-z (size, ext (n, x, size)) = move-z (n, x))

; the z-flag of sub.
; the unsigned integer interpretation.

Theorem: sub-beq-uint (nat-rangep (x, n) ∧ nat-rangep (y, n)) → (beq (sub-z (n, x, y))

= if nat-to-uint (x) = nat-to-uint (y) then 1 else 0 endif)

; the signed integer interpretation.

Theorem: sub-beq-int-0 (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (nat-to-int (x, n) ≠ nat-to-int (y, n))) → (beq (sub-z (n, x, y)) = 0)

Theorem: sub-beq-int-1 (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (nat-to-int (x, n) = nat-to-int (y, n))) → (beq (sub-z (n, x, y)) = 1)

; equality testing on two sign-extended bit vectors is equivalent to
; testing on their original values.

Theorem: sub-beq-ext (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≤ size) ∧ (n ≄ 0)) → (sub-z (size, ext (n, x, size), ext (n, y, size)) = sub-z (n, x, y))

; the z flag of logor.

Theorem: logor-beq-uint beq (or-z (n, x, y)) = if (nat-to-uint (x) = 0) ∧ (nat-to-uint (y) = 0) then 1

else 0 endif Theorem: logor-beq-int-0 (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ ((nat-to-int (x, n) ≠ 0) ∨ (nat-to-int (y, n) ≠ 0))) → (beq (or-z (n, x, y)) = 0)

Theorem: logor-beq-int-1 (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (nat-to-int (x, n) = 0) ∧ (nat-to-int (y, n) = 0)) → (beq (or-z (n, x, y)) = 1)

; the z flag of logeor.

Theorem: logeor-beq-uint beq (eor-z (n, x, y)) = if nat-to-uint (x) = nat-to-uint (y) then 1

else 0 endif

Theorem: logeor-beq-int-0 (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (nat-to-int (x, n) ≠ nat-to-int (y, n))) → (beq (eor-z (n, x, y)) = 0)

Theorem: logeor-beq-int-1 (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (nat-to-int (x, n) = nat-to-int (y, n))) → (beq (eor-z (n, x, y)) = 1)

; the z flag of logand.

Theorem: logand-beq-uint (exp (2, log (2, 1 + x)) = (1 + x)) → (beq (and-z (n, x, y))

= if (nat-to-uint (y) mod (1 + x)) = 0 then 1 else 0 endif)

Theorem: logand-or-beq-uint (exp (2, log (2, 1 + x)) = (1 + x)) → (beq (and-z (n, x, logor (y, z)))

= if ((nat-to-uint (y) mod (1 + x)) = 0)

∧ ((nat-to-uint (z) mod (1 + x)) = 0) then 1 else 0 endif)

Theorem: logand-eor-beq-uint (exp (2, log (2, 1 + x)) = (1 + x)) → (beq (and-z (n, x, logeor (y, z)))

= if (nat-to-uint (y) mod (1 + x))

= (nat-to-uint (z) mod (1 + x)) then 1 else 0 endif)

; the z-flag of mulu.  There are three cases to handle.

Theorem: mulu 1632-beq (nat-rangep (x, 16) ∧ nat-rangep (y, 16)) → (beq (mulu-z (32, x, y, 16))

= if (nat-to-uint (x) = 0) ∨ (nat-to-uint (y) = 0) then 1 else 0 endif)

Theorem: mulu 3264-beq (nat-rangep (x, 32) ∧ nat-rangep (y, 32)) → (beq (mulu-z (64, x, y, 32))

= if (nat-to-uint (x) = 0) ∨ (nat-to-uint (y) = 0) then 1 else 0 endif)

Theorem: mulu 3232-beq uint-rangep (nat-to-uint (x) ∗ nat-to-uint (y), 32) → (beq (mulu-z (32, x, y, 32))

= if (nat-to-uint (x) = 0) ∨ (nat-to-uint (y) = 0) then 1 else 0 endif)

; the z-flag of muls.  There are three cases to handle.

Theorem: muls 1632-beq (nat-rangep (x, 16) ∧ nat-rangep (y, 16)) → (beq (muls-z (32, x, y, 16))

= if (nat-to-int (x, 16) = 0) ∨ (nat-to-int (y, 16) = 0) then 1 else 0 endif)

Theorem: muls 3264-beq (nat-rangep (x, 32) ∧ nat-rangep (y, 32)) → (beq (muls-z (64, x, y, 32))

= if (nat-to-int (x, 32) = 0) ∨ (nat-to-int (y, 32) = 0) then 1 else 0 endif)

Theorem: muls 3232-beq (int-rangep (itimes (nat-to-int (x, 32), nat-to-int (y, 32)), 32)

∧ nat-rangep (x, 32) ∧ nat-rangep (y, 32)) → (beq (muls-z (32, x, y, 32))

= if (nat-to-int (x, 32) = 0) ∨ (nat-to-int (y, 32) = 0) then 1 else 0 endif)

; the z-flag of divu.

Theorem: divu-beq (nat-rangep (y, n) ∧ (nat-to-uint (x) ≠ 0)) → (beq (divu-z (n, x, y))

= if nat-to-uint (y) < nat-to-uint (x) then 1 else 0 endif)

; the z-flag of divs.

Theorem: iquotient=0 (integerp (y) ∧ (y ≠ 0)) → ((iquotient (x, y) = 0) = (abs (x) < abs (y)))

Theorem: divs-beq (int-rangep (iquotient (nat-to-int (y, j ), nat-to-int (x, i)), n) ∧ nat-rangep (x, i) ∧ (nat-to-int (x, i) ≠ 0) ∧ (n ≤ j )) → (beq (divs-z (n, x, i, y, j ))

= if abs (nat-to-int (y, j )) < abs (nat-to-int (x, i)) then 1 else 0 endif)

; the z-flag of lsl.

Theorem: lsl-beq uint-rangep (nat-to-uint (x), n − cnt) → (beq (lsl-z (n, x, cnt))

= if nat-to-uint (x) = 0 then 1 else 0 endif)

; the z-flag of lsr.

Theorem: lsr-beq beq (lsr-z (n, x, cnt)) = if nat-to-uint (x) < exp (2, cnt) then 1

else 0 endif

Theorem: z-flag-la (x ∈ N) → ((nat-to-int (x, n) = 0) = (x = 0))

; the z-flag of asl.

Theorem: asl-beq (nat-rangep (x, n) ∧ int-rangep (nat-to-int (x, n), n − cnt)) → (beq (asl-z (n, x, cnt))

= if nat-to-int (x, n) = 0 then 1 else 0 endif)

; the z-flag of asr.

Theorem: asr-beq nat-rangep (x, n) → (beq (asr-z (n, x, cnt))

= if negativep (nat-to-int (x, n)) then 0 elseif nat-to-int (x, n) < exp (2, cnt) then 1 else 0 endif)

; the z-flag of ext.

Theorem: ext-beq-uint (nat-rangep (x, n) ∧ (n ≤ size)) → (beq (ext-z (n, x, size))

= if nat-to-uint (x) = 0 then 1 else 0 endif)

Theorem: ext-beq-int-0 (nat-rangep (x, n) ∧ (n < size) ∧ (nat-to-int (x, n) ≠ 0)) → (beq (ext-z (n, x, size)) = 0)

Theorem: ext-beq-int-1 (nat-rangep (x, n) ∧ (n < size) ∧ (nat-to-int (x, n) = 0)) → (beq (ext-z (n, x, size)) = 1)

Event: Disable iquotient=0.

Event: Disable int-to-nat=0.

Event: Disable beq.

;                         BCS/BCC
; BCS/BCC means carry is set/cleared.
; the c-flag of sub.

Theorem: sub-bcs&cc (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (bcs (sub-c (n, x, y))

= if nat-to-uint (y) < nat-to-uint (x) then 1 else 0 endif)

; the c-flag of add.

Theorem: add-bcs&cc (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (bcs (add-c (n, x, y))

= if (nat-to-uint (x) + nat-to-uint (y)) < exp (2, n) then 0 else 1 endif)

Theorem: tail-mbit (x < exp (2, n)) → (tail (x, n − 1)

= if x < exp (2, n − 1) then 0 else 1 endif)

; the c-flag of lsl.  But we only consider special cases: cnt = 0 or 1.
; I don't know what the meaning of c-flag is when cnt > 1.

Theorem: lsl-c-0 lsl-c (n, x, 0) = 0

Theorem: lsl-1-bcs&cc (nat-rangep (x, n) ∧ (1 < n)) → (bcs (lsl-c (n, x, 1))

= if uint-rangep (nat-to-uint (x), n − 1) then 0 else 1 endif)

; the c-flag of lsr.  But we only consider special cases: cnt = 0 or 1.
; I don't know what the meaning of c-flag is when cnt > 1.

Theorem: lsr-c-0 lsr-c (n, x, 0) = 0

Theorem: lsr-1-bcs&cc (1 < n) → (bcs (lsr-c (n, x, 1)) = (nat-to-uint (x) mod 2))

Event: Disable tail-mbit.

Event: Disable bcs.

;                       BVS/BVC
; BVS/BVC means overflow is set/cleared.
; three bridge lemmas.

Theorem: add-addx-v add-v (n, x, y) = addx-v (n, 0, x, y)

Theorem: subx-addx-v (nat-rangep (x, n) ∧ (n ≄ 0)) → (subx-v (n, z, x, y) = addx-v (n, b-not (z), y, lognot (n, x)))

Theorem: sub-subx-v sub-v (n, x, y) = subx-v (n, 0, x, y)

; lemmas for addx-v and subx-v.

Theorem: mbit-means-negativep nat-rangep (x, n) → (bitn (x, n − 1)

= if negativep (nat-to-int (x, n)) then 1 else 0 endif)

Theorem: addx-v-la (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c) ∧ (n ≄ 0)) → (addx-v (n, c, x, y)

= if int-rangep (iplus (nat-to-int (x, n), iplus (nat-to-int (y, n), c)),

n) then 0

else 1 endif)

Theorem: subx-v-la (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ bitp (c) ∧ (n ≄ 0)) → (subx-v (n, c, x, y)

= if int-rangep (idifference (nat-to-int (y, n),

iplus (nat-to-int (x, n), c)),

n) then 0

else 1 endif)

Event: Disable addx-v-crock1.

Event: Disable addx-v-crock2.

; the v-flag of sub.

Theorem: sub-bvs&vc (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (bvs (sub-v (n, x, y))

= if int-rangep (idifference (nat-to-int (y, n), nat-to-int (x, n)), n) then 0 else 1 endif)

; the v-flag of add.

Theorem: add-bvs&vc (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (bvs (add-v (n, x, y))

= if int-rangep (iplus (nat-to-int (x, n), nat-to-int (y, n)), n) then 0 else 1 endif)

; three cases for the v-flag of mulu.

Theorem: mulu 1632-bvs (nat-rangep (x, 16) ∧ nat-rangep (y, 16)) → (mulu-v (32, x, y, 16) = 0)

Theorem: mulu 3264-bvs (nat-rangep (x, 32) ∧ nat-rangep (y, 32)) → (mulu-v (64, x, y, 32) = 0)

Theorem: mulu 3232-bvs bvs (mulu-v (32, x, y, 32)) = if (nat-to-uint (x) ∗ nat-to-uint (y)) < exp (2, 32) then 0

else 1 endif

; three cases for the v-flag of muls.

Theorem: muls 1632-bvs (nat-rangep (x, 16) ∧ nat-rangep (y, 16)) → (muls-v (32, x, y, 16) = 0)

Theorem: muls 3264-bvs (nat-rangep (x, 32) ∧ nat-rangep (y, 32)) → (muls-v (64, x, y, 32) = 0)

Theorem: muls 3232-bvs bvs (muls-v (32, x, y, 32)) = if int-rangep (itimes (nat-to-int (x, 32), nat-to-int (y, 32)), 32) then 0

else 1 endif

; the v-flag of asl.  It is an easy copy of the definition of asl-v.
; sometimes, it seems to be better to define those functions directly
; using the intended meaning.  But there are several problems:
; 1. the meaning is not completely clear. It is vague.

; 2. it is impossible to have a clean definition.
; 3. it is error prone. It does not always work the way you think.
;    Your intended interpretation is just a special case.
; In some sense,  a formal specification should be more syntax-oriented.
; syntax rules are clear and accurate. e.g. M68000 are well-documented.
; But it gives one a hard time to do formal proofs.  We need to assign
; meanings to these definitions.  To make sure our "intended" meanings
; are consistent with the specification, we need to prove the equivalence.
; this is done formally by a theorem prover, and sometimes, is very hard.

Theorem: asl-bvs bvs (asl-v (n, x, cnt)) = if int-rangep (nat-to-int (x, n), n − cnt) then 0

else 1 endif

Event: Disable bvs.

;                      BMI/BPL
; the n-flag of move.

Theorem: move-bmi nat-rangep (x, n) → (bmi (move-n (n, x))

= if negativep (nat-to-int (x, n)) then 1 else 0 endif)

; the n-flag of sub.

Theorem: sub-bmi (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (bmi (sub-n (n, x, y))

= if int-rangep (idifference (nat-to-int (y, n), nat-to-int (x, n)), n) then if ilessp (nat-to-int (y, n), nat-to-int (x, n)) then 1

else 0 endif elseif ilessp (nat-to-int (y, n), nat-to-int (x, n)) then 0 else 1 endif)

; the n-flag of add.

Theorem: add-bmi (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (bmi (add-n (n, x, y))

= if int-rangep (iplus (nat-to-int (x, n), nat-to-int (y, n)), n)

then if negativep (iplus (nat-to-int (x, n), nat-to-int (y, n))) then 1

else 0 endif elseif negativep (nat-to-int (x, n)) then 0 else 1 endif)

; the n-flag of muls.  There are three cases to handle.

Theorem: muls 1632-bmi (nat-rangep (x, 16) ∧ nat-rangep (y, 16)) → (bmi (muls-n (32, x, y, 16))

= if (nat-to-int (x, 16) = 0) ∨ (nat-to-int (y, 16) = 0) then 0 elseif negativep (nat-to-int (x, 16)) then if negativep (nat-to-int (y, 16)) then 0

else 1 endif elseif negativep (nat-to-int (y, 16)) then 1 else 0 endif)

Theorem: muls 3264-bmi (nat-rangep (x, 32) ∧ nat-rangep (y, 32)) → (bmi (muls-n (64, x, y, 32))

= if (nat-to-int (x, 32) = 0) ∨ (nat-to-int (y, 32) = 0) then 0 elseif negativep (nat-to-int (x, 32)) then if negativep (nat-to-int (y, 32)) then 0

else 1 endif elseif negativep (nat-to-int (y, 32)) then 1 else 0 endif)

Theorem: muls 3232-bmi (int-rangep (itimes (nat-to-int (x, 32), nat-to-int (y, 32)), 32) ∧ nat-rangep (x, 32) ∧ nat-rangep (y, 32)) → (bmi (muls-n (32, x, y, 32))

= if (nat-to-int (x, 32) = 0) ∨ (nat-to-int (y, 32) = 0) then 0 elseif negativep (nat-to-int (x, 32)) then if negativep (nat-to-int (y, 32)) then 0

else 1 endif elseif negativep (nat-to-int (y, 32)) then 1 else 0 endif)

; the n-flag of asl.

Theorem: asl-bmi (nat-rangep (x, n) ∧ int-rangep (nat-to-int (x, n), n − cnt))

→ (bmi (asl-n (n, x, cnt))

= if negativep (nat-to-int (x, n)) then 1 else 0 endif)

; the n-flag of asr.

Theorem: asr-bmi nat-rangep (x, n) → (bmi (asr-n (n, x, cnt))

= if negativep (nat-to-int (x, n)) then 1 else 0 endif)

; the n-flag of ext.

Theorem: ext-bmi (nat-rangep (x, n) ∧ (n < size)) → (bmi (ext-n (n, x, size))

= if negativep (nat-to-int (x, n)) then 1 else 0 endif)

;                   BGE/BLT

Theorem: bge-v0 bge (0, n) = b-not (bmi (n))

Theorem: blt-v0 blt (0, n) = bmi (n)

; bge of sub.

Theorem: sub-bge (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (bge (sub-v (n, x, y), sub-n (n, x, y))

= if ilessp (nat-to-int (y, n), nat-to-int (x, n)) then 0 else 1 endif)

; blt of sub.

Theorem: sub-blt (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (blt (sub-v (n, x, y), sub-n (n, x, y))

= if ilessp (nat-to-int (y, n), nat-to-int (x, n)) then 1 else 0 endif)

; the trivial relation between BGE and BLT.

Theorem: blt-bge blt (v, n) = b-not (bge (v, n))

Event: Disable bge.

Event: Disable blt.

;                       BGT/BLE

Theorem: sub-z-la1 (nat-rangep (x, n) ∧ nat-rangep (y, n)) → (sub-z (n, x, y)

= if nat-to-int (x, n) = nat-to-int (y, n) then 1 else 0 endif)

Event: Disable sub-z.

; bgt of sub.

Theorem: sub-bgt (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (bgt (sub-v (n, x, y), sub-z (n, x, y), sub-n (n, x, y))

= if ilessp (nat-to-int (x, n), nat-to-int (y, n)) then 1 else 0 endif)

; ble of sub.

Theorem: sub-ble (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ (n ≄ 0)) → (ble (sub-v (n, x, y), sub-z (n, x, y), sub-n (n, x, y))

= if ilessp (nat-to-int (x, n), nat-to-int (y, n)) then 0 else 1 endif)

; bgt of move.

Theorem: move-bgt nat-rangep (x, n) → (bgt (0, move-z (n, x), move-n (n, x))

= if 0 < nat-to-int (x, n) then 1 else 0 endif)

; ble of move.

Theorem: move-ble nat-rangep (x, n) → (ble (0, move-z (n, x), move-n (n, x))

= if 0 < nat-to-int (x, n) then 0

else 1 endif)

; the trivial relation between ble and bgt.

Theorem: ble-bgt ble (v, z, n) = b-not (bgt (v, z, n)) Event: Disable ble. Event: Disable bgt.

; the end of this subsection.  Some lemmas should be disabled, for we
; no longer need them.

Event: Disable mbit-means-negativep. Event: Disable bmi. Event: Disable add-addx-c. Event: Disable sub-subx-c. Event: Disable addx-c-la. Event: Disable subx-c-la. Event: Disable add-addx-v. Event: Disable subx-addx-v. Event: Disable sub-subx-v. Event: Disable addx-v-la. Event: Disable subx-v-la.

Event: Disable sub-z-la.

Event: Disable sub-z-la1.

Event: Disable ilessp-crock1.

Event: Disable ilessp-crock2.

Event: Disable add-bmi-crock1.

Event: Disable add-bmi-crock2.

Event: Disable nat-to-int=.

;                          STEPN
; stepping the state s (m+n) steps is equivalent to stepping s m steps and
; n steps further.

Definition: splus (x, y) = (x + y)

Theorem: stepn-lemma stepn (s, splus (m, n)) = stepn (stepn (s, m), n)

Theorem: stepn-rewriter0 stepn (s, 0) = s

Theorem: stepn-rewriter (mc-status (s) = 'running) → (stepn (s, 1 + n) = stepn (stepi (s), n))

;                     THEOREMS ABOUT THE MEMORY
; if a portion of memory is ROM, then it still is ROM after a write on memory.

Theorem: byte-write-maintain-rom-addrp rom-addrp (addr, byte-write (value, x, mem), n) = rom-addrp (addr, mem, n)

Theorem: write-mem-maintain-rom-addrp rom-addrp (addr, write-mem (value, x, mem, m), n) = rom-addrp (addr, mem, n)

; if a portion of memory is RAM, then it still is RAM after a write on memory.

Theorem: byte-write-maintain-ram-addrp ram-addrp (addr, byte-write (value, x, mem), n) = ram-addrp (addr, mem, n)

Theorem: write-mem-maintain-ram-addrp ram-addrp (addr, write-mem (value, x, mem, m), n) = ram-addrp (addr, mem, n)

; mcode-addrp claims that the machine code program lst is stored in the
; memory starting at addr.

Definition: mcode-addrp (addr, mem, lst) = if listp (lst)

then if car (lst) = -1 then mcode-addrp (add (32, addr, 1), mem, cdr (lst)) else (pc-byte-read (addr, mem) = car (lst))

∧ mcode-addrp (add (32, addr, 1), mem, cdr (lst)) endif

else t endif

Theorem: add-non-numberp (i ∉ N) → (add (n, x, i) = head (x, n))

Theorem: add-plus add (n, x, add (n, y, z)) = add (n, x, y + z)

; four lemmas about pc-read-memp.

Theorem: pc-read-memp-la0 (pc-read-memp (addr, mem, k) ∧ (k ≄ 0)) → pc-byte-readp (addr, mem)

Theorem: pc-read-memp-la1 (pc-read-memp (addr, mem, k) ∧ (j < k)) → pc-byte-readp (add (32, addr, j ), mem)

Theorem: pc-read-memp-la2 (pc-read-memp (addr, mem, k) ∧ (j ≤ k)) → pc-read-memp (addr, mem, j )

Theorem: pc-read-memp-la3 (pc-read-memp (addr, mem, k) ∧ ((i + j ) ≤ k)) → pc-read-memp (add (32, addr, i), mem, j )

Theorem: write-memp-la0 (write-memp (addr, mem, n) ∧ (n ≄ 0)) → byte-writep (addr, mem)

Theorem: write-memp-la1 (write-memp (addr, mem, n) ∧ (m < n)) → byte-writep (add (32, addr, m), mem)

Theorem: write-memp-la2 (write-memp (addr, mem, n) ∧ (m ≤ n)) → write-memp (addr, mem, m)

Theorem: write-memp-la3 (write-memp (addr, mem, n) ∧ ((i + j ) ≤ n)) → write-memp (add (32, addr, i), mem, j )

Event: Disable add-plus.

; array index.  There are some good reasons to distinguish this concept
; with add and sub.

Definition: index-n (x, y) = sub (32, y, x)

; ROM is pc-readable.

Theorem: pc-byte-readp-rom0 (rom-addrp (addr, mem, k) ∧ (k ≄ 0)) → pc-byte-readp (addr, mem)

Theorem: pc-byte-readp-rom1 (rom-addrp (addr, mem, k) ∧ (j < k)) → pc-byte-readp (add (32, addr, j ), mem)

Theorem: pc-byte-readp-rom2 (rom-addrp (add (32, addr, i), mem, k) ∧ (index-n (0, i) < k)) → pc-byte-readp (addr, mem)

Theorem: pc-byte-readp-rom3 (rom-addrp (add (32, addr, i), mem, k) ∧ (index-n (j , i) < k)) → pc-byte-readp (add (32, addr, j ), mem)

Theorem: pc-read-memp-rom0 (rom-addrp (addr, mem, k) ∧ (j ≤ k)) → pc-read-memp (addr, mem, j )

Theorem: pc-read-memp-rom1 (rom-addrp (addr, mem, k) ∧ ((i + j ) ≤ k)) → pc-read-memp (add (32, addr, i), mem, j )

Theorem: pc-read-memp-rom2 (rom-addrp (add (32, addr, i), mem, k) ∧ ((index-n (0, i) + j ) ≤ k)) → pc-read-memp (addr, mem, j )

Theorem: pc-read-memp-rom3 (rom-addrp (add (32, addr, i), mem, k) ∧ ((index-n (h, i) + j ) ≤ k)) → pc-read-memp (add (32, addr, h), mem, j )

; starting at the same address, a portion of the memory is ROM if a bigger
; portion of the memory is ROM.

Theorem: rom-addrp-la1 (rom-addrp (addr, mem, n) ∧ (m ≤ n)) → rom-addrp (addr, mem, m)

; a portion of the memory is also ROM, if a bigger portion of the memory
; is ROM.

Theorem: rom-addrp-la2 (rom-addrp (addr, mem, k) ∧ ((j + index-n (x, addr)) ≤ k)) → rom-addrp (x, mem, j )

Event: Disable rom-addrp.

; ROM is readable.

Theorem: byte-readp-rom0 (rom-addrp (addr, mem, k) ∧ (k ≄ 0)) → byte-readp (addr, mem)

Theorem: byte-readp-rom1 (rom-addrp (addr, mem, k) ∧ (j < k)) → byte-readp (add (32, addr, j ), mem)

Theorem: byte-readp-rom2 (rom-addrp (add (32, addr, i), mem, k) ∧ (index-n (0, i) < k)) → byte-readp (addr, mem)

Theorem: byte-readp-rom3 (rom-addrp (add (32, addr, i), mem, k) ∧ (index-n (j , i) < k)) → byte-readp (add (32, addr, j ), mem)

Theorem: read-memp-rom0 (rom-addrp (addr, mem, k) ∧ (j ≤ k)) → read-memp (addr, mem, j )

Theorem: read-memp-rom1 (rom-addrp (addr, mem, k) ∧ ((i + j ) ≤ k)) → read-memp (add (32, addr, i), mem, j )

Theorem: read-memp-rom2 (rom-addrp (add (32, addr, i), mem, k) ∧ ((index-n (0, i) + j ) ≤ k)) → read-memp (addr, mem, j )

Theorem: read-memp-rom3 (rom-addrp (add (32, addr, i), mem, k) ∧ ((index-n (h, i) + j ) ≤ k)) → read-memp (add (32, addr, h), mem, j )

; integer view.

Theorem: read-memp-rom1-int (rom-addrp (addr, mem, n) ∧ ((nat-to-int (x, 32) + j ) < n) ∧ (nat-to-int (x, 32) ∈ N)) → read-memp (add (32, addr, x), mem, j )

; RAM is writable.

Theorem: byte-writep-ram0 (ram-addrp (addr, mem, k) ∧ (k ≄ 0)) → byte-writep (addr, mem)

Theorem: byte-writep-ram1 (ram-addrp (addr, mem, k) ∧ (j < k)) → byte-writep (add (32, addr, j ), mem)

Theorem: byte-writep-ram2 (ram-addrp (add (32, addr, i), mem, k) ∧ (index-n (0, i) < k)) → byte-writep (addr, mem)

Theorem: byte-writep-ram3 (ram-addrp (add (32, addr, i), mem, k) ∧ (index-n (j , i) < k)) → byte-writep (add (32, addr, j ), mem)

Theorem: write-memp-ram0 (ram-addrp (addr, mem, k) ∧ (j ≤ k)) → write-memp (addr, mem, j )

Theorem: write-memp-ram1 (ram-addrp (addr, mem, k) ∧ ((i + j ) ≤ k)) → write-memp (add (32, addr, i), mem, j )

Theorem: write-memp-ram1-int (ram-addrp (addr, mem, k) ∧ (nat-to-int (i, 32) ∈ N) ∧ ((nat-to-int (i, 32) + j ) ≤ k)) → write-memp (add (32, addr, i), mem, j )

Theorem: write-memp-ram2 (ram-addrp (add (32, addr, i), mem, k) ∧ ((index-n (0, i) + j ) ≤ k)) → write-memp (addr, mem, j )

Theorem: write-memp-ram3 (ram-addrp (add (32, addr, i), mem, k) ∧ ((index-n (h, i) + j ) ≤ k)) → write-memp (add (32, addr, h), mem, j )

; a portion of a memory is also RAM, if a "bigger" portion of the memory
; is RAM.

Theorem: ram-addrp-la1 (ram-addrp (addr, mem, n) ∧ (m ≤ n)) → ram-addrp (addr, mem, m)

Theorem: ram-addrp-la2 (ram-addrp (addr, mem, n) ∧ ((j + index-n (x, addr)) ≤ n)) → ram-addrp (x, mem, j )

Event: Disable ram-addrp.

; RAM is readable.

Theorem: byte-readp-ram0 (ram-addrp (addr, mem, k) ∧ (k ≄ 0)) → byte-readp (addr, mem)

Theorem: byte-readp-ram1 (ram-addrp (addr, mem, k) ∧ (j < k)) → byte-readp (add (32, addr, j ), mem)

Theorem: byte-readp-ram2 (ram-addrp (add (32, addr, i), mem, k) ∧ (index-n (0, i) < k)) → byte-readp (addr, mem)

Theorem: byte-readp-ram3 (ram-addrp (add (32, addr, i), mem, k) ∧ (index-n (j , i) < k)) → byte-readp (add (32, addr, j ), mem)

Theorem: read-memp-ram0 (ram-addrp (addr, mem, k) ∧ (j ≤ k)) → read-memp (addr, mem, j )

Theorem: read-memp-ram1 (ram-addrp (addr, mem, k) ∧ ((i + j ) ≤ k)) → read-memp (add (32, addr, i), mem, j )

Theorem: read-memp-ram1-int (ram-addrp (addr, mem, k) ∧ (nat-to-int (i, 32) ∈ N) ∧ ((nat-to-int (i, 32) + j ) ≤ k)) → read-memp (add (32, addr, i), mem, j )

Theorem: read-memp-ram2 (ram-addrp (add (32, addr, i), mem, k) ∧ ((index-n (0, i) + j ) ≤ k)) → read-memp (addr, mem, j )

Theorem: read-memp-ram3 (ram-addrp (add (32, addr, i), mem, k) ∧ ((index-n (h, i) + j ) ≤ k)) → read-memp (add (32, addr, h), mem, j )

; please use the right induction.

Definition: mem-induct1 (i, addr, lst) = if i ≃ 0 then t

else mem-induct1 (i − 1, add (32, addr, 1), cdr (lst)) endif

;            OBTAIN MACHINE CODE FROM MEMORY
; please read the right thing.

Theorem: pc-byte-read-mcode0 (mcode-addrp (addr, mem, cons (x, lst)) ∧ (x ≠ -1)) → (pc-byte-read (addr, mem) = x)

Theorem: pc-byte-read-mcode1 (mcode-addrp (addr, mem, lst) ∧ (i < len (lst)) ∧ (get-nth (i, lst) ≠ -1)) → (pc-byte-read (add (32, addr, i), mem) = get-nth (i, lst))

Theorem: pc-byte-read-mcode2 (mcode-addrp (add (32, addr, i), mem, lst) ∧ (index-n (0, i) < len (lst)) ∧ (get-nth (index-n (0, i), lst) ≠ -1)) → (pc-byte-read (addr, mem) = get-nth (index-n (0, i), lst))

Theorem: pc-byte-read-mcode3 (mcode-addrp (add (32, addr, i), mem, lst) ∧ (index-n (j , i) < len (lst)) ∧ (get-nth (index-n (j , i), lst) ≠ -1)) → (pc-byte-read (add (32, addr, j ), mem) = get-nth (index-n (j , i), lst))

Definition: lst-numberp0 (lst, n) = if n ≃ 0 then 0

else (get-nth (n − 1, lst) ∈ N) ∧ lst-numberp0 (lst, n − 1) endif

Definition: read-lst0 (lst, n) = if n ≃ 0 then 0

else app (b, get-nth (n − 1, lst), read-lst0 (lst, n − 1)) endif

Definition: tail-lst (lst, n) = if n ≃ 0 then lst

else tail-lst (cdr (lst), n − 1) endif

Definition: lst-numberp (m, lst, n) = lst-numberp0 (tail-lst (lst, m), n)

Definition: read-lst (m, lst, n) = read-lst0 (tail-lst (lst, m), n)

Theorem: get-nth-tail-lst get-nth (n, tail-lst (x, m)) = get-nth (m + n, x)

Theorem: pc-read-mem-mcode0 (mcode-addrp (addr, mem, lst) ∧ (j ≤ len (lst)) ∧ lst-numberp (0, lst, j )) → (pc-read-mem (addr, mem, j ) = read-lst (0, lst, j ))

Theorem: pc-read-mem-mcode1 (mcode-addrp (addr, mem, lst) ∧ ((i + j ) ≤ len (lst)) ∧ lst-numberp (i, lst, j )) → (pc-read-mem (add (32, addr, i), mem, j ) = read-lst (i, lst, j ))

Event: Disable read-lst.

Event: Disable lst-numberp.

Theorem: pc-read-mem-mcode2 (mcode-addrp (add (32, addr, i), mem, lst) ∧ ((index-n (0, i) + k) ≤ len (lst)) ∧ lst-numberp (index-n (0, i), lst, k)) → (pc-read-mem (addr, mem, k) = read-lst (index-n (0, i), lst, k))

Theorem: pc-read-mem-mcode3 (mcode-addrp (add (32, addr, i), mem, lst) ∧ ((index-n (j , i) + k) ≤ len (lst)) ∧ lst-numberp (index-n (j , i), lst, k)) → (pc-read-mem (add (32, addr, j ), mem, k) = read-lst (index-n (j , i), lst, k))

; sometimes,  we obtain machine code by read-mem.

Theorem: read->pc-read-mem read-mem (x, mem, k) = pc-read-mem (x, mem, k)

Theorem: read-mem-mcode1-int (mcode-addrp (addr, mem, lst) ∧ ((nat-to-int (i, 32) + j ) ≤ len (lst)) ∧ (nat-to-int (i, 32) ∈ N) ∧ lst-numberp (nat-to-int (i, 32), lst, j )) → (read-mem (add (32, addr, i), mem, j )

= read-lst (nat-to-int (i, 32), lst, j ))

Theorem: read-mem-mcode2 (mcode-addrp (add (32, addr, i), mem, lst) ∧ ((index-n (0, i) + k) ≤ len (lst)) ∧ lst-numberp (index-n (0, i), lst, k)) → (read-mem (addr, mem, k) = read-lst (index-n (0, i), lst, k))

Theorem: read-mem-mcode3 (mcode-addrp (add (32, addr, i), mem, lst) ∧ ((index-n (j , i) + k) ≤ len (lst)) ∧ lst-numberp (index-n (j , i), lst, k)) → (read-mem (add (32, addr, j ), mem, k) = read-lst (index-n (j , i), lst, k))

Event: Disable read->pc-read-mem.

; program segment remains unchanged after any write on memory,  because
; program is in ROM.

Theorem: byte-write-mcode-addrp (pc-read-memp (pc, mem, len (lst)) ∧ byte-writep (x, mem)) → (mcode-addrp (pc, byte-write (value, x, mem), lst)

= mcode-addrp (pc, mem, lst))

Theorem: write-mem-mcode-addrp (pc-read-memp (pc, mem, len (lst)) ∧ write-memp (x, mem, n)) → (mcode-addrp (pc, write-mem (value, x, mem, n), lst)

= mcode-addrp (pc, mem, lst))

;               DISJOINT0 AND DISJOINT

Theorem: disjoint0-head (disjoint0 (head (x, 32), m, y) = disjoint0 (x, m, y)) ∧ (disjoint0 (x, m, head (y, 32)) = disjoint0 (x, m, y))

Theorem: disjoint-head (disjoint (head (x, 32), m, y, n) = disjoint (x, m, y, n)) ∧ (disjoint (x, m, head (y, 32), n) = disjoint (x, m, y, n))

Theorem: disjoint0-la0 (disjoint0 (a, m, b) ∧ (i < m)) → (¬ mod32-eq (add (32, a, i), b))

Theorem: disjoint0-la1 (disjoint0 (a, m, b) ∧ (i < m)) → disjoint0 (a, i, b)

Theorem: disjoint0-la2 (disjoint0 (a, m, b) ∧ ((i + j ) ≤ m)) → disjoint0 (add (32, a, i), j , b)

Theorem: disjoint-la0 (disjoint (a, m, b, n) ∧ (j < n)) → disjoint0 (a, m, add (32, b, j ))

Theorem: disjoint-la1 (disjoint (a, m, b, n) ∧ (i < m) ∧ (j < n)) → (¬ mod32-eq (add (32, a, i), add (32, b, j )))

Theorem: disjoint-la2 (disjoint (a, m, b, n) ∧ ((i + j ) ≤ m) ∧ (k < n)) → disjoint0 (add (32, a, i), j , add (32, b, k))

Theorem: disjoint-la3 (disjoint (a, m, b, n) ∧ ((i + j ) ≤ m) ∧ ((k + l) ≤ n)) → disjoint (add (32, a, i), j , add (32, b, k), l)

;

Theorem: disjoint-0 (disjoint (a, m, b, n) ∧ (j ≤ m) ∧ (l ≤ n)) → disjoint (a, j , b, l)

Theorem: disjoint-1 (disjoint (a, m, b, n) ∧ (j ≤ m) ∧ ((k + l) ≤ n)) → disjoint (a, j , add (32, b, k), l)

Theorem: disjoint-2 (disjoint (a, m, b, n) ∧ ((i + j ) ≤ m) ∧ (l ≤ n)) → disjoint (add (32, a, i), j , b, l)

Theorem: disjoint-3 (disjoint (a, m, b, n) ∧ ((i + j ) ≤ m) ∧ ((k + l) ≤ n)) → disjoint (add (32, a, i), j , add (32, b, k), l)

;

Theorem: disjoint-4 (disjoint (add (32, a, i), m, b, n) ∧ ((j + index-n (0, i)) ≤ m) ∧ (l ≤ n)) → disjoint (a, j , b, l)

Theorem: disjoint-5 (disjoint (add (32, a, i), m, b, n) ∧ ((j + index-n (0, i)) ≤ m) ∧ ((k + l) ≤ n)) → disjoint (a, j , add (32, b, k), l)

Theorem: disjoint-6 (disjoint (add (32, a, i), m, b, n) ∧ ((j + index-n (i1 , i)) ≤ m) ∧ (l ≤ n)) → disjoint (add (32, a, i1 ), j , b, l)

Theorem: disjoint-7 (disjoint (add (32, a, i), m, b, n) ∧ ((j + index-n (i1 , i)) ≤ m) ∧ ((k + l) ≤ n)) → disjoint (add (32, a, i1 ), j , add (32, b, k), l)

;

Theorem: disjoint-8 (disjoint (a, m, add (32, b, k), n) ∧ (j ≤ m) ∧ ((l + index-n (0, k)) ≤ n)) → disjoint (a, j , b, l)

Theorem: disjoint-9 (disjoint (a, m, add (32, b, k), n) ∧ ((i + j ) ≤ m) ∧ ((l + index-n (0, k)) ≤ n)) → disjoint (add (32, a, i), j , b, l)

Theorem: disjoint-10 (disjoint (a, m, add (32, b, k), n) ∧ (j ≤ m) ∧ ((l + index-n (k1 , k)) ≤ n)) → disjoint (a, j , add (32, b, k1 ), l)

Theorem: disjoint-11 (disjoint (a, m, add (32, b, k), n) ∧ ((i + j ) ≤ m) ∧ ((l + index-n (k1 , k)) ≤ n)) → disjoint (add (32, a, i), j , add (32, b, k1 ), l)

;

Theorem: disjoint-12 (disjoint (add (32, a, i), m, add (32, b, k), n) ∧ ((j + index-n (0, i)) ≤ m) ∧ ((l + index-n (0, k)) ≤ n)) → disjoint (a, j , b, l)

Theorem: disjoint-13 (disjoint (add (32, a, i), m, add (32, b, k), n) ∧ ((j + index-n (i1 , i)) ≤ m) ∧ ((l + index-n (0, k)) ≤ n)) → disjoint (add (32, a, i1 ), j , b, l)

Theorem: disjoint-14 (disjoint (add (32, a, i), m, add (32, b, k), n) ∧ ((j + index-n (0, i)) ≤ m) ∧ ((l + index-n (k1 , k)) ≤ n)) → disjoint (a, j , add (32, b, k1 ), l)

Theorem: disjoint-15 (disjoint (add (32, a, i), m, add (32, b, k), n) ∧ ((j + index-n (i1 , i)) ≤ m) ∧ ((l + index-n (k1 , k)) ≤ n)) → disjoint (add (32, a, i1 ), j , add (32, b, k1 ), l)

; the commutativity of disjoint.

Theorem: disjoint-commutativity disjoint (x, m, y, n) = disjoint (y, n, x, m)

; the dual events of the above 16 events.

Theorem: disjoint-0˜ (disjoint (a, m, b, n) ∧ (j ≤ m) ∧ (l ≤ n)) → disjoint (b, l, a, j )

Theorem: disjoint-1˜ (disjoint (a, m, b, n) ∧ (j ≤ m) ∧ ((k + l) ≤ n))

→ disjoint (add (32, b, k), l, a, j )

Theorem: disjoint-2˜ (disjoint (a, m, b, n) ∧ ((i + j ) ≤ m) ∧ (l ≤ n))

→ disjoint (b, l, add (32, a, i), j )

Theorem: disjoint-3˜ (disjoint (a, m, b, n) ∧ ((i + j ) ≤ m) ∧ ((k + l) ≤ n))

→ disjoint (add (32, b, k), l, add (32, a, i), j )

;

Theorem: disjoint-4˜ (disjoint (add (32, a, i), m, b, n) ∧ ((j + index-n (0, i)) ≤ m) ∧ (l ≤ n)) → disjoint (b, l, a, j )

Theorem: disjoint-5˜ (disjoint (add (32, a, i), m, b, n)

∧ ((j + index-n (0, i)) ≤ m)

∧ ((k + l) ≤ n))

→ disjoint (add (32, b, k), l, a, j )

Theorem: disjoint-6˜ (disjoint (add (32, a, i), m, b, n)

∧ ((j + index-n (i1 , i)) ≤ m)

∧ (l ≤ n))

→ disjoint (b, l, add (32, a, i1 ), j )

Theorem: disjoint-7˜ (disjoint (add (32, a, i), m, b, n)

∧ ((j + index-n (i1 , i)) ≤ m) ∧ ((k + l) ≤ n)) → disjoint (add (32, b, k), l, add (32, a, i1 ), j )

;

Theorem: disjoint-8˜ (disjoint (a, m, add (32, b, k), n) ∧ (j ≤ m) ∧ ((l + index-n (0, k)) ≤ n)) → disjoint (b, l, a, j )

Theorem: disjoint-9˜ (disjoint (a, m, add (32, b, k), n)

∧ ((i + j ) ≤ m) ∧ ((l + index-n (0, k)) ≤ n)) → disjoint (b, l, add (32, a, i), j )

Theorem: disjoint-10˜ (disjoint (a, m, add (32, b, k), n)

∧ (j ≤ m) ∧ ((l + index-n (k1 , k)) ≤ n)) → disjoint (add (32, b, k1 ), l, a, j )

Theorem: disjoint-11˜ (disjoint (a, m, add (32, b, k), n)

∧ ((i + j ) ≤ m) ∧ ((l + index-n (k1 , k)) ≤ n)) → disjoint (add (32, b, k1 ), l, add (32, a, i), j )

;

Theorem: disjoint-12˜ (disjoint (add (32, a, i), m, add (32, b, k), n)

∧ ((j + index-n (0, i)) ≤ m) ∧ ((l + index-n (0, k)) ≤ n)) → disjoint (b, l, a, j )

Theorem: disjoint-13˜ (disjoint (add (32, a, i), m, add (32, b, k), n)

∧ ((j + index-n (i1 , i)) ≤ m) ∧ ((l + index-n (0, k)) ≤ n)) → disjoint (b, l, add (32, a, i1 ), j )

Theorem: disjoint-14˜ (disjoint (add (32, a, i), m, add (32, b, k), n)

∧ ((j + index-n (0, i)) ≤ m) ∧ ((l + index-n (k1 , k)) ≤ n)) → disjoint (add (32, b, k1 ), l, a, j )

Theorem: disjoint-15˜ (disjoint (add (32, a, i), m, add (32, b, k), n)

∧ ((j + index-n (i1 , i)) ≤ m) ∧ ((l + index-n (k1 , k)) ≤ n)) → disjoint (add (32, b, k1 ), l, add (32, a, i1 ), j )

; disjoint with asl.

Theorem: times-plus-lessp-cancel ((a ≤ k) ∧ (b ≤ k) ∧ (a < b)) → (((a + (i ∗ k)) < (b + (j ∗ k))) = (i ≤ j ))

Theorem: disjoint-2-asl (disjoint (a, m, b, n) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (x, 32) < (m ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N) ∧ (l ≤ n)) → disjoint (add (32, a, asl (32, x, cnt)), opsz, b, l)

Theorem: disjoint-2˜-asl (disjoint (a, m, b, n) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (x, 32) < (m ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N) ∧ (l ≤ n)) → disjoint (b, l, add (32, a, asl (32, x, cnt)), opsz)

Theorem: disjoint-3-asl (disjoint (a, m, b, n) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (x, 32) < (m ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N) ∧ ((k + l) ≤ n)) → disjoint (add (32, a, asl (32, x, cnt)), opsz, add (32, b, k), l)

Theorem: disjoint-3˜-asl (disjoint (a, m, b, n) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (x, 32) < (m ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N) ∧ ((k + l) ≤ n)) → disjoint (add (32, b, k), l, add (32, a, asl (32, x, cnt)), opsz)

Theorem: disjoint-9-asl (disjoint (a, m, add (32, b, k), n) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (x, 32) < (m ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N) ∧ ((l + index-n (0, k)) ≤ n)) → disjoint (add (32, a, asl (32, x, cnt)), opsz, b, l)

Theorem: disjoint-9˜-asl (disjoint (a, m, add (32, b, k), n) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (x, 32) < (m ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N) ∧ ((l + index-n (0, k)) ≤ n)) → disjoint (b, l, add (32, a, asl (32, x, cnt)), opsz)

Theorem: disjoint-11-asl (disjoint (a, m, add (32, b, k), n) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (x, 32) < (m ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N) ∧ ((l + index-n (k1 , k)) ≤ n)) → disjoint (add (32, a, asl (32, x, cnt)), opsz, add (32, b, k1 ), l)

Theorem: disjoint-11˜-asl (disjoint (a, m, add (32, b, k), n) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (x, 32) < (m ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N) ∧ ((l + index-n (k1 , k)) ≤ n)) → disjoint (add (32, b, k1 ), l, add (32, a, asl (32, x, cnt)), opsz)

Event: Disable times-plus-lessp-cancel.

; a set of rewrite rules for disjoint0 and disjoint.

Theorem: disjoint0-x-x disjoint0 (x, m, x) = (m ≃ 0)

Theorem: disjoint0-deduction0 disjoint0 (x, 0, y)

Theorem: disjoint0-deduction1 (disjoint0 (x, m, add (32, x, y)) = disjoint0 (0, m, y)) ∧ (disjoint0 (add (32, x, y), m, x) = disjoint0 (y, m, 0))

Theorem: disjoint0-deduction2 disjoint0 (add (32, x, y), m, add (32, x, z)) = disjoint0 (y, m, z)

Theorem: disjoint-x-x disjoint (x, m, x, n) = ((m ≃ 0) ∨ (n ≃ 0))

Theorem: disjoint-deduction0 disjoint (x, m, y, 0) ∧ disjoint (x, 0, y, n)

Theorem: disjoint-deduction1 (disjoint (x, m, add (32, x, y), n) = disjoint (0, m, y, n)) ∧ (disjoint (add (32, x, y), m, x, n) = disjoint (y, m, 0, n))

Theorem: disjoint-deduction2 disjoint (add (32, x, y), m, add (32, x, z), n) = disjoint (y, m, z, n)

;                     INDEX-N

Theorem: index-n-0 (index-n (x, 0) = head (x, 32)) ∧ (index-n (0, x) = neg (32, x))

Theorem: index-n-x-x index-n (x, x) = 0

Theorem: index-n-deduction0 (index-n (x, neg (32, y)) = index-n (add (32, x, y), 0)) ∧ (index-n (neg (32, x), y) = index-n (0, add (32, x, y)))

Theorem: index-n-deduction1 (index-n (add (32, x, y), x) = index-n (y, 0)) ∧ (index-n (y, add (32, y, x)) = index-n (0, x))

Theorem: index-n-deduction2 index-n (add (32, z, x), add (32, z, y)) = index-n (x, y)

Theorem: disjoint-deduction3 disjoint (add (32, y, x), m, add (32, z, x), n) = disjoint (y, m, z, n)

Event: Disable index-n.

;           READ-MEM/WRITE-MEM WITH MEM-LST/MEM-ILST
;
; starting at address a, the contents of the memory are equal to the elements
; of lst.

Definition: mem-lst (opsz, a, mem, n, lst) = if n ≃ 0 then lst ≃ nil

else (read-mem (a, mem, opsz) = car (lst))

∧ mem-lst (opsz, add (l, a, opsz), mem, n − 1, cdr (lst)) endif

Definition: mem-ilst (opsz, a, mem, n, lst) = if n ≃ 0 then lst ≃ nil

else (nat-to-int (read-mem (a, mem, opsz), 8 ∗ opsz) = car (lst)) ∧ mem-ilst (opsz, add (l, a, opsz), mem, n − 1, cdr (lst)) endif

; every element in lst is in "good" range.

Theorem: mem-lst-nat-rangep (mem-lst (opsz, a, mem, n, lst) ∧ ((8 ∗ opsz) ≤ k)) → nat-rangep (get-nth (i, lst), k) Theorem: mem-ilst-int-rangep (mem-ilst (opsz, a, mem, n, lst) ∧ (oplen = (8 ∗ opsz))) → int-rangep (get-nth (i, lst), oplen)

; every element in lst is a natural number.

Theorem: mem-lst-numberp mem-lst (opsz, a, mem, n, lst) → (get-nth (i, lst) ∈ N)

; every element in lst is bounded by 2^(8*opsz).

Theorem: mem-lst-lessp (mem-lst (opsz, a, mem, n, lst) ∧ (k = exp (2, 8 ∗ opsz))) → (get-nth (i, lst) < k)

; every element in lst is an integer.

Theorem: mem-ilst-integerp mem-ilst (opsz, a, mem, n, lst) → integerp (get-nth (i, lst))

; a trivial, but useful, instantiation!

Theorem: readm-mem-lst mem-lst (opsz, a, mem, n, readm-mem (opsz, a, mem, n))

; head with mem-lst/mem-ilst.

Theorem: head-mem-lst mem-lst (opsz, head (x, 32), mem, n, lst) = mem-lst (opsz, x, mem, n, lst) Theorem: head-mem-ilst mem-ilst (opsz, head (x, 32), mem, n, lst) = mem-ilst (opsz, x, mem, n, lst) Theorem: read-mem-non-numberp (x ∉ N) → (read-mem (x, mem, k) = read-mem (0, mem, k)) Theorem: mem-lst-non-numberp (x ∉ N) → (mem-lst (opsz, x, mem, n, lst) = mem-lst (opsz, 0, mem, n, lst)) Theorem: mem-lst-same (mem-lst (opsz, x, mem, n, lst) ∧ (nat-to-uint (x) = nat-to-uint (y))) → mem-lst (opsz, y, mem, n, lst)

Event: Disable read-mem-non-numberp.

Event: Disable mem-lst-non-numberp.

Event: Disable mem-lst-same.

;                    CANONICAL FORMS
; Sometimes,  it is possible to have more than one representation
; for one concept.  We have to tell the prover only to use the canonical
; representations.

Theorem: pc-byte-read=pc-read-mem-1 pc-byte-read (addr, mem) = pc-read-mem (addr, mem, 1)

Theorem: byte-read=read-mem-1 byte-read (addr, mem) = read-mem (addr, mem, 1)

Theorem: byte-write=write-mem-1 byte-write (value, addr, mem) = write-mem (value, addr, mem, 1)

Theorem: byte-writep=write-memp-1 byte-writep (x, mem) = write-memp (x, mem, 1)

;        GET-LST, PUT-LST, GET-VALS, PUT-VALS, MCAR, and MCDR

Definition: get-lst (opsz, m, lst, n) = if n ≃ 0 then 0

else app (8 ∗ opsz, get-nth (m + (n − 1), lst), get-lst (opsz, m, lst, n − 1)) endif

Definition: put-lst (opsz, v, n, lst, k) = if k ≃ 0 then lst

else put-lst (opsz, tail (v, 8 ∗ opsz), n, put-nth (head (v, 8 ∗ opsz), n + (k − 1), lst), k − 1) endif

Definition: get-vals (m, lst, n) = if n ≃ 0 then nil

else append (get-vals (m, lst, n − 1), list (get-nth (m + (n − 1), lst))) endif Definition: put-vals (vals, m, lst, n) = if n ≃ 0 then lst

else put-vals (vals, m, put-nth (get-nth (n − 1, vals), m + (n − 1), lst), n − 1) endif

Definition: bv-to-lst (opsz, bv, n) = if n ≃ 0 then nil

else append (bv-to-lst (opsz, tail (bv, 8 ∗ opsz), n − 1), list (head (bv, 8 ∗ opsz))) endif

Definition: lst-to-bv (opsz, lst, n) = if n ≃ 0 then 0

else app (8 ∗ opsz, get-nth (n − 1, lst), lst-to-bv (opsz, lst, n − 1)) endif

; mcar returns the list consisting of the first n elements of lst.

Definition: mcar (n, lst) = if n ≃ 0 then nil

else cons (car (lst), mcar (n − 1, cdr (lst))) endif

; mcdr returns the list discarding the first n elements of lst.

Definition: mcdr (n, lst) = if n ≃ 0 then lst

else mcdr (n − 1, cdr (lst)) endif

; a predicate to recognize proper list.

Definition: proper-lstp (lst) = if lst ≃ nil then lst = nil

else proper-lstp (cdr (lst)) endif

Theorem: append-len len (append (x, y)) = (len (x) + len (y))

Theorem: get-vals-len len (get-vals (m, lst, n)) = fix (n)

Theorem: bv-to-lst-len len (bv-to-lst (opsz, bv, n)) = fix (n)

Theorem: get-vals-proper-lstp proper-lstp (get-vals (m, lst, n))

Theorem: bv-to-lst-proper-lstp proper-lstp (bv-to-lst (opsz, bv, n))

Theorem: mcdr-listp-len listp (mcdr (n, lst)) = (n < len (lst))

Theorem: cdr-mcdr cdr (mcdr (n, lst)) = mcdr (1 + n, lst)

Theorem: mcar-mcar (m ≤ n) → (mcar (m, mcar (n, lst)) = mcar (m, lst))

Theorem: mcdr-mcdr mcdr (n, mcdr (m, lst)) = mcdr (m + n, lst)

Theorem: mcar-nth get-nth (n, mcar (m, lst)) = if n < m then get-nth (n, lst)

else 0 endif

Theorem: mcdr-nth get-nth (n, mcdr (m, lst)) = get-nth (m + n, lst)

Theorem: get-lst-cdr get-lst (opsz, m, cdr (lst), n) = get-lst (opsz, 1 + m, lst, n)

Theorem: get-lst-mcdr get-lst (opsz, m, mcdr (j , lst), n) = get-lst (opsz, m + j , lst, n)

Theorem: get-lst-mcar ((m + n) ≤ j ) → (get-lst (opsz, m, mcar (j , lst), n) = get-lst (opsz, m, lst, n))

Theorem: get-vals-cdr get-vals (m, cdr (lst), n) = get-vals (1 + m, lst, n)

Theorem: get-vals-mcdr get-vals (m, mcdr (j , lst), n) = get-vals (m + j , lst, n)

Theorem: get-vals-mcar ((m + n) ≤ j ) → (get-vals (m, mcar (j , lst), n) = get-vals (m, lst, n))

Theorem: get-nth-append get-nth (i, append (x, y)) = if i < len (x) then get-nth (i, x)

else get-nth (i − len (x), y) endif

Theorem: get-vals-append (n ≤ len (x)) → (get-vals (0, append (x, y), n) = get-vals (0, x, n))

Theorem: put-vals-append (n ≤ len (x)) → (put-vals (append (x, y), m, lst, n) = put-vals (x, m, lst, n))

; another induction hint for many theorems about memory.

Definition: mem-induct2 (opsz, addr, i, n, lst, j ) = if n ≃ 0 then t

else mem-induct2 (opsz, add (32, addr, opsz), i − 1, n − 1, cdr (lst), j − opsz) endif

Theorem: read-mem-lst-la (mem-lst (opsz, a, mem, n, lst) ∧ ((j mod opsz) = 0) ∧ ((j ÷ opsz) < n)) → (read-mem (add (32, a, j ), mem, opsz) = get-nth (j ÷ opsz, lst))

Theorem: mem-lst-get-lst0 (mem-lst (1, a, mem, n, lst) ∧ (k ≤ n)) → (nat-to-uint (read-mem (a, mem, k)) = get-lst (1, 0, lst, k))

Theorem: mem-lst-get-lst (mem-lst (1, a, mem, n, lst) ∧ ((nat-to-uint (j ) + k) ≤ n)) → (nat-to-uint (read-mem (add (32, a, j ), mem, k))

= get-lst (1, nat-to-uint (j ), lst, k))

Theorem: mem-lst-get-vals0 (mem-lst (1, a, mem, n, lst) ∧ (k ≤ n)) → (bv-to-lst (1, read-mem (a, mem, k), k) = get-vals (0, lst, k))

Theorem: mem-lst-get-vals (mem-lst (1, a, mem, n, lst) ∧ ((nat-to-uint (j ) + k) ≤ n)) → (bv-to-lst (1, read-mem (add (32, a, j ), mem, k), k)

= get-vals (nat-to-uint (j ), lst, k))

; read is equivalent to get-nth.

Theorem: read-mem-lst0 (mem-lst (opsz, a, mem, n, lst) ∧ (n ≄ 0)) → (nat-to-uint (read-mem (a, mem, opsz)) = get-nth (0, lst))

Theorem: iread-mem-get0 (mem-ilst (opsz, a, mem, n, lst) ∧ (n ≄ 0) ∧ (oplen = (8 ∗ opsz))) → (nat-to-int (read-mem (a, mem, opsz), oplen) = get-nth (0, lst))

Theorem: read-mem-lst (mem-lst (opsz, a, mem, n, lst) ∧ ((nat-to-uint (j ) mod opsz) = 0) ∧ ((nat-to-uint (j ) ÷ opsz) < n)) → (nat-to-uint (read-mem (add (32, a, j ), mem, opsz))

= get-nth (nat-to-uint (j ) ÷ opsz, lst))

Theorem: read-mem-lst-int (mem-lst (opsz, a, mem, n, lst) ∧ ((nat-to-int (j , 32) mod opsz) = 0) ∧ ((nat-to-int (j , 32) ÷ opsz) < n) ∧ (nat-to-int (j , 32) ∈ N)) → (nat-to-uint (read-mem (add (32, a, j ), mem, opsz))

= get-nth (nat-to-int (j , 32) ÷ opsz, lst))

Theorem: read-mem-ilst (mem-ilst (opsz, a, mem, n, lst) ∧ (oplen = (8 ∗ opsz)) ∧ ((nat-to-uint (j ) mod opsz) = 0) ∧ ((nat-to-uint (j ) ÷ opsz) < n)) → (nat-to-int (read-mem (add (32, a, j ), mem, opsz), oplen)

= get-nth (nat-to-uint (j ) ÷ opsz, lst))

Theorem: read-mem-ilst-int (mem-ilst (opsz, a, mem, n, lst) ∧ (oplen = (8 ∗ opsz)) ∧ ((nat-to-uint (j ) mod opsz) = 0) ∧ ((nat-to-uint (j ) ÷ opsz) < n) ∧ (nat-to-int (j , 32) ∈ N)) → (nat-to-int (read-mem (add (32, a, j ), mem, opsz), oplen)

= get-nth (nat-to-uint (j ) ÷ opsz, lst))

; write to some location else does not affect mem-lst.

Theorem: write-else-mem-lst disjoint (a, opsz ∗ n, x, m) → (mem-lst (opsz, a, write-mem (value, x, mem, m), n, lst)

= mem-lst (opsz, a, mem, n, lst))

Theorem: write-else-mem-ilst disjoint (a, opsz ∗ n, x, m) → (mem-ilst (opsz, a, write-mem (value, x, mem, m), n, lst)

= mem-ilst (opsz, a, mem, n, lst))

; some conditions that makes disjoint true.

Theorem: disjoint0-leq (((a + m) ≤ 4294967296) ∧ (b < a)) → disjoint0 (a, m, b)

Theorem: disjoint-leq (((a + m) ≤ 4294967296) ∧ ((b + n) ≤ a)) → disjoint (a, m, b, n)

Theorem: disjoint-leq1 (((a + m) ≤ 4294967296) ∧ ((b + n) ≤ a)) → disjoint (b, n, a, m)

Theorem: plus-times-lessp (((x + (y ∗ z)) < w) ∧ (z1 < z)) → ((x + y + (y ∗ z1 )) < w)

Theorem: write-mem-lst-la (mem-lst (opsz, a, mem, n, lst) ∧ uint-rangep (opsz ∗ n, 32) ∧ (v1 = head (v, 8 ∗ opsz)) ∧ (j = (opsz ∗ i)) ∧ (i < n) ∧ (v ∈ N)) → mem-lst (opsz, a, write-mem (v, add (32, a, j ), mem, opsz), n, put-nth (v1 , i, lst))

Definition: mem-induct3 (v, v1 , a, mem, i, lst, k) = if k ≃ 0 then t

else mem-induct3 (tail (v, 8), tail (v1 , 8), a, byte-write (v, add (32, a, i + (k − 1)), mem), i, put-nth (head (v, 8), i + (k − 1), lst), k − 1) endif

Theorem: mem-lst-put-lst (mem-lst (1, a, mem, n, lst) ∧ uint-rangep (n, 32) ∧ nat-rangep (v, 8 ∗ k) ∧ (nat-to-uint (j ) = i)

∧ (v1 = nat-to-uint (v)) ∧ ((i + k) ≤ n) ∧ (j ∈ N) ∧ (v ∈ N)) → mem-lst (1, a, write-mem (v, add (32, a, j ), mem, k), n, put-lst (1, v1 , i, lst, k))

Definition: mem-induct4 (v, vals, a, mem, i, lst, k) = if k ≃ 0 then t

else mem-induct4 (tail (v, 8), get-vals (0, vals, k − 1), a, byte-write (v, add (32, a, i + (k − 1)), mem), i, put-nth (head (v, 8), i + (k − 1), lst), k − 1) endif

Theorem: get-vals-0 ((len (lst) = n) ∧ proper-lstp (lst)) → (get-vals (0, lst, n) = lst)

Theorem: mem-lst-put-vals (mem-lst (1, a, mem, n, lst) ∧ uint-rangep (n, 32) ∧ nat-rangep (v, 8 ∗ k) ∧ (nat-to-uint (j ) = i) ∧ (vals = bv-to-lst (1, v, k)) ∧ ((i + k) ≤ n) ∧ (j ∈ N) ∧ (v ∈ N)) → mem-lst (1, a, write-mem (v, add (32, a, j ), mem, k), n, put-vals (vals, i, lst, k))

Event: Disable get-vals-0.

Theorem: write-mem-lst (mem-lst (opsz, a, mem, n, lst) ∧ uint-rangep (opsz ∗ n, 32) ∧ nat-rangep (v, 8 ∗ opsz) ∧ (nat-to-uint (j ) = (opsz ∗ i)) ∧ (v1 = nat-to-uint (v)) ∧ (i < n) ∧ (j ∈ N) ∧ (v ∈ N)) → mem-lst (opsz, a, write-mem (v, add (32, a, j ), mem, opsz), n, put-nth (v1 , i, lst))

Theorem: write-mem-ilst (mem-ilst (opsz, a, mem, n, lst) ∧ uint-rangep (opsz ∗ n, 32) ∧ (nat-to-uint (j ) = (opsz ∗ i)) ∧ nat-rangep (v, 8 ∗ opsz) ∧ (v1 = nat-to-int (v, 8 ∗ opsz)) ∧ (i < n) ∧ (j ∈ N) ∧ (v ∈ N)) → mem-ilst (opsz,

a,

write-mem (v, add (32, a, j ), mem, opsz), n, put-nth (v1 , i, lst))

Theorem: write-mem-lst0 (mem-lst (opsz, a, mem, n, lst) ∧ uint-rangep (opsz ∗ n, 32) ∧ nat-rangep (v, 8 ∗ opsz) ∧ (v1 = nat-to-uint (v)) ∧ (n ≄ 0) ∧ (v ∈ N)) → mem-lst (opsz, a, write-mem (v, a, mem, opsz), n, put-nth (v1 , 0, lst))

Theorem: write-mem-ilst0 (mem-ilst (opsz, a, mem, n, lst) ∧ uint-rangep (opsz ∗ n, 32) ∧ nat-rangep (v, 8 ∗ opsz) ∧ (v1 = nat-to-int (v, 8 ∗ opsz)) ∧ (n ≄ 0) ∧ (v ∈ N)) → mem-ilst (opsz, a, write-mem (v, a, mem, opsz), n, put-nth (v1 , 0, lst))

Theorem: write-mem-lst-int (mem-lst (opsz, a, mem, n, lst) ∧ uint-rangep (opsz ∗ n, 32) ∧ ((opsz ∗ i) = nat-to-int (j , 32)) ∧ (nat-to-int (j , 32) ∈ N) ∧ nat-rangep (v, 8 ∗ opsz) ∧ (v1 = nat-to-uint (v)) ∧ (i < n) ∧ (opsz ≄ 0) ∧ (v ∈ N)) → mem-lst (opsz, a, write-mem (v, add (32, a, j ), mem, opsz), n, put-nth (v1 , i, lst))

Theorem: write-mem-ilst-int (mem-ilst (opsz, a, mem, n, lst) ∧ uint-rangep (opsz ∗ n, 32) ∧ ((opsz ∗ i) = nat-to-int (j , 32)) ∧ (nat-to-int (j , 32) ∈ N) ∧ nat-rangep (v, 8 ∗ opsz) ∧ (v1 = nat-to-int (v, 8 ∗ opsz)) ∧ (i < n) ∧ (opsz ≄ 0) ∧ (v ∈ N)) → mem-ilst (opsz,

a,

write-mem (v, add (32, a, j ), mem, opsz), n, put-nth (v1 , i, lst))

;                    INTEGER VIEWS
;                    A + OPSZ * I
; to deal with the address calculation a+2*i or a+4*i, we introduce
; the following set of lemmas.

Theorem: read-mem-lst-asl (mem-lst (opsz, a, mem, n, lst) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (i, 32) < n) ∧ (nat-to-int (i, 32) ∈ N)) → (nat-to-uint (read-mem (add (32, a, asl (32, i, cnt)), mem, opsz))

= get-nth (nat-to-int (i, 32), lst))

Theorem: read-mem-ilst-asl (mem-ilst (opsz, a, mem, n, lst) ∧ (opsz = exp (2, cnt)) ∧ (oplen = (8 ∗ opsz)) ∧ (nat-to-int (i, 32) < n) ∧ (nat-to-int (i, 32) ∈ N)) → (nat-to-int (read-mem (add (32, a, asl (32, i, cnt)), mem, opsz), oplen)

= get-nth (nat-to-int (i, 32), lst))

Theorem: write-mem-lst-asl (mem-lst (opsz, a, mem, n, lst) ∧ uint-rangep (opsz ∗ n, 32) ∧ (opsz = exp (2, cnt)) ∧ nat-rangep (v, 8 ∗ opsz) ∧ (j = nat-to-int (i, 32)) ∧ (v1 = nat-to-uint (v))

∧ (j < n) ∧ (j ∈ N) ∧ (v ∈ N)) → mem-lst (opsz,

a,

write-mem (v, add (32, a, asl (32, i, cnt)), mem, opsz), n, put-nth (v1 , j , lst))

Theorem: write-mem-ilst-asl (mem-ilst (opsz, a, mem, n, lst) ∧ uint-rangep (opsz ∗ n, 32) ∧ (opsz = exp (2, cnt)) ∧ nat-rangep (v, 8 ∗ opsz) ∧ (v1 = nat-to-int (v, 8 ∗ opsz)) ∧ (j = nat-to-int (i, 32)) ∧ (j < n) ∧ (v ∈ N) ∧ (j ∈ N)) → mem-ilst (opsz,

a,

write-mem (v, add (32, a, asl (32, i, cnt)), mem, opsz), n, put-nth (v1 , j , lst))

Theorem: times-lessp-cancel1 ((y ∗ x) < (x + (z ∗ x))) = ((x ≄ 0) ∧ (y ≤ z))

Theorem: read-memp-ram1-asl (ram-addrp (addr, mem, n) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (x, 32) < (n ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N)) → read-memp (add (32, addr, asl (32, x, cnt)), mem, opsz)

Theorem: read-memp-rom1-asl (rom-addrp (addr, mem, n) ∧ (opsz = exp (2, cnt)) ∧ (nat-to-int (x, 32) < (n ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N)) → read-memp (add (32, addr, asl (32, x, cnt)), mem, opsz)

Theorem: write-memp-ram1-asl (ram-addrp (addr, mem, n) ∧ (opsz = exp (2, cnt))

∧ (nat-to-int (x, 32) < (n ÷ opsz)) ∧ (nat-to-int (x, 32) ∈ N)) → write-memp (add (32, addr, asl (32, x, cnt)), mem, opsz)

;             BASIC READM-MEM/WRITEM-MEM EVENTS
;

Theorem: writem-mem-maintain-pc-byte-readp pc-byte-readp (x, writem-mem (opsz, vlst, addr, mem)) = pc-byte-readp (x, mem)

Theorem: writem-mem-maintain-pc-read-memp pc-read-memp (x, writem-mem (opsz, vlst, addr, mem), n) = pc-read-memp (x, mem, n)

Theorem: writem-mem-maintain-byte-readp byte-readp (x, writem-mem (opsz, vlst, addr, mem)) = byte-readp (x, mem)

Theorem: writem-mem-maintain-read-memp read-memp (x, writem-mem (opsz, vlst, addr, mem), n) = read-memp (x, mem, n)

Theorem: writem-mem-maintain-byte-writep byte-writep (x, writem-mem (opsz, vlst, addr, mem)) = byte-writep (x, mem)

Theorem: writem-mem-maintain-write-memp write-memp (x, writem-mem (opsz, vlst, addr, mem), n) = write-memp (x, mem, n)

Theorem: writem-mem-maintain-rom-addrp rom-addrp (x, writem-mem (opsz, vlst, addr, mem), n) = rom-addrp (x, mem, n)

Theorem: writem-mem-maintain-ram-addrp ram-addrp (x, writem-mem (opsz, vlst, addr, mem), n) = ram-addrp (x, mem, n)

Theorem: pc-read-mem-writem-mem (write-memp (addr, mem, opsz ∗ len (vlst)) ∧ pc-read-memp (x, mem, n)) → (pc-read-mem (x, writem-mem (opsz, vlst, addr, mem), n)

= pc-read-mem (x, mem, n))

Theorem: writem-mem-mcode-addrp (pc-read-memp (pc, mem, len (lst)) ∧ write-memp (addr, mem, opsz ∗ len (vlst))) → (mcode-addrp (pc, writem-mem (opsz, vlst, addr, mem), lst)

= mcode-addrp (pc, mem, lst))

Theorem: writem-else-mem-lst disjoint (addr, opsz1 ∗ len (vlst), a, opsz ∗ n) → (mem-lst (opsz, a, writem-mem (opsz1 , vlst, addr, mem), n, lst)

= mem-lst (opsz, a, mem, n, lst))

Theorem: writem-else-mem-ilst disjoint (a, opsz ∗ n, addr, opsz1 ∗ len (vlst)) → (mem-ilst (opsz, a, writem-mem (opsz1 , vlst, addr, mem), n, lst)

= mem-ilst (opsz, a, mem, n, lst))

Theorem: read-writem-mem disjoint (addr, n, addr1 , opsz ∗ len (vlst)) → (read-mem (addr, writem-mem (opsz, vlst, addr1 , mem), n)

= read-mem (addr, mem, n))

Theorem: readm-write-mem disjoint (addr, opsz ∗ n, addr1 , k) → (readm-mem (opsz, addr, write-mem (value, addr1 , mem, k), n)

= readm-mem (opsz, addr, mem, n))

Definition: modn-lst (n, lst) = if lst ≃ nil then nil

else cons (head (car (lst), n), modn-lst (n, cdr (lst))) endif

Theorem: modn-readm-rn modn-lst (oplen, readm-rn (oplen, rnlst, rfile)) = readm-rn (oplen, rnlst, rfile)

Theorem: readm-writem-mem (uint-rangep (opsz ∗ n, 32) ∧ (n = len (vlst))) → (readm-mem (opsz, addr, writem-mem (opsz, vlst, addr, mem), n)

= modn-lst (8 ∗ opsz, vlst))

Theorem: disjoint-leq-uint (((nat-to-uint (a) + m) ≤ 4294967296) ∧ ((nat-to-uint (b) + n) ≤ nat-to-uint (a))) → disjoint (a, m, b, n)

Theorem: disjoint-leq1-uint (((nat-to-uint (a) + m) ≤ 4294967296) ∧ ((nat-to-uint (b) + n) ≤ nat-to-uint (a))) → disjoint (b, n, a, m)

Event: Disable disjoint-leq.

Event: Disable disjoint-leq1.

Event: Disable disjoint0-leq.

Event: Disable disjoint-commutativity.

Event: Disable disjoint-leq-uint.

Event: Disable disjoint-leq1-uint.

;              MEM-LST WITH MCAR AND MCDR

Theorem: mem-lst-plus mem-lst (opsz, a, mem, m + n, lst) = (mem-lst (opsz, a, mem, m, mcar (m, lst))

∧ mem-lst (opsz, add (32, a, opsz ∗ m), mem, n, mcdr (m, lst)))

Theorem: mem-lst-mcar (mem-lst (opsz, a, mem, n, lst) ∧ (k ≤ n)) → mem-lst (opsz, a, mem, k, mcar (k, lst))

Theorem: mem-lst-mcar-1 mem-lst (opsz, a, mem, n, mcar (n, lst)) → mem-lst (opsz, a, mem, n − 1, mcar (n − 1, lst))

Theorem: mem-lst-mcar-2 (mem-lst (opsz, a, mem, n, mcar (n, lst)) ∧ (k ≤ n)) → mem-lst (opsz, a, mem, n − k, mcar (n − k, lst))

Theorem: plus-difference (m + (n − m)) = if n < m then fix (m)

else fix (n) endif

Theorem: mem-lst-len mem-lst (opsz, a, mem, n, lst) → (n ≮ len (lst))

Theorem: mem-lst-mcdr (mem-lst (opsz, a, mem, n, lst) ∧ (i = (opsz ∗ m))) → mem-lst (opsz, add (32, a, i), mem, n − m, mcdr (m, lst))

Theorem: mem-lst-mcdr-0 mem-lst (opsz, a, mem, n, lst) → mem-lst (opsz, add (32, a, opsz), mem, n − 1, mcdr (1, lst))

Theorem: mem-lst-mcdr-uint (mem-lst (opsz, a, mem, n, lst) ∧ (nat-to-uint (i) = (opsz ∗ m)) ∧ (opsz ≄ 0)) → mem-lst (opsz, add (32, a, i), mem, n − m, mcdr (m, lst))

Theorem: mem-lst-mcdr-1 mem-lst (1, add (32, x, i), mem, n − j , mcdr (k, lst)) → mem-lst (1, add (32, x, add (32, i, 1)), mem, (n − 1) − j , mcdr (1 + k, lst))

Theorem: mem-lst-mcdr-uint-1 (mem-lst (opsz, add (32, a, b), mem, n − j , mcdr (k, lst)) ∧ (nat-to-uint (i) = (opsz ∗ m)) ∧ (opsz ≄ 0)) → mem-lst (opsz,

add (32, a, add (32, b, i)), mem, n − (m + j ), mcdr (m + k, lst))

Event: Disable mem-lst-len.

Event: Disable plus-difference.

;                 LSTCPY AND LSTMCPY

Definition: lstcpy (i1 , lst1 , i2 , lst2 , n) = if n ≃ 0 then lst1

else lstcpy (1 + i1 , put-nth (get-nth (i2 , lst2 ), i1 , lst1 ), 1 + i2 , lst2 , n − 1) endif

Theorem: lstcpy-0 lstcpy (i1 , lst1 , i2 , lst2 , 0) = lst1

Theorem: lstcpy-lstcpy ((j1 = (h1 + i1 )) ∧ (j2 = (h1 + i2 ))) → (lstcpy (j1 , lstcpy (i1 , lst1 , i2 , lst2 , h1 ), j2 , lst2 , h2 )

= lstcpy (i1 , lst1 , i2 , lst2 , h1 + h2 ))

Definition: lstmcpy (opsz, i1 , lst1 , i2 , lst2 , n) = if n ≃ 0 then lst1

else lstmcpy (opsz, opsz + i1 , lstcpy (i1 , lst1 , i2 , lst2 , opsz), opsz + i2 , lst2 , n − 1) endif Theorem: lstmcpy-cpy lstmcpy (h, i1 , lst1 , i2 , lst2 , n) = lstcpy (i1 , lst1 , i2 , lst2 , h ∗ n)

Theorem: put-commutativity (j < i) → (put-nth (v1 , i, put-nth (v2 , j , lst)) = put-nth (v2 , j , put-nth (v1 , i, lst)))

Theorem: lstcpy-put-nth (i < j1 ) → (put-nth (v, i, lstcpy (j1 , lst1 , j2 , lst2 , n))

= lstcpy (j1 , put-nth (v, i, lst1 ), j2 , lst2 , n))

; a variant for lstcpy.

Definition: lstcpy1 (i1 , lst1 , i2 , lst2 , n) = if n ≃ 0 then lst1

else lstcpy1 (i1 ,

put-nth (get-nth (i2 + (n − 1), lst2 ), i1 + (n − 1), lst1 ),

i2 , lst2 , n − 1) endif

Theorem: lstcpy-add1 lstcpy (i1 , put-nth (get-nth (i2 + h, lst2 ), i1 + h, lst1 ), i2 , lst2 , h) = lstcpy (i1 , lst1 , i2 , lst2 , 1 + h)

Theorem: lstcpy-cpy1 lstcpy (i1 , lst1 , i2 , lst2 , n) = lstcpy1 (i1 , lst1 , i2 , lst2 , n)

Theorem: put-get-lst-is-cpy mem-lst (opsz, x, mem, n2 , lst2 ) → (put-lst (opsz, get-lst (opsz, i2 , lst2 , n), i1 , lst1 , n)

= lstcpy (i1 , lst1 , i2 , lst2 , n))

Theorem: put-get-vals-is-cpy put-vals (get-vals (i2 , lst2 , n), i1 , lst1 , n) = lstcpy (i1 , lst1 , i2 , lst2 , n)

Event: Disable lstcpy-cpy1.

;            MMOV1-LST, MMOV-LST1, MMOVN-LST AND MMOVN-LST1

Definition: mmov1-lst (i, lst1 , lst2 , n) = if n ≃ 0 then lst1

else mmov1-lst (1 + i, put-nth (get-nth (i, lst2 ), i, lst1 ), lst2 , n − 1) endif

; the same as mov1-lst.

Definition: mmov1-lst1 (i, lst1 , lst2 , n) = if n ≃ 0 then lst1

else mmov1-lst1 (i − 1, put-nth (get-nth (i − 1, lst2 ), i − 1, lst1 ), lst2 , n − 1) endif

Definition: movn-lst (n, lst1 , lst2 , i) = put-vals (get-vals (i, lst2 , n), i, lst1 , n)

Definition: mmovn-lst (h, lst1 , lst2 , i, nt) = if nt ≃ 0 then lst1

else mmovn-lst (h, movn-lst (h, lst1 , lst2 , i), lst2 , h + i, nt − 1) endif

Definition: mmovn-lst1 (h, lst1 , lst2 , i, nt) = if nt ≃ 0 then lst1

else mmovn-lst1 (h, movn-lst (h, lst1 , lst2 , i − h), lst2 , i − h, nt − 1) endif

Theorem: mmov1-lst-0 mmov1-lst (i, lst1 , lst2 , 0) = lst1

Theorem: mmov1-lst1-0 mmov1-lst1 (i, lst1 , lst2 , 0) = lst1

Theorem: mmovn-lst-0 mmovn-lst (n, lst1 , lst2 , i, 0) = lst1

Theorem: mmovn-lst1-0 mmovn-lst1 (n, lst1 , lst2 , i, 0) = lst1

;                     MOD32-EQ

Theorem: mod32-eq-deduction0 mod32-eq (x, x)

Theorem: mod32-eq-deduction1 (mod32-eq (0, neg (32, x)) = mod32-eq (x, 0)) ∧ (mod32-eq (neg (32, x), 0) = mod32-eq (x, 0))

Theorem: mod32-eq-deduction2 (mod32-eq (x, add (32, x, y)) = mod32-eq (0, y)) ∧ (mod32-eq (add (32, x, y), x) = mod32-eq (y, 0))

Theorem: mod32-eq-deduction3 mod32-eq (add (32, x, y), add (32, x, z)) = mod32-eq (y, z)

Event: Disable mod32-eq.

; generate all the cases from between-ileq.

Theorem: between-ileq-la (integerp (x) ∧ integerp (y) ∧ integerp (z)) → (between-ileq (x, y, z)

= if ilessp (z, x) then f else (x = y) ∨ between-ileq (iplus (x, 1), y, z) endif)

Event: Disable between-ileq.

; readm-mem, mem-lst, and mem-ilst is not changed if read-mem is not
; changed.

Theorem: read-mem-plus read-mem (addr, mem, m + k) = app (8 ∗ k, read-mem (add (32, addr, m), mem, k), read-mem (addr, mem, m))

Theorem: stepn-readm-mem (read-mem (x, mc-mem (stepn (s, n)), opsz ∗ k) = read-mem (x, mc-mem (s), opsz ∗ k)) → (readm-mem (opsz, x, mc-mem (stepn (s, n)), k)

= readm-mem (opsz, x, mc-mem (s), k))

Theorem: stepn-mem-lst (readm-mem (opsz, x, mc-mem (stepn (s, n)), k) = readm-mem (opsz, x, mc-mem (s), k)) → (mem-lst (opsz, x, mc-mem (stepn (s, n)), k, lst)

= mem-lst (opsz, x, mc-mem (s), k, lst))

Theorem: stepn-mem-ilst (readm-mem (opsz, x, mc-mem (stepn (s, n)), k) = readm-mem (opsz, x, mc-mem (s), k)) → (mem-ilst (opsz, x, mc-mem (stepn (s, n)), k, lst)

= mem-ilst (opsz, x, mc-mem (s), k, lst)) Event: Disable read-mem-plus.

;                   DISABLE EVENTS
; many events are no longer useful upon the completion of this system.
; before we enter the verification phase, we simply disable them.
;;;;;;;; disable arithmetic events.

Event: Disable plus-add1-1. Event: Disable remainder-exit. Event: Disable quotient-exit.

;;;;;;; disable definitions in the specification.
; operations:  The semantics of these operations has been established as
; rewrite rules in the library, which will be triggered to apply when
; nat-to-uint or nat-to-int are presented.

Event: Disable mulu. Event: Disable muls. Event: Disable quot. Event: Disable rem. Event: Disable iquot. Event: Disable irem. Event: Disable lsl. Event: Disable lsr.

Event: Disable asl. Event: Disable asr.

; condition codes:  To avoid to open up these flag definitions is one of the
; several efforts to keep the proving space managable.  Another point is
; that one flag might have different semantics in different situations.

Event: Disable fix-bit. Event: Disable add-v. Event: Disable add-z. Event: Disable add-n. Event: Disable addx-v. Event: Disable addx-z. Event: Disable addx-n. Event: Disable sub-v. Event: Disable sub-n. Event: Disable subx-v. Event: Disable subx-z. Event: Disable subx-n. Event: Disable and-z. Event: Disable and-n.

Event: Disable mulu-v. Event: Disable mulu-z. Event: Disable mulu-n. Event: Disable muls-v. Event: Disable muls-z. Event: Disable muls-n. Event: Disable or-z. Event: Disable or-n. Event: Disable divs-z. Event: Disable divs-n. Event: Disable divu-z. Event: Disable divu-n. Event: Disable rol-c. Event: Disable rol-z. Event: Disable rol-n. Event: Disable ror-c. Event: Disable ror-z. Event: Disable ror-n.

Event: Disable lsl-c. Event: Disable lsl-z. Event: Disable lsl-n. Event: Disable lsr-c. Event: Disable lsr-z. Event: Disable lsr-n. Event: Disable asl-c. Event: Disable asl-v. Event: Disable asl-z. Event: Disable asl-n. Event: Disable asr-c. Event: Disable asr-z. Event: Disable asr-n. Event: Disable roxl-c. Event: Disable roxl-z. Event: Disable roxl-n. Event: Disable roxr-c. Event: Disable roxr-z.

Event: Disable roxr-n. Event: Disable move-z. Event: Disable move-n. Event: Disable ext-z. Event: Disable ext-n. Event: Disable swap-z. Event: Disable swap-n. Event: Disable not-z. Event: Disable not-n. Event: Disable eor-z. Event: Disable eor-n.

; read/write defns:  for each of them, we have had a set of rewrite rules.
; their definitions are not needed to open up.

Event: Disable pc-read-memp. Event: Disable pc-read-mem. Event: Disable read-memp. Event: Disable read-mem. Event: Disable write-memp. Event: Disable write-mem.

Event: Disable readm-rn. Event: Disable writem-rn.

;;;;;;;; disable intermediate lemmas for read/write events:  to prove
; some important theorems about read/write,  we proved many intermediate
; lemmas.  It is time to discard them.

Event: Disable pc-read-memp-la0. Event: Disable pc-read-memp-la1. Event: Disable pc-read-memp-la2. Event: Disable pc-read-memp-la3. Event: Disable write-memp-la0. Event: Disable write-memp-la1. Event: Disable write-memp-la2. Event: Disable write-memp-la3.

;;;;;;;; disable intermediate lemmas for disjoint0/disjoint events.

Event: Disable disjoint0. Event: Disable disjoint. Event: Disable disjoint0-la0. Event: Disable disjoint0-la1. Event: Disable disjoint0-la2. Event: Disable disjoint-la0.

Event: Disable disjoint-la1.

Event: Disable disjoint-la2.

Event: Disable disjoint-la3.

;;;;;;;; disable intermediate lemmas for add/sub/neg events.

Event: Disable add-non-numberp.

Event: Disable add-commutativity.

Event: Disable add-commutativity1.

;;;;;;;;  disable mapping functions.

Event: Disable nat-to-uint.

Event: Disable uint-to-nat.

;;;;;;;;  disable miscellaneous lemmas.

Event: Disable stepn.

; addressing mode checking for each instruction.  Their arguments are
; always "concrete" values.  For all the instructions, the oplen and ins
; have to become known at the execution time.  Theoretically,  it would
; be nice to disable them.  But we do not want disabling to slow down
; the prover.  Therefore, we only disable them when we feel necessary.

Event: Let us define the theory mode-guards to consist of the following events: add-addr-modep1, add-addr-modep2, adda-addr-modep, sub-addr-modep1, subaddr-modep2, suba-addr-modep, and-addr-modep1, and-addr-modep2, mul&divaddr-modep, or-addr-modep1, or-addr-modep2, s&r-addr-modep, move-addr-modep, movea-addr-modep, lea-addr-modep, clr-addr-modep, move-from-ccr-addr-modep, negx-addr-modep, neg-addr-modep, move-to-ccr-addr-modep, peaaddr-modep, movem-rn-ea-addr-modep, movem-ea-rn-addr-modep, tst-addr-modep, tas-addr-modep, jmp-addr-modep, jsr-addr-modep, not-addr-modep, scc-addr-modep, addq-addr-modep, subq-addr-modep, cmp-addr-modep, cmpa-addr-modep, eor&eori-addr-modep, bchg-addr-modep, bclr-addr-modep, bset-addr-modep, btst-addr-modep, ori-addr-modep, andi-addr-modep, subi-addr-modep, addiaddr-modep, cmpi-addr-modep.

; the classification of instructions, according to the opcode.

Event: Let us define the theory groups to consist of the following events: bit-group, move-ins, move-group, misc-group, scc-group, bcc-group, or-group, sub-group, cmp-group, and-group, add-group, s&r-group.

;             INVARIANTS OF THE SPEC

Conservative Axiom: h-invariant (p (x, write-mem (value, y, mem, m), k) = p (x, mem, k)) ∧ ((p (x, mem, k) ∧ write-memp (y, mem, m))

→ (h (x, write-mem (value, y, mem, m), k) = h (x, mem, k)))

Simultaneously, we introduce the new function symbols p and h.

Theorem: addr-index2-mem mc-mem (car (addr-index2 (pc, addr, indexwd, s))) = mc-mem (s)

Theorem: immediate-mem mc-mem (car (immediate (oplen, pc, s))) = mc-mem (s)

Theorem: effec-addr-mem mc-mem (car (effec-addr (oplen, mode, rn, s))) = mc-mem (s)

Theorem: mc-instate-mem mc-mem (car (mc-instate (oplen, ins, s))) = mc-mem (s)

Theorem: mapping-h p (x, mc-mem (car (s&addr)), k) → (h (x, mc-mem (mapping (oplen, v&cvznx, s&addr)), k)

= h (x, mc-mem (car (s&addr)), k))

Definition: t3 (x, y, z) = t

; add-group.

Theorem: add-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (add-group (opmode, ins, s)), k) = h (x, mc-mem (s), k))

; sub-group.

Theorem: sub-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (sub-group (opmode, ins, s)), k) = h (x, mc-mem (s), k))

; and-group.

Theorem: and-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (and-group (oplen, ins, s)), k) = h (x, mc-mem (s), k))

; or-group.

Theorem: or-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (or-group (oplen, ins, s)), k) = h (x, mc-mem (s), k))

; scc-group.

Theorem: scc-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (scc-group (ins, s)), k) = h (x, mc-mem (s), k))

; cmp-group.

Theorem: cmp-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (cmp-group (oplen, ins, s)), k) = h (x, mc-mem (s), k))

; bcc-group.

Theorem: bcc-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (bcc-group (disp, ins, s)), k) = h (x, mc-mem (s), k))

; bit-group.

Theorem: write-mem-maintain-movep-writep movep-writep (addr, write-mem (value, x, mem, m), n) = movep-writep (addr, mem, n)

Theorem: movep-write-h (p (x, mem, k) ∧ movep-writep (addr, mem, n)) → (h (x, movep-write (value, addr, mem, n), k) = h (x, mem, k))

Theorem: bit-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (bit-group (ins, s)), k) = h (x, mc-mem (s), k))

; move-group.

Theorem: move-h p (x, mc-mem (s), k) → (h (x, mc-mem (move-ins (oplen, ins, s)), k) = h (x, mc-mem (s), k))

Theorem: move-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (move-group (oplen, ins, s)), k) = h (x, mc-mem (s), k))

; s&r-group.

Theorem: s&r-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (s&r-group (ins, s)), k) = h (x, mc-mem (s), k))

; misc-group.

Theorem: writem-mem-h (p (x, mem, k) ∧ write-memp (addr, mem, opsz ∗ len (vlst))) → (h (x, writem-mem (opsz, vlst, addr, mem), k) = h (x, mem, k))

Theorem: movem-rnlst-len len (movem-rnlst (mask, i)) = movem-len (mask)

Theorem: movem-pre-rnlst-len len (movem-pre-rnlst (mask, i, lst)) = (movem-len (mask) + len (lst))

Theorem: misc-group-h p (x, mc-mem (s), k) → (h (x, mc-mem (misc-group (ins, s)), k) = h (x, mc-mem (s), k))

Theorem: stepi-h p (x, mc-mem (s), k) → (h (x, mc-mem (stepi (s)), k) = h (x, mc-mem (s), k))

Theorem: stepi-p t3 (x, mc-mem (s), k) → (p (x, mc-mem (stepi (s)), k) = p (x, mc-mem (s), k))

Theorem: stepn-h p (x, mc-mem (s), k) → (h (x, mc-mem (stepn (s, n)), k) = h (x, mc-mem (s), k))

; the instantiations.

Theorem: stepn-pc-read-memp t3 (x, mc-mem (s), k) → (pc-read-memp (x, mc-mem (stepn (s, n)), k) = pc-read-memp (x, mc-mem (s), k))

Theorem: stepn-read-memp t3 (x, mc-mem (s), k) → (read-memp (x, mc-mem (stepn (s, n)), k) = read-memp (x, mc-mem (s), k))

Theorem: stepn-write-memp t3 (x, mc-mem (s), k) → (write-memp (x, mc-mem (stepn (s, n)), k) = write-memp (x, mc-mem (s), k))

; after the execution of n arbitrary instructions, ROM is still ROM.

Theorem: stepn-rom-addrp rom-addrp (x, mc-mem (stepn (s, n)), k) = rom-addrp (x, mc-mem (s), k)

; after the execution of n arbitrary instructions, RAM is still RAM.

Theorem: stepn-ram-addrp ram-addrp (x, mc-mem (stepn (s, n)), k) = ram-addrp (x, mc-mem (s), k)

; after the execution of n arbitrary instructions, the contents of
; the memory are not modified if that portion of the memory is ROM.

Theorem: stepn-pc-read-mem rom-addrp (x, mc-mem (s), k) → (pc-read-mem (x, mc-mem (stepn (s, n)), k) = pc-read-mem (x, mc-mem (s), k))

Theorem: stepn-read-mem rom-addrp (x, mc-mem (s), k) → (read-mem (x, mc-mem (stepn (s, n)), k) = read-mem (x, mc-mem (s), k))

; after the execution of n arbitrary instructions, the program segment
; maintains the same.  Since we always require programs in ROM.

Theorem: stepn-mcode-addrp rom-addrp (x, mc-mem (s), len (lst)) → (mcode-addrp (x, mc-mem (stepn (s, n)), lst)

= mcode-addrp (x, mc-mem (s), lst))

Event: Disable splus.

Event: Disable mcode-addrp.

; end of the proving phase. ****************
;-------------------------------------------------------------------------
;                  VERIFICATION PHASE
;-------------------------------------------------------------------------
; our goal is to verify programs at machine code level. Before we go to
; specific programs, we introduce some conventions of machine code program
; constructs.  This section provides some useful concepts for us to specify
; and verify machine code programs.
;
; look up as unsigned integers.

Definition: uread-mem (x, mem, n) = nat-to-uint (read-mem (x, mem, n)) Definition: uread-dn (oplen, dn, s) = nat-to-uint (read-dn (oplen, dn, s)) Definition: uread-an (oplen, an, s) = nat-to-uint (read-an (oplen, an, s))

; look up as signed integers.

Definition: iread-mem (x, mem, n) = nat-to-int (read-mem (x, mem, n), 8 ∗ n) Definition: iread-dn (oplen, dn, s) = nat-to-int (read-dn (oplen, dn, s), oplen) Definition: iread-an (oplen, an, s) = nat-to-int (read-an (oplen, an, s), oplen)

; the return address of subroutine call.

Definition: rts-addr (s) = read-mem (read-an (32, 7, s), mc-mem (s), 4) Definition: linked-rts-addr (s) = read-mem (add (32, read-an (32, 6, s), 4), mc-mem (s), 4)

; the saved A6 on the stack.

Definition: linked-a6 (s) = read-mem (read-an (32, 6, s), mc-mem (s), 4)

; for MOVEM instruction.  After the link, A6 points to some place
; on the stack.  s is the current machine state, opsz is the
; operation size of the MOVEM,  i is the offset relative to a6,
; and n is the number of registers moved.

Definition: movem-saved (s, opsz, i, n) = readm-mem (opsz, sub (32, i, read-an (32, 6, s)), mc-mem (s), n)

; when only one register is saved,  we use MOVE instead of MOVEM.

Definition: rn-saved (s) = read-mem (sub (32, 4, read-an (32, 6, s)), mc-mem (s), 4)

; We do not want to deal with nat-to-int and int-to-nat in the logic
; level.  In the logic level, the proof concerns purely the algorithmic
; correctness in the problem.  It is hoped to be machine independent.

Definition: lst-int (n, lst) = if lst ≃ nil then lst

else cons (nat-to-int (car (lst), n), lst-int (n, cdr (lst))) endif

Theorem: get-lst-int get-nth (i, lst-int (n, lst)) = nat-to-int (get-nth (i, lst), n)

Theorem: put-lst-int put-nth (nat-to-int (value, n), i, lst-int (n, lst)) = lst-int (n, put-nth (value, i, lst))

Definition: lst-integerp (lst) = if lst ≃ nil then t

else integerp (car (lst)) ∧ lst-integerp (cdr (lst)) endif

Theorem: get-lst-integerp lst-integerp (lst) → integerp (get-nth (n, lst))

Theorem: mem-lst-integerp (mem-lst (opsz, a, mem, n, lst) ∧ (oplen = (8 ∗ opsz))) → lst-integerp (lst-int (oplen, lst))

Theorem: mem-ilst-lst-integerp mem-ilst (opsz, a, mem, n, lst) → lst-integerp (lst)

Event: Disable mem-lst.

Event: Disable mem-ilst.

; a trick to get all the appearances of a term replaced by another
; term. For example, in subroutines, a6 is used as the addresss register
; for LINK. It is often relative to sp(a7).  We'd like to have a6
; replaced by a7.

Definition: equal* (x, y) = (x = y)

Theorem: equal*-reflex equal* (x, x)

Theorem: read-rn-equal* equal* (read-rn (oplen, rn, rfile), x) → (read-rn (oplen, rn, rfile) = x)

Event: Disable equal*.

; the registers d0, d1, a0, and a1 are available for any subroutines.
; There is no obligation for subroutines to restore their previous values.
; Therefore, we do not need to keep track of them.  We handle a7
; (the stack pointer) separately to make sure it is set correctly.
; a6 (the frame pointer) perhaps also deserves special treatment.

Definition: d2-7a2-5p (rn) = ((rn ≄ 0)

∧ (rn ≠ 1)

∧ (rn ≠ 8)
∧ (rn ≠ 9)
∧ (rn ≠ 14)
∧ (rn ≠ 15))

; d2 will be used for some purpose.

Definition: d3-7a2-5p (rn) = (d2-7a2-5p (rn) ∧ (rn ≠ 2))

; d2 and d3 will be used for some purpose.

Definition: d4-7a2-5p (rn) = (d2-7a2-5p (rn) ∧ (rn ≠ 2) ∧ (rn ≠ 3))

; d2, d3, and d4 will be used for some purpose.

Definition: d5-7a2-5p (rn) = (d2-7a2-5p (rn) ∧ (rn ≠ 2) ∧ (rn ≠ 3) ∧ (rn ≠ 4))

; a2 will be used for some purpose.

Definition: d2-7a3-5p (rn) = (d2-7a2-5p (rn) ∧ (rn ≠ 10))

Definition: d4-7a4-5p (rn) = (d4-7a2-5p (rn) ∧ (rn ≠ 10) ∧ (rn ≠ 11))

Definition: d4-7a5p (rn) = (d4-7a2-5p (rn) ∧ (rn ≠ 10) ∧ (rn ≠ 11) ∧ (rn ≠ 12))

Definition: d5-7a4-5p (rn) = (d4-7a2-5p (rn) ∧ (rn ≠ 4) ∧ (rn ≠ 10) ∧ (rn ≠ 11))

Definition: d6-7a2-5p (rn) = (d4-7a2-5p (rn) ∧ (rn ≠ 4) ∧ (rn ≠ 5))

; something I don't know where to put yet.
; the mean (i+j)/2 < j iff i < j.

Theorem: mean-lessp-lemma ((i + j ) < (2 ∗ j )) = (i < j )

Theorem: mean-lessp ((((i + j ) ÷ 2) < j ) = (i < j )) ∧ ((((j + i) ÷ 2) < j ) = (i < j ))

; swap the ith and jth elements of the list.

Definition: swap (i, j , lst) = put-nth (get-nth (i, lst), j , put-nth (get-nth (j , lst), i, lst))

Theorem: get-swap get-nth (k, swap (i, j , lst)) = if fix (k) = fix (i) then get-nth (j , lst)

elseif fix (k) = fix (j ) then get-nth (i, lst) else get-nth (k, lst) endif

Event: Disable get-nth.

Event: Disable put-nth.

; C conventions.

Definition: null = 0

Definition: eof = -1

; the Nqthm counterparts of the Berkeley C string functions.
; memchr.

Definition: memchr1 (i, n, lst, ch) = if get-nth (i, lst) = ch then fix (i)

elseif (n − 1) = 0 then f

else memchr1 (1 + i, n − 1, lst, ch) endif Definition: memchr (n, lst, ch) = if n = 0 then f

else memchr1 (0, n, lst, ch) endif

; memcmp.

Definition: memcmp1 (i, n, lst1 , lst2 ) = if get-nth (i, lst1 ) = get-nth (i, lst2 )

then if (n − 1) = 0 then 0

else memcmp1 (1 + i, n − 1, lst1 , lst2 ) endif else idifference (get-nth (i, lst1 ), get-nth (i, lst2 )) endif

Definition: memcmp (n, lst1 , lst2 ) = if n = 0 then 0

else memcmp1 (0, n, lst1 , lst2 ) endif

; memset.

Definition: memset1 (i, n, lst, ch) = if (n − 1) = 0 then put-nth (ch, i, lst)

else memset1 (1 + i, n − 1, put-nth (ch, i, lst), ch) endif

Definition: memset (n, lst, ch) = if n = 0 then lst

else memset1 (0, n, lst, ch) endif

; strlen.

Definition: strlen (i, n, lst) = if i < n

then if get-nth (i, lst) = null then i else strlen (1 + i, n, lst) endif

else i endif

; strcpy.

Definition: strcpy (i, lst1 , n2 , lst2 ) = if i < n2

then if get-nth (i, lst2 ) = null then put-nth (null, i, lst1 )

else strcpy (1 + i, put-nth (get-nth (i, lst2 ), i, lst1 ), n2 , lst2 ) endif else lst1 endif

; strcmp.

Definition: strcmp (i, n1 , lst1 , lst2 ) = if i < n1

then if get-nth (i, lst1 ) = get-nth (i, lst2 )

then if get-nth (i, lst1 ) = null then 0

else strcmp (1 + i, n1 , lst1 , lst2 ) endif else idifference (get-nth (i, lst1 ), get-nth (i, lst2 )) endif

else 0 endif

; strcoll.

Definition: strcoll (n1 , lst1 , lst2 ) = strcmp (0, n1 , lst1 , lst2 )

; strcat.

Definition: strcpy1 (i, lst1 , j , n2 , lst2 ) = if j < n2

then if get-nth (j , lst2 ) = null then put-nth (null, i, lst1 )

else strcpy1 (1 + i, put-nth (get-nth (j , lst2 ), i, lst1 ), 1 + j , n2 , lst2 ) endif

else lst1 endif

Definition: strcat (n1 , lst1 , n2 , lst2 ) = if get-nth (0, lst1 ) = null then strcpy1 (0, lst1 , 0, n2 , lst2 )

else strcpy1 (strlen (1, n1 , lst1 ), lst1 , 0, n2 , lst2 ) endif

; strncat.

Definition: strcpy2 (i, lst1 , j , n, lst2 ) = if get-nth (j , lst2 ) = null then put-nth (null, i, lst1 )

elseif (n − 1) = 0

then put-nth (null, 1 + i, put-nth (get-nth (j , lst2 ), i, lst1 )) else strcpy2 (1 + i,

put-nth (get-nth (j , lst2 ), i, lst1 ), 1 + j , n − 1, lst2 ) endif Definition: strncat (n1 , lst1 , n, lst2 ) = if n = 0 then lst1

elseif get-nth (0, lst1 ) = null then strcpy2 (0, lst1 , 0, n, lst2 )

else strcpy2 (strlen (1, n1 , lst1 ), lst1 , 0, n, lst2 ) endif

; strncmp.

Definition: strncmp1 (i, n, lst1 , lst2 ) = if get-nth (i, lst1 ) = get-nth (i, lst2 )

then if get-nth (i, lst1 ) = 0 then 0 elseif (n − 1) = 0 then 0 else strncmp1 (1 + i, n − 1, lst1 , lst2 ) endif else idifference (get-nth (i, lst1 ), get-nth (i, lst2 )) endif

Definition: strncmp (n, lst1 , lst2 ) = if n ≃ 0 then 0

else strncmp1 (0, n, lst1 , lst2 ) endif

; strncpy.

Definition: zero-list1 (i, n, lst) = if (n − 1) = 0 then lst

else zero-list1 (1 + i, n − 1, put-nth (0, i, lst)) endif

Definition: zero-list (i, n, lst) = zero-list1 (1 + i, n, put-nth (0, i, lst))

Definition: strncpy1 (i, n, lst1 , lst2 ) = if get-nth (i, lst2 ) = 0 then zero-list (i, n, lst1 )

elseif (n − 1) = 0 then put-nth (get-nth (i, lst2 ), i, lst1 )

else strncpy1 (1 + i, n − 1, put-nth (get-nth (i, lst2 ), i, lst1 ), lst2 ) endif

Definition: strncpy (n, lst1 , lst2 ) = if n ≃ 0 then lst1

else strncpy1 (0, n, lst1 , lst2 ) endif

; strchr.

Definition: strchr (i, n, lst, ch) = if i < n

then if get-nth (i, lst) = ch then fix (i) elseif get-nth (i, lst) = 0 then f else strchr (1 + i, n, lst, ch) endif

else f endif

; strcspn.

Definition: strcspn (i1 , n1 , lst1 , n2 , lst2 ) = if i1 < n1

then if strchr (0, n2 , lst2 , get-nth (i1 , lst1 )) then fix (i1 ) else strcspn (1 + i1 , n1 , lst1 , n2 , lst2 ) endif

else f endif

; strrchr.

Definition: strrchr (i, n, lst, ch, j ) = if i < n

then if get-nth (i, lst) = ch

then if get-nth (i, lst) = 0 then fix (i)

else strrchr (1 + i, n, lst, ch, fix (i)) endif elseif get-nth (i, lst) = 0 then j else strrchr (1 + i, n, lst, ch, j ) endif

else j endif

; strspn.

Definition: strchr1 (i, n, lst, ch) = if i < n

then if get-nth (i, lst) = 0 then f elseif get-nth (i, lst) = ch then fix (i) else strchr1 (1 + i, n, lst, ch) endif

else f endif

Theorem: strchr1-bounds (n ≮ strchr1 (i, n, lst, ch)) ∧ (strchr1 (i, n, lst, ch) → (strchr1 (i, n, lst, ch) ≮ i))

Theorem: strchr1-false-0 ¬ strchr1 (i, n, lst, 0)

Definition: strspn (i1 , n1 , lst1 , n2 , lst2 ) = if i1 < n1

then if strchr1 (0, n2 , lst2 , get-nth (i1 , lst1 )) then strspn (1 + i1 , n1 , lst1 , n2 , lst2 ) else fix (i1 ) endif

else f endif

; strpbrk.

Definition: strpbrk (i1 , n1 , lst1 , n2 , lst2 ) = if i1 < n1

then if get-nth (i1 , lst1 ) = 0 then f elseif strchr1 (0, n2 , lst2 , get-nth (i1 , lst1 )) then fix (i1 ) else strpbrk (1 + i1 , n1 , lst1 , n2 , lst2 ) endif

else f endif

; strstr.

Definition: strstr1 (i, n1 , lst1 , n2 , lst2 , len) = if i < n1

then let j be strchr1 (i, n1 , lst1 , get-nth (0, lst2 ))

in

if j ∈ N

then if strncmp (len, mcdr (1 + j , lst1 ), mcdr (1, lst2 ))

= 0 then j else strstr1 (1 + j , n1 , lst1 , n2 , lst2 , len) endif

else f endif endlet else f endif

Definition: strstr (n1 , lst1 , n2 , lst2 ) = if get-nth (0, lst2 ) = 0 then 0

else strstr1 (0, n1 , lst1 , n2 , lst2 , strlen (0, n2 − 1, mcdr (1, lst2 ))) endif

; memmove.

Definition: memmove-1 (lst1 , lst2 , i, nt, n) = if (n mod 4) = 0 then mmovn-lst (4, lst1 , lst2 , i, nt)

else mmov1-lst (i + (4 ∗ nt), mmovn-lst (4, lst1 , lst2 , i, nt), lst2 , n mod 4) endif Definition: memmove-0 (lst1 , lst2 , i, nt, n) = if n < 4 then mmov1-lst (i + nt, mmov1-lst (i, lst1 , lst2 , nt), lst2 , n)

else memmove-1 (mmov1-lst (i, lst1 , lst2 , nt), lst2 , i + nt, n ÷ 4,

n) endif

Definition: memmove-4 (lst1 , lst2 , i, nt, n) = if (n mod 4) = 0 then mmovn-lst1 (4, lst1 , lst2 , i, nt)

else mmov1-lst1 (i − (4 ∗ nt), mmovn-lst1 (4, lst1 , lst2 , i, nt), lst2 , n mod 4) endif

Definition: memmove-3 (lst1 , lst2 , i, nt, n) = if n < 4

then mmov1-lst1 (i − nt, mmov1-lst1 (i, lst1 , lst2 , nt), lst2 , n)

else memmove-4 (mmov1-lst1 (i, lst1 , lst2 , nt), lst2 , i − nt, n ÷ 4,

n) endif

Definition: memmove (str1 , str2 , n, lst1 , lst2 ) = if n ≃ 0 then lst1

elseif nat-to-uint (str1 ) = nat-to-uint (str2 ) then lst2 else let x1 be nat-to-uint (str1 ),

x2 be nat-to-uint (str2 ) in if x1 < x2 then if ((x1 mod 4) = 0)

∧ ((x2 mod 4) = 0) then if n < 4 then mmov1-lst (0, lst1 , lst2 , n)

else memmove-1 (lst1 , lst2 ,

                                 0,

n ÷ 4,

n) endif

elseif ((x1 mod 4) = (x2 mod 4))

∧ (3 < n) then memmove-0 (lst1 ,

lst2 ,

                 0,

4 − (x1 mod 4),

(n + (x1 mod 4)) − 4)

else memmove-0 (lst1 , lst2 , 0, n, 0) endif else let y1 be n + x1 ,

y2 be n + x2 in if ((y1 mod 4) = 0)

∧ ((y2 mod 4) = 0) then if n < 4

then mmov1-lst1 (n, lst1 , lst2 , n)

else memmove-4 (lst1 , lst2 , n, n ÷ 4,

n) endif

elseif ((y1 mod 4)

= (y2 mod 4)) ∧ (4 < n)

then memmove-3 (lst1 , lst2 , n, y1 mod 4, n − (y1 mod 4))

else memmove-3 (lst1 , lst2 , n, n,

0) endif endlet endif endlet endif

; dual events of string functions.  They are for internal use only and
; hardly visible for users.

Definition: strlen* (i* , i, n, lst) = if i < n

then if get-nth (i, lst) = null then i*

else strlen* (add (32, i* , 1), 1 + i, n, lst) endif else i* endif Definition: memchr* (i* , i, n, lst, ch) = if get-nth (i, lst) = ch then i*

elseif (n − 1) = 0 then f

else memchr* (add (32, i* , 1), 1 + i, n − 1, lst, ch) endif

Definition: strchr* (i* , i, n, lst, ch) = if i < n

then if get-nth (i, lst) = ch then i* elseif get-nth (i, lst) = 0 then f else strchr* (add (32, i* , 1), 1 + i, n, lst, ch) endif

else f endif

Definition: strchr1* (i* , i, n, lst, ch) = if i < n

then if get-nth (i, lst) = 0 then f elseif get-nth (i, lst) = ch then i* else strchr1* (add (32, i* , 1), 1 + i, n, lst, ch) endif

else f endif

Definition: strcspn* (i1* , i1 , n1 , lst1 , n2 , lst2 ) = if i1 < n1

then if strchr (0, n2 , lst2 , get-nth (i1 , lst1 )) then i1*

else strcspn* (add (32, i1* , 1), 1 + i1 , n1 , lst1 , n2 , lst2 ) endif else f endif

Definition: strrchr* (i* , i, n, lst, ch, j* ) = if i < n

then if get-nth (i, lst) = ch

then if get-nth (i, lst) = 0 then i*

else strrchr* (add (32, i* , 1), 1 + i, n, lst, ch, i* ) endif elseif get-nth (i, lst) = 0 then j* else strrchr* (add (32, i* , 1), 1 + i, n, lst, ch, j* ) endif

else j* endif

Definition: strpbrk* (i1* , i1 , n1 , lst1 , n2 , lst2 ) = if i1 < n1

then if get-nth (i1 , lst1 ) = 0 then f elseif strchr1 (0, n2 , lst2 , get-nth (i1 , lst1 )) then i1* else strpbrk* (add (32, i1* , 1), 1 + i1 , n1 , lst1 , n2 , lst2 ) endif

else f endif Definition: strspn* (i1* , i1 , n1 , lst1 , n2 , lst2 ) = if i1 < n1

then if strchr1 (0, n2 , lst2 , get-nth (i1 , lst1 ))

then strspn* (add (32, i1* , 1), 1 + i1 , n1 , lst1 , n2 , lst2 ) else i1* endif

else f endif

Definition: strstr1* (i* , i, n1 , lst1 , n2 , lst2 , len) = if i < n1

then let j* be strchr1* (i* , i, n1 , lst1 , get-nth (0, lst2 )), j be strchr1 (i, n1 , lst1 , get-nth (0, lst2 ))

in

if j ∈ N

then if strncmp (len, mcdr (1 + j , lst1 ), mcdr (1, lst2 ))

= 0 then j* else strstr1* (add (32, j* , 1), 1 + j , n1 , lst1 , n2 , lst2 , len) endif

else f endif endlet else f endif

Definition: strstr* (n1 , lst1 , n2 , lst2 ) = if get-nth (0, lst2 ) = 0 then 0

else strstr1* (0,

               0,

n1 , lst1 , n2 , lst2 , strlen (0, n2 − 1, mcdr (1, lst2 ))) endif

; strtok.
; the location of the token.

Definition: strtok-tok (str1 , last, n1 , lst1 , n2 , lst2 ) = let i* be strspn* (0, 0, n1 , lst1 , n2 , lst2 ),

i be strspn (0, n1 , lst1 , n2 , lst2 ) in if nat-to-uint (str1 ) = 0 then if nat-to-uint (last) = 0 then 0

elseif get-nth (i, lst1 ) = 0 then 0 else add (32, last, i* ) endif elseif get-nth (i, lst1 ) = 0 then 0 else add (32, str1 , i* ) endif endlet

; the new lst1.

Definition: strtok-lst0 (i1 , lst1 , ch) = if ch = 0 then lst1

else put-nth (0, i1 , lst1 ) endif

Definition: strtok-lst1 (i1 , n1 , lst1 , n2 , lst2 ) = let i be strcspn (i1 , n1 , lst1 , n2 , lst2 )

in

strtok-lst0 (i, lst1 , get-nth (i, lst1 )) endlet

Definition: strtok-lst2 (i1 , n1 , lst1 , n2 , lst2 ) = if get-nth (i1 , lst1 ) = 0 then lst1

else strtok-lst1 (1 + i1 , n1 , lst1 , n2 , lst2 ) endif

Definition: strtok-lst (n1 , lst1 , n2 , lst2 ) = strtok-lst2 (strspn (0, n1 , lst1 , n2 , lst2 ), n1 , lst1 , n2 , lst2 )

; the new value of the static variable.

Definition: strtok-last0 (str1 , i1* , i1 , n1 , lst1 , n2 , lst2 ) = let i* be strcspn* (i1* , i1 , n1 , lst1 , n2 , lst2 ),

i be strcspn (i1 , n1 , lst1 , n2 , lst2 ) in if get-nth (i, lst1 ) = 0 then 0 else add (32, str1 , add (32, i* , 1)) endif endlet

Definition: strtok-last1 (str1 , i1* , i1 , n1 , lst1 , n2 , lst2 ) = if get-nth (i1 , lst1 ) = 0 then 0

else strtok-last0 (str1 , add (32, i1* , 1), 1 + i1 , n1 , lst1 , n2 , lst2 ) endif Definition: strtok-last (str1 , last, n1 , lst1 , n2 , lst2 ) = let i* be strspn* (0, 0, n1 , lst1 , n2 , lst2 ),

i be strspn (0, n1 , lst1 , n2 , lst2 ) in if nat-to-uint (str1 ) = 0 then if nat-to-uint (last) = 0 then last

else strtok-last1 (last, i* , i, n1 , lst1 , n2 , lst2 ) endif else strtok-last1 (str1 , i* , i, n1 , lst1 , n2 , lst2 ) endif endlet

; strxfrm.

Definition: strxfrm1 (i, lst1 , lst2 , n) = if get-nth (i, lst2 ) = 0 then put-nth (0, i, lst1 )

elseif (n − 1) = 0 then put-nth (0, i, lst1 )

else strxfrm1 (1 + i, put-nth (get-nth (i, lst2 ), i, lst1 ), lst2 , n − 1) endif

Definition: strxfrm (lst1 , lst2 , n) = if n ≃ 0 then lst1

else strxfrm1 (0, lst1 , lst2 , n) endif

; a list of characters.

Definition: lst-of-chrp (lst) = if listp (lst)

then (car (lst) ∈ N)

∧ (car (lst) < 256) ∧ lst-of-chrp (cdr (lst))

else t endif

; theorems about lst-of-chrp.

Theorem: get-lst-of-chrp lst-of-chrp (lst) → ((get-nth (i, lst) < 256) ∧ (get-nth (i, lst) ∈ N))

Theorem: put-lst-of-chrp lst-of-chrp (lst) → (lst-of-chrp (put-nth (x, i, lst)) = ((x ∈ N) ∧ (x < 256)))

#|
(prove-lemma lessp-read-mem-1 (rewrite)
     (lessp (read-mem x mem 1) 256)
     ((use (byte-read-nat-rangep (n 8)))

      (enable nat-rangep)))
(prove-lemma mem-lst-of-chrp (rewrite)
     (implies (mem-lst 1 x mem n lst)
              (lst-of-chrp lst))
     ((enable mem-lst)))
|#

Event: Disable lst-of-chrp.

; the predicate stringp.

Definition: slen (i, n, lst) = if i < n

then if get-nth (i, lst) = null then fix (i) else slen (1 + i, n, lst) endif

else fix (i) endif

Definition: stringp (i, n, lst) = (slen (i, n, lst) < n)

; events for slen, which is part of stringp.

Theorem: slen-ubound (i ≤ n) → (n ≮ slen (i, n, lst))

Theorem: slen-lbound slen (i, n, lst) ≮ i

Theorem: slen-01 (slen (i, 0, lst) = fix (i)) ∧ (slen (i, 1, lst)

= if (i < 1) ∧ (get-nth (0, lst) ≠ 0) then 1 else fix (i) endif)

Theorem: slen-add1 slen (i, 1 + i, lst) = if get-nth (i, lst) = 0 then fix (i)

else 1 + i endif

Theorem: slen-put0 slen (i, n, put-nth (0, i, lst)) = fix (i)

Theorem: slen-put (j < i) → (slen (i, n, put-nth (v, j , lst)) = slen (i, n, lst))

Theorem: lessp-slen-mcdr (slen (i + k, n1 , lst1 ) < n1 ) → ((slen (i, n, mcdr (k, lst1 )) < (n1 − k)) = t)

Theorem: lessp-slen-mcdr-0 (slen (1 + i, n1 , lst1 ) < n1 ) → ((slen (i, n, mcdr (1, lst1 )) < (n1 − 1)) = t)

Theorem: slen-rec ((get-nth (i, lst) ≠ 0) ∧ (i < n)) → (slen (1 + i, n, lst) = slen (i, n, lst))

Event: Disable slen.

; theorems about stringp.

Theorem: stringp-la (stringp (i, n, lst) ∧ int-rangep (n, nn) ∧ (get-nth (i, lst) ≠ 0)) → int-rangep (1 + i, nn)

; theorems about strchr.

Theorem: strchr-bounds (n ≮ strchr (i, n, lst, ch)) ∧ (strchr (i, n, lst, ch) → (strchr (i, n, lst, ch) ≮ i))

Theorem: memchr-bounds ((i + n) ≮ memchr1 (i, n, lst, ch)) ∧ (memchr1 (i, n, lst, ch) → (memchr1 (i, n, lst, ch) ≮ i))

Theorem: strpbrk-bounds (n1 ≮ strpbrk (i1 , n1 , lst1 , n2 , lst2 )) ∧ (strpbrk (i1 , n1 , lst1 , n2 , lst2 ) → (strpbrk (i1 , n1 , lst1 , n2 , lst2 ) ≮ i1 ))

Theorem: strrchr-bounds (j ≤ n) → (n ≮ strrchr (i, n, lst, ch, j ))

Theorem: strstr-bounds (n1 ≮ strstr1 (i, n1 , lst1 , n2 , lst2 , len)) ∧ (strstr1 (i, n1 , lst1 , n2 , lst2 , len)

→ (strstr1 (i, n1 , lst1 , n2 , lst2 , len) ≮ i))

Theorem: strspn-ubound (n1 ≄ 0) → (strspn (i, n1 , lst1 , n2 , lst2 ) < n1 )

Theorem: strspn-bounds (n1 ≮ strspn (i, n1 , lst1 , n2 , lst2 )) ∧ (strspn (i, n1 , lst1 , n2 , lst2 ) → (strspn (i, n1 , lst1 , n2 , lst2 ) ≮ i))

Theorem: strcspn-bounds (n1 ≮ strcspn (i, n1 , lst1 , n2 , lst2 )) ∧ (strcspn (i, n1 , lst1 , n2 , lst2 ) → (strcspn (i, n1 , lst1 , n2 , lst2 ) ≮ i))

; a lemma to establish nat-rangep.

Theorem: nat-rangep-la (nat-to-uint (x) < exp (2, n)) → nat-rangep (x, n)

Event: Disable nat-rangep-la.

; some useful lemmas.  I do not know where to put them yet.
; I will put them in the right place.

Theorem: disjoint-1-int (disjoint (a, m, b, n) ∧ (j ≤ m) ∧ ((nat-to-int (k, 32) + l) ≤ n) ∧ (nat-to-int (k, 32) ∈ N)) → disjoint (a, j , add (32, b, k), l)

Theorem: disjoint-2-int (disjoint (a, m, b, n) ∧ ((nat-to-int (i, 32) + j ) ≤ m) ∧ (l ≤ n) ∧ (nat-to-int (i, 32) ∈ N)) → disjoint (add (32, a, i), j , b, l)

Theorem: disjoint-2˜-int (disjoint (a, m, b, n) ∧ ((nat-to-int (i, 32) + j ) ≤ m) ∧ (l ≤ n) ∧ (nat-to-int (i, 32) ∈ N)) → disjoint (b, l, add (32, a, i), j )

Theorem: disjoint-3-int (disjoint (a, m, b, n) ∧ ((nat-to-int (i, 32) + j ) ≤ m) ∧ ((nat-to-int (k, 32) + l) ≤ n) ∧ (nat-to-int (i, 32) ∈ N) ∧ (nat-to-int (k, 32) ∈ N)) → disjoint (add (32, a, i), j , add (32, b, k), l)

Theorem: read-memp-ram1-uint (ram-addrp (addr, mem, k) ∧ ((nat-to-uint (i) + j ) ≤ k)) → read-memp (add (32, addr, i), mem, j )

Theorem: write-memp-ram1-uint (ram-addrp (addr, mem, k) ∧ ((nat-to-uint (i) + j ) ≤ k)) → write-memp (add (32, addr, i), mem, j )

Theorem: disjoint-1-uint (disjoint (a, m, b, n) ∧ (j ≤ m) ∧ ((nat-to-uint (k) + l) ≤ n)) → disjoint (a, j , add (32, b, k), l)

Theorem: disjoint-2-uint (disjoint (a, m, b, n) ∧ ((nat-to-uint (i) + j ) ≤ m) ∧ (l ≤ n)) → disjoint (add (32, a, i), j , b, l)

Theorem: disjoint-2˜-uint (disjoint (a, m, b, n) ∧ ((nat-to-uint (i) + j ) ≤ m) ∧ (l ≤ n)) → disjoint (b, l, add (32, a, i), j )

Theorem: disjoint-3-uint (disjoint (a, m, b, n) ∧ ((nat-to-uint (i) + j ) ≤ m) ∧ ((nat-to-uint (k) + l) ≤ n)) → disjoint (add (32, a, i), j , add (32, b, k), l)

Theorem: disjoint-5-uint (disjoint (add (32, a, i), m, b, n) ∧ ((j + index-n (0, i)) ≤ m) ∧ ((nat-to-uint (k) + l) ≤ n)) → disjoint (a, j , add (32, b, k), l)

Theorem: disjoint-6-uint (disjoint (add (32, a, i), m, b, n) ∧ ((j + index-n (i1 , i)) ≤ m) ∧ (l ≤ n)) → disjoint (add (32, a, i1 ), j , b, l)

Theorem: disjoint-7-uint (disjoint (add (32, a, i), m, b, n) ∧ ((j + index-n (i1 , i)) ≤ m) ∧ ((nat-to-uint (k) + l) ≤ n)) → disjoint (add (32, a, i1 ), j , add (32, b, k), l)

Theorem: read-rn-int-8 32 nat-to-int (read-rn (8, rn, rfile), 32) = nat-to-uint (read-rn (8, rn, rfile))

Theorem: read-rn-int-16 32 nat-to-int (read-rn (16, rn, rfile), 32) = nat-to-uint (read-rn (16, rn, rfile))

Theorem: read-rn-int-8 16 nat-to-int (read-rn (8, rn, rfile), 16) = nat-to-uint (read-rn (8, rn, rfile))

Theorem: read-mem-int-8 32 nat-to-int (read-mem (x, mem, 1), 32) = nat-to-uint (read-mem (x, mem, 1))

Theorem: read-mem-int-16 32 nat-to-int (read-mem (x, mem, 2), 32) = nat-to-uint (read-mem (x, mem, 2))

Theorem: read-mem-int-8 16 nat-to-int (read-mem (x, mem, 1), 16) = nat-to-uint (read-mem (x, mem, 1))

Theorem: idifference-int-rangep ((x ∈ N) ∧ (y ∈ N) ∧ int-rangep (x, n) ∧ int-rangep (y, n)) → int-rangep (idifference (x, y), n)

Event: Disable idifference.

; some more arithmetic.

Theorem: difference-cancel-1 (i ≤ j ) → ((((i + j ) − (2 ∗ i)) = (j − i))

∧ (((2 ∗ j ) − (i + j )) = (j − i)))

Theorem: difference-is-1 ((x − y) = 1) = (x = (1 + y))

Theorem: mean-difference-1 (i ≤ j ) → ((((i + j ) ÷ 2) − i) = ((j − i) ÷ 2))

Theorem: mean-difference-2 (i ≤ j ) → (((j − i) ÷ 2) ≮ ((j − 1) − ((i + j ) ÷ 2)))

Theorem: plus-0 (0 + x) = fix (x)

Theorem: plus-times-sub1 (x + (x ∗ (y − 1))) = if y ≃ 0 then fix (x)

else x ∗ y endif

Event: Disable plus-times-sub1.

Theorem: plus2-times-sub1 (x + y + (x ∗ (z − 1))) = if z ≃ 0 then x + y

else y + (x ∗ z) endif

Theorem: plus3-times-sub1 (x + y + z + (x ∗ (z1 − 1))) = if z1 ≃ 0 then x + y + z

else y + z + (x ∗ z1 ) endif

Theorem: lessp-cancel-4294967295

((4294967295 + x) < 4294967296) = (x ≃ 0)

Theorem: difference-cancel-4294967295

((4294967295 + x) − 4294967296) = (x − 1)

Theorem: lessp-cancel-4294967292

((4294967292 + x) < 4294967296) = (x < 4)

Theorem: difference-cancel-4294967292

((4294967292 + x) − 4294967296) = (x − 4)

Theorem: difference-lessp-cancel-1 ((a − c) < (c ∗ (b − 1))) = if c ≤ a then a < (c ∗ b)

else 1 < b endif

Theorem: difference-lessp-cancel-2 (c ≤ a) → (((a − c) < (d + (c ∗ (b − 1))))

= if b ≃ 0 then (a − c) < d else a < (d + (c ∗ b)) endif)

; two funny lemmas.  But seems more useful than add-uint!

Theorem: add-uintxx (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ ((nat-to-uint (x) + nat-to-uint (y)) < exp (2, n))) → (nat-to-uint (add (n, x, y)) = (nat-to-uint (x) + nat-to-uint (y)))

Theorem: add-uintxxx (nat-rangep (x, n) ∧ nat-rangep (y, n) ∧ ((nat-to-uint (x) + nat-to-uint (y)) ≮ exp (2, n))) → (nat-to-uint (add (n, x, y))

= ((nat-to-uint (x) + nat-to-uint (y)) − exp (2, n)))

Event: Disable add-uintxxx.

Theorem: ram-addrp-3 (ram-addrp (add (32, addr, i), mem, k) ∧ ((index-n (h, i) + j ) ≤ k)) → ram-addrp (add (32, addr, h), mem, j )

Theorem: ram-addrp-4 (ram-addrp (addr, mem, k) ∧ ((nat-to-uint (h) + j ) ≤ k)) → ram-addrp (add (32, addr, h), mem, j )

Theorem: and-z-commutativity and-z (n, x, y) = and-z (n, y, x)

; finally, establish the database.

Event: Make the library "mc20-2" and compile it.

Index

abs, 17, 63 abs-lessp-int-rangep, 17 add, 2, 3, 7, 23–30, 48, 54, 55, 74–

88, 93–100, 102, 103, 106, 118, 128–131, 135, 136, 138, 139

add-0, 26 add-adder, 27 add-addx-c, 57 add-addx-v, 66 add-associativity, 26 add-bcs&cc, 65 add-bmi, 68 add-bmi-crock1, 14 add-bmi-crock2, 14 add-bvs&vc, 67 add-c, 49, 57, 65 add-c-bitp, 49 add-cancel, 28 add-cancel0, 28 add-commutativity, 26 add-commutativity1, 26 add-commutativity2, 28 add-equal-cancel-1, 55 add-evenp, 7 add-fringe, 54–57 add-group, 114 add-group-h, 114 add-head, 27 add-int, 30 add-leq, 26 add-n, 49, 68 add-n-bitp, 49 add-nat-la, 23 add-nat-rangep, 27 add-neg-0, 54 add-neg-adder, 27 add-neg-cancel, 54 add-non-numberp, 74 add-of-0, 25 add-plus, 74 add-sub, 28 add-sub-cancel, 27 add-tree, 54–57 add-tree-add-fringe, 55 add-tree-append, 55 add-tree-bagdiff, 55 add-tree-delete, 56 add-tree-delete-cond, 55, 56 add-tree-delete-equal, 55 add-tree-nat-rangep, 55 add-uint, 24 add-uintxx, 138 add-uintxxx, 138 add-v, 49, 66, 67 add-v-bitp, 49 add-z, 49 add-z-bitp, 49 adder, 7, 8, 24–29 adder-associativity, 25 adder-cancel, 28 adder-commutativity, 25 adder-commutativity1, 25 adder-head, 27 adder-int, 29 adder-int-bridge, 29 adder-int-end, 13, 29 adder-lognot, 8 adder-nat-la, 24 adder-nat-rangep, 26 adder-shift-carry, 25 adder-uint, 24 addr-index2, 114 addr-index2-mem, 114 addx-c, 50, 57, 58 addx-c-bitp, 50 addx-c-la, 58 addx-n, 50 addx-n-bitp, 50 addx-v, 50, 66 addx-v-bitp, 50 addx-v-crock1, 13 addx-v-crock2, 14 addx-v-la, 66 addx-z, 50 addx-z-bitp, 50 addy-y, 29 addy-y1, 29 and-group, 115 and-group-h, 115 and-n, 50 and-n-bitp, 50 and-z, 50, 61, 62, 139 and-z-bitp, 50 and-z-commutativity, 139 app, 9–11, 32–34, 44, 46, 79, 90, 91,

106 app-0, 9 app-associativity, 33 app-cancel, 44 app-head-tail, 33 app-nat-rangep, 34 append-len, 91 asl, 10, 12, 86, 87, 98–100 asl-0, 12 asl-asl, 12 asl-beq, 64 asl-bmi, 69 asl-bvs, 68 asl-c, 52 asl-c-bitp, 52 asl-int, 10 asl-int-crock1, 9 asl-int-crock2, 10 asl-n, 52, 70 asl-n-bitp, 52 asl-nat-rangep, 12 asl-v, 52, 68 asl-v-bitp, 52 asl-z, 52, 64 asl-z-bitp, 52 asr, 11, 12 asr-0, 12 asr-beq, 64 asr-bmi, 70 asr-c, 52 asr-c-bitp, 52 asr-int, 11 asr-int-crock, 11 asr-n, 52, 70 asr-n-bitp, 52 asr-nat-rangep, 12 asr-z, 52, 64 asr-z-bitp, 52

b, 49, 79 b-and, 4, 6 b-eor, 4, 6 b-not, 3, 6, 8, 35, 59, 66, 70–72 b-or, 4, 6 b0, 3, 4, 6 b0p, 3 b1, 3 bagdiff, 55, 56 bagint, 56 bcar, 2, 32, 33 bcar-1, 33 bcar-2, 33 bcar-app, 33 bcar-head, 33 bcar-lessp, 33 bcar-nonnumberp, 32 bcar-replace, 33 bcc-group, 115 bcc-group-h, 115 bcdr, 2, 32, 33 bcdr-1, 33 bcdr-2, 33 bcdr-lessp, 33 bcdr-nonnumberp, 32 bcs, 65 beq, 59–64 between-ileq, 58, 106 between-ileq-la, 106 bge, 70, 71 bge-v0, 70 bgt, 71, 72 bhi, 58, 59 bit, 3, 4, 6 bit-group, 115 bit-group-h, 115 bitn, 7, 12, 34, 35, 43, 44, 49, 66 bitn-0, 34 bitn-0-1, 34 bitn-app, 34 bitn-bitp, 49 bitn-head, 34 bitn-lognot, 35 bitn-replace, 34 bitn-tail, 34 bitp, 7, 8, 13–15, 24, 29, 30, 49–53,

58, 66 bitp-fix-bit, 49 ble, 71, 72 ble-bgt, 72 bls, 59 bls-bhi, 59 blt, 70, 71 blt-bge, 71 blt-v0, 70 bmi, 68–70 bv-adder, 4, 5, 7 bv-adder-bridge, 7 bv-adder-len, 5 bv-adder-listp, 5 bv-adder-nat, 7 bv-adder&carry, 6, 7 bv-adder&carry-len, 6 bv-adder&carry-nat, 7 bv-bitn, 4, 6, 7 bv-bitn-bitn, 7 bv-bitn-not, 6 bv-head, 3, 5–7 bv-head-len, 5 bv-head-listp, 5 bv-head-nat, 5 bv-len, 3–7 bv-len-listp, 4 bv-mbit, 4, 7 bv-mbit-bitn, 7 bv-not, 3, 6, 7 bv-not-lognot, 7 bv-sized-to-nat, 4–6 bv-sized-to-nat-head, 5 bv-sized-to-nat-to-bv-sized, 6 bv-tail, 3 bv-to-lst, 91–93, 96 bv-to-lst-len, 92 bv-to-lst-proper-lstp, 92 bv-to-nat, 4–7 bv-to-nat-rangep, 6 bv-to-nat-to-bv, 5 bv-to-nat-to-bv-sized, 5 bvs, 67, 68 byte-read, 36, 38, 45, 48, 90 byte-read-nat-rangep, 38 byte-read-write, 45 byte-read-write-mem, 48 byte-read-write-mem-end, 48 byte-read-write-mem-lemma, 48 byte-read=read-mem-1, 90 byte-readp, 36, 45, 46, 76, 78, 100 byte-readp-ram0, 78 byte-readp-ram1, 78 byte-readp-ram2, 78 byte-readp-ram3, 78 byte-readp-rom0, 76 byte-readp-rom1, 76 byte-readp-rom2, 76 byte-readp-rom3, 76 byte-write, 36, 45–49, 73, 81, 90, 95,

96 byte-write-app, 46 byte-write-maintain-byte-readp, 46 byte-write-maintain-byte-writep, 46 byte-write-maintain-pc-byte-rea

dp, 45 byte-write-maintain-pc-read-memp,

47 byte-write-maintain-ram-addrp, 73 byte-write-maintain-read-memp, 47 byte-write-maintain-rom-addrp, 73 byte-write-maintain-write-memp, 47 byte-write-mcode-addrp, 81 byte-write-write, 45 byte-write-write-la, 45 byte-write=write-mem-1, 90 byte-writep, 36, 45–47, 74, 77, 81,

90, 100 byte-writep->readp, 45 byte-writep-ram0, 77 byte-writep-ram1, 77 byte-writep-ram2, 77 byte-writep-ram3, 77 byte-writep=write-memp-1, 90

cancel-add-neg, 57 cancel-equal-add, 56 ccr-c, 39 ccr-n, 39 ccr-v, 39 ccr-x, 39 ccr-z, 39 cdr-mcdr, 92 cmp-group, 115 cmp-group-h, 115 correctness-of-cancel-add-neg, 57 correctness-of-cancel-equal-add, 56 cvznx, 39

d2-7a2-5p, 120 d2-7a3-5p, 120 d3-7a2-5p, 120 d4-7a2-5p, 120, 121 d4-7a4-5p, 120 d4-7a5p, 120 d5-7a2-5p, 120 d5-7a4-5p, 121 d6-7a2-5p, 121 delete, 55–57 difference-app-1s, 11 difference-cancel-1, 137 difference-cancel-4294967292, 138 difference-cancel-4294967295, 138 difference-int-rangep, 17 difference-is-1, 137 difference-lessp-cancel-1, 138 difference-lessp-cancel-2, 138 difference-nat-rangep, 37 disjoint, 3, 48, 81–88, 94, 95, 100,

101, 135, 136 disjoint-0, 82 disjoint-0˜, 84 disjoint-1, 82 disjoint-1-int, 135 disjoint-1-uint, 136 disjoint-10, 83 disjoint-10˜, 85 disjoint-11, 83 disjoint-11-asl, 87 disjoint-11˜, 85 disjoint-11˜-asl, 87 disjoint-12, 83 disjoint-12˜, 85 disjoint-13, 83 disjoint-13˜, 85 disjoint-14, 84 disjoint-14˜, 85 disjoint-15, 84 disjoint-15˜, 85 disjoint-1˜, 84 disjoint-2, 82 disjoint-2-asl, 86 disjoint-2-int, 135 disjoint-2-uint, 136 disjoint-2˜, 84 disjoint-2˜-asl, 86 disjoint-2˜-int, 135 disjoint-2˜-uint, 136 disjoint-3, 82 disjoint-3-asl, 86 disjoint-3-int, 135 disjoint-3-uint, 136 disjoint-3˜, 84 disjoint-3˜-asl, 86 disjoint-4, 82 disjoint-4˜, 84 disjoint-5, 82 disjoint-5-uint, 136 disjoint-5˜, 84 disjoint-6, 82 disjoint-6-uint, 136 disjoint-6˜, 84 disjoint-7, 83 disjoint-7-uint, 136 disjoint-7˜, 85 disjoint-8, 83 disjoint-8˜, 85 disjoint-9, 83 disjoint-9-asl, 86 disjoint-9˜, 85 disjoint-9˜-asl, 87 disjoint-commutativity, 84 disjoint-deduction0, 87 disjoint-deduction1, 88 disjoint-deduction2, 88 disjoint-deduction3, 88 disjoint-head, 81 disjoint-la0, 82 disjoint-la1, 82 disjoint-la2, 82 disjoint-la3, 82 disjoint-leq, 95 disjoint-leq-uint, 101 disjoint-leq1, 95 disjoint-leq1-uint, 101 disjoint-x-x, 87 disjoint0, 2, 3, 48, 49, 81, 82, 87, 95 disjoint0-deduction0, 87 disjoint0-deduction1, 87 disjoint0-deduction2, 87 disjoint0-head, 81 disjoint0-la0, 81 disjoint0-la1, 81 disjoint0-la2, 81 disjoint0-leq, 95 disjoint0-x-x, 87 divs-beq, 63 divs-n, 51 divs-n-bitp, 51 divs-overflow, 23 divs-v, 23 divs-z, 51, 63 divs-z-bitp, 51 divs 3232-overflow, 23 divu-beq, 63 divu-n, 51 divu-n-bitp, 51 divu-overflow, 23 divu-v, 23 divu-z, 51, 63 divu-z-bitp, 51

effec-addr, 114

effec-addr-mem, 114

eof, 121 eor-n, 53 eor-n-bitp, 53 eor-z, 53, 61 eor-z-bitp, 53 equal*, 119, 120 equal*-reflex, 119 eval$-add-member, 55 evenp, 7 exp, 5, 6, 8–15, 17, 21–25, 29–31,

35, 37, 58, 61–65, 67, 86, 87, 89, 98, 99, 135, 138

exp2-leq, 31 exp2-lessp, 12 exp2-lessp-crock, 21 ext, 12, 38, 45, 60 ext-0, 38 ext-beq-int-0, 64 ext-beq-int-1, 64 ext-beq-uint, 64 ext-bmi, 70 ext-equal, 45 ext-equal-0, 45 ext-int, 12 ext-lemma, 38 ext-n, 53, 70 ext-n-bitp, 53 ext-nat-rangep, 38 ext-z, 53, 64 ext-z-bitp, 53

fix-bit, 6, 7, 13, 39, 49

fix-bit-bitp, 49 fix-bv, 3, 6 fix-bv-adder&carry, 6 fix-int, 16–20 fix-int-integerp, 18

get-lst, 90, 92, 93, 104 get-lst-cdr, 92 get-lst-int, 119 get-lst-integerp, 119 get-lst-mcar, 92 get-lst-mcdr, 92 get-lst-of-chrp, 132 get-nth, 40, 41, 79, 80, 89–94, 98,

103–105, 119, 121–126, 128– 134

get-nth-0, 40 get-nth-append, 93 get-nth-nil, 41 get-nth-tail-lst, 80 get-put, 41 get-swap, 121 get-vals, 90–93, 96, 104, 105 get-vals-0, 96 get-vals-append, 93 get-vals-cdr, 92 get-vals-len, 91 get-vals-mcar, 92 get-vals-mcdr, 92 get-vals-proper-lstp, 92 get-vlst, 42, 43 get-vlst-member, 42 get-vlst-readm-rn, 43 groups, 114

h, 114–116 h-invariant, 114 head, 2, 8–12, 21, 26–28, 31–38, 41,

42, 44, 45, 48, 53–55, 74, 81, 88–91, 95, 96, 101

head-0, 8 head-app, 32 head-app-cancel, 44 head-app-head-tail, 33 head-byte-pc-read, 36 head-byte-read, 36 head-byte-readp, 36 head-byte-write, 36 head-byte-writep, 36 head-ext, 38 head-head, 31 head-int-crock, 21 head-lemma, 9 head-leq, 8 head-lessp, 8 head-mem-ilst, 89 head-mem-lst, 89 head-nat-rangep, 37 head-of-0, 8 head-pc-byte-readp, 36 head-pc-read, 36 head-pc-read-mem, 36 head-pc-read-memp, 36 head-pc-readp, 35 head-plus-cancel, 31 head-plus-cancel0, 31 head-plus-head, 31 head-read, 36 head-read-mem, 36 head-read-memp, 36 head-read-rn, 41 head-readm-mem, 37 head-readp, 35 head-recursion, 44 head-replace, 32 head-sub1-lessp, 48 head-write, 36 head-write-mem, 36 head-write-memp, 36 head-writep, 36

idifference, 15, 18, 19, 30, 66–68,

122–124, 137 idifference-int-rangep, 137 idifference-int-rangep1, 15 idifference-int-rangep2, 15 idifference-integerp, 18 idifference-negativep, 19 idifference-x-x, 19 ileq, 58 ilessp, 14, 15, 19, 68, 70, 71, 106 ilessp-crock1, 14 ilessp-crock2, 14 ilessp-entails-ileq, 19 ilessp-reflex, 19 immediate, 114 immediate-mem, 114 index-n, 75–88, 136, 139 index-n-0, 88 index-n-deduction0, 88 index-n-deduction1, 88 index-n-deduction2, 88 index-n-x-x, 88 ineg, 8, 18, 20 ineg-integerp, 18 ineg-iplus, 18 int-rangep, 10, 13–17, 21–23, 29, 30,

62–64, 66–69, 89, 134, 137 int-rangep-la, 15 int-rangep-of-0, 17 int-to-nat, 13, 16, 21 int-to-nat-0, 16 int-to-nat-rangep, 16 int-to-nat-to-int, 16 int-to-nat=0, 16 integerp, 13–19, 21, 63, 89, 106, 119 integerp-fix-int, 17 integerp-minus0, 18 iplus, 8, 11, 13–15, 18, 19, 29, 30,

66–68, 106 iplus-0, 19 iplus-1–1, 19 iplus-associativity, 18 iplus-commutativity, 18 iplus-commutativity1, 18 iplus-int-rangep1, 14 iplus-int-rangep2, 15 iplus-integerp, 18 iplus-with-carry-negativep, 13 iplus-with-carry-non-negativep, 13 iquot, 22, 38 iquot-int, 22 iquot-nat-rangep, 38 iquotient, 11, 17, 18, 20, 22, 23, 63 iquotient-int-rangep, 17 iquotient-integerp, 18 iquotient-wrt–1, 20 iquotient-wrt-1, 20 iquotient=0, 63 iread-an, 118 iread-dn, 118 iread-mem, 118 iread-mem-get0, 94 irem, 22, 38 irem-int, 22 irem-nat-rangep, 38 iremainder, 11, 17–20, 22 iremainder-int-rangep, 17 iremainder-integerp, 18 iremainder-wrt–1, 20 iremainder-wrt-1, 19 itimes, 10, 18, 19, 21, 62, 67, 69 itimes-0, 19 itimes-associativity, 19 itimes-commutativity, 19 itimes-equal-0, 19 itimes-equal-cancellation, 19 itimes-integerp, 18 itimes-sign, 19 izerop, 19

l, 88

len, 41, 42, 79–81, 91–93, 96, 100– 102, 116, 117

lessp-app-1s, 10

lessp-cancel-4294967292, 138 lessp-cancel-4294967295, 138 lessp-slen-mcdr, 134 lessp-slen-mcdr-0, 134 lessp-times-exp-1s, 10 linked-a6, 118 linked-rts-addr, 118 log, 35, 61, 62 logand, 35, 37 logand-beq-uint, 61 logand-commutativity, 35 logand-eor-beq-uint, 62 logand-logeor, 35 logand-logor, 35 logand-nat-rangep, 37 logand-or-beq-uint, 61 logand-uint, 35 logand-uint-la, 35 logeor, 35, 37, 62 logeor-beq-int-0, 61 logeor-beq-int-1, 61 logeor-beq-uint, 61 logeor-commutativity, 35 logeor-equal-0, 35 logeor-nat-rangep, 37 lognot, 7, 8, 27, 35, 66 lognot-0, 7 lognot-cancel, 8 lognot-int, 8 lognot-lognot, 8 lognot-nat-rangep, 7 logor, 35, 37, 61 logor-beq-int-0, 61 logor-beq-int-1, 61 logor-beq-uint, 60 logor-commutativity, 35 logor-equal-0, 35 logor-nat-rangep, 37 lsl, 9, 11 lsl-0, 11 lsl-1-bcs&cc, 65 lsl-beq, 63 lsl-c, 52, 65 lsl-c-0, 65 lsl-c-bitp, 52 lsl-lsl, 11 lsl-n, 52 lsl-n-bitp, 52 lsl-nat-rangep, 11 lsl-uint, 9 lsl-z, 52, 63 lsl-z-bitp, 52 lsr, 9, 11, 12 lsr-0, 11 lsr-1-bcs&cc, 65 lsr-beq, 63 lsr-c, 52, 65 lsr-c-0, 65 lsr-c-bitp, 52 lsr-lsr, 12 lsr-n, 52 lsr-n-bitp, 52 lsr-nat-rangep, 12 lsr-uint, 9 lsr-z, 52, 63 lsr-z-bitp, 52 lst-int, 119 lst-integerp, 119 lst-numberp, 79–81 lst-numberp0, 79 lst-of-chrp, 132 lst-to-bv, 91 lstcpy, 103, 104 lstcpy-0, 103 lstcpy-add1, 104 lstcpy-cpy1, 104 lstcpy-lstcpy, 103 lstcpy-put-nth, 104 lstcpy1, 104 lstmcpy, 103, 104 lstmcpy-cpy, 104

mapping, 114 mapping-h, 114 mbit-means-lessp, 12 mbit-means-negativep, 66 mc-ccr, 40 mc-ccr-rangep, 40 mc-ccr-rewrite, 40 mc-instate, 114 mc-instate-mem, 114 mc-mem, 40, 106, 107, 114–118 mc-mem-rewrite, 40 mc-pc, 40 mc-pc-rangep, 40 mc-pc-rewrite, 40 mc-rfile, 40 mc-rfile-rewrite, 40 mc-state, 40 mc-status, 40, 73 mc-status-rewrite, 40 mcar, 91, 92, 102 mcar-mcar, 92 mcar-nth, 92 mcdr, 91, 92, 102, 103, 126, 130, 134 mcdr-listp-len, 92 mcdr-mcdr, 92 mcdr-nth, 92 mcode-addrp, 74, 79–81, 100, 117 mean-difference-1, 137 mean-difference-2, 137 mean-lessp, 121 mean-lessp-lemma, 121 mem-ilst, 88, 89, 94, 95, 97–99, 101,

107, 119 mem-ilst-int-rangep, 89 mem-ilst-integerp, 89 mem-ilst-lst-integerp, 119 mem-induct0, 46 mem-induct1, 79 mem-induct2, 93 mem-induct3, 95 mem-induct4, 96 mem-lst, 88, 89, 93–100, 102–104,

106, 119 mem-lst-get-lst, 93 mem-lst-get-lst0, 93 mem-lst-get-vals, 93 mem-lst-get-vals0, 93 mem-lst-integerp, 119 mem-lst-len, 102 mem-lst-lessp, 89 mem-lst-mcar, 102 mem-lst-mcar-1, 102 mem-lst-mcar-2, 102 mem-lst-mcdr, 102 mem-lst-mcdr-0, 102 mem-lst-mcdr-1, 103 mem-lst-mcdr-uint, 102 mem-lst-mcdr-uint-1, 103 mem-lst-nat-rangep, 89 mem-lst-non-numberp, 89 mem-lst-numberp, 89 mem-lst-plus, 102 mem-lst-put-lst, 95 mem-lst-put-vals, 96 mem-lst-same, 89 memchr, 122 memchr*, 129 memchr-bounds, 134 memchr1, 121, 122, 134 memcmp, 122 memcmp1, 122 memmove, 127 memmove-0, 127, 128 memmove-1, 126, 127 memmove-3, 127, 128 memmove-4, 127, 128 memset, 122 memset1, 122 minus-integerp, 18 misc-group, 116 misc-group-h, 116 mmov1-lst, 105, 126, 127 mmov1-lst-0, 105 mmov1-lst1, 105, 127, 128 mmov1-lst1-0, 105 mmovn-lst, 105, 126 mmovn-lst-0, 105 mmovn-lst1, 105, 127 mmovn-lst1-0, 105 mod-eq, 2 mod32-eq, 2, 45, 81, 82, 106 mod32-eq-deduction0, 106 mod32-eq-deduction1, 106 mod32-eq-deduction2, 106 mod32-eq-deduction3, 106 mode-guards, 114 modn-eq, 43, 44 modn-eq-equal, 44 modn-lst, 101 modn-readm-rn, 101 move-beq-ext, 60 move-beq-int-0, 59 move-beq-int-1, 60 move-beq-uint, 59 move-bgt, 71 move-ble, 72 move-bmi, 68 move-group, 116 move-group-h, 116 move-h, 116 move-ins, 116 move-n, 53, 68, 71, 72 move-n-bitp, 53 move-z, 53, 59, 60, 71, 72 move-z-bitp, 53 movem-len, 116 movem-pre-rnlst, 116 movem-pre-rnlst-len, 116 movem-rnlst, 116 movem-rnlst-len, 116 movem-saved, 118 movep-write, 115 movep-write-h, 115 movep-writep, 115 movn-lst, 105 muls, 21, 38 muls-crock, 21 muls-n, 51, 69 muls-n-bitp, 51 muls-nat-rangep, 38 muls-v, 51, 67 muls-v-bitp, 51 muls-z, 51, 62, 63 muls-z-bitp, 51 muls 1632-beq, 62 muls 1632-bmi, 69 muls 1632-bvs, 67 muls 1632-int, 21 muls 3232-beq, 62 muls 3232-bmi, 69 muls 3232-bvs, 67 muls 3232-int, 21 muls 3264-beq, 62 muls 3264-bmi, 69 muls 3264-bvs, 67 muls 3264-int, 21 mulu, 20, 38 mulu-n, 51 mulu-n-bitp, 51 mulu-nat-rangep, 38 mulu-v, 50, 67 mulu-v-bitp, 50 mulu-z, 50, 62 mulu-z-bitp, 50 mulu 1632-beq, 62 mulu 1632-bvs, 67 mulu 1632-nat, 20 mulu 3232-beq, 62 mulu 3232-bvs, 67 mulu 3232-nat, 20 mulu 3264-beq, 62 mulu 3264-bvs, 67 mulu 3264-nat, 20

n-member, 2, 42, 43 nat-plus-rangep, 37 nat-rangep, 6–12, 15, 16, 20–30, 34,

35, 37–40, 45, 46, 48, 54, 55, 58–72, 89, 95–99, 135, 138 nat-rangep-0, 37 nat-rangep-la, 135 nat-rangep-of-0, 37 nat-rangep-ub, 37 nat-to-bv, 4, 5 nat-to-bv-sized, 4–6 nat-to-bv-sized-head, 5 nat-to-bv-sized-la0, 5 nat-to-bv-sized-len, 5 nat-to-bv-sized-sized-to-nat, 6 nat-to-bv-sized-to-nat, 6 nat-to-bv-to-nat, 5 nat-to-int, 8, 10–13, 16, 21–23, 29,

30, 58–64, 66–72, 77, 78, 80, 86–88, 94, 97–100, 118, 119, 135–137

nat-to-int-0, 16

nat-to-int-integerp, 16 nat-to-int-rangep, 16 nat-to-int-to-nat, 16 nat-to-int=, 16 nat-to-uint, 9, 15, 16, 20, 22–25, 35,

59–65, 67, 89, 93–98, 101– 103, 118, 127, 131, 132, 135– 139 nat-to-uint-rangep, 16 nat-to-uint-to-nat, 15 neg, 2, 25, 27, 30, 38, 53, 54, 88, 106 neg-add, 54 neg-cancel, 54 neg-head, 53 neg-nat-rangep, 38 neg-neg, 53 negativep-guts0, 18 not-n, 53 not-n-bitp, 53 not-z, 53 not-z-bitp, 53 null, 121–124, 128, 133 numberp-eval$-add, 55 numberp-eval$-add-tree, 55 numberp-integerp, 18

or-group, 115 or-group-h, 115 or-n, 51 or-n-bitp, 51 or-z, 51, 60, 61 or-z-bitp, 51

p, 114–116 pc-byte-read, 36, 38, 45, 47, 74, 79,

90 pc-byte-read-mcode0, 79 pc-byte-read-mcode1, 79 pc-byte-read-mcode2, 79 pc-byte-read-mcode3, 79 pc-byte-read-nat-rangep, 38 pc-byte-read-write, 45 pc-byte-read-write-mem, 47 pc-byte-read=pc-read-mem-1, 90 pc-byte-readp, 36, 45–47, 74, 75, 100 pc-byte-readp->byte-readp, 45 pc-byte-readp-rom0, 75 pc-byte-readp-rom1, 75 pc-byte-readp-rom2, 75 pc-byte-readp-rom3, 75 pc-read, 36, 44 pc-read-mem, 36, 46, 47, 80, 90, 100,

117 pc-read-mem-byte-write, 47 pc-read-mem-mcode0, 80 pc-read-mem-mcode1, 80 pc-read-mem-mcode2, 80 pc-read-mem-mcode3, 80 pc-read-mem-nat-rangep, 46 pc-read-mem-write-mem, 47 pc-read-mem-writem-mem, 100 pc-read-memp, 2, 36, 47, 74, 75, 81,

100, 116 pc-read-memp->read-memp, 47 pc-read-memp-la0, 74 pc-read-memp-la1, 74 pc-read-memp-la2, 74 pc-read-memp-la3, 74 pc-read-memp-rom0, 75 pc-read-memp-rom1, 75 pc-read-memp-rom2, 75 pc-read-memp-rom3, 75 pc-read-write, 44 pc-readp, 35, 43, 44 pc-readp->readp, 43 plus-0, 137 plus-add1-sub1, 27 plus-difference, 102 plus-numberp, 24 plus-times-equal, 44 plus-times-lessp, 95 plus-times-sub1, 137 plus-to-iplus, 13 plus2-times-sub1, 138 plus3-times-sub1, 138 proper-lstp, 91, 92, 96 put-commutativity, 104 put-get, 41 put-get-lst-is-cpy, 104 put-get-vals-is-cpy, 104 put-lst, 90, 96, 104 put-lst-int, 119 put-lst-of-chrp, 132 put-nth, 41, 90, 91, 95–99, 103–105,

119, 121–124, 131–133 put-nth-0, 41 put-nth-len, 41 put-put, 41 put-vals, 91, 93, 96, 104, 105 put-vals-append, 93 quot, 23, 38 quot-nat, 23 quot-nat-rangep, 38 quotient-diff, 10 quotient-diff-la, 10 quotient-exp-lessp, 10 quotient-int-rangep, 17 quotient-nat-rangep, 37 quotient-plus-times-exp2-1, 31 quotient-plus-times-exp2-2, 31

ram-addrp, 2, 73, 74, 77, 78, 99,

100, 117, 136, 139 ram-addrp-3, 139 ram-addrp-4, 139 ram-addrp-la1, 78 ram-addrp-la2, 78 read, 36, 44 read->pc-read-mem, 80 read-an, 118 read-dn, 118 read-lst, 80, 81 read-lst0, 79, 80 read-mem, 36, 46, 48, 80, 81, 88–90,

93, 94, 98, 101, 106, 117, 118, 137

read-mem-byte-write, 48 read-mem-byte-write-end, 48 read-mem-ilst, 94 read-mem-ilst-asl, 98 read-mem-ilst-int, 94 read-mem-int-16 32, 137 read-mem-int-8 16, 137 read-mem-int-8 32, 137 read-mem-lst, 94 read-mem-lst-asl, 98 read-mem-lst-int, 94 read-mem-lst-la, 93 read-mem-lst0, 94 read-mem-mcode1-int, 80 read-mem-mcode2, 81 read-mem-mcode3, 81 read-mem-nat-rangep, 46 read-mem-non-numberp, 89 read-mem-plus, 106 read-memp, 36, 47, 76–78, 99, 100,

116, 136 read-memp-ram0, 78 read-memp-ram1, 78 read-memp-ram1-asl, 99 read-memp-ram1-int, 78 read-memp-ram1-uint, 136 read-memp-ram2, 78 read-memp-ram3, 78 read-memp-rom0, 76 read-memp-rom1, 76 read-memp-rom1-asl, 99 read-memp-rom1-int, 77 read-memp-rom2, 76 read-memp-rom3, 76 read-rn, 38, 41–43, 120, 136, 137 read-rn-0, 43 read-rn-equal*, 120 read-rn-int-16 32, 137 read-rn-int-8 16, 137 read-rn-int-8 32, 136 read-rn-nat-rangep, 38 read-write, 44 read-write-mem-end, 48 read-write-mem1, 48 read-write-mem2, 48 read-write-rn, 41 read-write-rn-end, 41 read-writem-mem, 101 read-writem-rn, 42 read-writem-rn-end, 42, 43 readm-mem, 37, 89, 101, 106, 107,

118 readm-mem-lst, 89 readm-rn, 42, 43, 101 readm-rn-len, 42 readm-write-mem, 101 readm-write-rn, 43 readm-writem-mem, 101 readp, 35, 43 rem, 22, 38 rem-nat, 22 rem-nat-rangep, 38 remainder-diff, 10 remainder-diff-la, 9 remainder-int-rangep, 17 remainder-leq, 26 remainder-plus-times-exp2-1, 31 remainder-plus-times-exp2-2, 31 remainder-quotient-exp2, 31 remainder2-plus-times-exp2, 31 replace, 9, 32–34, 41 replace-0, 9 replace-associativity, 32 replace-head, 32 replace-leq, 32 replace-leq1, 32 replace-nat-rangep, 34 replace-reflex, 32 rn-saved, 118 rol-c, 51 rol-c-bitp, 51 rol-n, 51 rol-n-bitp, 51 rol-z, 51 rol-z-bitp, 51 rom-addrp, 2, 73, 75–77, 99, 100,

117 rom-addrp-la1, 76 rom-addrp-la2, 76 ror-c, 51 ror-c-bitp, 51 ror-n, 51 ror-n-bitp, 51 ror-z, 51 ror-z-bitp, 51 roxl-c, 52 roxl-c-bitp, 52 roxl-n, 52 roxl-n-bitp, 52 roxl-z, 52 roxl-z-bitp, 52 roxr-c, 53 roxr-c-bitp, 53 roxr-n, 53 roxr-n-bitp, 53 roxr-z, 53 roxr-z-bitp, 53 rts-addr, 118

s&r-group, 116 s&r-group-h, 116 scc-group, 115 scc-group-h, 115 set-cvznx, 39 set-cvznx-c, 39 set-cvznx-ccr, 39 set-cvznx-n, 39 set-cvznx-nat-rangep, 39 set-cvznx-v, 39 set-cvznx-x, 39 set-cvznx-z, 39 set-set-cvznx1, 39 set-set-cvznx2, 39 slen, 133, 134 slen-01, 133 slen-add1, 133 slen-lbound, 133 slen-put, 133 slen-put0, 133 slen-rec, 134 slen-ubound, 133 splus, 73 stepi, 73, 116 stepi-h, 116 stepi-p, 116 stepn, 73, 106, 107, 116, 117 stepn-h, 116 stepn-lemma, 73 stepn-mcode-addrp, 117 stepn-mem-ilst, 107 stepn-mem-lst, 106 stepn-pc-read-mem, 117 stepn-pc-read-memp, 116 stepn-ram-addrp, 117 stepn-read-mem, 117 stepn-read-memp, 116 stepn-readm-mem, 106 stepn-rewriter, 73 stepn-rewriter0, 73 stepn-rom-addrp, 117 stepn-write-memp, 117 strcat, 123 strchr, 125, 129, 134 strchr*, 129 strchr-bounds, 134 strchr1, 125, 126, 129, 130 strchr1*, 129, 130 strchr1-bounds, 125 strchr1-false-0, 125 strcmp, 123 strcoll, 123 strcpy, 122 strcpy1, 123 strcpy2, 123, 124 strcspn, 125, 131, 135 strcspn*, 129, 131 strcspn-bounds, 135 stringp, 133, 134 stringp-la, 134 strlen, 122–124, 126, 130 strlen*, 128 strncat, 124 strncmp, 124, 126, 130 strncmp1, 124 strncpy, 124 strncpy1, 124 strpbrk, 126, 134 strpbrk*, 129 strpbrk-bounds, 134 strrchr, 125, 134 strrchr*, 129 strrchr-bounds, 134 strspn, 126, 130–132, 134, 135 strspn*, 130, 132 strspn-bounds, 135 strspn-ubound, 134 strstr, 126 strstr*, 130 strstr-bounds, 134 strstr1, 126, 134 strstr1*, 130 strtok-last, 132 strtok-last0, 131 strtok-last1, 131, 132 strtok-lst, 131 strtok-lst0, 131 strtok-lst1, 131 strtok-lst2, 131 strtok-tok, 130 strxfrm, 132 strxfrm1, 132 sub, 2, 23, 26–29, 54, 56, 75, 118 sub-0, 26 sub-add, 28 sub-adder, 27 sub-bcs&cc, 65 sub-beq-ext, 60 sub-beq-int-0, 60 sub-beq-int-1, 60 sub-beq-uint, 60 sub-bge, 70 sub-bgt, 71 sub-bhi-0, 59 sub-bhi-1, 59 sub-bhi-int, 58 sub-ble, 71 sub-bls, 59 sub-blt, 70 sub-bmi, 68 sub-bvs&vc, 67 sub-c, 50, 58, 59, 65 sub-c-bitp, 50 sub-cancel, 28 sub-cancel0, 28 sub-equal-0, 27 sub-group, 115 sub-group-h, 115 sub-int, 30 sub-leq-1, 54 sub-leq-2, 54 sub-leq-la, 26 sub-n, 50, 68, 70, 71 sub-n-bitp, 50 sub-nat-la, 23 sub-nat-rangep, 27 sub-neg, 54 sub-sub, 28 sub-sub1, 28 sub-subx-c, 58 sub-subx-v, 66 sub-uint, 25 sub-v, 50, 66, 67, 70, 71 sub-v-bitp, 50 sub-x-x, 26 sub-z, 50, 58–60, 71 sub-z-bitp, 50 sub-z-la, 58 sub-z-la1, 71 sub1-int-rangep, 17 sub1-nat-rangep, 37 sub1-times2-nat-rangep, 37 subbagp, 55 subtracter, 24, 26, 30 subtracter-int, 30 subtracter-nat-la, 24 subtracter-nat-rangep, 26 subtracter-uint, 24 subx-addx-v, 66 subx-c, 50, 58 subx-c-bitp, 50 subx-c-la, 58 subx-n, 50 subx-n-bitp, 50 subx-v, 50, 66 subx-v-bitp, 50 subx-v-la, 66 subx-z, 50 subx-z-bitp, 50 swap, 121 swap-n, 53 swap-n-bitp, 53 swap-z, 53 swap-z-bitp, 53

t3, 114, 116, 117 tail, 8, 9, 31–34, 37, 49, 65, 90, 91,

95, 96 tail-0, 8 tail-app, 32 tail-equal-0, 9 tail-head, 32 tail-lemma, 9 tail-leq, 8 tail-lessp, 8 tail-lst, 79, 80 tail-mbit, 65 tail-nat-rangep, 37 tail-of-0, 8 tail-replace, 32 tail-tail, 31 times-exp2-nat-rangep, 37 times-lessp-cancel1, 99 times-lessp 1, 20 times-lessp 2, 21 times-lessp 3, 21 times-lessp 4, 21 times-plus-lessp-cancel, 86 times-sub1, 11

uint-rangep, 9, 15, 16, 20, 23, 48, 62, 63, 65, 95–99, 101

uint-rangep-la, 15 uint-to-nat, 15 uint-to-nat-rangep, 15 uint-to-nat-to-uint, 15 uread-an, 118 uread-dn, 118 uread-mem, 118

vec, 3, 4, 6

write, 36, 44

write-else-mem-ilst, 95 write-else-mem-lst, 94 write-mem, 36, 46–49, 73, 74, 81,

90, 94–99, 101, 114, 115 write-mem-byte-write, 49 write-mem-ilst, 97 write-mem-ilst-asl, 99 write-mem-ilst-int, 98 write-mem-ilst0, 97 write-mem-lst, 96 write-mem-lst-asl, 98 write-mem-lst-int, 97 write-mem-lst-la, 95 write-mem-lst0, 97 write-mem-maintain-byte-readp, 46 write-mem-maintain-byte-writep, 47 write-mem-maintain-movep-writep, 115 write-mem-maintain-pc-byte-readp,

46 write-mem-maintain-pc-read-memp,

47 write-mem-maintain-ram-addrp, 74 write-mem-maintain-read-memp, 47 write-mem-maintain-rom-addrp, 73 write-mem-maintain-write-memp, 47 write-mem-mcode-addrp, 81 write-memp, 2, 36, 47, 74, 75, 77,

81, 90, 100, 114, 116, 117, 136

write-memp->read-memp, 47 write-memp-la0, 74 write-memp-la1, 74 write-memp-la2, 74 write-memp-la3, 75 write-memp-ram0, 77 write-memp-ram1, 77 write-memp-ram1-asl, 99 write-memp-ram1-int, 77 write-memp-ram1-uint, 136 write-memp-ram2, 77 write-memp-ram3, 77 write-rn, 41–43 write-rn-len, 42 write-write, 44 write-write-induct, 49 write-write-la, 44 write-write-mem, 49 write-write-rn, 42 writem-else-mem-ilst, 101 writem-else-mem-lst, 100 writem-mem, 100, 101, 116 writem-mem-h, 116 writem-mem-maintain-byte-readp, 100 writem-mem-maintain-byte-writep, 100 writem-mem-maintain-pc-byte-rea

dp, 100 writem-mem-maintain-pc-read-memp,

100 writem-mem-maintain-ram-addrp, 100 writem-mem-maintain-read-memp, 100 writem-mem-maintain-rom-addrp, 100 writem-mem-maintain-write-memp,

100 writem-mem-mcode-addrp, 100 writem-rn, 42 writep, 36, 43, 44 writep->readp, 43

z-flag-la, 63 zero-list, 124 zero-list1, 124