(NOTE-LIB "mc20-0" T)
Loading ./yu/mc20-0.lib
Finished loading ./yu/mc20-0.lib
Loading ./yu/mc20-0.o
Finished loading ./yu/mc20-0.o
(#./yu/mc20-0.lib #./yu/mc20-0)
(DEFN B NIL 8)
From the definition we can conclude that (NUMBERP (B)) is a theorem.
[ 0.0 0.0 0.0 ]
B
(DEFN W NIL 16)
From the definition we can conclude that (NUMBERP (W)) is a theorem.
[ 0.0 0.0 0.0 ]
W
(DEFN L NIL 32)
From the definition we can conclude that (NUMBERP (L)) is a theorem.
[ 0.0 0.0 0.0 ]
L
(DEFN Q NIL 64)
From the definition we can conclude that (NUMBERP (Q)) is a theorem.
[ 0.0 0.0 0.0 ]
Q
(DEFN BSZ NIL 1)
From the definition we can conclude that (NUMBERP (BSZ)) is a theorem.
[ 0.0 0.0 0.0 ]
BSZ
(DEFN WSZ NIL 2)
From the definition we can conclude that (NUMBERP (WSZ)) is a theorem.
[ 0.0 0.0 0.0 ]
WSZ
(DEFN LSZ NIL 4)
From the definition we can conclude that (NUMBERP (LSZ)) is a theorem.
[ 0.0 0.0 0.0 ]
LSZ
(DEFN QSZ NIL 8)
From the definition we can conclude that (NUMBERP (QSZ)) is a theorem.
[ 0.0 0.0 0.0 ]
QSZ
(DEFN READ-SIGNAL NIL 'READ_UNAVAILABLE_MEMORY)
From the definition we can conclude that (LITATOM (READ-SIGNAL)) is a
theorem.
[ 0.0 0.0 0.0 ]
READ-SIGNAL
(DEFN WRITE-SIGNAL NIL 'WRITE_ROM_OR_UNAVAILABLE_MEMORY)
From the definition we can conclude that (LITATOM (WRITE-SIGNAL)) is a
theorem.
[ 0.0 0.0 0.0 ]
WRITE-SIGNAL
(DEFN RESERVED-SIGNAL NIL 'MOTOROLA_RESERVED_FOR_FUTURE_DEVELOPMENT)
From the definition we can conclude that (LITATOM (RESERVED-SIGNAL)) is a
theorem.
[ 0.0 0.0 0.0 ]
RESERVED-SIGNAL
(DEFN PC-SIGNAL NIL 'PC_OUTSIDE_ROM)
From the definition we can conclude that (LITATOM (PC-SIGNAL)) is a
theorem.
[ 0.0 0.0 0.0 ]
PC-SIGNAL
(DEFN PC-ODD-SIGNAL NIL 'PC_AT_ODD_ADDRESS)
From the definition we can conclude that (LITATOM (PC-ODD-SIGNAL)) is a
theorem.
[ 0.0 0.0 0.0 ]
PC-ODD-SIGNAL
(DEFN MODE-SIGNAL NIL 'ILLEGAL_ADDRESSING_MODE_IN_CURRENT_INSTRUCTION)
From the definition we can conclude that (LITATOM (MODE-SIGNAL)) is a
theorem.
[ 0.0 0.0 0.0 ]
MODE-SIGNAL
(DEFN BITP
(X)
(OR (EQUAL X 0) (EQUAL X 1)))
Observe that (OR (FALSEP (BITP X)) (TRUEP (BITP X))) is a theorem.
[ 0.0 0.0 0.0 ]
BITP
(DEFN B1 NIL 1)
From the definition we can conclude that (NUMBERP (B1)) is a theorem.
[ 0.0 0.0 0.0 ]
B1
(DEFN B0 NIL 0)
From the definition we can conclude that (NUMBERP (B0)) is a theorem.
[ 0.0 0.0 0.0 ]
B0
(DEFN B0P (X) (EQUAL X (B0)))
From the definition we can conclude that:
(OR (FALSEP (B0P X)) (TRUEP (B0P X)))
is a theorem.
[ 0.0 0.0 0.0 ]
B0P
(DEFN B1P (X) (NOT (EQUAL X (B0))))
Note that (OR (FALSEP (B1P X)) (TRUEP (B1P X))) is a theorem.
[ 0.0 0.0 0.0 ]
B1P
(DEFN FIX-BIT
(C)
(IF (B0P C) (B0) (B1)))
Note that (NUMBERP (FIX-BIT C)) is a theorem.
[ 0.0 0.0 0.0 ]
FIX-BIT
(DEFN B-NOT
(X)
(IF (B0P X) (B1) (B0)))
Note that (NUMBERP (B-NOT X)) is a theorem.
[ 0.0 0.0 0.0 ]
B-NOT
(DEFN B-AND
(X Y)
(IF (B0P X)
(B0)
(IF (B0P Y) (B0) (B1))))
Observe that (NUMBERP (B-AND X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
B-AND
(DEFN B-OR
(X Y)
(IF (B0P X)
(IF (B0P Y) (B0) (B1))
(B1)))
Observe that (NUMBERP (B-OR X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
B-OR
(DEFN B-NOR
(X Y)
(IF (B0P X)
(IF (B0P Y) (B1) (B0))
(B0)))
Observe that (NUMBERP (B-NOR X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
B-NOR
(DEFN B-NAND
(X Y)
(IF (B0P X)
(B1)
(IF (B0P Y) (B1) (B0))))
Observe that (NUMBERP (B-NAND X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
B-NAND
(DEFN B-EOR
(X Y)
(IF (B0P X)
(IF (B0P Y) (B0) (B1))
(IF (B0P Y) (B1) (B0))))
From the definition we can conclude that (NUMBERP (B-EOR X Y)) is a
theorem.
[ 0.0 0.0 0.0 ]
B-EOR
(DEFN B-EQUAL
(X Y)
(IF (B0P X) (B0P Y) (B1P Y)))
Note that (OR (FALSEP (B-EQUAL X Y)) (TRUEP (B-EQUAL X Y))) is a theorem.
[ 0.0 0.0 0.0 ]
B-EQUAL
(DEFN BCAR (X) (REMAINDER X 2))
Observe that (NUMBERP (BCAR X)) is a theorem.
[ 0.0 0.0 0.0 ]
BCAR
(DEFN BCDR (X) (QUOTIENT X 2))
Observe that (NUMBERP (BCDR X)) is a theorem.
[ 0.0 0.0 0.0 ]
BCDR
(DEFN HEAD
(X N)
(REMAINDER X (EXP 2 N)))
From the definition we can conclude that (NUMBERP (HEAD X N)) is a
theorem.
[ 0.0 0.0 0.0 ]
HEAD
(DEFN TAIL
(X N)
(QUOTIENT X (EXP 2 N)))
From the definition we can conclude that (NUMBERP (TAIL X N)) is a
theorem.
[ 0.0 0.0 0.0 ]
TAIL
(DEFN LOGNOT
(N X)
(SUB1 (DIFFERENCE (EXP 2 N) (HEAD X N))))
Note that (NUMBERP (LOGNOT N X)) is a theorem.
[ 0.0 0.0 0.0 ]
LOGNOT
(DEFN LOGAND
(X Y)
(IF (OR (ZEROP X) (ZEROP Y))
0
(PLUS (B-AND (BCAR X) (BCAR Y))
(TIMES 2
(LOGAND (BCDR X) (BCDR Y))))))
Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, and
COUNT-NUMBERP, and the definitions of NUMBERP, EQUAL, BCDR, OR, and ZEROP
inform us that the measure (COUNT X) decreases according to the well-founded
relation LESSP in each recursive call. Hence, LOGAND is accepted under the
principle of definition. The definition of LOGAND can be justified in another
way. Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, and
COUNT-NUMBERP, and the definitions of NUMBERP, EQUAL, BCDR, OR, and ZEROP
establish that the measure (COUNT Y) decreases according to the well-founded
relation LESSP in each recursive call. Observe that (NUMBERP (LOGAND X Y)) is
a theorem.
[ 0.0 0.0 0.0 ]
LOGAND
(DEFN LOGOR
(X Y)
(IF (ZEROP X)
(FIX Y)
(IF (ZEROP Y)
(FIX X)
(PLUS (B-OR (BCAR X) (BCAR Y))
(TIMES 2
(LOGOR (BCDR X) (BCDR Y)))))))
Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, and
COUNT-NUMBERP, and the definitions of NUMBERP, EQUAL, BCDR, and ZEROP inform
us that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each recursive call. Hence, LOGOR is accepted under the definitional
principle. The definition of LOGOR can be justified in another way. Linear
arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, and COUNT-NUMBERP,
and the definitions of NUMBERP, EQUAL, BCDR, and ZEROP establish that the
measure (COUNT Y) decreases according to the well-founded relation LESSP in
each recursive call. Note that (NUMBERP (LOGOR X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
LOGOR
(DEFN LOGEOR
(X Y)
(IF (AND (ZEROP X) (ZEROP Y))
0
(PLUS (B-EOR (BCAR X) (BCAR Y))
(TIMES 2 (LOGEOR (BCDR X) (BCDR Y)))))
((LESSP (PLUS X Y))))
Linear arithmetic, the lemmas QUOTIENT-LEQ and QUOTIENT-LESSP-LINEAR, and
the definitions of BCDR, AND, ZEROP, and LESSP inform us that the measure
(PLUS X Y) decreases according to the well-founded relation LESSP in each
recursive call. Hence, LOGEOR is accepted under the principle of definition.
Note that (NUMBERP (LOGEOR X Y)) is a theorem.
[ 0.0 0.1 0.0 ]
LOGEOR
(DEFN BITN (X N) (BCAR (TAIL X N)))
Note that (NUMBERP (BITN X N)) is a theorem.
[ 0.0 0.0 0.0 ]
BITN
(DEFN MBIT (X N) (BITN X (SUB1 N)))
Note that (NUMBERP (MBIT X N)) is a theorem.
[ 0.0 0.0 0.0 ]
MBIT
(DEFN BITS
(X I J)
(HEAD (TAIL X I)
(ADD1 (DIFFERENCE J I))))
Observe that (NUMBERP (BITS X I J)) is a theorem.
[ 0.0 0.0 0.0 ]
BITS
(DEFN SETN
(X N C)
(IF (ZEROP N)
(PLUS (FIX-BIT C) (TIMES 2 (BCDR X)))
(PLUS (BCAR X)
(TIMES 2
(SETN (BCDR X) (SUB1 N) C)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, SETN is accepted under the
principle of definition. Note that (NUMBERP (SETN X N C)) is a theorem.
[ 0.0 0.0 0.0 ]
SETN
(DEFN ADDER
(N C X Y)
(HEAD (PLUS C X Y) N))
From the definition we can conclude that (NUMBERP (ADDER N C X Y)) is a
theorem.
[ 0.0 0.0 0.0 ]
ADDER
(DEFN ADD (N X Y) (HEAD (PLUS X Y) N))
Note that (NUMBERP (ADD N X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
ADD
(DEFN SUBTRACTER
(N C X Y)
(ADDER N (B-NOT C) Y (LOGNOT N X)))
Observe that (NUMBERP (SUBTRACTER N C X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
SUBTRACTER
(DEFN SUB
(N X Y)
(HEAD (PLUS Y
(DIFFERENCE (EXP 2 N) (HEAD X N)))
N))
Note that (NUMBERP (SUB N X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
SUB
(DEFN APP
(N X Y)
(PLUS (HEAD X N) (TIMES Y (EXP 2 N))))
Observe that (NUMBERP (APP N X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
APP
(DEFN REPLACE
(N X Y)
(APP N X (TAIL Y N)))
From the definition we can conclude that (NUMBERP (REPLACE N X Y)) is a
theorem.
[ 0.0 0.0 0.0 ]
REPLACE
(DEFN EXT
(N X SIZE)
(IF (LESSP N SIZE)
(IF (B0P (BITN X (SUB1 N)))
(HEAD X N)
(APP N X
(SUB1 (EXP 2 (DIFFERENCE SIZE N)))))
(HEAD X SIZE)))
From the definition we can conclude that (NUMBERP (EXT N X SIZE)) is a
theorem.
[ 0.0 0.0 0.0 ]
EXT
(DEFN LSL
(LEN X CNT)
(HEAD (TIMES X (EXP 2 CNT)) LEN))
Observe that (NUMBERP (LSL LEN X CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
LSL
(DEFN ASL
(LEN X CNT)
(HEAD (TIMES X (EXP 2 CNT)) LEN))
Observe that (NUMBERP (ASL LEN X CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ASL
(DEFN LSR (X CNT) (TAIL X CNT))
From the definition we can conclude that (NUMBERP (LSR X CNT)) is a
theorem.
[ 0.0 0.0 0.0 ]
LSR
(DEFN ASR
(N X CNT)
(IF (LESSP X (EXP 2 (SUB1 N)))
(TAIL X CNT)
(IF (LESSP N CNT)
(SUB1 (EXP 2 N))
(APP (DIFFERENCE N CNT)
(TAIL X CNT)
(SUB1 (EXP 2 CNT))))))
Note that (NUMBERP (ASR N X CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ASR
(DEFN NEGP
(I)
(AND (NEGATIVEP I)
(NOT (EQUAL I (MINUS 0)))))
From the definition we can conclude that:
(OR (FALSEP (NEGP I))
(TRUEP (NEGP I)))
is a theorem.
[ 0.0 0.0 0.0 ]
NEGP
(DEFN INTEGERP
(X)
(OR (NUMBERP X) (NEGP X)))
Observe that (OR (FALSEP (INTEGERP X)) (TRUEP (INTEGERP X))) is a theorem.
[ 0.0 0.0 0.0 ]
INTEGERP
(DEFN FIX-INT
(X)
(IF (INTEGERP X) X 0))
Note that (OR (NUMBERP (FIX-INT X)) (EQUAL (FIX-INT X) X)) is a theorem.
[ 0.0 0.0 0.0 ]
FIX-INT
(DEFN IZEROP
(X)
(EQUAL (FIX-INT X) 0))
Observe that (OR (FALSEP (IZEROP X)) (TRUEP (IZEROP X))) is a theorem.
[ 0.0 0.0 0.0 ]
IZEROP
(DEFN ABS
(X)
(IF (NEGP X)
(NEGATIVE-GUTS X)
(FIX X)))
Observe that (NUMBERP (ABS X)) is a theorem.
[ 0.0 0.0 0.0 ]
ABS
(DEFN ILESSP
(I J)
(IF (NEGP I)
(IF (NEGP J)
(LESSP (NEGATIVE-GUTS J)
(NEGATIVE-GUTS I))
T)
(IF (NEGP J) F (LESSP I J))))
Note that (OR (FALSEP (ILESSP I J)) (TRUEP (ILESSP I J))) is a theorem.
[ 0.0 0.0 0.0 ]
ILESSP
(DEFN ILEQ (I J) (NOT (ILESSP J I)))
Note that (OR (FALSEP (ILEQ I J)) (TRUEP (ILEQ I J))) is a theorem.
[ 0.0 0.0 0.0 ]
ILEQ
(DEFN IPLUS
(X Y)
(IF (NEGP X)
(IF (NEGP Y)
(MINUS (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))
(IF (LESSP Y (NEGATIVE-GUTS X))
(MINUS (DIFFERENCE (NEGATIVE-GUTS X) Y))
(DIFFERENCE Y (NEGATIVE-GUTS X))))
(IF (NEGP Y)
(IF (LESSP X (NEGATIVE-GUTS Y))
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y) X))
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(PLUS X Y))))
From the definition we can conclude that:
(OR (NUMBERP (IPLUS X Y))
(NEGATIVEP (IPLUS X Y)))
is a theorem.
[ 0.0 0.0 0.0 ]
IPLUS
(DEFN INEG
(X)
(IF (IZEROP X)
0
(IF (NEGP X)
(NEGATIVE-GUTS X)
(MINUS X))))
From the definition we can conclude that:
(OR (NUMBERP (INEG X))
(NEGATIVEP (INEG X)))
is a theorem.
[ 0.0 0.0 0.0 ]
INEG
(DEFN IDIFFERENCE
(X Y)
(IPLUS X (INEG Y)))
Note that (OR (NUMBERP (IDIFFERENCE X Y)) (NEGATIVEP (IDIFFERENCE X Y)))
is a theorem.
[ 0.0 0.0 0.0 ]
IDIFFERENCE
(DEFN ITIMES
(X Y)
(IF (NEGP X)
(IF (NEGP Y)
(TIMES (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
(FIX-INT (MINUS (TIMES (NEGATIVE-GUTS X) Y))))
(IF (NEGP Y)
(FIX-INT (MINUS (TIMES X (NEGATIVE-GUTS Y))))
(TIMES X Y))))
Note that (OR (NUMBERP (ITIMES X Y)) (NEGATIVEP (ITIMES X Y))) is a
theorem.
[ 0.0 0.0 0.0 ]
ITIMES
(DEFN IREMAINDER
(X Y)
(IF (NEGP X)
(FIX-INT (MINUS (REMAINDER (NEGATIVE-GUTS X)
(ABS Y))))
(REMAINDER X (ABS Y))))
From the definition we can conclude that:
(OR (NUMBERP (IREMAINDER X Y))
(NEGATIVEP (IREMAINDER X Y)))
is a theorem.
[ 0.0 0.0 0.0 ]
IREMAINDER
(DEFN IQUOTIENT
(X Y)
(IF (NEGP X)
(IF (NEGP Y)
(QUOTIENT (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
(FIX-INT (MINUS (QUOTIENT (NEGATIVE-GUTS X) Y))))
(IF (NEGP Y)
(FIX-INT (MINUS (QUOTIENT X (NEGATIVE-GUTS Y))))
(QUOTIENT X Y))))
Note that (OR (NUMBERP (IQUOTIENT X Y)) (NEGATIVEP (IQUOTIENT X Y))) is a
theorem.
[ 0.0 0.0 0.0 ]
IQUOTIENT
(DEFN NAT-RANGEP
(NAT N)
(LESSP NAT (EXP 2 N)))
From the definition we can conclude that:
(OR (FALSEP (NAT-RANGEP NAT N))
(TRUEP (NAT-RANGEP NAT N)))
is a theorem.
[ 0.0 0.0 0.0 ]
NAT-RANGEP
(DEFN UINT-RANGEP
(X N)
(LESSP X (EXP 2 N)))
From the definition we can conclude that:
(OR (FALSEP (UINT-RANGEP X N))
(TRUEP (UINT-RANGEP X N)))
is a theorem.
[ 0.0 0.0 0.0 ]
UINT-RANGEP
(DEFN NAT-TO-UINT (X) (FIX X))
Observe that (NUMBERP (NAT-TO-UINT X)) is a theorem.
[ 0.0 0.0 0.0 ]
NAT-TO-UINT
(DEFN UINT-TO-NAT (X) (FIX X))
Observe that (NUMBERP (UINT-TO-NAT X)) is a theorem.
[ 0.0 0.0 0.0 ]
UINT-TO-NAT
(DEFN INT-RANGEP
(INT N)
(IF (ZEROP N)
(EQUAL (FIX-INT INT) 0)
(IF (NEGATIVEP INT)
(LEQ (NEGATIVE-GUTS INT)
(EXP 2 (SUB1 N)))
(LESSP INT (EXP 2 (SUB1 N))))))
Note that (OR (FALSEP (INT-RANGEP INT N)) (TRUEP (INT-RANGEP INT N))) is
a theorem.
[ 0.0 0.0 0.0 ]
INT-RANGEP
(DEFN NAT-TO-INT
(X N)
(IF (LESSP X (EXP 2 (SUB1 N)))
(FIX X)
(MINUS (DIFFERENCE (EXP 2 N) X))))
Observe that (OR (NUMBERP (NAT-TO-INT X N)) (NEGATIVEP (NAT-TO-INT X N)))
is a theorem.
[ 0.0 0.0 0.0 ]
NAT-TO-INT
(DEFN INT-TO-NAT
(X SIZE)
(IF (NEGATIVEP X)
(DIFFERENCE (EXP 2 SIZE)
(NEGATIVE-GUTS X))
(FIX X)))
Note that (NUMBERP (INT-TO-NAT X SIZE)) is a theorem.
[ 0.0 0.0 0.0 ]
INT-TO-NAT
(DEFN VALUE-FIELD
(BT)
(IF (LISTP BT) (CAR BT) 0))
[ 0.0 0.0 0.0 ]
VALUE-FIELD
(DEFN BRANCH0
(BT)
(IF (LISTP BT) (CADR BT) NIL))
[ 0.0 0.0 0.0 ]
BRANCH0
(DEFN BRANCH1
(BT)
(IF (AND (LISTP BT) (LISTP (CDR BT)))
(CDDR BT)
NIL))
[ 0.0 0.0 0.0 ]
BRANCH1
(DEFN MAKE-BT
(VALUE BR0 BR1)
(CONS VALUE (CONS BR0 BR1)))
Note that (LISTP (MAKE-BT VALUE BR0 BR1)) is a theorem.
[ 0.0 0.0 0.0 ]
MAKE-BT
(DEFN READP
(X N MAP)
(IF (MEMBER 'UNAVAILABLE
(VALUE-FIELD MAP))
F
(IF (OR (NLISTP MAP) (ZEROP N))
T
(IF (B0P (BITN X (SUB1 N)))
(READP X (SUB1 N) (BRANCH0 MAP))
(READP X (SUB1 N) (BRANCH1 MAP)))))
((LESSP (COUNT N))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definitions of B0P, B0,
BITN, TAIL, BCAR, OR, ZEROP, NLISTP, and VALUE-FIELD establish that the
measure (COUNT N) decreases according to the well-founded relation LESSP in
each recursive call. Hence, READP is accepted under the principle of
definition. From the definition we can conclude that:
(OR (FALSEP (READP X N MAP))
(TRUEP (READP X N MAP)))
is a theorem.
[ 0.0 0.1 0.0 ]
READP
(DEFN PC-READP
(X N MAP)
(IF (MEMBER 'UNAVAILABLE
(VALUE-FIELD MAP))
F
(IF (MEMBER 'ROM (VALUE-FIELD MAP))
(READP X N MAP)
(IF (OR (NLISTP MAP) (ZEROP N))
F
(IF (B0P (BITN X (SUB1 N)))
(PC-READP X (SUB1 N) (BRANCH0 MAP))
(PC-READP X
(SUB1 N)
(BRANCH1 MAP))))))
((LESSP (COUNT N))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definitions of B0P, B0,
BITN, TAIL, BCAR, OR, ZEROP, NLISTP, MEMBER, and VALUE-FIELD inform us that
the measure (COUNT N) decreases according to the well-founded relation LESSP
in each recursive call. Hence, PC-READP is accepted under the definitional
principle. Note that:
(OR (FALSEP (PC-READP X N MAP))
(TRUEP (PC-READP X N MAP)))
is a theorem.
[ 0.0 0.1 0.0 ]
PC-READP
(DEFN WRITEP
(X N MAP)
(IF (OR (MEMBER 'UNAVAILABLE
(VALUE-FIELD MAP))
(MEMBER 'ROM (VALUE-FIELD MAP)))
F
(IF (OR (NLISTP MAP) (ZEROP N))
T
(IF (B0P (BITN X (SUB1 N)))
(WRITEP X (SUB1 N) (BRANCH0 MAP))
(WRITEP X (SUB1 N) (BRANCH1 MAP)))))
((LESSP (COUNT N))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definitions of B0P, B0,
BITN, TAIL, BCAR, ZEROP, NLISTP, OR, and VALUE-FIELD inform us that the
measure (COUNT N) decreases according to the well-founded relation LESSP in
each recursive call. Hence, WRITEP is accepted under the principle of
definition. From the definition we can conclude that:
(OR (FALSEP (WRITEP X N MAP))
(TRUEP (WRITEP X N MAP)))
is a theorem.
[ 0.0 0.1 0.0 ]
WRITEP
(DEFN READ
(X N BT)
(IF (ZEROP N)
(VALUE-FIELD BT)
(IF (B0P (BITN X (SUB1 N)))
(READ X (SUB1 N) (BRANCH0 BT))
(READ X (SUB1 N) (BRANCH1 BT)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definitions of B0P, B0,
BITN, TAIL, BCAR, and ZEROP can be used to prove that the measure (COUNT N)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, READ is accepted under the principle of definition.
[ 0.0 0.1 0.0 ]
READ
(DEFN PC-READ (X N BT) (READ X N BT))
[ 0.0 0.0 0.0 ]
PC-READ
(DEFN WRITE
(VALUE X N BT)
(IF (ZEROP N)
(MAKE-BT VALUE
(BRANCH0 BT)
(BRANCH1 BT))
(IF (B0P (BITN X (SUB1 N)))
(MAKE-BT (VALUE-FIELD BT)
(WRITE VALUE X (SUB1 N) (BRANCH0 BT))
(BRANCH1 BT))
(MAKE-BT (VALUE-FIELD BT)
(BRANCH0 BT)
(WRITE VALUE X
(SUB1 N)
(BRANCH1 BT))))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definitions of B0P, B0,
BITN, TAIL, BCAR, and ZEROP can be used to establish that the measure
(COUNT N) decreases according to the well-founded relation LESSP in each
recursive call. Hence, WRITE is accepted under the definitional principle.
Observe that (LISTP (WRITE VALUE X N BT)) is a theorem.
[ 0.0 0.1 0.0 ]
WRITE
(DEFN GET-NTH
(N LST)
(IF (ZEROP N)
(CAR LST)
(GET-NTH (SUB1 N) (CDR LST))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, GET-NTH is accepted under the
principle of definition.
[ 0.0 0.0 0.0 ]
GET-NTH
(DEFN PUT-NTH
(VALUE N LST)
(IF (ZEROP N)
(CONS VALUE (CDR LST))
(CONS (CAR LST)
(PUT-NTH VALUE (SUB1 N) (CDR LST)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP can
be used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call. Hence, PUT-NTH is
accepted under the definitional principle. Observe that:
(LISTP (PUT-NTH VALUE N LST))
is a theorem.
[ 0.0 0.0 0.0 ]
PUT-NTH
(DEFN OP-SZ
(OPLEN)
(QUOTIENT OPLEN (B)))
From the definition we can conclude that (NUMBERP (OP-SZ OPLEN)) is a
theorem.
[ 0.0 0.0 0.0 ]
OP-SZ
(DEFN READ-RN
(OPLEN RN REGS)
(HEAD (GET-NTH RN REGS) OPLEN))
Note that (NUMBERP (READ-RN OPLEN RN REGS)) is a theorem.
[ 0.0 0.0 0.0 ]
READ-RN
(DEFN WRITE-RN
(OPLEN VALUE RN REGS)
(PUT-NTH (REPLACE OPLEN VALUE
(GET-NTH RN REGS))
RN REGS))
Note that (LISTP (WRITE-RN OPLEN VALUE RN REGS)) is a theorem.
[ 0.0 0.0 0.0 ]
WRITE-RN
(DEFN MC-STATE
(STATUS REGS PC CCR MEM)
(LIST STATUS REGS PC CCR MEM))
Observe that (LISTP (MC-STATE STATUS REGS PC CCR MEM)) is a theorem.
[ 0.0 0.0 0.0 ]
MC-STATE
(DEFN MC-STATUS (S) (CAR S))
[ 0.0 0.0 0.0 ]
MC-STATUS
(DEFN MC-RFILE (S) (CADR S))
[ 0.0 0.0 0.0 ]
MC-RFILE
(DEFN MC-PC (S) (HEAD (CADDR S) (L)))
Observe that (NUMBERP (MC-PC S)) is a theorem.
[ 0.0 0.0 0.0 ]
MC-PC
(DEFN MC-CCR
(S)
(HEAD (CADDDR S) (B)))
From the definition we can conclude that (NUMBERP (MC-CCR S)) is a
theorem.
[ 0.0 0.0 0.0 ]
MC-CCR
(DEFN MC-MEM (S) (CADDDDR S))
[ 0.0 0.0 0.0 ]
MC-MEM
(DEFN LEN
(LST)
(IF (NLISTP LST)
0
(ADD1 (LEN (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
LEN is accepted under the principle of definition. From the definition we can
conclude that (NUMBERP (LEN LST)) is a theorem.
[ 0.0 0.0 0.0 ]
LEN
(DEFN MC-HALTP
(S)
(NOT (EQUAL (MC-STATUS S) 'RUNNING)))
From the definition we can conclude that:
(OR (FALSEP (MC-HALTP S))
(TRUEP (MC-HALTP S)))
is a theorem.
[ 0.0 0.0 0.0 ]
MC-HALTP
(DEFN BYTE-READP
(X MEM)
(READP X 32 (CAR MEM)))
From the definition we can conclude that:
(OR (FALSEP (BYTE-READP X MEM))
(TRUEP (BYTE-READP X MEM)))
is a theorem.
[ 0.0 0.0 0.0 ]
BYTE-READP
(DEFN READ-MEMP
(X MEM K)
(IF (ZEROP K)
T
(AND (BYTE-READP (ADD 32 X (SUB1 K)) MEM)
(READ-MEMP X MEM (SUB1 K)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
establish that the measure (COUNT K) decreases according to the well-founded
relation LESSP in each recursive call. Hence, READ-MEMP is accepted under the
principle of definition. From the definition we can conclude that:
(OR (FALSEP (READ-MEMP X MEM K))
(TRUEP (READ-MEMP X MEM K)))
is a theorem.
[ 0.0 0.0 0.0 ]
READ-MEMP
(DEFN WORD-READP
(X MEM)
(READ-MEMP X MEM (WSZ)))
Note that (OR (FALSEP (WORD-READP X MEM)) (TRUEP (WORD-READP X MEM))) is
a theorem.
[ 0.0 0.0 0.0 ]
WORD-READP
(DEFN LONG-READP
(X MEM)
(READ-MEMP X MEM (LSZ)))
Note that (OR (FALSEP (LONG-READP X MEM)) (TRUEP (LONG-READP X MEM))) is
a theorem.
[ 0.0 0.0 0.0 ]
LONG-READP
(DEFN PC-BYTE-READP
(X MEM)
(PC-READP X 32 (CAR MEM)))
From the definition we can conclude that:
(OR (FALSEP (PC-BYTE-READP X MEM))
(TRUEP (PC-BYTE-READP X MEM)))
is a theorem.
[ 0.0 0.0 0.0 ]
PC-BYTE-READP
(DEFN PC-READ-MEMP
(X MEM K)
(IF (ZEROP K)
T
(AND (PC-BYTE-READP (ADD 32 X (SUB1 K))
MEM)
(PC-READ-MEMP X MEM (SUB1 K)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
establish that the measure (COUNT K) decreases according to the well-founded
relation LESSP in each recursive call. Hence, PC-READ-MEMP is accepted under
the principle of definition. From the definition we can conclude that:
(OR (FALSEP (PC-READ-MEMP X MEM K))
(TRUEP (PC-READ-MEMP X MEM K)))
is a theorem.
[ 0.0 0.0 0.0 ]
PC-READ-MEMP
(DEFN PC-WORD-READP
(X MEM)
(PC-READ-MEMP X MEM (WSZ)))
Note that:
(OR (FALSEP (PC-WORD-READP X MEM))
(TRUEP (PC-WORD-READP X MEM)))
is a theorem.
[ 0.0 0.0 0.0 ]
PC-WORD-READP
(DEFN PC-LONG-READP
(X MEM)
(PC-READ-MEMP X MEM (LSZ)))
Note that:
(OR (FALSEP (PC-LONG-READP X MEM))
(TRUEP (PC-LONG-READP X MEM)))
is a theorem.
[ 0.0 0.0 0.0 ]
PC-LONG-READP
(DEFN BYTE-READ
(X MEM)
(HEAD (READ X 32 (CDR MEM)) (B)))
Observe that (NUMBERP (BYTE-READ X MEM)) is a theorem.
[ 0.0 0.0 0.0 ]
BYTE-READ
(DEFN READ-MEM
(X MEM K)
(IF (ZEROP K)
0
(APP (B)
(BYTE-READ (ADD 32 X (SUB1 K)) MEM)
(READ-MEM X MEM (SUB1 K)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
establish that the measure (COUNT K) decreases according to the well-founded
relation LESSP in each recursive call. Hence, READ-MEM is accepted under the
principle of definition. Note that (NUMBERP (READ-MEM X MEM K)) is a theorem.
[ 0.0 0.0 0.0 ]
READ-MEM
(DEFN WORD-READ
(X MEM)
(READ-MEM X MEM (WSZ)))
Note that (NUMBERP (WORD-READ X MEM)) is a theorem.
[ 0.0 0.0 0.0 ]
WORD-READ
(DEFN LONG-READ
(X MEM)
(READ-MEM X MEM (LSZ)))
Note that (NUMBERP (LONG-READ X MEM)) is a theorem.
[ 0.0 0.0 0.0 ]
LONG-READ
(DEFN PC-BYTE-READ
(PC MEM)
(HEAD (PC-READ PC 32 (CDR MEM)) (B)))
Observe that (NUMBERP (PC-BYTE-READ PC MEM)) is a theorem.
[ 0.0 0.0 0.0 ]
PC-BYTE-READ
(DEFN PC-READ-MEM
(PC MEM K)
(IF (ZEROP K)
0
(APP (B)
(PC-BYTE-READ (ADD 32 PC (SUB1 K))
MEM)
(PC-READ-MEM PC MEM (SUB1 K)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
establish that the measure (COUNT K) decreases according to the well-founded
relation LESSP in each recursive call. Hence, PC-READ-MEM is accepted under
the principle of definition. Note that (NUMBERP (PC-READ-MEM PC MEM K)) is a
theorem.
[ 0.0 0.0 0.0 ]
PC-READ-MEM
(DEFN PC-WORD-READ
(PC MEM)
(PC-READ-MEM PC MEM (WSZ)))
Note that (NUMBERP (PC-WORD-READ PC MEM)) is a theorem.
[ 0.0 0.0 0.0 ]
PC-WORD-READ
(DEFN PC-LONG-READ
(PC MEM)
(PC-READ-MEM PC MEM (LSZ)))
Note that (NUMBERP (PC-LONG-READ PC MEM)) is a theorem.
[ 0.0 0.0 0.0 ]
PC-LONG-READ
(DEFN S_RN (INS) (BITS INS 0 2))
Note that (NUMBERP (S_RN INS)) is a theorem.
[ 0.0 0.0 0.0 ]
S_RN
(DEFN S_MODE (INS) (BITS INS 3 5))
Note that (NUMBERP (S_MODE INS)) is a theorem.
[ 0.0 0.0 0.0 ]
S_MODE
(DEFN D_MODE (INS) (BITS INS 6 8))
Note that (NUMBERP (D_MODE INS)) is a theorem.
[ 0.0 0.0 0.0 ]
D_MODE
(DEFN D_RN (INS) (BITS INS 9 11))
Note that (NUMBERP (D_RN INS)) is a theorem.
[ 0.0 0.0 0.0 ]
D_RN
(DEFN OPMODE-FIELD
(INS)
(BITS INS 6 8))
Note that (NUMBERP (OPMODE-FIELD INS)) is a theorem.
[ 0.0 0.0 0.0 ]
OPMODE-FIELD
(DEFN COND-FIELD
(INS)
(BITS INS 8 11))
Note that (NUMBERP (COND-FIELD INS)) is a theorem.
[ 0.0 0.0 0.0 ]
COND-FIELD
(DEFN OP-LEN
(INS)
(TIMES (B) (EXP 2 (BITS INS 6 7))))
Note that (NUMBERP (OP-LEN INS)) is a theorem.
[ 0.0 0.0 0.0 ]
OP-LEN
(DEFN BYTE-WRITEP
(X MEM)
(WRITEP X 32 (CAR MEM)))
From the definition we can conclude that:
(OR (FALSEP (BYTE-WRITEP X MEM))
(TRUEP (BYTE-WRITEP X MEM)))
is a theorem.
[ 0.0 0.0 0.0 ]
BYTE-WRITEP
(DEFN WRITE-MEMP
(X MEM K)
(IF (ZEROP K)
T
(AND (BYTE-WRITEP (ADD 32 X (SUB1 K)) MEM)
(WRITE-MEMP X MEM (SUB1 K)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
establish that the measure (COUNT K) decreases according to the well-founded
relation LESSP in each recursive call. Hence, WRITE-MEMP is accepted under
the principle of definition. From the definition we can conclude that:
(OR (FALSEP (WRITE-MEMP X MEM K))
(TRUEP (WRITE-MEMP X MEM K)))
is a theorem.
[ 0.0 0.0 0.0 ]
WRITE-MEMP
(DEFN BYTE-WRITE
(VALUE X MEM)
(CONS (CAR MEM)
(WRITE (HEAD VALUE (B))
X 32
(CDR MEM))))
From the definition we can conclude that (LISTP (BYTE-WRITE VALUE X MEM))
is a theorem.
[ 0.0 0.0 0.0 ]
BYTE-WRITE
(DEFN WRITE-MEM
(VALUE X MEM K)
(IF (ZEROP K)
MEM
(WRITE-MEM (TAIL VALUE (B))
X
(BYTE-WRITE VALUE
(ADD 32 X (SUB1 K))
MEM)
(SUB1 K))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
establish that the measure (COUNT K) decreases according to the well-founded
relation LESSP in each recursive call. Hence, WRITE-MEM is accepted under the
principle of definition. Note that:
(OR (LISTP (WRITE-MEM VALUE X MEM K))
(EQUAL (WRITE-MEM VALUE X MEM K) MEM))
is a theorem.
[ 0.0 0.0 0.0 ]
WRITE-MEM
(DEFN CCR-C (CCR) (BITN CCR 0))
Observe that (NUMBERP (CCR-C CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
CCR-C
(DEFN CCR-V (CCR) (BITN CCR 1))
Observe that (NUMBERP (CCR-V CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
CCR-V
(DEFN CCR-Z (CCR) (BITN CCR 2))
Observe that (NUMBERP (CCR-Z CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
CCR-Z
(DEFN CCR-N (CCR) (BITN CCR 3))
Observe that (NUMBERP (CCR-N CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
CCR-N
(DEFN CCR-X (CCR) (BITN CCR 4))
Observe that (NUMBERP (CCR-X CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
CCR-X
(DEFN CVZNX
(C V Z N X)
(PLUS (FIX-BIT C)
(PLUS (TIMES 2 (FIX-BIT V))
(PLUS (TIMES 4 (FIX-BIT Z))
(PLUS (TIMES 8 (FIX-BIT N))
(TIMES 16 (FIX-BIT X)))))))
Observe that (NUMBERP (CVZNX C V Z N X)) is a theorem.
[ 0.0 0.0 0.0 ]
CVZNX
(DEFN SET-CVZNX
(CVZNX CCR)
(REPLACE 5 CVZNX CCR))
Observe that (NUMBERP (SET-CVZNX CVZNX CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
SET-CVZNX
(DEFN SET-C
(C CCR)
(SET-CVZNX (CVZNX C
(CCR-V CCR)
(CCR-Z CCR)
(CCR-N CCR)
(CCR-X CCR))
CCR))
From the definition we can conclude that (NUMBERP (SET-C C CCR)) is a
theorem.
[ 0.0 0.0 0.0 ]
SET-C
(DEFN SET-V
(V CCR)
(SET-CVZNX (CVZNX (CCR-C CCR)
V
(CCR-Z CCR)
(CCR-N CCR)
(CCR-X CCR))
CCR))
From the definition we can conclude that (NUMBERP (SET-V V CCR)) is a
theorem.
[ 0.0 0.0 0.0 ]
SET-V
(DEFN SET-Z
(Z CCR)
(SET-CVZNX (CVZNX (CCR-C CCR)
(CCR-V CCR)
Z
(CCR-N CCR)
(CCR-X CCR))
CCR))
From the definition we can conclude that (NUMBERP (SET-Z Z CCR)) is a
theorem.
[ 0.0 0.0 0.0 ]
SET-Z
(DEFN SET-N
(N CCR)
(SET-CVZNX (CVZNX (CCR-C CCR)
(CCR-V CCR)
(CCR-Z CCR)
N
(CCR-X CCR))
CCR))
From the definition we can conclude that (NUMBERP (SET-N N CCR)) is a
theorem.
[ 0.0 0.0 0.0 ]
SET-N
(DEFN SET-X
(X CCR)
(SET-CVZNX (CVZNX (CCR-C CCR)
(CCR-V CCR)
(CCR-Z CCR)
(CCR-N CCR)
X)
CCR))
From the definition we can conclude that (NUMBERP (SET-X X CCR)) is a
theorem.
[ 0.0 0.0 0.0 ]
SET-X
(DEFN HALT
(SIGNAL S)
(MC-STATE SIGNAL
(MC-RFILE S)
(MC-PC S)
(MC-CCR S)
(MC-MEM S)))
From the definition we can conclude that (LISTP (HALT SIGNAL S)) is a
theorem.
[ 0.0 0.0 0.0 ]
HALT
(DEFN UPDATE-RFILE
(NEW-RFILE S)
(MC-STATE (MC-STATUS S)
NEW-RFILE
(MC-PC S)
(MC-CCR S)
(MC-MEM S)))
From the definition we can conclude that:
(LISTP (UPDATE-RFILE NEW-RFILE S))
is a theorem.
[ 0.0 0.0 0.0 ]
UPDATE-RFILE
(DEFN UPDATE-PC
(NEW-PC S)
(MC-STATE (MC-STATUS S)
(MC-RFILE S)
NEW-PC
(MC-CCR S)
(MC-MEM S)))
From the definition we can conclude that (LISTP (UPDATE-PC NEW-PC S)) is
a theorem.
[ 0.0 0.0 0.0 ]
UPDATE-PC
(DEFN UPDATE-CCR
(NEW-CCR S)
(MC-STATE (MC-STATUS S)
(MC-RFILE S)
(MC-PC S)
(SET-CVZNX NEW-CCR (MC-CCR S))
(MC-MEM S)))
From the definition we can conclude that (LISTP (UPDATE-CCR NEW-CCR S))
is a theorem.
[ 0.0 0.0 0.0 ]
UPDATE-CCR
(DEFN UPDATE-MEM
(NEW-MEM S)
(MC-STATE (MC-STATUS S)
(MC-RFILE S)
(MC-PC S)
(MC-CCR S)
NEW-MEM))
From the definition we can conclude that (LISTP (UPDATE-MEM NEW-MEM S))
is a theorem.
[ 0.0 0.0 0.0 ]
UPDATE-MEM
(DEFN READ-DN
(OPLEN DN S)
(READ-RN OPLEN DN (MC-RFILE S)))
Note that (NUMBERP (READ-DN OPLEN DN S)) is a theorem.
[ 0.0 0.0 0.0 ]
READ-DN
(DEFN READ-AN
(OPLEN AN S)
(READ-RN OPLEN
(PLUS 8 AN)
(MC-RFILE S)))
Observe that (NUMBERP (READ-AN OPLEN AN S)) is a theorem.
[ 0.0 0.0 0.0 ]
READ-AN
(DEFN WRITE-DN
(OPLEN VALUE DN S)
(UPDATE-RFILE (WRITE-RN OPLEN VALUE DN (MC-RFILE S))
S))
Observe that (LISTP (WRITE-DN OPLEN VALUE DN S)) is a theorem.
[ 0.0 0.0 0.0 ]
WRITE-DN
(DEFN WRITE-AN
(OPLEN VALUE AN S)
(UPDATE-RFILE (WRITE-RN OPLEN VALUE
(PLUS 8 AN)
(MC-RFILE S))
S))
From the definition we can conclude that:
(LISTP (WRITE-AN OPLEN VALUE AN S))
is a theorem.
[ 0.0 0.0 0.0 ]
WRITE-AN
(DEFN SP NIL 7)
From the definition we can conclude that (NUMBERP (SP)) is a theorem.
[ 0.0 0.0 0.0 ]
SP
(DEFN READ-SP
(S)
(READ-AN (L) (SP) S))
Note that (NUMBERP (READ-SP S)) is a theorem.
[ 0.0 0.0 0.0 ]
READ-SP
(DEFN WRITE-SP
(VALUE S)
(WRITE-AN (L) VALUE (SP) S))
Note that (LISTP (WRITE-SP VALUE S)) is a theorem.
[ 0.0 0.0 0.0 ]
WRITE-SP
(DEFN PUSH-SP
(OPSZ VALUE S)
(LET ((SP (SUB (L) OPSZ (READ-SP S))))
(IF (WRITE-MEMP SP (MC-MEM S) OPSZ)
(UPDATE-MEM (WRITE-MEM VALUE SP (MC-MEM S) OPSZ)
(WRITE-SP SP S))
(HALT (WRITE-SIGNAL) S))))
Note that (LISTP (PUSH-SP OPSZ VALUE S)) is a theorem.
[ 0.0 0.0 0.0 ]
PUSH-SP
(DEFN OPERAND
(OPLEN ADDR S)
(IF (EQUAL (CAR ADDR) 'D)
(READ-DN OPLEN (CDR ADDR) S)
(IF (EQUAL (CAR ADDR) 'A)
(READ-AN OPLEN (CDR ADDR) S)
(IF (EQUAL (CAR ADDR) 'M)
(READ-MEM (CDR ADDR)
(MC-MEM S)
(OP-SZ OPLEN))
(CDR ADDR)))))
[ 0.0 0.0 0.0 ]
OPERAND
(DEFN POST-EFFECT
(OPLEN RN ADDR)
(IF (AND (EQUAL RN (SP))
(EQUAL OPLEN (B)))
(ADD (L) ADDR (WSZ))
(ADD (L) ADDR (OP-SZ OPLEN))))
Observe that (NUMBERP (POST-EFFECT OPLEN RN ADDR)) is a theorem.
[ 0.0 0.0 0.0 ]
POST-EFFECT
(DEFN PRE-EFFECT
(OPLEN RN ADDR)
(IF (AND (EQUAL RN (SP))
(EQUAL OPLEN (B)))
(SUB (L) (WSZ) ADDR)
(SUB (L) (OP-SZ OPLEN) ADDR)))
Observe that (NUMBERP (PRE-EFFECT OPLEN RN ADDR)) is a theorem.
[ 0.0 0.0 0.0 ]
PRE-EFFECT
(DEFN DN-DIRECT
(RN S)
(CONS S (CONS 'D RN)))
From the definition we can conclude that (LISTP (DN-DIRECT RN S)) is a
theorem.
[ 0.0 0.0 0.0 ]
DN-DIRECT
(DEFN AN-DIRECT
(RN S)
(CONS S (CONS 'A RN)))
From the definition we can conclude that (LISTP (AN-DIRECT RN S)) is a
theorem.
[ 0.0 0.0 0.0 ]
AN-DIRECT
(DEFN ADDR-INDIRECT
(RN S)
(CONS S
(CONS 'M (READ-AN (L) RN S))))
Note that (LISTP (ADDR-INDIRECT RN S)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-INDIRECT
(DEFN ADDR-POSTINC
(OPLEN RN S)
(LET ((ADDR (READ-AN (L) RN S)))
(CONS (WRITE-AN (L)
(POST-EFFECT OPLEN RN ADDR)
RN S)
(CONS 'M ADDR))))
Observe that (LISTP (ADDR-POSTINC OPLEN RN S)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-POSTINC
(DEFN ADDR-PREDEC
(OPLEN RN S)
(LET ((ADDR (READ-AN (L) RN S)))
(CONS (WRITE-AN (L)
(PRE-EFFECT OPLEN RN ADDR)
RN S)
(CONS 'M
(PRE-EFFECT OPLEN RN ADDR)))))
From the definition we can conclude that (LISTP (ADDR-PREDEC OPLEN RN S))
is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-PREDEC
(DEFN ADDR-DISP
(PC RN S)
(IF (PC-WORD-READP PC (MC-MEM S))
(CONS (UPDATE-PC (ADD (L) PC (WSZ)) S)
(CONS 'M
(ADD (L)
(READ-AN (L) RN S)
(EXT (W)
(PC-WORD-READ PC (MC-MEM S))
(L)))))
(CONS (HALT (PC-SIGNAL) S) NIL)))
Note that (LISTP (ADDR-DISP PC RN S)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-DISP
(DEFN INDEX-RN
(INDEXWD)
(BITS INDEXWD 12 14))
Note that (NUMBERP (INDEX-RN INDEXWD)) is a theorem.
[ 0.0 0.0 0.0 ]
INDEX-RN
(DEFN INDEX-REGISTER
(INDEXWD S)
(IF (B0P (BITN INDEXWD 15))
(IF (B0P (BITN INDEXWD 11))
(EXT (W)
(READ-DN (W) (INDEX-RN INDEXWD) S)
(L))
(READ-DN (L) (INDEX-RN INDEXWD) S))
(IF (B0P (BITN INDEXWD 11))
(EXT (W)
(READ-AN (W) (INDEX-RN INDEXWD) S)
(L))
(READ-AN (L) (INDEX-RN INDEXWD) S))))
Observe that (NUMBERP (INDEX-REGISTER INDEXWD S)) is a theorem.
[ 0.0 0.0 0.0 ]
INDEX-REGISTER
(DEFN IR-SCALED
(INDEXWD S)
(ASL (L)
(INDEX-REGISTER INDEXWD S)
(BITS INDEXWD 9 10)))
Note that (NUMBERP (IR-SCALED INDEXWD S)) is a theorem.
[ 0.0 0.0 0.0 ]
IR-SCALED
(DEFN ADDR-INDEX-DISP
(PC RN INDEXWD S)
(CONS (UPDATE-PC PC S)
(CONS 'M
(ADD (L)
(ADD (L)
(READ-AN (L) RN S)
(EXT (B) (HEAD INDEXWD (B)) (L)))
(IR-SCALED INDEXWD S)))))
Note that (LISTP (ADDR-INDEX-DISP PC RN INDEXWD S)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-INDEX-DISP
(DEFN ADDR-INDEX-BD
(PC ADDR INDEXWD S)
(CONS (UPDATE-PC PC S)
(CONS 'M
(ADD (L)
ADDR
(IR-SCALED INDEXWD S)))))
Note that (LISTP (ADDR-INDEX-BD PC ADDR INDEXWD S)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-INDEX-BD
(DEFN MEM-INDIRECT
(PC ADDR OLEN S)
(IF (LONG-READP ADDR (MC-MEM S))
(IF (PC-READ-MEMP PC
(MC-MEM S)
(OP-SZ OLEN))
(CONS (UPDATE-PC (ADD (L) PC (OP-SZ OLEN))
S)
(CONS 'M
(ADD (L)
(LONG-READ ADDR (MC-MEM S))
(EXT OLEN
(PC-READ-MEM PC
(MC-MEM S)
(OP-SZ OLEN))
(L)))))
(CONS (HALT (PC-SIGNAL) S) NIL))
(CONS (HALT (READ-SIGNAL) S) NIL)))
Observe that (LISTP (MEM-INDIRECT PC ADDR OLEN S)) is a theorem.
[ 0.0 0.0 0.0 ]
MEM-INDIRECT
(DEFN MEM-POSTINDEX
(PC ADDR INDEXWD OLEN S)
(IF (LONG-READP ADDR (MC-MEM S))
(IF (PC-READ-MEMP PC
(MC-MEM S)
(OP-SZ OLEN))
(CONS (UPDATE-PC (ADD (L) PC (OP-SZ OLEN))
S)
(CONS 'M
(ADD (L)
(ADD (L)
(LONG-READ ADDR (MC-MEM S))
(IR-SCALED INDEXWD S))
(EXT OLEN
(PC-READ-MEM PC
(MC-MEM S)
(OP-SZ OLEN))
(L)))))
(CONS (HALT (PC-SIGNAL) S) NIL))
(CONS (HALT (READ-SIGNAL) S) NIL)))
Note that (LISTP (MEM-POSTINDEX PC ADDR INDEXWD OLEN S)) is a theorem.
[ 0.0 0.0 0.0 ]
MEM-POSTINDEX
(DEFN MEM-PREINDEX
(PC ADDR INDEXWD OLEN S)
(MEM-INDIRECT PC
(ADD (L) ADDR (IR-SCALED INDEXWD S))
OLEN S))
Note that (LISTP (MEM-PREINDEX PC ADDR INDEXWD OLEN S)) is a theorem.
[ 0.0 0.0 0.0 ]
MEM-PREINDEX
(DEFN I-IS
(INDEXWD)
(BITS INDEXWD 0 2))
Note that (NUMBERP (I-IS INDEXWD)) is a theorem.
[ 0.0 0.0 0.0 ]
I-IS
(DEFN ADDR-INDEX3
(PC ADDR INDEXWD S)
(IF (B0P (BITN INDEXWD 6))
(IF (LESSP (I-IS INDEXWD) 4)
(IF (LESSP (I-IS INDEXWD) 2)
(IF (EQUAL (I-IS INDEXWD) 0)
(ADDR-INDEX-BD PC ADDR INDEXWD S)
(MEM-PREINDEX PC ADDR INDEXWD 0 S))
(IF (EQUAL (I-IS INDEXWD) 2)
(MEM-PREINDEX PC ADDR INDEXWD (W) S)
(MEM-PREINDEX PC ADDR INDEXWD (L) S)))
(IF (LESSP (I-IS INDEXWD) 6)
(IF (EQUAL (I-IS INDEXWD) 4)
(CONS (HALT (RESERVED-SIGNAL) S) NIL)
(MEM-POSTINDEX PC ADDR INDEXWD 0 S))
(IF (EQUAL (I-IS INDEXWD) 6)
(MEM-POSTINDEX PC ADDR INDEXWD (W) S)
(MEM-POSTINDEX PC ADDR INDEXWD
(L)
S))))
(IF (LESSP (I-IS INDEXWD) 4)
(IF (LESSP (I-IS INDEXWD) 2)
(IF (EQUAL (I-IS INDEXWD) 0)
(CONS (UPDATE-PC PC S)
(CONS 'M ADDR))
(MEM-INDIRECT PC ADDR 0 S))
(IF (EQUAL (I-IS INDEXWD) 2)
(MEM-INDIRECT PC ADDR (W) S)
(MEM-INDIRECT PC ADDR (L) S)))
(CONS (HALT (RESERVED-SIGNAL) S)
NIL))))
From the definition we can conclude that:
(LISTP (ADDR-INDEX3 PC ADDR INDEXWD S))
is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-INDEX3
(DEFN BD-SZ
(INDEXWD)
(BITS INDEXWD 4 5))
Note that (NUMBERP (BD-SZ INDEXWD)) is a theorem.
[ 0.2 0.0 0.0 ]
BD-SZ
(DEFN ADDR-INDEX2
(PC ADDR INDEXWD S)
(IF (LESSP (BD-SZ INDEXWD) 2)
(IF (EQUAL (BD-SZ INDEXWD) 0)
(CONS (HALT (RESERVED-SIGNAL) S) NIL)
(ADDR-INDEX3 PC ADDR INDEXWD S))
(IF (EQUAL (BD-SZ INDEXWD) 2)
(IF (PC-WORD-READP PC (MC-MEM S))
(ADDR-INDEX3 (ADD (L) PC (WSZ))
(ADD (L)
ADDR
(EXT (W)
(PC-WORD-READ PC (MC-MEM S))
(L)))
INDEXWD S)
(CONS (HALT (PC-SIGNAL) S) NIL))
(IF (PC-LONG-READP PC (MC-MEM S))
(ADDR-INDEX3 (ADD (L) PC (LSZ))
(ADD (L)
ADDR
(PC-LONG-READ PC (MC-MEM S)))
INDEXWD S)
(CONS (HALT (PC-SIGNAL) S) NIL)))))
Note that (LISTP (ADDR-INDEX2 PC ADDR INDEXWD S)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-INDEX2
(DEFN BS-REGISTER
(RN INDEXWD S)
(IF (B0P (BITN INDEXWD 7))
(READ-AN (L) RN S)
0))
From the definition we can conclude that:
(NUMBERP (BS-REGISTER RN INDEXWD S))
is a theorem.
[ 0.0 0.0 0.0 ]
BS-REGISTER
(DEFN ADDR-INDEX1
(PC RN INDEXWD S)
(IF (B0P (BITN INDEXWD 8))
(ADDR-INDEX-DISP PC RN INDEXWD S)
(IF (B0P (BITN INDEXWD 3))
(ADDR-INDEX2 PC
(BS-REGISTER RN INDEXWD S)
INDEXWD S)
(CONS (HALT (RESERVED-SIGNAL) S)
NIL))))
From the definition we can conclude that:
(LISTP (ADDR-INDEX1 PC RN INDEXWD S))
is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-INDEX1
(DEFN ADDR-INDEX
(PC RN S)
(IF (PC-WORD-READP PC (MC-MEM S))
(ADDR-INDEX1 (ADD (L) PC (WSZ))
RN
(PC-WORD-READ PC (MC-MEM S))
S)
(CONS (HALT (PC-SIGNAL) S) NIL)))
Note that (LISTP (ADDR-INDEX PC RN S)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-INDEX
(DEFN ABSOLUTE-SHORT
(PC S)
(IF (PC-WORD-READP PC (MC-MEM S))
(CONS (UPDATE-PC (ADD (L) PC (WSZ)) S)
(CONS 'M
(EXT (W)
(PC-WORD-READ PC (MC-MEM S))
(L))))
(CONS (HALT (PC-SIGNAL) S) NIL)))
Note that (LISTP (ABSOLUTE-SHORT PC S)) is a theorem.
[ 0.0 0.0 0.0 ]
ABSOLUTE-SHORT
(DEFN ABSOLUTE-LONG
(PC S)
(IF (PC-LONG-READP PC (MC-MEM S))
(CONS (UPDATE-PC (ADD (L) PC (LSZ)) S)
(CONS 'M
(PC-LONG-READ PC (MC-MEM S))))
(CONS (HALT (PC-SIGNAL) S) NIL)))
Observe that (LISTP (ABSOLUTE-LONG PC S)) is a theorem.
[ 0.0 0.0 0.0 ]
ABSOLUTE-LONG
(DEFN PC-DISP
(PC S)
(IF (PC-WORD-READP PC (MC-MEM S))
(CONS (UPDATE-PC (ADD (L) PC (WSZ)) S)
(CONS 'M
(ADD (L)
PC
(EXT (W)
(PC-WORD-READ PC (MC-MEM S))
(L)))))
(CONS (HALT (PC-SIGNAL) S) NIL)))
Observe that (LISTP (PC-DISP PC S)) is a theorem.
[ 0.0 0.0 0.0 ]
PC-DISP
(DEFN PC-INDEX-DISP
(PC INDEXWD S)
(CONS (UPDATE-PC (ADD (L) PC (WSZ)) S)
(CONS 'M
(ADD (L)
(ADD (L)
PC
(EXT (B) (HEAD INDEXWD (B)) (L)))
(IR-SCALED INDEXWD S)))))
Note that (LISTP (PC-INDEX-DISP PC INDEXWD S)) is a theorem.
[ 0.0 0.0 0.0 ]
PC-INDEX-DISP
(DEFN BS-PC
(PC INDEXWD)
(IF (B0P (BITN INDEXWD 7)) PC 0))
Note that (OR (NUMBERP (BS-PC PC INDEXWD)) (EQUAL (BS-PC PC INDEXWD) PC))
is a theorem.
[ 0.0 0.0 0.0 ]
BS-PC
(DEFN PC-INDEX1
(PC INDEXWD S)
(IF (B0P (BITN INDEXWD 8))
(PC-INDEX-DISP PC INDEXWD S)
(IF (B0P (BITN INDEXWD 3))
(ADDR-INDEX2 (ADD (L) PC (WSZ))
(BS-PC PC INDEXWD)
INDEXWD S)
(CONS (HALT (RESERVED-SIGNAL) S)
NIL))))
From the definition we can conclude that (LISTP (PC-INDEX1 PC INDEXWD S))
is a theorem.
[ 0.0 0.0 0.0 ]
PC-INDEX1
(DEFN PC-INDEX
(PC S)
(IF (PC-WORD-READP PC (MC-MEM S))
(PC-INDEX1 PC
(PC-WORD-READ PC (MC-MEM S))
S)
(CONS (HALT (PC-SIGNAL) S) NIL)))
Note that (LISTP (PC-INDEX PC S)) is a theorem.
[ 0.0 0.0 0.0 ]
PC-INDEX
(DEFN IMMEDIATE
(OPLEN PC S)
(IF (EQUAL OPLEN (B))
(IF (PC-WORD-READP PC (MC-MEM S))
(CONS (UPDATE-PC (ADD (L) PC (WSZ)) S)
(CONS 'I
(PC-BYTE-READ (ADD (L) PC (BSZ))
(MC-MEM S))))
(CONS (HALT (PC-SIGNAL) S) NIL))
(IF (PC-READ-MEMP PC
(MC-MEM S)
(OP-SZ OPLEN))
(CONS (UPDATE-PC (ADD (L) PC (OP-SZ OPLEN))
S)
(CONS 'I
(PC-READ-MEM PC
(MC-MEM S)
(OP-SZ OPLEN))))
(CONS (HALT (PC-SIGNAL) S) NIL))))
Note that (LISTP (IMMEDIATE OPLEN PC S)) is a theorem.
[ 0.0 0.0 0.0 ]
IMMEDIATE
(DEFN EFFEC-ADDR
(OPLEN MODE RN S)
(IF (LESSP MODE 4)
(IF (LESSP MODE 2)
(IF (EQUAL MODE 0)
(DN-DIRECT RN S)
(AN-DIRECT RN S))
(IF (EQUAL MODE 2)
(ADDR-INDIRECT RN S)
(ADDR-POSTINC OPLEN RN S)))
(IF (LESSP MODE 6)
(IF (EQUAL MODE 4)
(ADDR-PREDEC OPLEN RN S)
(ADDR-DISP (MC-PC S) RN S))
(IF (EQUAL MODE 6)
(ADDR-INDEX (MC-PC S) RN S)
(IF (LESSP RN 4)
(IF (LESSP RN 2)
(IF (EQUAL RN 0)
(ABSOLUTE-SHORT (MC-PC S) S)
(ABSOLUTE-LONG (MC-PC S) S))
(IF (EQUAL RN 2)
(PC-DISP (MC-PC S) S)
(PC-INDEX (MC-PC S) S)))
(IMMEDIATE OPLEN (MC-PC S) S))))))
From the definition we can conclude that:
(LISTP (EFFEC-ADDR OPLEN MODE RN S))
is a theorem.
[ 0.0 0.0 0.0 ]
EFFEC-ADDR
(DEFN ADDR-MODEP
(MODE RN)
(IF (EQUAL MODE 7) (LEQ RN 4) T))
Note that (OR (FALSEP (ADDR-MODEP MODE RN)) (TRUEP (ADDR-MODEP MODE RN)))
is a theorem.
[ 0.0 0.0 0.0 ]
ADDR-MODEP
(DEFN DATA-ADDR-MODEP
(MODE RN)
(IF (EQUAL MODE 7)
(LEQ RN 4)
(NOT (EQUAL MODE 1))))
Observe that:
(OR (FALSEP (DATA-ADDR-MODEP MODE RN))
(TRUEP (DATA-ADDR-MODEP MODE RN)))
is a theorem.
[ 0.0 0.0 0.0 ]
DATA-ADDR-MODEP
(DEFN MEMORY-ADDR-MODEP
(MODE RN)
(IF (EQUAL MODE 7)
(LEQ RN 4)
(GEQ MODE 2)))
Note that:
(OR (FALSEP (MEMORY-ADDR-MODEP MODE RN))
(TRUEP (MEMORY-ADDR-MODEP MODE RN)))
is a theorem.
[ 0.0 0.0 0.0 ]
MEMORY-ADDR-MODEP
(DEFN CONTROL-ADDR-MODEP
(MODE RN)
(IF (EQUAL MODE 7)
(LEQ RN 3)
(OR (EQUAL MODE 2) (GEQ MODE 5))))
Observe that:
(OR (FALSEP (CONTROL-ADDR-MODEP MODE RN))
(TRUEP (CONTROL-ADDR-MODEP MODE RN)))
is a theorem.
[ 0.0 0.0 0.0 ]
CONTROL-ADDR-MODEP
(DEFN ALTERABLE-ADDR-MODEP
(MODE RN)
(OR (NOT (EQUAL MODE 7))
(EQUAL RN 0)
(EQUAL RN 1)))
Observe that:
(OR (FALSEP (ALTERABLE-ADDR-MODEP MODE RN))
(TRUEP (ALTERABLE-ADDR-MODEP MODE RN)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALTERABLE-ADDR-MODEP
(DEFN DN-DIRECT-MODEP
(MODE)
(EQUAL MODE 0))
Observe that:
(OR (FALSEP (DN-DIRECT-MODEP MODE))
(TRUEP (DN-DIRECT-MODEP MODE)))
is a theorem.
[ 0.0 0.0 0.0 ]
DN-DIRECT-MODEP
(DEFN AN-DIRECT-MODEP
(MODE)
(EQUAL MODE 1))
Observe that:
(OR (FALSEP (AN-DIRECT-MODEP MODE))
(TRUEP (AN-DIRECT-MODEP MODE)))
is a theorem.
[ 0.0 0.0 0.0 ]
AN-DIRECT-MODEP
(DEFN POSTINC-MODEP
(MODE)
(EQUAL MODE 3))
Observe that:
(OR (FALSEP (POSTINC-MODEP MODE))
(TRUEP (POSTINC-MODEP MODE)))
is a theorem.
[ 0.0 0.0 0.0 ]
POSTINC-MODEP
(DEFN PREDEC-MODEP
(MODE)
(EQUAL MODE 4))
Observe that:
(OR (FALSEP (PREDEC-MODEP MODE))
(TRUEP (PREDEC-MODEP MODE)))
is a theorem.
[ 0.0 0.0 0.0 ]
PREDEC-MODEP
(DEFN IDATA-MODEP
(MODE RN)
(AND (EQUAL MODE 7) (EQUAL RN 4)))
Note that:
(OR (FALSEP (IDATA-MODEP MODE RN))
(TRUEP (IDATA-MODEP MODE RN)))
is a theorem.
[ 0.0 0.0 0.0 ]
IDATA-MODEP
(DEFN BYTE-AN-DIRECT-MODEP
(OPLEN MODE)
(AND (EQUAL OPLEN (B))
(AN-DIRECT-MODEP MODE)))
Observe that:
(OR (FALSEP (BYTE-AN-DIRECT-MODEP OPLEN MODE))
(TRUEP (BYTE-AN-DIRECT-MODEP OPLEN MODE)))
is a theorem.
[ 0.0 0.0 0.0 ]
BYTE-AN-DIRECT-MODEP
(DEFN MC-INSTATE
(OPLEN INS S)
(LET ((S&ADDR (EFFEC-ADDR OPLEN
(S_MODE INS)
(S_RN INS)
S)))
(IF (EQUAL (CADR S&ADDR) 'M)
(IF (READ-MEMP (CDDR S&ADDR)
(MC-MEM S)
(OP-SZ OPLEN))
S&ADDR
(CONS (HALT (READ-SIGNAL) S) NIL))
S&ADDR)))
From the definition we can conclude that (LISTP (MC-INSTATE OPLEN INS S))
is a theorem.
[ 0.0 0.0 0.0 ]
MC-INSTATE
(DEFN D-MAPPING
(OPLEN V&CVZNX ADDR S)
(MC-STATE (MC-STATUS S)
(WRITE-RN OPLEN
(CAR V&CVZNX)
ADDR
(MC-RFILE S))
(MC-PC S)
(SET-CVZNX (CDR V&CVZNX) (MC-CCR S))
(MC-MEM S)))
Note that (LISTP (D-MAPPING OPLEN V&CVZNX ADDR S)) is a theorem.
[ 0.0 0.0 0.0 ]
D-MAPPING
(DEFN A-MAPPING
(OPLEN V&CVZNX ADDR S)
(MC-STATE (MC-STATUS S)
(WRITE-RN OPLEN
(CAR V&CVZNX)
(PLUS 8 ADDR)
(MC-RFILE S))
(MC-PC S)
(SET-CVZNX (CDR V&CVZNX) (MC-CCR S))
(MC-MEM S)))
Note that (LISTP (A-MAPPING OPLEN V&CVZNX ADDR S)) is a theorem.
[ 0.0 0.0 0.0 ]
A-MAPPING
(DEFN M-MAPPING
(OPLEN V&CVZNX ADDR S)
(IF (WRITE-MEMP ADDR
(MC-MEM S)
(OP-SZ OPLEN))
(MC-STATE (MC-STATUS S)
(MC-RFILE S)
(MC-PC S)
(SET-CVZNX (CDR V&CVZNX) (MC-CCR S))
(WRITE-MEM (CAR V&CVZNX)
ADDR
(MC-MEM S)
(OP-SZ OPLEN)))
(HALT (WRITE-SIGNAL) S)))
Observe that (LISTP (M-MAPPING OPLEN V&CVZNX ADDR S)) is a theorem.
[ 0.0 0.0 0.0 ]
M-MAPPING
(DEFN MAPPING
(OPLEN V&CVZNX S&ADDR)
(IF (EQUAL (CADR S&ADDR) 'D)
(D-MAPPING OPLEN V&CVZNX
(CDDR S&ADDR)
(CAR S&ADDR))
(IF (EQUAL (CADR S&ADDR) 'A)
(A-MAPPING OPLEN V&CVZNX
(CDDR S&ADDR)
(CAR S&ADDR))
(M-MAPPING OPLEN V&CVZNX
(CDDR S&ADDR)
(CAR S&ADDR)))))
Note that (LISTP (MAPPING OPLEN V&CVZNX S&ADDR)) is a theorem.
[ 0.0 0.0 0.0 ]
MAPPING
(DEFN ADD-C
(N SOPD DOPD)
(LET ((RESULT (ADD N SOPD DOPD)))
(B-OR (B-OR (B-AND (MBIT SOPD N) (MBIT DOPD N))
(B-AND (B-NOT (MBIT RESULT N))
(MBIT DOPD N)))
(B-AND (MBIT SOPD N)
(B-NOT (MBIT RESULT N))))))
Note that (NUMBERP (ADD-C N SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
ADD-C
(DEFN ADD-V
(N SOPD DOPD)
(LET ((RESULT (ADD N SOPD DOPD)))
(B-OR (B-AND (B-AND (MBIT SOPD N) (MBIT DOPD N))
(B-NOT (MBIT RESULT N)))
(B-AND (B-AND (B-NOT (MBIT SOPD N))
(B-NOT (MBIT DOPD N)))
(MBIT RESULT N)))))
Observe that (NUMBERP (ADD-V N SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
ADD-V
(DEFN ADD-Z
(OPLEN SOPD DOPD)
(IF (EQUAL (ADD OPLEN DOPD SOPD) 0)
(B1)
(B0)))
Note that (NUMBERP (ADD-Z OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
ADD-Z
(DEFN ADD-N
(OPLEN SOPD DOPD)
(MBIT (ADD OPLEN DOPD SOPD) OPLEN))
From the definition we can conclude that:
(NUMBERP (ADD-N OPLEN SOPD DOPD))
is a theorem.
[ 0.0 0.0 0.0 ]
ADD-N
(DEFN ADD-CVZNX
(OPLEN SOPD DOPD)
(CVZNX (ADD-C OPLEN SOPD DOPD)
(ADD-V OPLEN SOPD DOPD)
(ADD-Z OPLEN SOPD DOPD)
(ADD-N OPLEN SOPD DOPD)
(ADD-C OPLEN SOPD DOPD)))
Note that (NUMBERP (ADD-CVZNX OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
ADD-CVZNX
(DEFN ADD-EFFECT
(OPLEN SOPD DOPD)
(CONS (ADD OPLEN DOPD SOPD)
(ADD-CVZNX OPLEN SOPD DOPD)))
Observe that (LISTP (ADD-EFFECT OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
ADD-EFFECT
(DEFN ADD-ADDR-MODEP1
(OPLEN INS)
(AND (ADDR-MODEP (S_MODE INS) (S_RN INS))
(NOT (BYTE-AN-DIRECT-MODEP OPLEN
(S_MODE INS)))))
From the definition we can conclude that:
(OR (FALSEP (ADD-ADDR-MODEP1 OPLEN INS))
(TRUEP (ADD-ADDR-MODEP1 OPLEN INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
ADD-ADDR-MODEP1
(DEFN ADD-ADDR-MODEP2
(INS)
(AND (ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(MEMORY-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (ADD-ADDR-MODEP2 INS))
(TRUEP (ADD-ADDR-MODEP2 INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
ADD-ADDR-MODEP2
(DEFN ADD-INS1
(OPLEN INS S)
(IF (ADD-ADDR-MODEP1 OPLEN INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(D-MAPPING OPLEN
(ADD-EFFECT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
(READ-DN OPLEN (D_RN INS) S))
(D_RN INS)
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
ADD-INS1
(DEFN ADD-MAPPING
(OPD OPLEN INS S)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING OPLEN
(ADD-EFFECT OPLEN OPD
(OPERAND OPLEN (CDR S&ADDR) S))
S&ADDR))))
[ 0.0 0.0 0.0 ]
ADD-MAPPING
(DEFN ADD-INS2
(OPLEN INS S)
(IF (ADD-ADDR-MODEP2 INS)
(ADD-MAPPING (READ-DN OPLEN (D_RN INS) S)
OPLEN INS S)
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
ADD-INS2
(DEFN ADDA-ADDR-MODEP
(INS)
(ADDR-MODEP (S_MODE INS) (S_RN INS)))
Observe that:
(OR (FALSEP (ADDA-ADDR-MODEP INS))
(TRUEP (ADDA-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
ADDA-ADDR-MODEP
(DEFN ADDA-INS
(OPLEN INS S)
(IF (ADDA-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(WRITE-AN (L)
(ADD (L)
(READ-AN (L) (D_RN INS) (CAR S&ADDR))
(EXT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
(L)))
(D_RN INS)
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
ADDA-INS
(DEFN ADDX-C
(N X SOPD DOPD)
(LET ((RESULT (ADDER N X SOPD DOPD)))
(B-OR (B-OR (B-AND (MBIT SOPD N) (MBIT DOPD N))
(B-AND (B-NOT (MBIT RESULT N))
(MBIT DOPD N)))
(B-AND (MBIT SOPD N)
(B-NOT (MBIT RESULT N))))))
Note that (NUMBERP (ADDX-C N X SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDX-C
(DEFN ADDX-V
(N X SOPD DOPD)
(LET ((RESULT (ADDER N X SOPD DOPD)))
(B-OR (B-AND (B-AND (MBIT SOPD N) (MBIT DOPD N))
(B-NOT (MBIT RESULT N)))
(B-AND (B-AND (B-NOT (MBIT SOPD N))
(B-NOT (MBIT DOPD N)))
(MBIT RESULT N)))))
Observe that (NUMBERP (ADDX-V N X SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDX-V
(DEFN ADDX-Z
(OPLEN Z X SOPD DOPD)
(B-AND Z
(IF (EQUAL (ADDER OPLEN X DOPD SOPD) 0)
(B1)
(B0))))
From the definition we can conclude that:
(NUMBERP (ADDX-Z OPLEN Z X SOPD DOPD))
is a theorem.
[ 0.0 0.0 0.0 ]
ADDX-Z
(DEFN ADDX-N
(OPLEN X SOPD DOPD)
(MBIT (ADDER OPLEN X DOPD SOPD)
OPLEN))
Note that (NUMBERP (ADDX-N OPLEN X SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDX-N
(DEFN ADDX-CVZNX
(OPLEN Z X SOPD DOPD)
(CVZNX (ADDX-C OPLEN X SOPD DOPD)
(ADDX-V OPLEN X SOPD DOPD)
(ADDX-Z OPLEN Z X SOPD DOPD)
(ADDX-N OPLEN X SOPD DOPD)
(ADDX-C OPLEN X SOPD DOPD)))
Note that (NUMBERP (ADDX-CVZNX OPLEN Z X SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDX-CVZNX
(DEFN ADDX-EFFECT
(OPLEN SOPD DOPD CCR)
(CONS (ADDER OPLEN (CCR-X CCR) DOPD SOPD)
(ADDX-CVZNX OPLEN
(CCR-Z CCR)
(CCR-X CCR)
SOPD DOPD)))
From the definition we can conclude that:
(LISTP (ADDX-EFFECT OPLEN SOPD DOPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
ADDX-EFFECT
(DEFN ADDX-INS1
(OPLEN INS S)
(D-MAPPING OPLEN
(ADDX-EFFECT OPLEN
(READ-DN OPLEN (S_RN INS) S)
(READ-DN OPLEN (D_RN INS) S)
(MC-CCR S))
(D_RN INS)
S))
Note that (LISTP (ADDX-INS1 OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
ADDX-INS1
(DEFN ADDX-INS2
(OPLEN INS S)
(LET ((S&ADDR0 (ADDR-PREDEC OPLEN (S_RN INS) S)))
(IF (READ-MEMP (CDDR S&ADDR0)
(MC-MEM S)
(OP-SZ OPLEN))
(LET ((S&ADDR (ADDR-PREDEC OPLEN
(D_RN INS)
(CAR S&ADDR0))))
(IF (READ-MEMP (CDDR S&ADDR)
(MC-MEM S)
(OP-SZ OPLEN))
(MAPPING OPLEN
(ADDX-EFFECT OPLEN
(OPERAND OPLEN
(CDR S&ADDR0)
(CAR S&ADDR0))
(OPERAND OPLEN
(CDR S&ADDR)
(CAR S&ADDR))
(MC-CCR S))
S&ADDR)
(HALT (READ-SIGNAL) S)))
(HALT (READ-SIGNAL) S))))
From the definition we can conclude that (LISTP (ADDX-INS2 OPLEN INS S))
is a theorem.
[ 0.0 0.0 0.0 ]
ADDX-INS2
(DEFN ADD-GROUP
(OPMODE INS S)
(IF (LESSP OPMODE 4)
(IF (EQUAL OPMODE 3)
(ADDA-INS (W) INS S)
(ADD-INS1 (OP-LEN INS) INS S))
(IF (EQUAL OPMODE 7)
(ADDA-INS (L) INS S)
(IF (EQUAL (S_MODE INS) 0)
(ADDX-INS1 (OP-LEN INS) INS S)
(IF (EQUAL (S_MODE INS) 1)
(ADDX-INS2 (OP-LEN INS) INS S)
(ADD-INS2 (OP-LEN INS) INS S))))))
[ 0.0 0.0 0.0 ]
ADD-GROUP
(DEFN SUB-C
(N SOPD DOPD)
(LET ((RESULT (SUB N SOPD DOPD)))
(B-OR (B-OR (B-AND (MBIT SOPD N)
(B-NOT (MBIT DOPD N)))
(B-AND (MBIT RESULT N)
(B-NOT (MBIT DOPD N))))
(B-AND (MBIT SOPD N)
(MBIT RESULT N)))))
Note that (NUMBERP (SUB-C N SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SUB-C
(DEFN SUB-V
(N SOPD DOPD)
(LET ((RESULT (SUB N SOPD DOPD)))
(B-OR (B-AND (B-AND (B-NOT (MBIT SOPD N))
(MBIT DOPD N))
(B-NOT (MBIT RESULT N)))
(B-AND (B-AND (MBIT SOPD N)
(B-NOT (MBIT DOPD N)))
(MBIT RESULT N)))))
Observe that (NUMBERP (SUB-V N SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SUB-V
(DEFN SUB-Z
(OPLEN SOPD DOPD)
(IF (EQUAL (SUB OPLEN SOPD DOPD) 0)
(B1)
(B0)))
Note that (NUMBERP (SUB-Z OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SUB-Z
(DEFN SUB-N
(OPLEN SOPD DOPD)
(MBIT (SUB OPLEN SOPD DOPD) OPLEN))
From the definition we can conclude that:
(NUMBERP (SUB-N OPLEN SOPD DOPD))
is a theorem.
[ 0.0 0.0 0.0 ]
SUB-N
(DEFN SUB-CVZNX
(OPLEN SOPD DOPD)
(CVZNX (SUB-C OPLEN SOPD DOPD)
(SUB-V OPLEN SOPD DOPD)
(SUB-Z OPLEN SOPD DOPD)
(SUB-N OPLEN SOPD DOPD)
(SUB-C OPLEN SOPD DOPD)))
Note that (NUMBERP (SUB-CVZNX OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SUB-CVZNX
(DEFN SUB-EFFECT
(OPLEN SOPD DOPD)
(CONS (SUB OPLEN SOPD DOPD)
(SUB-CVZNX OPLEN SOPD DOPD)))
Observe that (LISTP (SUB-EFFECT OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SUB-EFFECT
(DEFN SUB-ADDR-MODEP1
(OPLEN INS)
(AND (ADDR-MODEP (S_MODE INS) (S_RN INS))
(NOT (BYTE-AN-DIRECT-MODEP OPLEN
(S_MODE INS)))))
From the definition we can conclude that:
(OR (FALSEP (SUB-ADDR-MODEP1 OPLEN INS))
(TRUEP (SUB-ADDR-MODEP1 OPLEN INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
SUB-ADDR-MODEP1
(DEFN SUB-ADDR-MODEP2
(INS)
(AND (ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(MEMORY-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (SUB-ADDR-MODEP2 INS))
(TRUEP (SUB-ADDR-MODEP2 INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
SUB-ADDR-MODEP2
(DEFN SUB-INS1
(OPLEN INS S)
(IF (SUB-ADDR-MODEP1 OPLEN INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(D-MAPPING OPLEN
(SUB-EFFECT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
(READ-DN OPLEN (D_RN INS) S))
(D_RN INS)
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
SUB-INS1
(DEFN SUB-MAPPING
(OPD OPLEN INS S)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING OPLEN
(SUB-EFFECT OPLEN OPD
(OPERAND OPLEN (CDR S&ADDR) S))
S&ADDR))))
[ 0.0 0.0 0.0 ]
SUB-MAPPING
(DEFN SUB-INS2
(OPLEN INS S)
(IF (SUB-ADDR-MODEP2 INS)
(SUB-MAPPING (READ-DN OPLEN (D_RN INS) S)
OPLEN INS S)
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
SUB-INS2
(DEFN SUBA-ADDR-MODEP
(INS)
(ADDR-MODEP (S_MODE INS) (S_RN INS)))
Observe that:
(OR (FALSEP (SUBA-ADDR-MODEP INS))
(TRUEP (SUBA-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
SUBA-ADDR-MODEP
(DEFN SUBA-INS
(OPLEN INS S)
(IF (SUBA-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(WRITE-AN (L)
(SUB (L)
(EXT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
(L))
(READ-AN (L) (D_RN INS) (CAR S&ADDR)))
(D_RN INS)
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
SUBA-INS
(DEFN SUBX-C
(N X SOPD DOPD)
(LET ((RESULT (SUBTRACTER N X SOPD DOPD)))
(B-OR (B-OR (B-AND (MBIT SOPD N)
(B-NOT (MBIT DOPD N)))
(B-AND (MBIT RESULT N)
(B-NOT (MBIT DOPD N))))
(B-AND (MBIT SOPD N)
(MBIT RESULT N)))))
Note that (NUMBERP (SUBX-C N X SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SUBX-C
(DEFN SUBX-V
(N X SOPD DOPD)
(LET ((RESULT (SUBTRACTER N X SOPD DOPD)))
(B-OR (B-AND (B-AND (B-NOT (MBIT SOPD N))
(MBIT DOPD N))
(B-NOT (MBIT RESULT N)))
(B-AND (B-AND (MBIT SOPD N)
(B-NOT (MBIT DOPD N)))
(MBIT RESULT N)))))
Observe that (NUMBERP (SUBX-V N X SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SUBX-V
(DEFN SUBX-Z
(OPLEN Z X SOPD DOPD)
(B-AND Z
(IF (EQUAL (SUBTRACTER OPLEN X SOPD DOPD)
0)
(B1)
(B0))))
From the definition we can conclude that:
(NUMBERP (SUBX-Z OPLEN Z X SOPD DOPD))
is a theorem.
[ 0.0 0.0 0.0 ]
SUBX-Z
(DEFN SUBX-N
(OPLEN X SOPD DOPD)
(MBIT (SUBTRACTER OPLEN X SOPD DOPD)
OPLEN))
Note that (NUMBERP (SUBX-N OPLEN X SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SUBX-N
(DEFN SUBX-CVZNX
(OPLEN Z X SOPD DOPD)
(CVZNX (SUBX-C OPLEN X SOPD DOPD)
(SUBX-V OPLEN X SOPD DOPD)
(SUBX-Z OPLEN Z X SOPD DOPD)
(SUBX-N OPLEN X SOPD DOPD)
(SUBX-C OPLEN X SOPD DOPD)))
Note that (NUMBERP (SUBX-CVZNX OPLEN Z X SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SUBX-CVZNX
(DEFN SUBX-EFFECT
(OPLEN SOPD DOPD CCR)
(CONS (SUBTRACTER OPLEN
(CCR-X CCR)
SOPD DOPD)
(SUBX-CVZNX OPLEN
(CCR-Z CCR)
(CCR-X CCR)
SOPD DOPD)))
From the definition we can conclude that:
(LISTP (SUBX-EFFECT OPLEN SOPD DOPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
SUBX-EFFECT
(DEFN SUBX-INS1
(OPLEN INS S)
(D-MAPPING OPLEN
(SUBX-EFFECT OPLEN
(READ-DN OPLEN (S_RN INS) S)
(READ-DN OPLEN (D_RN INS) S)
(MC-CCR S))
(D_RN INS)
S))
Note that (LISTP (SUBX-INS1 OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
SUBX-INS1
(DEFN SUBX-INS2
(OPLEN INS S)
(LET ((S&ADDR0 (ADDR-PREDEC OPLEN (S_RN INS) S)))
(IF (READ-MEMP (CDDR S&ADDR0)
(MC-MEM S)
(OP-SZ OPLEN))
(LET ((S&ADDR (ADDR-PREDEC OPLEN
(D_RN INS)
(CAR S&ADDR0))))
(IF (READ-MEMP (CDDR S&ADDR)
(MC-MEM S)
(OP-SZ OPLEN))
(MAPPING OPLEN
(SUBX-EFFECT OPLEN
(OPERAND OPLEN
(CDR S&ADDR0)
(CAR S&ADDR0))
(OPERAND OPLEN
(CDR S&ADDR)
(CAR S&ADDR))
(MC-CCR S))
S&ADDR)
(HALT (READ-SIGNAL) S)))
(HALT (READ-SIGNAL) S))))
From the definition we can conclude that (LISTP (SUBX-INS2 OPLEN INS S))
is a theorem.
[ 0.0 0.0 0.0 ]
SUBX-INS2
(DEFN SUB-GROUP
(OPMODE INS S)
(IF (LESSP OPMODE 4)
(IF (EQUAL OPMODE 3)
(SUBA-INS (W) INS S)
(SUB-INS1 (OP-LEN INS) INS S))
(IF (EQUAL OPMODE 7)
(SUBA-INS (L) INS S)
(IF (EQUAL (S_MODE INS) 0)
(SUBX-INS1 (OP-LEN INS) INS S)
(IF (EQUAL (S_MODE INS) 1)
(SUBX-INS2 (OP-LEN INS) INS S)
(SUB-INS2 (OP-LEN INS) INS S))))))
[ 0.0 0.0 0.0 ]
SUB-GROUP
(DEFN AND-Z
(OPLEN SOPD DOPD)
(IF (EQUAL (LOGAND SOPD DOPD) 0)
(B1)
(B0)))
WARNING: OPLEN is in the arglist but not in the body of the definition of
AND-Z.
Observe that (NUMBERP (AND-Z OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
AND-Z
(DEFN AND-N
(OPLEN SOPD DOPD)
(MBIT (LOGAND SOPD DOPD) OPLEN))
Note that (NUMBERP (AND-N OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
AND-N
(DEFN AND-CVZNX
(OPLEN SOPD DOPD CCR)
(CVZNX (B0)
(B0)
(AND-Z OPLEN SOPD DOPD)
(AND-N OPLEN SOPD DOPD)
(CCR-X CCR)))
Observe that (NUMBERP (AND-CVZNX OPLEN SOPD DOPD CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
AND-CVZNX
(DEFN AND-EFFECT
(OPLEN SOPD DOPD CCR)
(CONS (LOGAND SOPD DOPD)
(AND-CVZNX OPLEN SOPD DOPD CCR)))
Note that (LISTP (AND-EFFECT OPLEN SOPD DOPD CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
AND-EFFECT
(DEFN AND-ADDR-MODEP1
(INS)
(DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS)))
Observe that:
(OR (FALSEP (AND-ADDR-MODEP1 INS))
(TRUEP (AND-ADDR-MODEP1 INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
AND-ADDR-MODEP1
(DEFN AND-ADDR-MODEP2
(INS)
(AND (ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(MEMORY-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (AND-ADDR-MODEP2 INS))
(TRUEP (AND-ADDR-MODEP2 INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
AND-ADDR-MODEP2
(DEFN AND-INS1
(OPLEN INS S)
(IF (AND-ADDR-MODEP1 INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(D-MAPPING OPLEN
(AND-EFFECT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
(READ-DN OPLEN (D_RN INS) S)
(MC-CCR S))
(D_RN INS)
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
AND-INS1
(DEFN AND-MAPPING
(SOPD OPLEN INS S)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING OPLEN
(AND-EFFECT OPLEN SOPD
(OPERAND OPLEN (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR))))
[ 0.0 0.0 0.0 ]
AND-MAPPING
(DEFN AND-INS2
(OPLEN INS S)
(IF (AND-ADDR-MODEP2 INS)
(AND-MAPPING (READ-DN OPLEN (D_RN INS) S)
OPLEN INS S)
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
AND-INS2
(DEFN MULU
(N X Y I)
(HEAD (TIMES X Y) N))
WARNING: I is in the arglist but not in the body of the definition of MULU.
From the definition we can conclude that (NUMBERP (MULU N X Y I)) is a
theorem.
[ 0.0 0.0 0.0 ]
MULU
(DEFN MULS
(N X Y I)
(HEAD (INT-TO-NAT (ITIMES (NAT-TO-INT X I)
(NAT-TO-INT Y I))
(TIMES 2 I))
N))
From the definition we can conclude that (NUMBERP (MULS N X Y I)) is a
theorem.
[ 0.0 0.0 0.0 ]
MULS
(DEFN MUL&DIV-ADDR-MODEP
(INS)
(DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS)))
Observe that:
(OR (FALSEP (MUL&DIV-ADDR-MODEP INS))
(TRUEP (MUL&DIV-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
MUL&DIV-ADDR-MODEP
(DEFN MULU-V
(N SOPD DOPD I)
(IF (LESSP (TIMES SOPD DOPD) (EXP 2 N))
(B0)
(B1)))
WARNING: I is in the arglist but not in the body of the definition of MULU-V.
From the definition we can conclude that (NUMBERP (MULU-V N SOPD DOPD I))
is a theorem.
[ 0.0 0.0 0.0 ]
MULU-V
(DEFN MULU-Z
(N SOPD DOPD I)
(IF (EQUAL (MULU N SOPD DOPD I) 0)
(B1)
(B0)))
Note that (NUMBERP (MULU-Z N SOPD DOPD I)) is a theorem.
[ 0.0 0.0 0.0 ]
MULU-Z
(DEFN MULU-N
(N SOPD DOPD I)
(MBIT (MULU N SOPD DOPD I) N))
Note that (NUMBERP (MULU-N N SOPD DOPD I)) is a theorem.
[ 0.0 0.0 0.0 ]
MULU-N
(DEFN MULU-CVZNX
(N SOPD DOPD I CCR)
(CVZNX (B0)
(MULU-V N SOPD DOPD I)
(MULU-Z N SOPD DOPD I)
(MULU-N N SOPD DOPD I)
(CCR-X CCR)))
Note that (NUMBERP (MULU-CVZNX N SOPD DOPD I CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
MULU-CVZNX
(DEFN MULU_W-INS
(SOPD DN S)
(LET ((DOPD (READ-DN (W) DN S)))
(UPDATE-CCR (MULU-CVZNX (L)
SOPD DOPD
(W)
(MC-CCR S))
(WRITE-DN (L)
(MULU (L) SOPD DOPD (W))
DN S))))
Observe that (LISTP (MULU_W-INS SOPD DN S)) is a theorem.
[ 0.0 0.0 0.0 ]
MULU_W-INS
(DEFN MULS-V
(N SOPD DOPD I)
(IF (INT-RANGEP (ITIMES (NAT-TO-INT SOPD I)
(NAT-TO-INT DOPD I))
N)
(B0)
(B1)))
Observe that (NUMBERP (MULS-V N SOPD DOPD I)) is a theorem.
[ 0.0 0.0 0.0 ]
MULS-V
(DEFN MULS-Z
(N SOPD DOPD I)
(IF (EQUAL (MULS N SOPD DOPD I) 0)
(B1)
(B0)))
Note that (NUMBERP (MULS-Z N SOPD DOPD I)) is a theorem.
[ 0.0 0.0 0.0 ]
MULS-Z
(DEFN MULS-N
(N SOPD DOPD I)
(MBIT (MULS N SOPD DOPD I) N))
Note that (NUMBERP (MULS-N N SOPD DOPD I)) is a theorem.
[ 0.0 0.0 0.0 ]
MULS-N
(DEFN MULS-CVZNX
(N SOPD DOPD I CCR)
(CVZNX (B0)
(MULS-V N SOPD DOPD I)
(MULS-Z N SOPD DOPD I)
(MULS-N N SOPD DOPD I)
(CCR-X CCR)))
Note that (NUMBERP (MULS-CVZNX N SOPD DOPD I CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
MULS-CVZNX
(DEFN MULS_W-INS
(SOPD DN S)
(LET ((DOPD (READ-DN (W) DN S)))
(UPDATE-CCR (MULS-CVZNX (L)
SOPD DOPD
(W)
(MC-CCR S))
(WRITE-DN (L)
(MULS (L) SOPD DOPD (W))
DN S))))
Observe that (LISTP (MULS_W-INS SOPD DN S)) is a theorem.
[ 0.0 0.0 0.0 ]
MULS_W-INS
(DEFN EXG-DRDR-INS
(INS S)
(LET ((DX (READ-DN (L) (D_RN INS) S))
(DY (READ-DN (L) (S_RN INS) S)))
(WRITE-DN (L)
DY
(D_RN INS)
(WRITE-DN (L) DX (S_RN INS) S))))
Note that (LISTP (EXG-DRDR-INS INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
EXG-DRDR-INS
(DEFN EXG-ARAR-INS
(INS S)
(LET ((AX (READ-AN (L) (D_RN INS) S))
(AY (READ-AN (L) (S_RN INS) S)))
(WRITE-AN (L)
AY
(D_RN INS)
(WRITE-AN (L) AX (S_RN INS) S))))
Note that (LISTP (EXG-ARAR-INS INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
EXG-ARAR-INS
(DEFN EXG-DRAR-INS
(INS S)
(LET ((DX (READ-DN (L) (D_RN INS) S))
(AY (READ-AN (L) (S_RN INS) S)))
(WRITE-DN (L)
AY
(D_RN INS)
(WRITE-AN (L) DX (S_RN INS) S))))
Note that (LISTP (EXG-DRAR-INS INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
EXG-DRAR-INS
(DEFN MUL_W-INS
(INS S)
(IF (MUL&DIV-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(LET ((SOPD (OPERAND (W) (CDR S&ADDR) S)))
(IF (B0P (BITN INS 8))
(MULU_W-INS SOPD
(D_RN INS)
(CAR S&ADDR))
(MULS_W-INS SOPD
(D_RN INS)
(CAR S&ADDR))))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MUL_W-INS
(DEFN AND-GROUP
(OPLEN INS S)
(IF (EQUAL OPLEN (Q))
(MUL_W-INS INS S)
(IF (B0P (BITN INS 8))
(AND-INS1 OPLEN INS S)
(IF (LESSP (S_MODE INS) 2)
(IF (EQUAL OPLEN (B))
(HALT 'ABCD-UNSPECIFIED S)
(IF (EQUAL OPLEN (W))
(IF (EQUAL (S_MODE INS) 0)
(EXG-DRDR-INS INS S)
(EXG-ARAR-INS INS S))
(IF (EQUAL (S_MODE INS) 0)
(HALT (RESERVED-SIGNAL) S)
(EXG-DRAR-INS INS S))))
(AND-INS2 OPLEN INS S)))))
[ 0.0 0.0 0.0 ]
AND-GROUP
(DEFN OR-Z
(OPLEN SOPD DOPD)
(IF (EQUAL (LOGOR SOPD DOPD) 0)
(B1)
(B0)))
WARNING: OPLEN is in the arglist but not in the body of the definition of
OR-Z.
Observe that (NUMBERP (OR-Z OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
OR-Z
(DEFN OR-N
(OPLEN SOPD DOPD)
(B-OR (MBIT SOPD OPLEN)
(MBIT DOPD OPLEN)))
Note that (NUMBERP (OR-N OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
OR-N
(DEFN OR-CVZNX
(OPLEN SOPD DOPD CCR)
(CVZNX (B0)
(B0)
(OR-Z OPLEN SOPD DOPD)
(OR-N OPLEN SOPD DOPD)
(CCR-X CCR)))
Observe that (NUMBERP (OR-CVZNX OPLEN SOPD DOPD CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
OR-CVZNX
(DEFN OR-EFFECT
(OPLEN SOPD DOPD CCR)
(CONS (LOGOR SOPD DOPD)
(OR-CVZNX OPLEN SOPD DOPD CCR)))
Note that (LISTP (OR-EFFECT OPLEN SOPD DOPD CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
OR-EFFECT
(DEFN OR-ADDR-MODEP1
(INS)
(DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS)))
Observe that:
(OR (FALSEP (OR-ADDR-MODEP1 INS))
(TRUEP (OR-ADDR-MODEP1 INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
OR-ADDR-MODEP1
(DEFN OR-ADDR-MODEP2
(INS)
(AND (ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(MEMORY-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that (OR (FALSEP (OR-ADDR-MODEP2 INS)) (TRUEP (OR-ADDR-MODEP2 INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
OR-ADDR-MODEP2
(DEFN OR-INS1
(OPLEN INS S)
(IF (OR-ADDR-MODEP1 INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(D-MAPPING OPLEN
(OR-EFFECT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
(READ-DN OPLEN (D_RN INS) S)
(MC-CCR S))
(D_RN INS)
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
OR-INS1
(DEFN OR-MAPPING
(SOPD OPLEN INS S)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING OPLEN
(OR-EFFECT OPLEN SOPD
(OPERAND OPLEN (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR))))
[ 0.0 0.0 0.0 ]
OR-MAPPING
(DEFN OR-INS2
(OPLEN INS S)
(IF (OR-ADDR-MODEP2 INS)
(OR-MAPPING (READ-DN OPLEN (D_RN INS) S)
OPLEN INS S)
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
OR-INS2
(DEFN IQUOT
(N S I D J)
(HEAD (INT-TO-NAT (IQUOTIENT (NAT-TO-INT D J)
(NAT-TO-INT S I))
J)
N))
Note that (NUMBERP (IQUOT N S I D J)) is a theorem.
[ 0.0 0.0 0.0 ]
IQUOT
(DEFN IREM
(N S I D J)
(HEAD (INT-TO-NAT (IREMAINDER (NAT-TO-INT D J)
(NAT-TO-INT S I))
I)
N))
Note that (NUMBERP (IREM N S I D J)) is a theorem.
[ 0.0 0.0 0.0 ]
IREM
(DEFN DIVS-V
(N SOPD I DOPD J)
(IF (INT-RANGEP (IQUOTIENT (NAT-TO-INT DOPD J)
(NAT-TO-INT SOPD I))
N)
(B0)
(B1)))
Note that (NUMBERP (DIVS-V N SOPD I DOPD J)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVS-V
(DEFN DIVS-Z
(N SOPD I DOPD J)
(IF (EQUAL (IQUOT N SOPD I DOPD J) 0)
(B1)
(B0)))
Observe that (NUMBERP (DIVS-Z N SOPD I DOPD J)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVS-Z
(DEFN DIVS-N
(N SOPD I DOPD J)
(MBIT (IQUOT N SOPD I DOPD J) N))
Observe that (NUMBERP (DIVS-N N SOPD I DOPD J)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVS-N
(DEFN DIVS-CVZNX
(N SOPD I DOPD J CCR)
(CVZNX (B0)
(B0)
(DIVS-Z N SOPD I DOPD J)
(DIVS-N N SOPD I DOPD J)
(CCR-X CCR)))
Observe that (NUMBERP (DIVS-CVZNX N SOPD I DOPD J CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVS-CVZNX
(DEFN DIVS_W-INS
(SOPD DN S)
(IF (EQUAL (NAT-TO-INT SOPD (W)) 0)
(HALT 'TRAP-EXCEPTION S)
(LET ((DOPD (READ-DN (L) DN S)))
(IF (B0P (DIVS-V (W) SOPD (W) DOPD (L)))
(UPDATE-CCR (DIVS-CVZNX (W)
SOPD
(W)
DOPD
(L)
(MC-CCR S))
(WRITE-DN (L)
(APP (W)
(IQUOT (W) SOPD (W) DOPD (L))
(IREM (W) SOPD (W) DOPD (L)))
DN S))
(HALT 'DIVS-OVERFLOW
(UPDATE-CCR (SET-V (B1) (MC-CCR S))
S))))))
Observe that (LISTP (DIVS_W-INS SOPD DN S)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVS_W-INS
(DEFN QUOT
(N X Y)
(HEAD (QUOTIENT Y X) N))
Note that (NUMBERP (QUOT N X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
QUOT
(DEFN REM
(N X Y)
(HEAD (REMAINDER Y X) N))
Note that (NUMBERP (REM N X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
REM
(DEFN DIVU-V
(N SOPD DOPD)
(IF (LESSP (QUOTIENT DOPD SOPD) (EXP 2 N))
(B0)
(B1)))
Note that (NUMBERP (DIVU-V N SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVU-V
(DEFN DIVU-Z
(N SOPD DOPD)
(IF (EQUAL (QUOT N SOPD DOPD) 0)
(B1)
(B0)))
Note that (NUMBERP (DIVU-Z N SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVU-Z
(DEFN DIVU-N
(N SOPD DOPD)
(MBIT (QUOT N SOPD DOPD) N))
From the definition we can conclude that (NUMBERP (DIVU-N N SOPD DOPD))
is a theorem.
[ 0.0 0.0 0.0 ]
DIVU-N
(DEFN DIVU-CVZNX
(N SOPD DOPD CCR)
(CVZNX (B0)
(B0)
(DIVU-Z N SOPD DOPD)
(DIVU-N N SOPD DOPD)
(CCR-X CCR)))
Observe that (NUMBERP (DIVU-CVZNX N SOPD DOPD CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVU-CVZNX
(DEFN DIVU_W-INS
(SOPD DN S)
(IF (EQUAL (NAT-TO-UINT SOPD) 0)
(HALT 'TRAP-EXCEPTION S)
(LET ((DOPD (READ-DN (L) DN S)))
(IF (B0P (DIVU-V (W) SOPD DOPD))
(UPDATE-CCR (DIVU-CVZNX (W) SOPD DOPD (MC-CCR S))
(WRITE-DN (L)
(APP (W)
(QUOT (W) SOPD DOPD)
(REM (W) SOPD DOPD))
DN S))
(HALT 'DIVU-OVERFLOW
(UPDATE-CCR (SET-V (B1) (MC-CCR S))
S))))))
Note that (LISTP (DIVU_W-INS SOPD DN S)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVU_W-INS
(DEFN DIV_W-INS
(INS S)
(IF (MUL&DIV-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(LET ((SOPD (OPERAND (W) (CDR S&ADDR) S)))
(IF (B0P (BITN INS 8))
(DIVU_W-INS SOPD
(D_RN INS)
(CAR S&ADDR))
(DIVS_W-INS SOPD
(D_RN INS)
(CAR S&ADDR))))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
DIV_W-INS
(DEFN OR-GROUP
(OPLEN INS S)
(IF (EQUAL OPLEN (Q))
(DIV_W-INS INS S)
(IF (B0P (BITN INS 8))
(OR-INS1 OPLEN INS S)
(IF (LESSP (S_MODE INS) 2)
(HALT 'SBCD-PACK-UNPK-UNSPECIFIED S)
(OR-INS2 OPLEN INS S)))))
[ 0.0 0.0 0.0 ]
OR-GROUP
(DEFN ROL
(LEN X CNT)
(LET ((N (REMAINDER CNT LEN)))
(APP N
(TAIL X (DIFFERENCE LEN N))
(HEAD X (DIFFERENCE LEN N)))))
Observe that (NUMBERP (ROL LEN X CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ROL
(DEFN ROR
(LEN X CNT)
(LET ((N (REMAINDER CNT LEN)))
(APP (DIFFERENCE LEN N)
(TAIL X N)
(HEAD X N))))
Observe that (NUMBERP (ROR LEN X CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ROR
(DEFN S&R-ADDR-MODEP
(INS)
(AND (MEMORY-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that (OR (FALSEP (S&R-ADDR-MODEP INS)) (TRUEP (S&R-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
S&R-ADDR-MODEP
(DEFN I-DATA (N) (IF (ZEROP N) 8 N))
Note that (NUMBERP (I-DATA N)) is a theorem.
[ 0.0 0.0 0.0 ]
I-DATA
(DEFN SR-CNT
(INS S)
(IF (B0P (BITN INS 5))
(I-DATA (D_RN INS))
(REMAINDER (READ-DN (B) (D_RN INS) S)
64)))
Note that (NUMBERP (SR-CNT INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
SR-CNT
(DEFN ROL-C
(LEN X CNT)
(IF (EQUAL CNT 0)
(B0)
(LET ((N (REMAINDER CNT LEN)))
(IF (ZEROP N)
(BCAR X)
(BITN X (DIFFERENCE LEN N))))))
Observe that (NUMBERP (ROL-C LEN X CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ROL-C
(DEFN ROL-Z
(LEN X CNT)
(IF (EQUAL X 0) (B1) (B0)))
WARNING: LEN and CNT are in the arglist but not in the body of the definition
of ROL-Z.
Observe that (NUMBERP (ROL-Z LEN X CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ROL-Z
(DEFN ROL-N
(LEN X CNT)
(BITN X
(SUB1 (DIFFERENCE LEN
(REMAINDER CNT LEN)))))
Observe that (NUMBERP (ROL-N LEN X CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ROL-N
(DEFN ROL-CVZNX
(LEN OPD CNT CCR)
(CVZNX (ROL-C LEN OPD CNT)
(B0)
(ROL-Z LEN OPD CNT)
(ROL-N LEN OPD CNT)
(CCR-X CCR)))
Observe that (NUMBERP (ROL-CVZNX LEN OPD CNT CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
ROL-CVZNX
(DEFN ROL-EFFECT
(LEN OPD CNT CCR)
(CONS (ROL LEN OPD CNT)
(ROL-CVZNX LEN OPD CNT CCR)))
From the definition we can conclude that:
(LISTP (ROL-EFFECT LEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
ROL-EFFECT
(DEFN REGISTER-ROL-INS
(OPLEN INS S)
(D-MAPPING OPLEN
(ROL-EFFECT OPLEN
(READ-DN OPLEN (S_RN INS) S)
(SR-CNT INS S)
(MC-CCR S))
(S_RN INS)
S))
Note that (LISTP (REGISTER-ROL-INS OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
REGISTER-ROL-INS
(DEFN ROR-C
(LEN X CNT)
(IF (EQUAL CNT 0)
(B0)
(LET ((N (REMAINDER CNT LEN)))
(IF (EQUAL N 0)
(BITN X (SUB1 LEN))
(BITN X (SUB1 N))))))
From the definition we can conclude that (NUMBERP (ROR-C LEN X CNT)) is a
theorem.
[ 0.0 0.0 0.0 ]
ROR-C
(DEFN ROR-Z
(LEN OPD CNT)
(IF (EQUAL OPD 0) (B1) (B0)))
WARNING: LEN and CNT are in the arglist but not in the body of the definition
of ROR-Z.
Observe that (NUMBERP (ROR-Z LEN OPD CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ROR-Z
(DEFN ROR-N
(LEN X CNT)
(LET ((N (REMAINDER CNT LEN)))
(IF (ZEROP N)
(BITN X (SUB1 LEN))
(BITN X (SUB1 N)))))
Observe that (NUMBERP (ROR-N LEN X CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ROR-N
(DEFN ROR-CVZNX
(LEN OPD CNT CCR)
(CVZNX (ROR-C LEN OPD CNT)
(B0)
(ROR-Z LEN OPD CNT)
(ROR-N LEN OPD CNT)
(CCR-X CCR)))
Observe that (NUMBERP (ROR-CVZNX LEN OPD CNT CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
ROR-CVZNX
(DEFN ROR-EFFECT
(OPLEN OPD CNT CCR)
(CONS (ROR OPLEN OPD CNT)
(ROR-CVZNX OPLEN OPD CNT CCR)))
From the definition we can conclude that:
(LISTP (ROR-EFFECT OPLEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
ROR-EFFECT
(DEFN REGISTER-ROR-INS
(OPLEN INS S)
(D-MAPPING OPLEN
(ROR-EFFECT OPLEN
(READ-DN OPLEN (S_RN INS) S)
(SR-CNT INS S)
(MC-CCR S))
(S_RN INS)
S))
Note that (LISTP (REGISTER-ROR-INS OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
REGISTER-ROR-INS
(DEFN MEM-ROL-EFFECT
(OPD CCR)
(ROL-EFFECT (W) OPD 1 CCR))
From the definition we can conclude that (LISTP (MEM-ROL-EFFECT OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
MEM-ROL-EFFECT
(DEFN MEM-ROL-INS
(INS S)
(IF (S&R-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (W)
(MEM-ROL-EFFECT (OPERAND (W) (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MEM-ROL-INS
(DEFN MEM-ROR-EFFECT
(OPD CCR)
(ROR-EFFECT (W) OPD 1 CCR))
From the definition we can conclude that (LISTP (MEM-ROR-EFFECT OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
MEM-ROR-EFFECT
(DEFN MEM-ROR-INS
(INS S)
(IF (S&R-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (W)
(MEM-ROR-EFFECT (OPERAND (W) (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MEM-ROR-INS
(DEFN LSL-C
(LEN OPD CNT)
(IF (EQUAL CNT 0)
(B0)
(IF (LESSP LEN CNT)
(B0)
(BITN OPD (DIFFERENCE LEN CNT)))))
From the definition we can conclude that (NUMBERP (LSL-C LEN OPD CNT)) is
a theorem.
[ 0.0 0.0 0.0 ]
LSL-C
(DEFN LSL-Z
(LEN OPD CNT)
(IF (EQUAL (LSL LEN OPD CNT) 0)
(B1)
(B0)))
Note that (NUMBERP (LSL-Z LEN OPD CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
LSL-Z
(DEFN LSL-N
(LEN OPD CNT)
(MBIT (LSL LEN OPD CNT) LEN))
From the definition we can conclude that (NUMBERP (LSL-N LEN OPD CNT)) is
a theorem.
[ 0.0 0.0 0.0 ]
LSL-N
(DEFN LSL-X
(LEN OPD CNT CCR)
(IF (EQUAL CNT 0)
(CCR-X CCR)
(LSL-C LEN OPD CNT)))
From the definition we can conclude that:
(NUMBERP (LSL-X LEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
LSL-X
(DEFN LSL-CVZNX
(LEN OPD CNT CCR)
(CVZNX (LSL-C LEN OPD CNT)
(B0)
(LSL-Z LEN OPD CNT)
(LSL-N LEN OPD CNT)
(LSL-X LEN OPD CNT CCR)))
Observe that (NUMBERP (LSL-CVZNX LEN OPD CNT CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
LSL-CVZNX
(DEFN LSL-EFFECT
(LEN OPD CNT CCR)
(CONS (LSL LEN OPD CNT)
(LSL-CVZNX LEN OPD CNT CCR)))
From the definition we can conclude that:
(LISTP (LSL-EFFECT LEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
LSL-EFFECT
(DEFN REGISTER-LSL-INS
(OPLEN INS S)
(D-MAPPING OPLEN
(LSL-EFFECT OPLEN
(READ-DN OPLEN (S_RN INS) S)
(SR-CNT INS S)
(MC-CCR S))
(S_RN INS)
S))
Note that (LISTP (REGISTER-LSL-INS OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
REGISTER-LSL-INS
(DEFN LSR-C
(LEN OPD CNT)
(IF (EQUAL CNT 0)
(B0)
(IF (LESSP LEN CNT)
(B0)
(BITN OPD (SUB1 CNT)))))
Note that (NUMBERP (LSR-C LEN OPD CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
LSR-C
(DEFN LSR-Z
(LEN OPD CNT)
(IF (EQUAL (LSR OPD CNT) 0)
(B1)
(B0)))
WARNING: LEN is in the arglist but not in the body of the definition of LSR-Z.
Observe that (NUMBERP (LSR-Z LEN OPD CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
LSR-Z
(DEFN LSR-N
(LEN OPD CNT)
(MBIT (LSR OPD CNT) LEN))
Note that (NUMBERP (LSR-N LEN OPD CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
LSR-N
(DEFN LSR-X
(LEN OPD CNT CCR)
(IF (EQUAL CNT 0)
(CCR-X CCR)
(LSR-C LEN OPD CNT)))
From the definition we can conclude that:
(NUMBERP (LSR-X LEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
LSR-X
(DEFN LSR-CVZNX
(LEN OPD CNT CCR)
(CVZNX (LSR-C LEN OPD CNT)
(B0)
(LSR-Z LEN OPD CNT)
(LSR-N LEN OPD CNT)
(LSR-X LEN OPD CNT CCR)))
Observe that (NUMBERP (LSR-CVZNX LEN OPD CNT CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
LSR-CVZNX
(DEFN LSR-EFFECT
(LEN OPD CNT CCR)
(CONS (LSR OPD CNT)
(LSR-CVZNX LEN OPD CNT CCR)))
Note that (LISTP (LSR-EFFECT LEN OPD CNT CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
LSR-EFFECT
(DEFN REGISTER-LSR-INS
(OPLEN INS S)
(D-MAPPING OPLEN
(LSR-EFFECT OPLEN
(READ-DN OPLEN (S_RN INS) S)
(SR-CNT INS S)
(MC-CCR S))
(S_RN INS)
S))
Note that (LISTP (REGISTER-LSR-INS OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
REGISTER-LSR-INS
(DEFN MEM-LSL-EFFECT
(OPD CCR)
(LSL-EFFECT (W) OPD 1 CCR))
From the definition we can conclude that (LISTP (MEM-LSL-EFFECT OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
MEM-LSL-EFFECT
(DEFN MEM-LSL-INS
(INS S)
(IF (S&R-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (W)
(MEM-LSL-EFFECT (OPERAND (W) (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MEM-LSL-INS
(DEFN MEM-LSR-EFFECT
(OPD CCR)
(LSR-EFFECT (W) OPD 1 CCR))
From the definition we can conclude that (LISTP (MEM-LSR-EFFECT OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
MEM-LSR-EFFECT
(DEFN MEM-LSR-INS
(INS S)
(IF (S&R-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (W)
(MEM-LSR-EFFECT (OPERAND (W) (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MEM-LSR-INS
(DEFN ASL-C
(LEN OPD CNT)
(LSL-C LEN OPD CNT))
Note that (NUMBERP (ASL-C LEN OPD CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ASL-C
(DEFN ASL-V
(LEN OPD CNT)
(IF (INT-RANGEP (NAT-TO-INT OPD LEN)
(DIFFERENCE LEN CNT))
(B0)
(B1)))
Note that (NUMBERP (ASL-V LEN OPD CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ASL-V
(DEFN ASL-Z
(LEN OPD CNT)
(IF (EQUAL (ASL LEN OPD CNT) 0)
(B1)
(B0)))
Note that (NUMBERP (ASL-Z LEN OPD CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ASL-Z
(DEFN ASL-N
(LEN OPD CNT)
(MBIT (ASL LEN OPD CNT) LEN))
From the definition we can conclude that (NUMBERP (ASL-N LEN OPD CNT)) is
a theorem.
[ 0.0 0.0 0.0 ]
ASL-N
(DEFN ASL-X
(LEN OPD CNT CCR)
(IF (EQUAL CNT 0)
(CCR-X CCR)
(ASL-C LEN OPD CNT)))
From the definition we can conclude that:
(NUMBERP (ASL-X LEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
ASL-X
(DEFN ASL-CVZNX
(LEN OPD CNT CCR)
(CVZNX (ASL-C LEN OPD CNT)
(ASL-V LEN OPD CNT)
(ASL-Z LEN OPD CNT)
(ASL-N LEN OPD CNT)
(ASL-X LEN OPD CNT CCR)))
Observe that (NUMBERP (ASL-CVZNX LEN OPD CNT CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
ASL-CVZNX
(DEFN ASL-EFFECT
(LEN OPD CNT CCR)
(CONS (ASL LEN OPD CNT)
(ASL-CVZNX LEN OPD CNT CCR)))
From the definition we can conclude that:
(LISTP (ASL-EFFECT LEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
ASL-EFFECT
(DEFN REGISTER-ASL-INS
(OPLEN INS S)
(D-MAPPING OPLEN
(ASL-EFFECT OPLEN
(READ-DN OPLEN (S_RN INS) S)
(SR-CNT INS S)
(MC-CCR S))
(S_RN INS)
S))
Note that (LISTP (REGISTER-ASL-INS OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
REGISTER-ASL-INS
(DEFN ASR-C
(LEN OPD CNT)
(IF (EQUAL CNT 0)
(B0)
(IF (LESSP CNT LEN)
(BITN OPD (SUB1 CNT))
(BITN OPD (SUB1 LEN)))))
From the definition we can conclude that (NUMBERP (ASR-C LEN OPD CNT)) is
a theorem.
[ 0.0 0.0 0.0 ]
ASR-C
(DEFN ASR-Z
(LEN OPD CNT)
(IF (EQUAL (ASR LEN OPD CNT) 0)
(B1)
(B0)))
Note that (NUMBERP (ASR-Z LEN OPD CNT)) is a theorem.
[ 0.0 0.0 0.0 ]
ASR-Z
(DEFN ASR-N
(LEN OPD CNT)
(MBIT (ASR LEN OPD CNT) LEN))
From the definition we can conclude that (NUMBERP (ASR-N LEN OPD CNT)) is
a theorem.
[ 0.2 0.0 0.0 ]
ASR-N
(DEFN ASR-X
(LEN OPD CNT CCR)
(IF (EQUAL CNT 0)
(CCR-X CCR)
(ASR-C LEN OPD CNT)))
From the definition we can conclude that:
(NUMBERP (ASR-X LEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
ASR-X
(DEFN ASR-CVZNX
(LEN OPD CNT CCR)
(CVZNX (ASR-C LEN OPD CNT)
(B0)
(ASR-Z LEN OPD CNT)
(ASR-N LEN OPD CNT)
(ASR-X LEN OPD CNT CCR)))
Observe that (NUMBERP (ASR-CVZNX LEN OPD CNT CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
ASR-CVZNX
(DEFN ASR-EFFECT
(LEN OPD CNT CCR)
(CONS (ASR LEN OPD CNT)
(ASR-CVZNX LEN OPD CNT CCR)))
From the definition we can conclude that:
(LISTP (ASR-EFFECT LEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
ASR-EFFECT
(DEFN REGISTER-ASR-INS
(OPLEN INS S)
(D-MAPPING OPLEN
(ASR-EFFECT OPLEN
(READ-DN OPLEN (S_RN INS) S)
(SR-CNT INS S)
(MC-CCR S))
(S_RN INS)
S))
Note that (LISTP (REGISTER-ASR-INS OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
REGISTER-ASR-INS
(DEFN MEM-ASL-EFFECT
(OPD CCR)
(ASL-EFFECT (W) OPD 1 CCR))
From the definition we can conclude that (LISTP (MEM-ASL-EFFECT OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
MEM-ASL-EFFECT
(DEFN MEM-ASL-INS
(INS S)
(IF (S&R-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (W)
(MEM-ASL-EFFECT (OPERAND (W) (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MEM-ASL-INS
(DEFN MEM-ASR-EFFECT
(OPD CCR)
(ASR-EFFECT (W) OPD 1 CCR))
From the definition we can conclude that (LISTP (MEM-ASR-EFFECT OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
MEM-ASR-EFFECT
(DEFN MEM-ASR-INS
(INS S)
(IF (S&R-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (W)
(MEM-ASR-EFFECT (OPERAND (W) (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MEM-ASR-INS
(DEFN ROXL
(LEN OPD CNT X)
(LET ((TEMP (PLUS X (TIMES 2 OPD))))
(BCDR (ROL (ADD1 LEN) TEMP CNT))))
Note that (NUMBERP (ROXL LEN OPD CNT X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROXL
(DEFN ROXR
(LEN OPD CNT X)
(LET ((TEMP (PLUS OPD (TIMES X (EXP 2 LEN)))))
(HEAD (ROR (ADD1 LEN) TEMP CNT) LEN)))
From the definition we can conclude that (NUMBERP (ROXR LEN OPD CNT X))
is a theorem.
[ 0.0 0.0 0.0 ]
ROXR
(DEFN ROXL-C
(LEN OPD CNT X)
(LET ((TMP (REMAINDER CNT (ADD1 LEN))))
(IF (EQUAL TMP 0)
(FIX-BIT X)
(BITN OPD (DIFFERENCE LEN TMP)))))
Observe that (NUMBERP (ROXL-C LEN OPD CNT X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROXL-C
(DEFN ROXL-Z
(LEN OPD CNT X)
(IF (EQUAL (ROXL LEN OPD CNT X) 0)
(B1)
(B0)))
Note that (NUMBERP (ROXL-Z LEN OPD CNT X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROXL-Z
(DEFN ROXL-N
(LEN OPD CNT X)
(BITN (ROXL LEN OPD CNT X)
(SUB1 LEN)))
Observe that (NUMBERP (ROXL-N LEN OPD CNT X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROXL-N
(DEFN ROXL-CVZNX
(LEN OPD CNT X)
(CVZNX (ROXL-C LEN OPD CNT X)
(B0)
(ROXL-Z LEN OPD CNT X)
(ROXL-N LEN OPD CNT X)
(ROXL-C LEN OPD CNT X)))
Observe that (NUMBERP (ROXL-CVZNX LEN OPD CNT X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROXL-CVZNX
(DEFN ROXL-EFFECT
(LEN OPD CNT CCR)
(CONS (ROXL LEN OPD CNT (CCR-X CCR))
(ROXL-CVZNX LEN OPD CNT (CCR-X CCR))))
From the definition we can conclude that:
(LISTP (ROXL-EFFECT LEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
ROXL-EFFECT
(DEFN REGISTER-ROXL-INS
(OPLEN INS S)
(D-MAPPING OPLEN
(ROXL-EFFECT OPLEN
(READ-DN OPLEN (S_RN INS) S)
(SR-CNT INS S)
(MC-CCR S))
(S_RN INS)
S))
Note that (LISTP (REGISTER-ROXL-INS OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
REGISTER-ROXL-INS
(DEFN ROXR-C
(LEN OPD CNT X)
(LET ((TMP (REMAINDER CNT (ADD1 LEN))))
(IF (EQUAL TMP 0)
(FIX-BIT X)
(BITN OPD (SUB1 TMP)))))
From the definition we can conclude that (NUMBERP (ROXR-C LEN OPD CNT X))
is a theorem.
[ 0.0 0.0 0.0 ]
ROXR-C
(DEFN ROXR-Z
(LEN OPD CNT X)
(IF (EQUAL (ROXR LEN OPD CNT X) 0)
(B1)
(B0)))
Note that (NUMBERP (ROXR-Z LEN OPD CNT X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROXR-Z
(DEFN ROXR-N
(LEN OPD CNT X)
(BITN (ROXR LEN OPD CNT X)
(SUB1 LEN)))
Observe that (NUMBERP (ROXR-N LEN OPD CNT X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROXR-N
(DEFN ROXR-CVZNX
(LEN OPD CNT X)
(CVZNX (ROXR-C LEN OPD CNT X)
(B0)
(ROXR-Z LEN OPD CNT X)
(ROXR-N LEN OPD CNT X)
(ROXR-C LEN OPD CNT X)))
Observe that (NUMBERP (ROXR-CVZNX LEN OPD CNT X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROXR-CVZNX
(DEFN ROXR-EFFECT
(LEN OPD CNT CCR)
(CONS (ROXR LEN OPD CNT (CCR-X CCR))
(ROXR-CVZNX LEN OPD CNT (CCR-X CCR))))
From the definition we can conclude that:
(LISTP (ROXR-EFFECT LEN OPD CNT CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
ROXR-EFFECT
(DEFN REGISTER-ROXR-INS
(OPLEN INS S)
(D-MAPPING OPLEN
(ROXR-EFFECT OPLEN
(READ-DN OPLEN (S_RN INS) S)
(SR-CNT INS S)
(MC-CCR S))
(S_RN INS)
S))
Note that (LISTP (REGISTER-ROXR-INS OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
REGISTER-ROXR-INS
(DEFN MEM-ROXL-EFFECT
(OPD CCR)
(ROXL-EFFECT (W) OPD 1 CCR))
From the definition we can conclude that:
(LISTP (MEM-ROXL-EFFECT OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
MEM-ROXL-EFFECT
(DEFN MEM-ROXL-INS
(INS S)
(IF (S&R-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (W)
(MEM-ROXL-EFFECT (OPERAND (W) (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MEM-ROXL-INS
(DEFN MEM-ROXR-EFFECT
(OPD CCR)
(ROXR-EFFECT (W) OPD 1 CCR))
From the definition we can conclude that:
(LISTP (MEM-ROXR-EFFECT OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
MEM-ROXR-EFFECT
(DEFN MEM-ROXR-INS
(INS S)
(IF (S&R-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (W)
(MEM-ROXR-EFFECT (OPERAND (W) (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MEM-ROXR-INS
(DEFN MEMORY-SHIFT-ROTATE
(INS S)
(IF (B0P (BITN INS 10))
(IF (B0P (BITN INS 9))
(IF (B0P (BITN INS 8))
(MEM-ASR-INS INS S)
(MEM-ASL-INS INS S))
(IF (B0P (BITN INS 8))
(MEM-LSR-INS INS S)
(MEM-LSL-INS INS S)))
(IF (B0P (BITN INS 9))
(IF (B0P (BITN INS 8))
(MEM-ROXR-INS INS S)
(MEM-ROXL-INS INS S))
(IF (B0P (BITN INS 8))
(MEM-ROR-INS INS S)
(MEM-ROL-INS INS S)))))
[ 0.0 0.0 0.0 ]
MEMORY-SHIFT-ROTATE
(DEFN REGISTER-SHIFT-ROTATE
(OPLEN INS S)
(IF (B0P (BITN INS 4))
(IF (B0P (BITN INS 3))
(IF (B0P (BITN INS 8))
(REGISTER-ASR-INS OPLEN INS S)
(REGISTER-ASL-INS OPLEN INS S))
(IF (B0P (BITN INS 8))
(REGISTER-LSR-INS OPLEN INS S)
(REGISTER-LSL-INS OPLEN INS S)))
(IF (B0P (BITN INS 3))
(IF (B0P (BITN INS 8))
(REGISTER-ROXR-INS OPLEN INS S)
(REGISTER-ROXL-INS OPLEN INS S))
(IF (B0P (BITN INS 8))
(REGISTER-ROR-INS OPLEN INS S)
(REGISTER-ROL-INS OPLEN INS S)))))
Note that (LISTP (REGISTER-SHIFT-ROTATE OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
REGISTER-SHIFT-ROTATE
(DEFN BF-SUBGROUP
(INS S)
(HALT 'I-WILL-DO-IT-LATER S))
WARNING: INS is in the arglist but not in the body of the definition of
BF-SUBGROUP.
Note that (LISTP (BF-SUBGROUP INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
BF-SUBGROUP
(DEFN S&R-GROUP
(INS S)
(IF (EQUAL (OP-LEN INS) (Q))
(IF (B0P (BITN INS 11))
(MEMORY-SHIFT-ROTATE INS S)
(BF-SUBGROUP INS S))
(REGISTER-SHIFT-ROTATE (OP-LEN INS)
INS S)))
[ 0.0 0.0 0.0 ]
S&R-GROUP
(DEFN MOVE-ADDR-MODEP
(OPLEN INS)
(AND (ADDR-MODEP (S_MODE INS) (S_RN INS))
(DATA-ADDR-MODEP (D_MODE INS)
(D_RN INS))
(ALTERABLE-ADDR-MODEP (D_MODE INS)
(D_RN INS))
(NOT (BYTE-AN-DIRECT-MODEP OPLEN
(S_MODE INS)))))
Observe that:
(OR (FALSEP (MOVE-ADDR-MODEP OPLEN INS))
(TRUEP (MOVE-ADDR-MODEP OPLEN INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVE-ADDR-MODEP
(DEFN MOVE-Z
(OPLEN SOPD)
(IF (EQUAL (HEAD SOPD OPLEN) 0)
(B1)
(B0)))
From the definition we can conclude that (NUMBERP (MOVE-Z OPLEN SOPD)) is
a theorem.
[ 0.0 0.0 0.0 ]
MOVE-Z
(DEFN MOVE-N
(OPLEN SOPD)
(MBIT SOPD OPLEN))
From the definition we can conclude that (NUMBERP (MOVE-N OPLEN SOPD)) is
a theorem.
[ 0.0 0.0 0.0 ]
MOVE-N
(DEFN MOVE-CVZNX
(OPLEN SOPD CCR)
(CVZNX (B0)
(B0)
(MOVE-Z OPLEN SOPD)
(MOVE-N OPLEN SOPD)
(CCR-X CCR)))
From the definition we can conclude that:
(NUMBERP (MOVE-CVZNX OPLEN SOPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVE-CVZNX
(DEFN MOVE-EFFECT
(OPLEN SOPD CCR)
(CONS SOPD
(MOVE-CVZNX OPLEN SOPD CCR)))
From the definition we can conclude that:
(LISTP (MOVE-EFFECT OPLEN SOPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVE-EFFECT
(DEFN MOVE-MAPPING
(SOPD OPLEN INS S)
(LET ((S&ADDR (EFFEC-ADDR OPLEN
(D_MODE INS)
(D_RN INS)
S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING OPLEN
(MOVE-EFFECT OPLEN SOPD (MC-CCR S))
S&ADDR))))
[ 0.0 0.0 0.0 ]
MOVE-MAPPING
(DEFN MOVE-INS
(OPLEN INS S)
(IF (MOVE-ADDR-MODEP OPLEN INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MOVE-MAPPING (OPERAND OPLEN (CDR S&ADDR) S)
OPLEN INS
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MOVE-INS
(DEFN MOVEA-ADDR-MODEP
(INS)
(ADDR-MODEP (S_MODE INS) (S_RN INS)))
Observe that:
(OR (FALSEP (MOVEA-ADDR-MODEP INS))
(TRUEP (MOVEA-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEA-ADDR-MODEP
(DEFN MOVEA-INS
(OPLEN INS S)
(IF (MOVEA-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(WRITE-AN (L)
(EXT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
(L))
(D_RN INS)
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MOVEA-INS
(DEFN MOVE-GROUP
(OPLEN INS S)
(IF (EQUAL (D_MODE INS) 1)
(MOVEA-INS OPLEN INS S)
(MOVE-INS OPLEN INS S)))
[ 0.0 0.0 0.0 ]
MOVE-GROUP
(DEFN LEA-ADDR-MODEP
(INS)
(CONTROL-ADDR-MODEP (S_MODE INS)
(S_RN INS)))
Observe that:
(OR (FALSEP (LEA-ADDR-MODEP INS))
(TRUEP (LEA-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
LEA-ADDR-MODEP
(DEFN LEA-INS
(SMODE INS S)
(IF (LEA-ADDR-MODEP INS)
(LET ((S&ADDR (EFFEC-ADDR (L) SMODE (S_RN INS) S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(WRITE-AN (L)
(CDDR S&ADDR)
(D_RN INS)
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
LEA-INS
(DEFN EXT-Z
(OPLEN OPD SIZE)
(IF (EQUAL (EXT OPLEN OPD SIZE) 0)
(B1)
(B0)))
Note that (NUMBERP (EXT-Z OPLEN OPD SIZE)) is a theorem.
[ 0.0 0.0 0.0 ]
EXT-Z
(DEFN EXT-N
(OPLEN OPD SIZE)
(MBIT (EXT OPLEN OPD SIZE) SIZE))
From the definition we can conclude that (NUMBERP (EXT-N OPLEN OPD SIZE))
is a theorem.
[ 0.0 0.0 0.0 ]
EXT-N
(DEFN EXT-CVZNX
(OPLEN OPD SIZE CCR)
(CVZNX (B0)
(B0)
(EXT-Z OPLEN OPD SIZE)
(EXT-N OPLEN OPD SIZE)
(CCR-X CCR)))
Observe that (NUMBERP (EXT-CVZNX OPLEN OPD SIZE CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
EXT-CVZNX
(DEFN EXT-EFFECT
(OPLEN OPD SIZE CCR)
(CONS (EXT OPLEN OPD SIZE)
(EXT-CVZNX OPLEN OPD SIZE CCR)))
From the definition we can conclude that:
(LISTP (EXT-EFFECT OPLEN OPD SIZE CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
EXT-EFFECT
(DEFN EXTB-INS
(INS S)
(D-MAPPING (L)
(EXT-EFFECT (B)
(READ-DN (B) (S_RN INS) S)
(L)
(MC-CCR S))
(S_RN INS)
S))
Note that (LISTP (EXTB-INS INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
EXTB-INS
(DEFN LEA-SUBGROUP
(INS S)
(IF (EQUAL (S_MODE INS) 0)
(IF (EQUAL (BITS INS 9 11) 4)
(EXTB-INS INS S)
(HALT (RESERVED-SIGNAL) S))
(LEA-INS (S_MODE INS) INS S)))
[ 0.0 0.0 0.0 ]
LEA-SUBGROUP
(DEFN CLR-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that (OR (FALSEP (CLR-ADDR-MODEP INS)) (TRUEP (CLR-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
CLR-ADDR-MODEP
(DEFN CLR-CVZNX
(CCR)
(CVZNX (B0)
(B0)
(B1)
(B0)
(CCR-X CCR)))
From the definition we can conclude that (NUMBERP (CLR-CVZNX CCR)) is a
theorem.
[ 0.0 0.0 0.0 ]
CLR-CVZNX
(DEFN CLR-EFFECT
(CCR)
(CONS 0 (CLR-CVZNX CCR)))
Observe that (LISTP (CLR-EFFECT CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
CLR-EFFECT
(DEFN CLR-INS
(OPLEN INS S)
(IF (CLR-ADDR-MODEP INS)
(LET ((S&ADDR (EFFEC-ADDR OPLEN
(S_MODE INS)
(S_RN INS)
S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING OPLEN
(CLR-EFFECT (MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
CLR-INS
(DEFN MOVE-FROM-CCR-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (MOVE-FROM-CCR-ADDR-MODEP INS))
(TRUEP (MOVE-FROM-CCR-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVE-FROM-CCR-ADDR-MODEP
(DEFN MOVE-FROM-CCR-EFFECT
(CCR)
(CONS CCR CCR))
Note that (LISTP (MOVE-FROM-CCR-EFFECT CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
MOVE-FROM-CCR-EFFECT
(DEFN MOVE-FROM-CCR-INS
(INS S)
(IF (MOVE-FROM-CCR-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (W)
(MOVE-FROM-CCR-EFFECT (MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MOVE-FROM-CCR-INS
(DEFN CLR-SUBGROUP
(INS S)
(IF (EQUAL (OP-LEN INS) (Q))
(MOVE-FROM-CCR-INS INS S)
(CLR-INS (OP-LEN INS) INS S)))
[ 0.0 0.0 0.0 ]
CLR-SUBGROUP
(DEFN NEGX-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (NEGX-ADDR-MODEP INS))
(TRUEP (NEGX-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
NEGX-ADDR-MODEP
(DEFN NEGX-INS
(OPLEN INS S)
(IF (NEGX-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING OPLEN
(SUBX-EFFECT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
0
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
NEGX-INS
(DEFN NEGX-SUBGROUP
(INS S)
(IF (EQUAL (OP-LEN INS) (Q))
(HALT 'MOVE-FROM-SR-PRIVILEGED S)
(NEGX-INS (OP-LEN INS) INS S)))
[ 0.0 0.0 0.0 ]
NEGX-SUBGROUP
(DEFN NEG-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that (OR (FALSEP (NEG-ADDR-MODEP INS)) (TRUEP (NEG-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
NEG-ADDR-MODEP
(DEFN NEG-INS
(OPLEN INS S)
(IF (NEG-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING OPLEN
(SUB-EFFECT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
0)
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
NEG-INS
(DEFN MOVE-TO-CCR-ADDR-MODEP
(INS)
(DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS)))
Observe that:
(OR (FALSEP (MOVE-TO-CCR-ADDR-MODEP INS))
(TRUEP (MOVE-TO-CCR-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVE-TO-CCR-ADDR-MODEP
(DEFN MOVE-TO-CCR-INS
(INS S)
(IF (MOVE-TO-CCR-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (W) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(UPDATE-CCR (HEAD (OPERAND (W) (CDR S&ADDR) S)
(B))
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MOVE-TO-CCR-INS
(DEFN NEG-SUBGROUP
(INS S)
(IF (EQUAL (OP-LEN INS) (Q))
(MOVE-TO-CCR-INS INS S)
(NEG-INS (OP-LEN INS) INS S)))
[ 0.0 0.0 0.0 ]
NEG-SUBGROUP
(DEFN PEA-ADDR-MODEP
(INS)
(CONTROL-ADDR-MODEP (S_MODE INS)
(S_RN INS)))
Observe that:
(OR (FALSEP (PEA-ADDR-MODEP INS))
(TRUEP (PEA-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
PEA-ADDR-MODEP
(DEFN PEA-INS
(SMODE INS S)
(IF (PEA-ADDR-MODEP INS)
(LET ((S&ADDR (EFFEC-ADDR (L) SMODE (S_RN INS) S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(PUSH-SP (LSZ)
(CDDR S&ADDR)
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
PEA-INS
(DEFN SWAP-Z
(OPD)
(IF (EQUAL (FIX OPD) 0) (B1) (B0)))
Observe that (NUMBERP (SWAP-Z OPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SWAP-Z
(DEFN SWAP-N (OPD) (BITN OPD 15))
Observe that (NUMBERP (SWAP-N OPD)) is a theorem.
[ 0.0 0.0 0.0 ]
SWAP-N
(DEFN SWAP-CVZNX
(OPD CCR)
(CVZNX (B0)
(B0)
(SWAP-Z OPD)
(SWAP-N OPD)
(CCR-X CCR)))
From the definition we can conclude that (NUMBERP (SWAP-CVZNX OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
SWAP-CVZNX
(DEFN SWAP-EFFECT
(OPD CCR)
(CONS (APP (W)
(TAIL OPD (W))
(HEAD OPD (W)))
(SWAP-CVZNX OPD CCR)))
From the definition we can conclude that (LISTP (SWAP-EFFECT OPD CCR)) is
a theorem.
[ 0.0 0.0 0.0 ]
SWAP-EFFECT
(DEFN SWAP-INS
(INS S)
(D-MAPPING (L)
(SWAP-EFFECT (READ-DN (L) (S_RN INS) S)
(MC-CCR S))
(S_RN INS)
S))
Observe that (LISTP (SWAP-INS INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
SWAP-INS
(DEFN PEA-SUBGROUP
(INS S)
(IF (LESSP (S_MODE INS) 2)
(IF (EQUAL (S_MODE INS) 0)
(SWAP-INS INS S)
(HALT 'BKPT-UNSPECIFIED S))
(PEA-INS (S_MODE INS) INS S)))
[ 0.0 0.0 0.0 ]
PEA-SUBGROUP
(DEFN EXT-INS
(INS S)
(IF (B0P (BITN INS 6))
(D-MAPPING (W)
(EXT-EFFECT (B)
(READ-DN (B) (S_RN INS) S)
(W)
(MC-CCR S))
(S_RN INS)
S)
(D-MAPPING (L)
(EXT-EFFECT (W)
(READ-DN (W) (S_RN INS) S)
(L)
(MC-CCR S))
(S_RN INS)
S)))
Observe that (LISTP (EXT-INS INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
EXT-INS
(DEFN READM-MEM
(OPSZ ADDR MEM N)
(IF (ZEROP N)
NIL
(CONS (READ-MEM ADDR MEM OPSZ)
(READM-MEM OPSZ
(ADD (L) ADDR OPSZ)
MEM
(SUB1 N)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, READM-MEM is accepted under the
principle of definition. From the definition we can conclude that:
(OR (LITATOM (READM-MEM OPSZ ADDR MEM N))
(LISTP (READM-MEM OPSZ ADDR MEM N)))
is a theorem.
[ 0.0 0.0 0.0 ]
READM-MEM
(DEFN WRITEM-MEM
(OPSZ VLST ADDR MEM)
(IF (LISTP VLST)
(WRITEM-MEM OPSZ
(CDR VLST)
(ADD (L) ADDR OPSZ)
(WRITE-MEM (CAR VLST) ADDR MEM OPSZ))
MEM))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT VLST) decreases according to the well-founded relation LESSP in each
recursive call. Hence, WRITEM-MEM is accepted under the principle of
definition. Note that:
(OR (LISTP (WRITEM-MEM OPSZ VLST ADDR MEM))
(EQUAL (WRITEM-MEM OPSZ VLST ADDR MEM)
MEM))
is a theorem.
[ 0.0 0.0 0.0 ]
WRITEM-MEM
(DEFN READM-RN
(OPLEN RNLST RFILE)
(IF (LISTP RNLST)
(CONS (READ-RN OPLEN (CAR RNLST) RFILE)
(READM-RN OPLEN (CDR RNLST) RFILE))
NIL))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT RNLST) decreases according to the well-founded relation LESSP in each
recursive call. Hence, READM-RN is accepted under the definitional principle.
Note that:
(OR (LITATOM (READM-RN OPLEN RNLST RFILE))
(LISTP (READM-RN OPLEN RNLST RFILE)))
is a theorem.
[ 0.0 0.0 0.0 ]
READM-RN
(DEFN WRITEM-RN
(OPLEN VLST RNLST RFILE)
(IF (LISTP RNLST)
(WRITEM-RN OPLEN
(CDR VLST)
(CDR RNLST)
(WRITE-RN (L)
(EXT OPLEN (CAR VLST) (L))
(CAR RNLST)
RFILE))
RFILE))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT RNLST) decreases according to the well-founded relation LESSP in each
recursive call. Hence, WRITEM-RN is accepted under the definitional principle.
Observe that:
(OR (LISTP (WRITEM-RN OPLEN VLST RNLST RFILE))
(EQUAL (WRITEM-RN OPLEN VLST RNLST RFILE)
RFILE))
is a theorem.
[ 0.0 0.0 0.0 ]
WRITEM-RN
(DEFN MOVEM-RNLST
(MASK I)
(IF (ZEROP MASK)
NIL
(IF (B0P (BCAR MASK))
(MOVEM-RNLST (BCDR MASK) (ADD1 I))
(CONS I
(MOVEM-RNLST (BCDR MASK) (ADD1 I))))))
Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, and
COUNT-NUMBERP, and the definitions of NUMBERP, EQUAL, BCDR, B0P, B0, BCAR, and
ZEROP can be used to show that the measure (COUNT MASK) decreases according to
the well-founded relation LESSP in each recursive call. Hence, MOVEM-RNLST is
accepted under the definitional principle. Note that:
(OR (LITATOM (MOVEM-RNLST MASK I))
(LISTP (MOVEM-RNLST MASK I)))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEM-RNLST
(DEFN MOVEM-LEN
(MASK)
(IF (ZEROP MASK)
0
(IF (B0P (BCAR MASK))
(MOVEM-LEN (BCDR MASK))
(ADD1 (MOVEM-LEN (BCDR MASK))))))
Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, and
COUNT-NUMBERP, and the definitions of NUMBERP, EQUAL, BCDR, B0P, B0, BCAR, and
ZEROP can be used to show that the measure (COUNT MASK) decreases according to
the well-founded relation LESSP in each recursive call. Hence, MOVEM-LEN is
accepted under the definitional principle. Observe that:
(NUMBERP (MOVEM-LEN MASK))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEM-LEN
(DEFN WRITEMP
(MASK OPLEN ADDR MEM)
(WRITE-MEMP ADDR MEM
(TIMES (OP-SZ OPLEN)
(MOVEM-LEN MASK))))
Note that:
(OR (FALSEP (WRITEMP MASK OPLEN ADDR MEM))
(TRUEP (WRITEMP MASK OPLEN ADDR MEM)))
is a theorem.
[ 0.0 0.0 0.0 ]
WRITEMP
(DEFN MOVEM-PRE-RNLST
(MASK I LST)
(IF (ZEROP MASK)
LST
(IF (B0P (BCAR MASK))
(MOVEM-PRE-RNLST (BCDR MASK)
(SUB1 I)
LST)
(MOVEM-PRE-RNLST (BCDR MASK)
(SUB1 I)
(CONS I LST)))))
Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, and
COUNT-NUMBERP, and the definitions of NUMBERP, EQUAL, BCDR, B0P, B0, BCAR, and
ZEROP establish that the measure (COUNT MASK) decreases according to the
well-founded relation LESSP in each recursive call. Hence, MOVEM-PRE-RNLST is
accepted under the definitional principle. Note that:
(OR (LISTP (MOVEM-PRE-RNLST MASK I LST))
(EQUAL (MOVEM-PRE-RNLST MASK I LST)
LST))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEM-PRE-RNLST
(DEFN MOVEM-PREDEC
(MASK OPLEN RN S)
(LET ((ADDR (READ-AN (L) RN S)))
(CONS (WRITE-AN (L)
(PRE-EFFECT OPLEN RN ADDR)
RN S)
(CONS 'M
(SUB (L)
(TIMES (OP-SZ OPLEN) (MOVEM-LEN MASK))
ADDR)))))
From the definition we can conclude that:
(LISTP (MOVEM-PREDEC MASK OPLEN RN S))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEM-PREDEC
(DEFN MOVEM-RN-EA-ADDR-MODEP
(INS)
(AND (ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(CONTROL-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (MOVEM-RN-EA-ADDR-MODEP INS))
(TRUEP (MOVEM-RN-EA-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEM-RN-EA-ADDR-MODEP
(DEFN MOVEM-RN-EA-INS
(MASK OPLEN INS S)
(IF
(PREDEC-MODEP (S_MODE INS))
(LET
((S&ADDR (MOVEM-PREDEC MASK OPLEN
(S_RN INS)
S)))
(IF
(WRITEMP MASK OPLEN
(CDDR S&ADDR)
(MC-MEM S))
(WRITE-AN (L)
(CDDR S&ADDR)
(S_RN INS)
(UPDATE-MEM (WRITEM-MEM (OP-SZ OPLEN)
(READM-RN OPLEN
(MOVEM-PRE-RNLST MASK 15 NIL)
(MC-RFILE (CAR S&ADDR)))
(CDDR S&ADDR)
(MC-MEM S))
(CAR S&ADDR)))
(HALT (WRITE-SIGNAL) S)))
(IF (MOVEM-RN-EA-ADDR-MODEP INS)
(LET ((S&ADDR (EFFEC-ADDR OPLEN
(S_MODE INS)
(S_RN INS)
S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(IF (WRITEMP MASK OPLEN
(CDDR S&ADDR)
(MC-MEM S))
(UPDATE-MEM (WRITEM-MEM (OP-SZ OPLEN)
(READM-RN OPLEN
(MOVEM-RNLST MASK 0)
(MC-RFILE S))
(CDDR S&ADDR)
(MC-MEM S))
(CAR S&ADDR))
(HALT (WRITE-SIGNAL) S))))
(HALT (MODE-SIGNAL) S))))
[ 0.0 0.0 0.0 ]
MOVEM-RN-EA-INS
(DEFN EXT-SUBGROUP
(INS S)
(IF (EQUAL (S_MODE INS) 0)
(EXT-INS INS S)
(IF (PC-WORD-READP (MC-PC S) (MC-MEM S))
(MOVEM-RN-EA-INS (PC-WORD-READ (MC-PC S) (MC-MEM S))
(IF (B0P (BITN INS 6)) (W) (L))
INS
(UPDATE-PC (ADD (L) (MC-PC S) (WSZ))
S))
(HALT (PC-SIGNAL) S))))
[ 0.0 0.0 0.0 ]
EXT-SUBGROUP
(DEFN TST-ADDR-MODEP
(OPLEN INS)
(IF (EQUAL OPLEN (B))
(DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ADDR-MODEP (S_MODE INS) (S_RN INS))))
From the definition we can conclude that:
(OR (FALSEP (TST-ADDR-MODEP OPLEN INS))
(TRUEP (TST-ADDR-MODEP OPLEN INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
TST-ADDR-MODEP
(DEFN TST-INS
(OPLEN INS S)
(IF (TST-ADDR-MODEP OPLEN INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(UPDATE-CCR (MOVE-CVZNX OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
(MC-CCR S))
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
TST-INS
(DEFN TAS-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that (OR (FALSEP (TAS-ADDR-MODEP INS)) (TRUEP (TAS-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
TAS-ADDR-MODEP
(DEFN TAS-EFFECT
(OPD CCR)
(CONS (SETN OPD 7 (B1))
(MOVE-CVZNX (B) OPD CCR)))
Observe that (LISTP (TAS-EFFECT OPD CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
TAS-EFFECT
(DEFN TAS-INS
(INS S)
(IF (TAS-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (B) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (B)
(TAS-EFFECT (OPERAND (B) (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
TAS-INS
(DEFN TST-SUBGROUP
(INS S)
(IF (EQUAL (OP-LEN INS) (Q))
(IF (EQUAL (HEAD INS 6) 60)
(HALT 'ILLEGAL-UNSPECIFIED S)
(TAS-INS INS S))
(TST-INS (OP-LEN INS) INS S)))
[ 0.0 0.0 0.0 ]
TST-SUBGROUP
(DEFN DIVSL_L
(SOPD DOPD DQ DR S)
(IF (B0P (DIVS-V (L) SOPD (L) DOPD (L)))
(LET ((Q (IQUOT (L) SOPD (L) DOPD (L)))
(R (IREM (L) SOPD (L) DOPD (L))))
(UPDATE-CCR (DIVS-CVZNX (L)
SOPD
(L)
DOPD
(L)
(MC-CCR S))
(WRITE-DN (L)
Q DQ
(WRITE-DN (L) R DR S))))
(HALT 'DIVS-OVERFLOW
(UPDATE-CCR (SET-V (B1) (MC-CCR S))
S))))
Note that (LISTP (DIVSL_L SOPD DOPD DQ DR S)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVSL_L
(DEFN DIVS_L
(SOPD DOPD_LOW DQ DR S)
(LET ((DOPD (APP (L)
DOPD_LOW
(READ-DN (L) DR S))))
(IF (B0P (DIVS-V (L) SOPD (L) DOPD (Q)))
(LET ((Q (IQUOT (L) SOPD (L) DOPD (Q)))
(R (IREM (L) SOPD (L) DOPD (Q))))
(UPDATE-CCR (DIVS-CVZNX (L)
SOPD
(L)
DOPD
(Q)
(MC-CCR S))
(WRITE-DN (L)
Q DQ
(WRITE-DN (L) R DR S))))
(HALT 'DIVS-OVERFLOW
(UPDATE-CCR (SET-V (B1) (MC-CCR S))
S)))))
From the definition we can conclude that:
(LISTP (DIVS_L SOPD DOPD_LOW DQ DR S))
is a theorem.
[ 0.0 0.0 0.0 ]
DIVS_L
(DEFN DIVUL_L
(SOPD DOPD DQ DR S)
(LET ((Q (QUOT (L) SOPD DOPD))
(R (REM (L) SOPD DOPD)))
(UPDATE-CCR (DIVU-CVZNX (L) SOPD DOPD (MC-CCR S))
(WRITE-DN (L)
Q DQ
(WRITE-DN (L) R DR S)))))
From the definition we can conclude that:
(LISTP (DIVUL_L SOPD DOPD DQ DR S))
is a theorem.
[ 0.0 0.0 0.0 ]
DIVUL_L
(DEFN DIVU_L
(SOPD DOPD_LOW DQ DR S)
(LET ((DOPD (APP (L)
DOPD_LOW
(READ-DN (L) DR S))))
(IF (B0P (DIVU-V (L) SOPD DOPD))
(LET ((Q (QUOT (L) SOPD DOPD))
(R (REM (L) SOPD DOPD)))
(UPDATE-CCR (DIVU-CVZNX (L) SOPD DOPD (MC-CCR S))
(WRITE-DN (L)
Q DQ
(WRITE-DN (L) R DR S))))
(HALT 'DIVU-OVERFLOW
(UPDATE-CCR (SET-V (B1) (MC-CCR S))
S)))))
Observe that (LISTP (DIVU_L SOPD DOPD_LOW DQ DR S)) is a theorem.
[ 0.0 0.0 0.0 ]
DIVU_L
(DEFN DQ (WORD) (BITS WORD 12 14))
Note that (NUMBERP (DQ WORD)) is a theorem.
[ 0.0 0.0 0.0 ]
DQ
(DEFN DR (WORD) (BITS WORD 0 2))
Note that (NUMBERP (DR WORD)) is a theorem.
[ 0.0 0.0 0.0 ]
DR
(DEFN DIV_L-INS
(SOPD WORD S)
(LET ((DOPD_LOW (READ-DN (L) (DQ WORD) S)))
(IF (B0P (BITN WORD 11))
(IF (EQUAL (NAT-TO-UINT SOPD) 0)
(HALT 'TRAP-EXCEPTION S)
(IF (B0P (BITN WORD 10))
(DIVUL_L SOPD DOPD_LOW
(DQ WORD)
(DR WORD)
S)
(DIVU_L SOPD DOPD_LOW
(DQ WORD)
(DR WORD)
S)))
(IF (EQUAL (NAT-TO-INT SOPD (L)) 0)
(HALT 'TRAP-EXCEPTION S)
(IF (B0P (BITN WORD 10))
(DIVSL_L SOPD DOPD_LOW
(DQ WORD)
(DR WORD)
S)
(DIVS_L SOPD DOPD_LOW
(DQ WORD)
(DR WORD)
S))))))
From the definition we can conclude that (LISTP (DIV_L-INS SOPD WORD S))
is a theorem.
[ 0.0 0.0 0.0 ]
DIV_L-INS
(DEFN MULU_L_DL
(SOPD DOPD DL S)
(UPDATE-CCR (MULU-CVZNX (L)
SOPD DOPD
(L)
(MC-CCR S))
(WRITE-DN (L)
(MULU (L) SOPD DOPD (L))
DL S)))
From the definition we can conclude that:
(LISTP (MULU_L_DL SOPD DOPD DL S))
is a theorem.
[ 0.0 0.0 0.0 ]
MULU_L_DL
(DEFN MULU_L_DLDH
(SOPD DOPD DL DH S)
(IF (EQUAL DL DH)
(HALT 'MC-UNDEFINED S)
(UPDATE-CCR (MULU-CVZNX (Q)
SOPD DOPD
(L)
(MC-CCR S))
(WRITE-DN (L)
(TAIL (MULU (Q) SOPD DOPD (L)) (L))
DH
(WRITE-DN (L)
(HEAD (MULU (Q) SOPD DOPD (L)) (L))
DL S)))))
Observe that (LISTP (MULU_L_DLDH SOPD DOPD DL DH S)) is a theorem.
[ 0.0 0.0 0.0 ]
MULU_L_DLDH
(DEFN MULS_L_DL
(SOPD DOPD DL S)
(UPDATE-CCR (MULS-CVZNX (L)
SOPD DOPD
(L)
(MC-CCR S))
(WRITE-DN (L)
(MULS (L) SOPD DOPD (L))
DL S)))
From the definition we can conclude that:
(LISTP (MULS_L_DL SOPD DOPD DL S))
is a theorem.
[ 0.0 0.0 0.0 ]
MULS_L_DL
(DEFN MULS_L_DLDH
(SOPD DOPD DL DH S)
(IF (EQUAL DL DH)
(HALT 'MC-UNDEFINED S)
(UPDATE-CCR (MULS-CVZNX (Q)
SOPD DOPD
(L)
(MC-CCR S))
(WRITE-DN (L)
(TAIL (MULS (Q) SOPD DOPD (L)) (L))
DH
(WRITE-DN (L)
(HEAD (MULS (Q) SOPD DOPD (L)) (L))
DL S)))))
Observe that (LISTP (MULS_L_DLDH SOPD DOPD DL DH S)) is a theorem.
[ 0.0 0.0 0.0 ]
MULS_L_DLDH
(DEFN DL (WORD) (BITS WORD 12 14))
Note that (NUMBERP (DL WORD)) is a theorem.
[ 0.0 0.0 0.0 ]
DL
(DEFN DH (WORD) (BITS WORD 0 2))
Note that (NUMBERP (DH WORD)) is a theorem.
[ 0.0 0.0 0.0 ]
DH
(DEFN MUL_L-INS
(SOPD WORD S)
(LET ((DOPD (READ-DN (L) (DL WORD) S)))
(IF (B0P (BITN WORD 11))
(IF (B0P (BITN WORD 10))
(MULU_L_DL SOPD DOPD (DL WORD) S)
(MULU_L_DLDH SOPD DOPD
(DL WORD)
(DH WORD)
S))
(IF (B0P (BITN WORD 10))
(MULS_L_DL SOPD DOPD (DL WORD) S)
(MULS_L_DLDH SOPD DOPD
(DL WORD)
(DH WORD)
S)))))
Note that (LISTP (MUL_L-INS SOPD WORD S)) is a theorem.
[ 0.0 0.0 0.0 ]
MUL_L-INS
(DEFN MUL-DIV_L-INS
(WORD INS S)
(IF (AND (B0P (BITN WORD 15))
(EQUAL (BITS WORD 3 9) 0))
(IF (MUL&DIV-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (L) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(LET ((SOPD (OPERAND (L)
(CDR S&ADDR)
(CAR S&ADDR))))
(IF (B0P (BITN INS 6))
(MUL_L-INS SOPD WORD (CAR S&ADDR))
(DIV_L-INS SOPD WORD (CAR S&ADDR))))))
(HALT (MODE-SIGNAL) S))
(HALT (RESERVED-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MUL-DIV_L-INS
(DEFN MOVEM-EA-RN-ADDR-MODEP
(INS)
(CONTROL-ADDR-MODEP (S_MODE INS)
(S_RN INS)))
Observe that:
(OR (FALSEP (MOVEM-EA-RN-ADDR-MODEP INS))
(TRUEP (MOVEM-EA-RN-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEM-EA-RN-ADDR-MODEP
(DEFN READMP
(MASK OPLEN ADDR MEM)
(READ-MEMP ADDR MEM
(TIMES (OP-SZ OPLEN)
(MOVEM-LEN MASK))))
Note that:
(OR (FALSEP (READMP MASK OPLEN ADDR MEM))
(TRUEP (READMP MASK OPLEN ADDR MEM)))
is a theorem.
[ 0.0 0.0 0.0 ]
READMP
(DEFN MOVEM-EA-RN-INS
(MASK OPLEN INS S)
(IF (POSTINC-MODEP (S_MODE INS))
(LET ((ADDR (READ-AN (L) (S_RN INS) S)))
(IF (READMP MASK OPLEN ADDR (MC-MEM S))
(WRITE-AN (L)
(ADD (L)
ADDR
(TIMES (OP-SZ OPLEN)
(MOVEM-LEN MASK)))
(S_RN INS)
(UPDATE-RFILE (WRITEM-RN OPLEN
(READM-MEM (OP-SZ OPLEN)
ADDR
(MC-MEM S)
(MOVEM-LEN MASK))
(MOVEM-RNLST MASK 0)
(MC-RFILE S))
S))
(HALT (READ-SIGNAL) S)))
(IF (MOVEM-EA-RN-ADDR-MODEP INS)
(LET ((S&ADDR (EFFEC-ADDR OPLEN
(S_MODE INS)
(S_RN INS)
S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(IF (READMP MASK OPLEN
(CDDR S&ADDR)
(MC-MEM S))
(UPDATE-RFILE (WRITEM-RN OPLEN
(READM-MEM (OP-SZ OPLEN)
(CDDR S&ADDR)
(MC-MEM S)
(MOVEM-LEN MASK))
(MOVEM-RNLST MASK 0)
(MC-RFILE S))
(CAR S&ADDR))
(HALT (READ-SIGNAL) S))))
(HALT (MODE-SIGNAL) S))))
[ 0.0 0.0 0.0 ]
MOVEM-EA-RN-INS
(DEFN MOVEM-EA-RN-SUBGROUP
(INS S)
(IF (PC-WORD-READP (MC-PC S) (MC-MEM S))
(LET ((WORD (PC-WORD-READ (MC-PC S) (MC-MEM S))))
(IF (B0P (BITN INS 7))
(MUL-DIV_L-INS WORD INS
(UPDATE-PC (ADD (L) (MC-PC S) (WSZ))
S))
(MOVEM-EA-RN-INS WORD
(IF (B0P (BITN INS 6)) (W) (L))
INS
(UPDATE-PC (ADD (L) (MC-PC S) (WSZ))
S))))
(HALT (PC-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
MOVEM-EA-RN-SUBGROUP
(DEFN LINK-MAPPING
(AN DISP S)
(LET ((SP (SUB (L) (LSZ) (READ-SP S))))
(IF (WRITE-MEMP SP (MC-MEM S) (LSZ))
(UPDATE-MEM (WRITE-MEM (READ-AN (L) AN S)
SP
(MC-MEM S)
(LSZ))
(WRITE-SP (ADD (L) SP DISP)
(WRITE-AN (L) SP AN S)))
(HALT (WRITE-SIGNAL) S))))
From the definition we can conclude that (LISTP (LINK-MAPPING AN DISP S))
is a theorem.
[ 0.0 0.0 0.0 ]
LINK-MAPPING
(DEFN LINK_L-INS
(AN S)
(IF (PC-LONG-READP (MC-PC S) (MC-MEM S))
(LINK-MAPPING AN
(PC-LONG-READ (MC-PC S) (MC-MEM S))
(UPDATE-PC (ADD (L) (MC-PC S) (LSZ))
S))
(HALT (PC-SIGNAL) S)))
Observe that (LISTP (LINK_L-INS AN S)) is a theorem.
[ 0.0 0.0 0.0 ]
LINK_L-INS
(DEFN LINK_W-INS
(AN S)
(IF (PC-WORD-READP (MC-PC S) (MC-MEM S))
(LINK-MAPPING AN
(EXT (W)
(PC-WORD-READ (MC-PC S) (MC-MEM S))
(L))
(UPDATE-PC (ADD (L) (MC-PC S) (WSZ))
S))
(HALT (PC-SIGNAL) S)))
Observe that (LISTP (LINK_W-INS AN S)) is a theorem.
[ 0.0 0.0 0.0 ]
LINK_W-INS
(DEFN UNLK-INS
(AN S)
(LET ((SP (READ-AN (L) AN S)))
(IF (LONG-READP SP (MC-MEM S))
(WRITE-AN (L)
(LONG-READ SP (MC-MEM S))
AN
(WRITE-SP (ADD (L) SP (LSZ)) S))
(HALT (READ-SIGNAL) S))))
Observe that (LISTP (UNLK-INS AN S)) is a theorem.
[ 0.0 0.0 0.0 ]
UNLK-INS
(DEFN UNLK-SUBGROUP
(INS S)
(IF (B0P (BITN INS 4))
(HALT 'TRAP-UNSPECIFIED S)
(IF (B0P (BITN INS 3))
(LINK_W-INS (S_RN INS) S)
(UNLK-INS (S_RN INS) S))))
Observe that (LISTP (UNLK-SUBGROUP INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
UNLK-SUBGROUP
(DEFN NOP-INS (S) S)
Note that (EQUAL (NOP-INS S) S) is a theorem.
[ 0.0 0.0 0.0 ]
NOP-INS
(DEFN RTD-MAPPING
(SP DISP S)
(IF (LONG-READP SP (MC-MEM S))
(LET ((NEW-SP (ADD (L)
(ADD (L) SP (LSZ))
(EXT (W) DISP (L)))))
(UPDATE-PC (LONG-READ SP (MC-MEM S))
(WRITE-SP NEW-SP S)))
(HALT (READ-SIGNAL) S)))
From the definition we can conclude that (LISTP (RTD-MAPPING SP DISP S))
is a theorem.
[ 0.0 0.0 0.0 ]
RTD-MAPPING
(DEFN RTD-INS
(S)
(IF (PC-WORD-READP (MC-PC S) (MC-MEM S))
(RTD-MAPPING (READ-SP S)
(PC-WORD-READ (MC-PC S) (MC-MEM S))
S)
(HALT (PC-SIGNAL) S)))
Note that (LISTP (RTD-INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
RTD-INS
(DEFN RTS-INS
(S)
(RTD-MAPPING (READ-SP S) 0 S))
Note that (LISTP (RTS-INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
RTS-INS
(DEFN RTR-INS
(S)
(LET ((SP (READ-SP S)))
(IF (WORD-READP SP (MC-MEM S))
(RTD-MAPPING (ADD (L) SP (WSZ))
0
(UPDATE-CCR (WORD-READ SP (MC-MEM S))
S))
(HALT (READ-SIGNAL) S))))
Note that (LISTP (RTR-INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
RTR-INS
(DEFN BVS (V) (FIX-BIT V))
Observe that (NUMBERP (BVS V)) is a theorem.
[ 0.0 0.0 0.0 ]
BVS
(DEFN TRAPV-INS
(S)
(IF (B1P (BVS (CCR-V (MC-CCR S))))
(HALT 'TRAPV-EXCEPTION S)
S))
Note that (OR (LISTP (TRAPV-INS S)) (EQUAL (TRAPV-INS S) S)) is a theorem.
[ 0.0 0.0 0.0 ]
TRAPV-INS
(DEFN NOP-SUBGROUP
(INS S)
(IF (B0P (BITN INS 2))
(IF (B0P (BITN INS 1))
(IF (B0P (BITN INS 0))
(HALT 'RESET-PRIVILEGED S)
(NOP-INS S))
(IF (B0P (BITN INS 0))
(HALT 'STOP-PRIVILEGED S)
(HALT 'RTE-PRIVILEGED S)))
(IF (B0P (BITN INS 1))
(IF (B0P (BITN INS 0))
(RTD-INS S)
(RTS-INS S))
(IF (B0P (BITN INS 0))
(TRAPV-INS S)
(RTR-INS S)))))
Note that:
(OR (LISTP (NOP-SUBGROUP INS S))
(EQUAL (NOP-SUBGROUP INS S) S))
is a theorem.
[ 0.0 0.0 0.0 ]
NOP-SUBGROUP
(DEFN JMP-ADDR-MODEP
(INS)
(CONTROL-ADDR-MODEP (S_MODE INS)
(S_RN INS)))
Observe that:
(OR (FALSEP (JMP-ADDR-MODEP INS))
(TRUEP (JMP-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
JMP-ADDR-MODEP
(DEFN JMP-MAPPING
(ADDR S)
(IF (MC-HALTP S)
S
(UPDATE-PC ADDR S)))
Observe that:
(OR (LISTP (JMP-MAPPING ADDR S))
(EQUAL (JMP-MAPPING ADDR S) S))
is a theorem.
[ 0.0 0.0 0.0 ]
JMP-MAPPING
(DEFN JMP-INS
(INS S)
(IF (JMP-ADDR-MODEP INS)
(LET ((S&ADDR (EFFEC-ADDR (L)
(S_MODE INS)
(S_RN INS)
S)))
(JMP-MAPPING (CDDR S&ADDR)
(CAR S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
JMP-INS
(DEFN JSR-ADDR-MODEP
(INS)
(CONTROL-ADDR-MODEP (S_MODE INS)
(S_RN INS)))
Observe that:
(OR (FALSEP (JSR-ADDR-MODEP INS))
(TRUEP (JSR-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
JSR-ADDR-MODEP
(DEFN JSR-INS
(INS S)
(IF (JSR-ADDR-MODEP INS)
(LET ((S&ADDR (EFFEC-ADDR (L)
(S_MODE INS)
(S_RN INS)
S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(JMP-MAPPING (CDDR S&ADDR)
(PUSH-SP (LSZ)
(MC-PC (CAR S&ADDR))
(CAR S&ADDR)))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
JSR-INS
(DEFN NOT-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that (OR (FALSEP (NOT-ADDR-MODEP INS)) (TRUEP (NOT-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
NOT-ADDR-MODEP
(DEFN NOT-Z
(OPLEN OPD)
(IF (EQUAL (LOGNOT OPLEN OPD) 0)
(B1)
(B0)))
From the definition we can conclude that (NUMBERP (NOT-Z OPLEN OPD)) is a
theorem.
[ 0.0 0.0 0.0 ]
NOT-Z
(DEFN NOT-N
(OPLEN OPD)
(MBIT (LOGNOT OPLEN OPD) OPLEN))
Observe that (NUMBERP (NOT-N OPLEN OPD)) is a theorem.
[ 0.0 0.0 0.0 ]
NOT-N
(DEFN NOT-CVZNX
(OPLEN OPD CCR)
(CVZNX (B0)
(B0)
(NOT-Z OPLEN OPD)
(NOT-N OPLEN OPD)
(CCR-X CCR)))
From the definition we can conclude that:
(NUMBERP (NOT-CVZNX OPLEN OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
NOT-CVZNX
(DEFN NOT-EFFECT
(OPLEN OPD CCR)
(CONS (LOGNOT OPLEN OPD)
(NOT-CVZNX OPLEN OPD CCR)))
From the definition we can conclude that:
(LISTP (NOT-EFFECT OPLEN OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
NOT-EFFECT
(DEFN NOT-INS
(OPLEN INS S)
(IF (NOT-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING OPLEN
(NOT-EFFECT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
NOT-INS
(DEFN NOT-SUBGROUP
(INS S)
(IF (EQUAL (OP-LEN INS) (Q))
(HALT 'MOVE-TO-SR-PRIVILEGED S)
(NOT-INS (OP-LEN INS) INS S)))
[ 0.0 0.0 0.0 ]
NOT-SUBGROUP
(DEFN MISC-GROUP
(INS S)
(IF (B0P (BITN INS 8))
(IF (B0P (BITN INS 11))
(IF (B0P (BITN INS 10))
(IF (B0P (BITN INS 9))
(NEGX-SUBGROUP INS S)
(CLR-SUBGROUP INS S))
(IF (B0P (BITN INS 9))
(NEG-SUBGROUP INS S)
(NOT-SUBGROUP INS S)))
(IF (B0P (BITN INS 10))
(IF (B0P (BITN INS 9))
(IF (B0P (BITN INS 7))
(IF (B0P (BITN INS 6))
(IF (AND (B0P (BITN INS 5))
(B0P (BITN INS 4))
(B1P (BITN INS 3)))
(LINK_L-INS (S_RN INS) S)
(HALT 'NBCD-UNSPECIFIED S))
(PEA-SUBGROUP INS S))
(EXT-SUBGROUP INS S))
(TST-SUBGROUP INS S))
(IF (B0P (BITN INS 9))
(MOVEM-EA-RN-SUBGROUP INS S)
(IF (B0P (BITN INS 7))
(IF (B0P (BITN INS 6))
(HALT (RESERVED-SIGNAL) S)
(IF (B0P (BITN INS 5))
(UNLK-SUBGROUP INS S)
(IF (B0P (BITN INS 4))
(HALT 'MOVE-USP-UNSPECIFIED S)
(IF (B0P (BITN INS 3))
(NOP-SUBGROUP INS S)
(HALT 'MOVEC-UNSPECIFIED S)))))
(IF (B0P (BITN INS 6))
(JSR-INS INS S)
(JMP-INS INS S))))))
(IF (AND (B1P (BITN INS 6))
(B1P (BITN INS 7)))
(LEA-SUBGROUP INS S)
(HALT 'CHK-UNSPECIFIED S))))
[ 0.0 0.0 0.0 ]
MISC-GROUP
(DEFN BCS (C) (FIX-BIT C))
Observe that (NUMBERP (BCS C)) is a theorem.
[ 0.0 0.0 0.0 ]
BCS
(DEFN BEQ (Z) (FIX-BIT Z))
Observe that (NUMBERP (BEQ Z)) is a theorem.
[ 0.0 0.0 0.0 ]
BEQ
(DEFN BMI (N) (FIX-BIT N))
Observe that (NUMBERP (BMI N)) is a theorem.
[ 0.0 0.0 0.0 ]
BMI
(DEFN BLE
(V Z N)
(B-OR Z
(B-OR (B-AND N (B-NOT V))
(B-AND (B-NOT N) V))))
From the definition we can conclude that (NUMBERP (BLE V Z N)) is a
theorem.
[ 0.0 0.0 0.0 ]
BLE
(DEFN BGT
(V Z N)
(B-AND (B-OR (B-AND N V)
(B-AND (B-NOT N) (B-NOT V)))
(B-NOT Z)))
From the definition we can conclude that (NUMBERP (BGT V Z N)) is a
theorem.
[ 0.0 0.0 0.0 ]
BGT
(DEFN BLT
(V N)
(B-OR (B-AND N (B-NOT V))
(B-AND (B-NOT N) V)))
Note that (NUMBERP (BLT V N)) is a theorem.
[ 0.0 0.0 0.0 ]
BLT
(DEFN BGE
(V N)
(B-OR (B-AND N V)
(B-AND (B-NOT N) (B-NOT V))))
Note that (NUMBERP (BGE V N)) is a theorem.
[ 0.0 0.0 0.0 ]
BGE
(DEFN BLS (C Z) (B-OR C Z))
From the definition we can conclude that (NUMBERP (BLS C Z)) is a theorem.
[ 0.0 0.0 0.0 ]
BLS
(DEFN BHI
(C Z)
(B-AND (B-NOT C) (B-NOT Z)))
Note that (NUMBERP (BHI C Z)) is a theorem.
[ 0.0 0.0 0.0 ]
BHI
(DEFN BRANCH-CC
(COND CCR)
(IF (LESSP COND 8)
(IF (LESSP COND 4)
(IF (LESSP COND 2)
(IF (EQUAL COND 0) (B1) (B0))
(IF (EQUAL COND 2)
(BHI (CCR-C CCR) (CCR-Z CCR))
(BLS (CCR-C CCR) (CCR-Z CCR))))
(IF (LESSP COND 6)
(IF (EQUAL COND 4)
(B-NOT (BCS (CCR-C CCR)))
(BCS (CCR-C CCR)))
(IF (EQUAL COND 6)
(B-NOT (BEQ (CCR-Z CCR)))
(BEQ (CCR-Z CCR)))))
(IF (LESSP COND 12)
(IF (LESSP COND 10)
(IF (EQUAL COND 8)
(B-NOT (BVS (CCR-V CCR)))
(BVS (CCR-V CCR)))
(IF (EQUAL COND 10)
(B-NOT (BMI (CCR-N CCR)))
(BMI (CCR-N CCR))))
(IF (LESSP COND 14)
(IF (EQUAL COND 12)
(BGE (CCR-V CCR) (CCR-N CCR))
(BLT (CCR-V CCR) (CCR-N CCR)))
(IF (EQUAL COND 14)
(BGT (CCR-V CCR)
(CCR-Z CCR)
(CCR-N CCR))
(BLE (CCR-V CCR)
(CCR-Z CCR)
(CCR-N CCR)))))))
From the definition we can conclude that (NUMBERP (BRANCH-CC COND CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
BRANCH-CC
(DEFN BSR-INS
(PC DISP S)
(PUSH-SP (LSZ)
PC
(UPDATE-PC (ADD (L) (MC-PC S) DISP)
S)))
Note that (LISTP (BSR-INS PC DISP S)) is a theorem.
[ 0.0 0.0 0.0 ]
BSR-INS
(DEFN BCC-RA-SR
(PC COND DISP S)
(IF (EQUAL COND 0)
(UPDATE-PC (ADD (L) (MC-PC S) DISP) S)
(IF (EQUAL COND 1)
(BSR-INS PC DISP S)
(IF (B0P (BRANCH-CC COND (MC-CCR S)))
(UPDATE-PC PC S)
(UPDATE-PC (ADD (L) (MC-PC S) DISP)
S)))))
From the definition we can conclude that:
(LISTP (BCC-RA-SR PC COND DISP S))
is a theorem.
[ 0.0 0.0 0.0 ]
BCC-RA-SR
(DEFN BCC-GROUP
(DISP INS S)
(IF (EQUAL DISP 0)
(IF (PC-WORD-READP (MC-PC S) (MC-MEM S))
(BCC-RA-SR (ADD (L) (MC-PC S) (WSZ))
(COND-FIELD INS)
(EXT (W)
(PC-WORD-READ (MC-PC S) (MC-MEM S))
(L))
S)
(HALT (PC-SIGNAL) S))
(IF (EQUAL DISP 255)
(IF (PC-LONG-READP (MC-PC S) (MC-MEM S))
(BCC-RA-SR (ADD (L) (MC-PC S) (LSZ))
(COND-FIELD INS)
(PC-LONG-READ (MC-PC S) (MC-MEM S))
S)
(HALT (PC-SIGNAL) S))
(BCC-RA-SR (MC-PC S)
(COND-FIELD INS)
(EXT (B) DISP (L))
S))))
From the definition we can conclude that (LISTP (BCC-GROUP DISP INS S))
is a theorem.
[ 0.0 0.0 0.0 ]
BCC-GROUP
(DEFN SCC-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that (OR (FALSEP (SCC-ADDR-MODEP INS)) (TRUEP (SCC-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
SCC-ADDR-MODEP
(DEFN SCC-EFFECT
(COND CCR)
(CONS (IF (B0P (BRANCH-CC COND CCR)) 0 255)
CCR))
Note that (LISTP (SCC-EFFECT COND CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
SCC-EFFECT
(DEFN SCC-INS
(INS S)
(IF (SCC-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (B) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (B)
(SCC-EFFECT (COND-FIELD INS)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
SCC-INS
(DEFN DBCC-LOOP
(RN S)
(LET ((CNT (SUB (W) 1 (READ-DN (W) RN S))))
(IF (EQUAL (NAT-TO-INT CNT (W)) -1)
(UPDATE-PC (ADD (L) (MC-PC S) (WSZ))
(WRITE-DN (W) CNT RN S))
(UPDATE-PC (ADD (L)
(MC-PC S)
(EXT (W)
(PC-WORD-READ (MC-PC S) (MC-MEM S))
(L)))
(WRITE-DN (W) CNT RN S)))))
From the definition we can conclude that (LISTP (DBCC-LOOP RN S)) is a
theorem.
[ 0.0 0.0 0.0 ]
DBCC-LOOP
(DEFN DBCC-INS
(INS S)
(IF (PC-WORD-READP (MC-PC S) (MC-MEM S))
(IF (B0P (BRANCH-CC (COND-FIELD INS)
(MC-CCR S)))
(DBCC-LOOP (S_RN INS) S)
(UPDATE-PC (ADD (L) (MC-PC S) (WSZ))
S))
(HALT (PC-SIGNAL) S)))
From the definition we can conclude that (LISTP (DBCC-INS INS S)) is a
theorem.
[ 0.0 0.0 0.0 ]
DBCC-INS
(DEFN ADDQ-ADDR-MODEP
(OPLEN INS)
(AND (ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(NOT (BYTE-AN-DIRECT-MODEP OPLEN
(S_MODE INS)))))
From the definition we can conclude that:
(OR (FALSEP (ADDQ-ADDR-MODEP OPLEN INS))
(TRUEP (ADDQ-ADDR-MODEP OPLEN INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
ADDQ-ADDR-MODEP
(DEFN ADDQ-INS
(OPLEN INS S)
(IF (ADDQ-ADDR-MODEP OPLEN INS)
(IF (AN-DIRECT-MODEP (S_MODE INS))
(WRITE-AN (L)
(ADD (L)
(READ-AN (L) (S_RN INS) S)
(I-DATA (D_RN INS)))
(S_RN INS)
S)
(ADD-MAPPING (I-DATA (D_RN INS))
OPLEN INS S))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
ADDQ-INS
(DEFN SUBQ-ADDR-MODEP
(OPLEN INS)
(AND (ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(NOT (BYTE-AN-DIRECT-MODEP OPLEN
(S_MODE INS)))))
From the definition we can conclude that:
(OR (FALSEP (SUBQ-ADDR-MODEP OPLEN INS))
(TRUEP (SUBQ-ADDR-MODEP OPLEN INS)))
is a theorem.
[ 0.2 0.0 0.0 ]
SUBQ-ADDR-MODEP
(DEFN SUBQ-INS
(OPLEN INS S)
(IF (SUBQ-ADDR-MODEP OPLEN INS)
(IF (AN-DIRECT-MODEP (S_MODE INS))
(WRITE-AN (L)
(SUB (L)
(I-DATA (D_RN INS))
(READ-AN (L) (S_RN INS) S))
(S_RN INS)
S)
(SUB-MAPPING (I-DATA (D_RN INS))
OPLEN INS S))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
SUBQ-INS
(DEFN SCC-GROUP
(INS S)
(IF (EQUAL (OP-LEN INS) (Q))
(IF (EQUAL (S_MODE INS) 1)
(DBCC-INS INS S)
(IF (AND (EQUAL (S_MODE INS) 7)
(LESSP 1 (S_RN INS)))
(HALT 'TRAPCC-UNSPECIFIED S)
(SCC-INS INS S)))
(IF (B0P (BITN INS 8))
(ADDQ-INS (OP-LEN INS) INS S)
(SUBQ-INS (OP-LEN INS) INS S))))
[ 0.0 0.0 0.0 ]
SCC-GROUP
(DEFN MOVEQ-INS
(INS S)
(IF (B0P (BITN INS 8))
(D-MAPPING (L)
(MOVE-EFFECT (L)
(EXT (B) (HEAD INS (B)) (L))
(MC-CCR S))
(D_RN INS)
S)
(HALT (RESERVED-SIGNAL) S)))
Observe that (LISTP (MOVEQ-INS INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
MOVEQ-INS
(DEFN CMP-CVZNX
(OPLEN SOPD DOPD CCR)
(CVZNX (SUB-C OPLEN SOPD DOPD)
(SUB-V OPLEN SOPD DOPD)
(SUB-Z OPLEN SOPD DOPD)
(SUB-N OPLEN SOPD DOPD)
(CCR-X CCR)))
Observe that (NUMBERP (CMP-CVZNX OPLEN SOPD DOPD CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
CMP-CVZNX
(DEFN CMP-ADDR-MODEP
(OPLEN INS)
(AND (ADDR-MODEP (S_MODE INS) (S_RN INS))
(NOT (BYTE-AN-DIRECT-MODEP OPLEN
(S_MODE INS)))))
From the definition we can conclude that:
(OR (FALSEP (CMP-ADDR-MODEP OPLEN INS))
(TRUEP (CMP-ADDR-MODEP OPLEN INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
CMP-ADDR-MODEP
(DEFN CMP-INS
(OPLEN INS S)
(IF (CMP-ADDR-MODEP OPLEN INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(UPDATE-CCR (CMP-CVZNX OPLEN
(OPERAND OPLEN
(CDR S&ADDR)
(CAR S&ADDR))
(READ-DN OPLEN (D_RN INS) S)
(MC-CCR S))
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
CMP-INS
(DEFN CMPA-ADDR-MODEP
(INS)
(ADDR-MODEP (S_MODE INS) (S_RN INS)))
Observe that:
(OR (FALSEP (CMPA-ADDR-MODEP INS))
(TRUEP (CMPA-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
CMPA-ADDR-MODEP
(DEFN CMPA-INS
(OPLEN INS S)
(IF (CMPA-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(UPDATE-CCR (CMP-CVZNX (L)
(EXT OPLEN
(OPERAND OPLEN (CDR S&ADDR) S)
(L))
(READ-AN (L) (D_RN INS) (CAR S&ADDR))
(MC-CCR S))
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
CMPA-INS
(DEFN EOR-Z
(OPLEN SOPD DOPD)
(IF (EQUAL (LOGEOR SOPD DOPD) 0)
(B1)
(B0)))
WARNING: OPLEN is in the arglist but not in the body of the definition of
EOR-Z.
Observe that (NUMBERP (EOR-Z OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
EOR-Z
(DEFN EOR-N
(OPLEN SOPD DOPD)
(B-EOR (MBIT SOPD OPLEN)
(MBIT DOPD OPLEN)))
Note that (NUMBERP (EOR-N OPLEN SOPD DOPD)) is a theorem.
[ 0.0 0.0 0.0 ]
EOR-N
(DEFN EOR-CVZNX
(OPLEN SOPD DOPD CCR)
(CVZNX (B0)
(B0)
(EOR-Z OPLEN SOPD DOPD)
(EOR-N OPLEN SOPD DOPD)
(CCR-X CCR)))
Observe that (NUMBERP (EOR-CVZNX OPLEN SOPD DOPD CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
EOR-CVZNX
(DEFN EOR-EFFECT
(OPLEN SOPD DOPD CCR)
(CONS (LOGEOR SOPD DOPD)
(EOR-CVZNX OPLEN SOPD DOPD CCR)))
Note that (LISTP (EOR-EFFECT OPLEN SOPD DOPD CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
EOR-EFFECT
(DEFN EOR&EORI-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (EOR&EORI-ADDR-MODEP INS))
(TRUEP (EOR&EORI-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
EOR&EORI-ADDR-MODEP
(DEFN EOR-MAPPING
(SOPD OPLEN INS S)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING OPLEN
(EOR-EFFECT OPLEN SOPD
(OPERAND OPLEN (CDR S&ADDR) S)
(MC-CCR S))
S&ADDR))))
[ 0.0 0.0 0.0 ]
EOR-MAPPING
(DEFN EOR-INS
(OPLEN INS S)
(IF (EOR&EORI-ADDR-MODEP INS)
(EOR-MAPPING (READ-DN OPLEN (D_RN INS) S)
OPLEN INS S)
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
EOR-INS
(DEFN CMPM-MAPPING
(ADDR OPLEN INS S)
(LET ((S&ADDR (ADDR-POSTINC OPLEN (D_RN INS) S)))
(IF (READ-MEMP (CDDR S&ADDR)
(MC-MEM S)
(OP-SZ OPLEN))
(UPDATE-CCR (CMP-CVZNX OPLEN
(OPERAND OPLEN ADDR S)
(OPERAND OPLEN (CDR S&ADDR) S)
(MC-CCR S))
(CAR S&ADDR))
(HALT (READ-SIGNAL) S))))
Observe that (LISTP (CMPM-MAPPING ADDR OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
CMPM-MAPPING
(DEFN CMPM-INS
(OPLEN INS S)
(LET ((S&ADDR (ADDR-POSTINC OPLEN (S_RN INS) S)))
(IF (READ-MEMP (CDDR S&ADDR)
(MC-MEM S)
(OP-SZ OPLEN))
(CMPM-MAPPING (CDR S&ADDR)
OPLEN INS
(CAR S&ADDR))
(HALT (READ-SIGNAL) S))))
Observe that (LISTP (CMPM-INS OPLEN INS S)) is a theorem.
[ 0.0 0.0 0.0 ]
CMPM-INS
(DEFN CMP-GROUP
(OPLEN INS S)
(IF (B0P (BITN INS 8))
(IF (EQUAL OPLEN (Q))
(CMPA-INS (W) INS S)
(CMP-INS OPLEN INS S))
(IF (EQUAL OPLEN (Q))
(CMPA-INS (L) INS S)
(IF (EQUAL (S_MODE INS) 1)
(CMPM-INS OPLEN INS S)
(EOR-INS OPLEN INS S)))))
[ 0.0 0.0 0.0 ]
CMP-GROUP
(DEFN MOVEP-WRITEP
(ADDR MEM N)
(IF (ZEROP N)
T
(AND (BYTE-WRITEP (ADD (L) ADDR (TIMES 2 (SUB1 N)))
MEM)
(MOVEP-WRITEP ADDR MEM (SUB1 N)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP can
be used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call. Hence, MOVEP-WRITEP is
accepted under the definitional principle. Note that:
(OR (FALSEP (MOVEP-WRITEP ADDR MEM N))
(TRUEP (MOVEP-WRITEP ADDR MEM N)))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEP-WRITEP
(DEFN MOVEP-WRITE
(VALUE ADDR MEM N)
(IF (ZEROP N)
MEM
(MOVEP-WRITE (TAIL VALUE (B))
ADDR
(BYTE-WRITE VALUE
(ADD (L) ADDR (TIMES 2 (SUB1 N)))
MEM)
(SUB1 N))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, MOVEP-WRITE is accepted under
the principle of definition. Observe that:
(OR (LISTP (MOVEP-WRITE VALUE ADDR MEM N))
(EQUAL (MOVEP-WRITE VALUE ADDR MEM N)
MEM))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEP-WRITE
(DEFN MOVEP-TO-MEM
(ADDR OPLEN INS S)
(IF (MOVEP-WRITEP ADDR
(MC-MEM S)
(OP-SZ OPLEN))
(UPDATE-MEM (MOVEP-WRITE (READ-DN OPLEN (D_RN INS) S)
ADDR
(MC-MEM S)
(OP-SZ OPLEN))
S)
(HALT (WRITE-SIGNAL) S)))
From the definition we can conclude that:
(LISTP (MOVEP-TO-MEM ADDR OPLEN INS S))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEP-TO-MEM
(DEFN MOVEP-READP
(ADDR MEM N)
(IF (ZEROP N)
T
(AND (BYTE-READP ADDR MEM)
(MOVEP-READP (ADD (L) ADDR (WSZ))
MEM
(SUB1 N)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, MOVEP-READP is accepted under
the principle of definition. Note that:
(OR (FALSEP (MOVEP-READP ADDR MEM N))
(TRUEP (MOVEP-READP ADDR MEM N)))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEP-READP
(DEFN MOVEP-READ
(ADDR MEM N)
(IF (ZEROP N)
0
(APP (B)
(BYTE-READ (ADD (L) ADDR (TIMES 2 (SUB1 N)))
MEM)
(MOVEP-READ ADDR MEM (SUB1 N)))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, MOVEP-READ is accepted under
the principle of definition. Observe that (NUMBERP (MOVEP-READ ADDR MEM N))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEP-READ
(DEFN MOVEP-TO-REG
(ADDR OPLEN INS S)
(IF (MOVEP-READP ADDR
(MC-MEM S)
(OP-SZ OPLEN))
(WRITE-DN OPLEN
(MOVEP-READ ADDR
(MC-MEM S)
(OP-SZ OPLEN))
(D_RN INS)
S)
(HALT (READ-SIGNAL) S)))
From the definition we can conclude that:
(LISTP (MOVEP-TO-REG ADDR OPLEN INS S))
is a theorem.
[ 0.0 0.0 0.0 ]
MOVEP-TO-REG
(DEFN EVENP (X) (B0P (BCAR X)))
From the definition we can conclude that:
(OR (FALSEP (EVENP X))
(TRUEP (EVENP X)))
is a theorem.
[ 0.0 0.0 0.0 ]
EVENP
(DEFN MOVEP-ADDR
(S&ADDR)
(IF (EVENP (CDDR S&ADDR))
(CDDR S&ADDR)
(ADD (L) (CDDR S&ADDR) (BSZ))))
[ 0.0 0.0 0.0 ]
MOVEP-ADDR
(DEFN MOVEP-INS
(OPMODE INS S)
(LET ((S&ADDR (ADDR-DISP (MC-PC S) (S_RN INS) S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(IF (LESSP OPMODE 6)
(IF (EQUAL OPMODE 4)
(MOVEP-TO-REG (MOVEP-ADDR S&ADDR)
(W)
INS
(CAR S&ADDR))
(MOVEP-TO-REG (MOVEP-ADDR S&ADDR)
(L)
INS
(CAR S&ADDR)))
(IF (EQUAL OPMODE 6)
(MOVEP-TO-MEM (MOVEP-ADDR S&ADDR)
(W)
INS
(CAR S&ADDR))
(MOVEP-TO-MEM (MOVEP-ADDR S&ADDR)
(L)
INS
(CAR S&ADDR)))))))
[ 0.0 0.0 0.0 ]
MOVEP-INS
(DEFN BXXX-OPLEN
(SMODE)
(IF (DN-DIRECT-MODEP SMODE) (L) (B)))
Note that (NUMBERP (BXXX-OPLEN SMODE)) is a theorem.
[ 0.0 0.0 0.0 ]
BXXX-OPLEN
(DEFN BXXX-NUM
(SMODE BNUM)
(IF (DN-DIRECT-MODEP SMODE)
(HEAD BNUM 5)
(HEAD BNUM 3)))
Note that (NUMBERP (BXXX-NUM SMODE BNUM)) is a theorem.
[ 0.0 0.0 0.0 ]
BXXX-NUM
(DEFN BXXX-OPD
(SMODE S&ADDR)
(IF (DN-DIRECT-MODEP SMODE)
(READ-DN (L)
(CDDR S&ADDR)
(CAR S&ADDR))
(OPERAND (B)
(CDR S&ADDR)
(CAR S&ADDR))))
[ 0.0 0.0 0.0 ]
BXXX-OPD
(DEFN BCHG-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (BCHG-ADDR-MODEP INS))
(TRUEP (BCHG-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
BCHG-ADDR-MODEP
(DEFN BCHG-EFFECT
(BNUM OPD CCR)
(CONS (SETN OPD BNUM
(B-NOT (BITN OPD BNUM)))
(SET-Z (B-NOT (BITN OPD BNUM)) CCR)))
Note that (LISTP (BCHG-EFFECT BNUM OPD CCR)) is a theorem.
[ 0.0 0.0 0.0 ]
BCHG-EFFECT
(DEFN BCHG-INS
(BNUM INS S)
(IF (BCHG-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (B) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (BXXX-OPLEN (S_MODE INS))
(BCHG-EFFECT (BXXX-NUM (S_MODE INS) BNUM)
(BXXX-OPD (S_MODE INS) S&ADDR)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
BCHG-INS
(DEFN BCLR-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (BCLR-ADDR-MODEP INS))
(TRUEP (BCLR-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
BCLR-ADDR-MODEP
(DEFN BCLR-EFFECT
(BNUM OPD CCR)
(CONS (SETN OPD BNUM (B0))
(SET-Z (B-NOT (BITN OPD BNUM)) CCR)))
From the definition we can conclude that:
(LISTP (BCLR-EFFECT BNUM OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
BCLR-EFFECT
(DEFN BCLR-INS
(BNUM INS S)
(IF (BCLR-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (B) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (BXXX-OPLEN (S_MODE INS))
(BCLR-EFFECT (BXXX-NUM (S_MODE INS) BNUM)
(BXXX-OPD (S_MODE INS) S&ADDR)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
BCLR-INS
(DEFN BSET-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (BSET-ADDR-MODEP INS))
(TRUEP (BSET-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
BSET-ADDR-MODEP
(DEFN BSET-EFFECT
(BNUM OPD CCR)
(CONS (SETN OPD BNUM (B1))
(SET-Z (B-NOT (BITN OPD BNUM)) CCR)))
From the definition we can conclude that:
(LISTP (BSET-EFFECT BNUM OPD CCR))
is a theorem.
[ 0.0 0.0 0.0 ]
BSET-EFFECT
(DEFN BSET-INS
(BNUM INS S)
(IF (BSET-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (B) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(MAPPING (BXXX-OPLEN (S_MODE INS))
(BSET-EFFECT (BXXX-NUM (S_MODE INS) BNUM)
(BXXX-OPD (S_MODE INS) S&ADDR)
(MC-CCR S))
S&ADDR)))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
BSET-INS
(DEFN BTST-ADDR-MODEP
(INS)
(DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS)))
Observe that:
(OR (FALSEP (BTST-ADDR-MODEP INS))
(TRUEP (BTST-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
BTST-ADDR-MODEP
(DEFN BTST-INS
(BNUM INS S)
(IF (BTST-ADDR-MODEP INS)
(LET ((S&ADDR (MC-INSTATE (B) INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(UPDATE-CCR (SET-Z (B-NOT (BITN (BXXX-OPD (S_MODE INS) S&ADDR)
(BXXX-NUM (S_MODE INS) BNUM)))
(MC-CCR S))
(CAR S&ADDR))))
(HALT (MODE-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
BTST-INS
(DEFN BIT-INS
(BNUM INS S)
(LET ((TYPE (BITS INS 6 7)))
(IF (LESSP TYPE 2)
(IF (EQUAL TYPE 0)
(BTST-INS BNUM INS S)
(BCHG-INS BNUM INS S))
(IF (EQUAL TYPE 2)
(BCLR-INS BNUM INS S)
(BSET-INS BNUM INS S)))))
[ 0.0 0.0 0.0 ]
BIT-INS
(DEFN D-BIT-SUBGROUP
(INS S)
(IF (EQUAL (S_MODE INS) 1)
(MOVEP-INS (OPMODE-FIELD INS) INS S)
(BIT-INS (READ-DN (L) (D_RN INS) S)
INS S)))
[ 0.0 0.0 0.0 ]
D-BIT-SUBGROUP
(DEFN S-BIT-SUBGROUP
(INS S)
(IF (PC-WORD-READP (MC-PC S) (MC-MEM S))
(IF (EQUAL (PC-BYTE-READ (MC-PC S) (MC-MEM S))
0)
(BIT-INS (PC-BYTE-READ (ADD (L) (MC-PC S) (BSZ))
(MC-MEM S))
INS
(UPDATE-PC (ADD (L) (MC-PC S) (WSZ))
S))
(HALT (RESERVED-SIGNAL) S))
(HALT (PC-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
S-BIT-SUBGROUP
(DEFN ORI-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that (OR (FALSEP (ORI-ADDR-MODEP INS)) (TRUEP (ORI-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
ORI-ADDR-MODEP
(DEFN ORI-INS
(OPLEN INS S)
(LET ((S&IDATA (IMMEDIATE OPLEN (MC-PC S) S)))
(IF (MC-HALTP (CAR S&IDATA))
(CAR S&IDATA)
(IF (ORI-ADDR-MODEP INS)
(OR-MAPPING (CDDR S&IDATA)
OPLEN INS
(CAR S&IDATA))
(HALT (MODE-SIGNAL) S)))))
[ 0.0 0.0 0.0 ]
ORI-INS
(DEFN ORI-TO-CCR-INS
(PC S)
(IF (PC-WORD-READP PC (MC-MEM S))
(IF (EQUAL (PC-BYTE-READ PC (MC-MEM S)) 0)
(UPDATE-CCR (LOGOR (PC-BYTE-READ (ADD (L) PC (BSZ))
(MC-MEM S))
(MC-CCR S))
(UPDATE-PC (ADD (L) PC (WSZ)) S))
(HALT (RESERVED-SIGNAL) S))
(HALT (PC-SIGNAL) S)))
Observe that (LISTP (ORI-TO-CCR-INS PC S)) is a theorem.
[ 0.0 0.0 0.0 ]
ORI-TO-CCR-INS
(DEFN ORI-SUBGROUP
(OPLEN INS S)
(IF (EQUAL OPLEN (Q))
(HALT 'CMP2-CHK2-UNSPECIFIED S)
(IF (EQUAL (HEAD INS 6) 60)
(IF (EQUAL OPLEN (B))
(ORI-TO-CCR-INS (MC-PC S) S)
(IF (EQUAL OPLEN (W))
(HALT 'ORI-TO-SR-PRIVILEGED S)
(HALT (RESERVED-SIGNAL) S)))
(ORI-INS OPLEN INS S))))
[ 0.0 0.0 0.0 ]
ORI-SUBGROUP
(DEFN ANDI-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (ANDI-ADDR-MODEP INS))
(TRUEP (ANDI-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
ANDI-ADDR-MODEP
(DEFN ANDI-INS
(OPLEN INS S)
(LET ((S&IDATA (IMMEDIATE OPLEN (MC-PC S) S)))
(IF (MC-HALTP S)
(CAR S&IDATA)
(IF (ANDI-ADDR-MODEP INS)
(AND-MAPPING (CDDR S&IDATA)
OPLEN INS
(CAR S&IDATA))
(HALT (MODE-SIGNAL) S)))))
[ 0.0 0.0 0.0 ]
ANDI-INS
(DEFN ANDI-TO-CCR-INS
(PC S)
(IF (PC-WORD-READP PC (MC-MEM S))
(IF (EQUAL (PC-BYTE-READ PC (MC-MEM S)) 0)
(UPDATE-CCR (LOGAND (PC-BYTE-READ (ADD (L) PC (BSZ))
(MC-MEM S))
(MC-CCR S))
(UPDATE-PC (ADD (L) PC (WSZ)) S))
(HALT (RESERVED-SIGNAL) S))
(HALT (PC-SIGNAL) S)))
Observe that (LISTP (ANDI-TO-CCR-INS PC S)) is a theorem.
[ 0.0 0.0 0.0 ]
ANDI-TO-CCR-INS
(DEFN ANDI-SUBGROUP
(OPLEN INS S)
(IF (EQUAL OPLEN (Q))
(HALT 'CMP2-CHK2-UNSPECIFIED S)
(IF (EQUAL (HEAD INS 6) 60)
(IF (EQUAL OPLEN (B))
(ANDI-TO-CCR-INS (MC-PC S) S)
(IF (EQUAL OPLEN (W))
(HALT 'ANDI-TO-SR-UNSPECIFIED S)
(HALT (RESERVED-SIGNAL) S)))
(ANDI-INS OPLEN INS S))))
[ 0.0 0.0 0.0 ]
ANDI-SUBGROUP
(DEFN SUBI-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (SUBI-ADDR-MODEP INS))
(TRUEP (SUBI-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
SUBI-ADDR-MODEP
(DEFN SUBI-INS
(OPLEN INS S)
(LET ((S&IDATA (IMMEDIATE OPLEN (MC-PC S) S)))
(IF (MC-HALTP (CAR S&IDATA))
(CAR S&IDATA)
(IF (SUBI-ADDR-MODEP INS)
(SUB-MAPPING (CDDR S&IDATA)
OPLEN INS
(CAR S&IDATA))
(HALT (MODE-SIGNAL) S)))))
[ 0.0 0.0 0.0 ]
SUBI-INS
(DEFN SUBI-SUBGROUP
(OPLEN INS S)
(IF (EQUAL OPLEN (Q))
(HALT 'CMP2-CHK2-UNSPECIFIED S)
(SUBI-INS OPLEN INS S)))
[ 0.0 0.0 0.0 ]
SUBI-SUBGROUP
(DEFN ADDI-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(ALTERABLE-ADDR-MODEP (S_MODE INS)
(S_RN INS))))
Note that:
(OR (FALSEP (ADDI-ADDR-MODEP INS))
(TRUEP (ADDI-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
ADDI-ADDR-MODEP
(DEFN ADDI-INS
(OPLEN INS S)
(LET ((S&IDATA (IMMEDIATE OPLEN (MC-PC S) S)))
(IF (MC-HALTP (CAR S&IDATA))
(CAR S&IDATA)
(IF (ADDI-ADDR-MODEP INS)
(ADD-MAPPING (CDDR S&IDATA)
OPLEN INS
(CAR S&IDATA))
(HALT (MODE-SIGNAL) S)))))
[ 0.0 0.0 0.0 ]
ADDI-INS
(DEFN ADDI-SUBGROUP
(OPLEN INS S)
(IF (EQUAL OPLEN (Q))
(HALT 'RTM-CALLM-UNSPECIFIED S)
(ADDI-INS OPLEN INS S)))
[ 0.0 0.0 0.0 ]
ADDI-SUBGROUP
(DEFN EORI-INS
(OPLEN INS S)
(LET ((S&IDATA (IMMEDIATE OPLEN (MC-PC S) S)))
(IF (MC-HALTP (CAR S&IDATA))
(CAR S&IDATA)
(IF (EOR&EORI-ADDR-MODEP INS)
(EOR-MAPPING (CDDR S&IDATA)
OPLEN INS
(CAR S&IDATA))
(HALT (MODE-SIGNAL) S)))))
[ 0.0 0.0 0.0 ]
EORI-INS
(DEFN EORI-TO-CCR-INS
(PC S)
(IF (PC-WORD-READP PC (MC-MEM S))
(IF (EQUAL (PC-BYTE-READ PC (MC-MEM S)) 0)
(UPDATE-CCR (LOGEOR (PC-BYTE-READ (ADD (L) PC (BSZ))
(MC-MEM S))
(MC-CCR S))
(UPDATE-PC (ADD (L) PC (WSZ)) S))
(HALT (RESERVED-SIGNAL) S))
(HALT (PC-SIGNAL) S)))
Observe that (LISTP (EORI-TO-CCR-INS PC S)) is a theorem.
[ 0.0 0.0 0.0 ]
EORI-TO-CCR-INS
(DEFN EORI-SUBGROUP
(OPLEN INS S)
(IF (EQUAL OPLEN (Q))
(HALT 'CAS-CAS2-UNSPECIFIED S)
(IF (EQUAL (HEAD INS 6) 60)
(IF (EQUAL OPLEN (B))
(EORI-TO-CCR-INS (MC-PC S) S)
(IF (EQUAL OPLEN (W))
(HALT 'EORI-TO-SR-UNSPECIFIED S)
(HALT (RESERVED-SIGNAL) S)))
(EORI-INS OPLEN INS S))))
[ 0.0 0.0 0.0 ]
EORI-SUBGROUP
(DEFN CMPI-ADDR-MODEP
(INS)
(AND (DATA-ADDR-MODEP (S_MODE INS)
(S_RN INS))
(NOT (IDATA-MODEP (S_MODE INS)
(S_RN INS)))))
Note that:
(OR (FALSEP (CMPI-ADDR-MODEP INS))
(TRUEP (CMPI-ADDR-MODEP INS)))
is a theorem.
[ 0.0 0.0 0.0 ]
CMPI-ADDR-MODEP
(DEFN CMPI-MAPPING
(IDATA OPLEN INS S)
(LET ((S&ADDR (MC-INSTATE OPLEN INS S)))
(IF (MC-HALTP (CAR S&ADDR))
(CAR S&ADDR)
(UPDATE-CCR (CMP-CVZNX OPLEN IDATA
(OPERAND OPLEN (CDR S&ADDR) S)
(MC-CCR S))
(CAR S&ADDR)))))
[ 0.0 0.0 0.0 ]
CMPI-MAPPING
(DEFN CMPI-INS
(OPLEN INS S)
(LET ((S&IDATA (IMMEDIATE OPLEN (MC-PC S) S)))
(IF (MC-HALTP (CAR S&IDATA))
(CAR S&IDATA)
(IF (CMPI-ADDR-MODEP INS)
(CMPI-MAPPING (CDDR S&IDATA)
OPLEN INS
(CAR S&IDATA))
(HALT (MODE-SIGNAL) S)))))
[ 0.0 0.0 0.0 ]
CMPI-INS
(DEFN CMPI-SUBGROUP
(OPLEN INS S)
(IF (EQUAL OPLEN (Q))
(HALT 'CAS-CAS2-UNSPECIFIED S)
(CMPI-INS OPLEN INS S)))
[ 0.0 0.0 0.0 ]
CMPI-SUBGROUP
(DEFN BIT-GROUP
(INS S)
(IF (B0P (BITN INS 8))
(IF (B0P (BITN INS 11))
(IF (B0P (BITN INS 10))
(IF (B0P (BITN INS 9))
(ORI-SUBGROUP (OP-LEN INS) INS S)
(ANDI-SUBGROUP (OP-LEN INS) INS S))
(IF (B0P (BITN INS 9))
(SUBI-SUBGROUP (OP-LEN INS) INS S)
(ADDI-SUBGROUP (OP-LEN INS) INS S)))
(IF (B0P (BITN INS 10))
(IF (B0P (BITN INS 9))
(S-BIT-SUBGROUP INS S)
(EORI-SUBGROUP (OP-LEN INS) INS S))
(IF (B0P (BITN INS 9))
(CMPI-SUBGROUP (OP-LEN INS) INS S)
(HALT 'MOVES-CAS-CAS2-UNSPECIFIED
S))))
(D-BIT-SUBGROUP INS S)))
[ 0.0 0.0 0.0 ]
BIT-GROUP
(DEFN OPCODE-FIELD
(INS)
(BITS INS 12 15))
Note that (NUMBERP (OPCODE-FIELD INS)) is a theorem.
[ 0.0 0.0 0.0 ]
OPCODE-FIELD
(DEFN EXECUTE-INS
(INS S)
(LET ((OPCODE (OPCODE-FIELD INS)))
(IF (LESSP OPCODE 8)
(IF (LESSP OPCODE 4)
(IF (LESSP OPCODE 2)
(IF (EQUAL OPCODE 0)
(BIT-GROUP INS S)
(MOVE-INS (B) INS S))
(IF (EQUAL OPCODE 2)
(MOVE-GROUP (L) INS S)
(MOVE-GROUP (W) INS S)))
(IF (LESSP OPCODE 6)
(IF (EQUAL OPCODE 4)
(MISC-GROUP INS S)
(SCC-GROUP INS S))
(IF (EQUAL OPCODE 6)
(BCC-GROUP (HEAD INS (B)) INS S)
(MOVEQ-INS INS S))))
(IF (LESSP OPCODE 12)
(IF (LESSP OPCODE 10)
(IF (EQUAL OPCODE 8)
(OR-GROUP (OP-LEN INS) INS S)
(SUB-GROUP (OPMODE-FIELD INS) INS S))
(IF (EQUAL OPCODE 10)
(HALT (RESERVED-SIGNAL) S)
(CMP-GROUP (OP-LEN INS) INS S)))
(IF (LESSP OPCODE 14)
(IF (EQUAL OPCODE 12)
(AND-GROUP (OP-LEN INS) INS S)
(ADD-GROUP (OPMODE-FIELD INS) INS S))
(IF (EQUAL OPCODE 14)
(S&R-GROUP INS S)
(HALT 'COPROCESSOR-UNSPECIFIED
S)))))))
[ 0.0 0.0 0.0 ]
EXECUTE-INS
(DEFN CURRENT-INS
(PC S)
(PC-WORD-READ PC (MC-MEM S)))
Note that (NUMBERP (CURRENT-INS PC S)) is a theorem.
[ 0.0 0.0 0.0 ]
CURRENT-INS
(DEFN STEPI
(S)
(IF (EVENP (MC-PC S))
(IF (PC-WORD-READP (MC-PC S) (MC-MEM S))
(EXECUTE-INS (CURRENT-INS (MC-PC S) S)
(UPDATE-PC (ADD (L) (MC-PC S) (WSZ))
S))
(HALT (PC-SIGNAL) S))
(HALT (PC-ODD-SIGNAL) S)))
[ 0.0 0.0 0.0 ]
STEPI
(DEFN STEPN
(S N)
(IF (OR (MC-HALTP S) (ZEROP N))
S
(STEPN (STEPI S) (SUB1 N)))
((LESSP (COUNT N))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definitions of OR, ZEROP,
MC-HALTP, and MC-STATUS establish that the measure (COUNT N) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
STEPN is accepted under the principle of definition.
[ 0.0 0.0 0.0 ]
STEPN
(DEFN CONS-KEY-LST
(KEY LST)
(IF (MEMBER KEY LST)
LST
(CONS KEY LST)))
Note that:
(OR (LISTP (CONS-KEY-LST KEY LST))
(EQUAL (CONS-KEY-LST KEY LST) LST))
is a theorem.
[ 0.0 0.0 0.0 ]
CONS-KEY-LST
(DEFN KEY-FIELD
(MAP)
(IF (LISTP MAP) (CAR MAP) NIL))
[ 0.0 0.0 0.0 ]
KEY-FIELD
(DEFN MAKE-MAP
(KEY MAP)
(MAKE-BT (CONS-KEY-LST KEY (KEY-FIELD MAP))
(BRANCH0 MAP)
(BRANCH1 MAP)))
Note that (LISTP (MAKE-MAP KEY MAP)) is a theorem.
[ 0.0 0.0 0.0 ]
MAKE-MAP
(DEFN MAP-UPDATE
(KEY X N MAP)
(IF (ZEROP N)
(MAKE-MAP KEY MAP)
(IF (B0P (BITN X (SUB1 N)))
(MAKE-BT (KEY-FIELD MAP)
(MAP-UPDATE KEY X
(SUB1 N)
(BRANCH0 MAP))
(BRANCH1 MAP))
(MAKE-BT (KEY-FIELD MAP)
(BRANCH0 MAP)
(MAP-UPDATE KEY X
(SUB1 N)
(BRANCH1 MAP))))))
The lemmas LESSP-SUB1 and COUNT-NUMBERP and the definitions of B0P, B0,
BITN, TAIL, BCAR, and ZEROP can be used to prove that the measure (COUNT N)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, MAP-UPDATE is accepted under the principle of definition. Observe that:
(LISTP (MAP-UPDATE KEY X N MAP))
is a theorem.
[ 0.0 0.1 0.0 ]
MAP-UPDATE
(DEFN LOAD-LST-MEM
(OPSZ LST ADDR MEM)
(IF (LISTP LST)
(LOAD-LST-MEM OPSZ
(CDR LST)
(ADD 32 ADDR OPSZ)
(WRITE-MEM (CAR LST) ADDR MEM OPSZ))
MEM))
Linear arithmetic and the lemma CDR-LESSP can be used to establish that
the measure (COUNT LST) decreases according to the well-founded relation LESSP
in each recursive call. Hence, LOAD-LST-MEM is accepted under the principle
of definition. Note that:
(OR (LISTP (LOAD-LST-MEM OPSZ LST ADDR MEM))
(EQUAL (LOAD-LST-MEM OPSZ LST ADDR MEM)
MEM))
is a theorem.
[ 0.0 0.0 0.0 ]
LOAD-LST-MEM
(COMPILE-UNCOMPILED-DEFNS "tmp")
Loading ./yu/tmp.o
Finished loading ./yu/tmp.o
/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/yu/tmp.lisp
(PROVE-LEMMA GCD-EXAMPLE NIL
(IMPLIES (AND (EQUAL STACK-POINTER 251657792)
(EQUAL RFILE
'(0 0 0 0 0 0 0 0 0 0 0 0 0 0 251657804
251657792))
(EQUAL PC 8886)
(EQUAL CCR 0)
(EQUAL GCD-CODE
'(78 86 0 0 72 231 48 0 36 46 0 8 38 46 0
12 74 130 103 28 74 131 102 4 32 2 96
22 182 130 108 8 76 67 40 0 36 0 96
232 76 66 56 0 38 0 96 224 32 3 76 238
0 12 255 248 78 94 78 117))
(EQUAL EMPTY-MEMORY
'((NIL (NIL (NIL (NIL (NIL ((ROM) NIL))))))))
(EQUAL MEM
(LOAD-LST-MEM 4
'(8882 54 42)
STACK-POINTER
(LOAD-LST-MEM 1 GCD-CODE PC
EMPTY-MEMORY)))
(EQUAL INITIAL-STATE
(MC-STATE 'RUNNING RFILE PC CCR MEM))
(EQUAL FINAL-STATE
(STEPN INITIAL-STATE 37)))
(AND (EQUAL (MC-STATUS FINAL-STATE)
'RUNNING)
(EQUAL (MC-RFILE FINAL-STATE)
'(6 0 0 0 0 0 0 0 0 0 0 0 0 0 251657804
251657796))
(EQUAL (MC-PC FINAL-STATE) 8882))))
This formula can be simplified, using the abbreviations AND, IMPLIES, L, HEAD,
MC-PC, MC-RFILE, MC-STATUS, and MC-STATE, to:
(IMPLIES (AND (EQUAL STACK-POINTER 251657792)
(EQUAL RFILE
'(0 0 0 0 0 0 0 0 0 0 0 0 0 0 251657804 251657792))
(EQUAL PC 8886)
(EQUAL CCR 0)
(EQUAL GCD-CODE
'(78 86 0 0 72 231 48 0 36 46 0 8 38 46 0 12 74
130 103 28 74 131 102 4 32 2 96 22 182 130
108 8 76 67 40 0 36 0 96 232 76 66 56 0 38 0
96 224 32 3 76 238 0 12 255 248 78 94 78 117))
(EQUAL EMPTY-MEMORY
'((NIL (NIL (NIL (NIL (NIL ((ROM) NIL))))))))
(EQUAL MEM
(LOAD-LST-MEM 4
'(8882 54 42)
STACK-POINTER
(LOAD-LST-MEM 1 GCD-CODE PC
EMPTY-MEMORY)))
(EQUAL INITIAL-STATE
(LIST 'RUNNING RFILE PC CCR MEM))
(EQUAL FINAL-STATE
(STEPN INITIAL-STATE 37)))
(AND (EQUAL (CAR FINAL-STATE) 'RUNNING)
(EQUAL (CADR FINAL-STATE)
'(6 0 0 0 0 0 0 0 0 0 0 0 0 0 251657804 251657796))
(EQUAL (REMAINDER (CADDR FINAL-STATE)
(EXP 2 32))
8882))),
which simplifies, opening up the functions LOAD-LST-MEM, CONS, STEPN, CAR,
EQUAL, CDR, EXP, REMAINDER, and AND, to:
T.
Q.E.D.
[ 0.0 4.1 0.0 ]
GCD-EXAMPLE
(MAKE-LIB "mc20-1" T)
Making the lib for "mc20-1".
Compiling the lib for "mc20-1".
Loading ./yu/mc20-1.o
Finished loading ./yu/mc20-1.o
Finished compiling the lib for "mc20-1".
Finished making the lib for "mc20-1".
(/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/yu/mc20-1.lib
/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/yu/mc20-1.lisp)