(NOTE-LIB "mc20-2" T)
Loading ./yu/mc20-2.lib
Finished loading ./yu/mc20-2.lib
Loading ./yu/mc20-2.o
Loading ./yu/0mc20-2.o
Finished loading ./yu/0mc20-2.o
Loading ./yu/1mc20-2.o
Finished loading ./yu/1mc20-2.o
Finished loading ./yu/mc20-2.o
(#./yu/mc20-2.lib #./yu/mc20-2)
(DEFN BSEARCH-CODE NIL
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0 12 66 129 36 46 0 16 180 129
111 32 32 1 208 130 106 2 82 128 226 128 182 176 12 0 108 4 36 0 96
232 182 176 12 0 111 8 34 0 82 129 96 220 112 255 76 238 0 12 255
248 78 94 78 117))
Observe that (LISTP (BSEARCH-CODE)) is a theorem.
[ 0.0 0.0 0.0 ]
BSEARCH-CODE
(PROVE-LEMMA MEAN-BOUNDS
(REWRITE)
(IMPLIES (LESSP I J)
(AND (LESSP (QUOTIENT (PLUS I J) 2) J)
(NOT (LESSP (QUOTIENT (PLUS I J) 2) I)))))
WARNING: Note that the proposed lemma MEAN-BOUNDS is to be stored as zero
type prescription rules, zero compound recognizer rules, two linear rules, and
zero replacement rules.
This formula can be simplified, using the abbreviations IMPLIES and MEAN-LESSP,
to:
(IMPLIES (LESSP I J)
(AND (LESSP I J) (NOT (LESSP J I)))),
which simplifies, expanding the functions NOT and AND, to:
(IMPLIES (LESSP I J)
(NOT (LESSP J I))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
MEAN-BOUNDS
(PROVE-LEMMA ILESSP-LESSP
(REWRITE)
(IMPLIES (AND (NUMBERP X) (NUMBERP Y))
(EQUAL (ILESSP X Y) (LESSP X Y))))
WARNING: Note that the rewrite rule ILESSP-LESSP will be stored so as to
apply only to terms with the nonrecursive function symbol ILESSP.
This conjecture simplifies, expanding the definitions of NEGP and ILESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ILESSP-LESSP
(DISABLE ILESSP)
[ 0.0 0.0 0.0 ]
ILESSP-OFF
(DEFN BSEARCH1
(X LST I J)
(LET ((K (QUOTIENT (PLUS I J) 2)))
(IF (LESSP I J)
(IF (ILESSP X (GET-NTH K LST))
(BSEARCH1 X LST I K)
(IF (ILESSP (GET-NTH K LST) X)
(BSEARCH1 X LST (ADD1 K) J)
K))
-1))
((LESSP (DIFFERENCE J I))))
Linear arithmetic and the lemma MEAN-BOUNDS can be used to show that the
measure (DIFFERENCE J I) decreases according to the well-founded relation
LESSP in each recursive call. Hence, BSEARCH1 is accepted under the
definitional principle. Note that:
(OR (NUMBERP (BSEARCH1 X LST I J))
(NEGATIVEP (BSEARCH1 X LST I J)))
is a theorem.
[ 0.0 0.1 0.0 ]
BSEARCH1
(DEFN BSEARCH
(X N LST)
(BSEARCH1 X LST 0 N))
From the definition we can conclude that:
(OR (NUMBERP (BSEARCH X N LST))
(NEGATIVEP (BSEARCH X N LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
BSEARCH
(DEFN BSEARCH1-T
(X LST I J)
(LET ((K (QUOTIENT (PLUS I J) 2)))
(IF (LESSP I J)
(IF (ILESSP X (GET-NTH K LST))
(SPLUS 10 (BSEARCH1-T X LST I K))
(IF (ILESSP (GET-NTH K LST) X)
(SPLUS 13
(BSEARCH1-T X LST (ADD1 K) J))
13))
6))
((LESSP (DIFFERENCE J I))))
Linear arithmetic and the lemma MEAN-BOUNDS establish that the measure
(DIFFERENCE J I) decreases according to the well-founded relation LESSP in
each recursive call. Hence, BSEARCH1-T is accepted under the principle of
definition. From the definition we can conclude that:
(NUMBERP (BSEARCH1-T X LST I J))
is a theorem.
[ 0.0 0.5 0.0 ]
BSEARCH1-T
(DEFN BSEARCH-T
(X N LST)
(SPLUS 6 (BSEARCH1-T X LST 0 N)))
Note that (NUMBERP (BSEARCH-T X N LST)) is a theorem.
[ 0.0 0.0 0.0 ]
BSEARCH-T
(DEFN BSEARCH-INDUCT
(S X LST I J)
(LET ((K (QUOTIENT (PLUS I J) 2)))
(IF (LESSP I J)
(IF (ILESSP X (GET-NTH K LST))
(BSEARCH-INDUCT (STEPN S 10)
X LST I K)
(IF (ILESSP (GET-NTH K LST) X)
(BSEARCH-INDUCT (STEPN S 13)
X LST
(ADD1 K)
J)
T))
T))
((LESSP (DIFFERENCE J I))))
Linear arithmetic and the lemma MEAN-BOUNDS inform us that the measure
(DIFFERENCE J I) decreases according to the well-founded relation LESSP in
each recursive call. Hence, BSEARCH-INDUCT is accepted under the definitional
principle. From the definition we can conclude that:
(TRUEP (BSEARCH-INDUCT S X LST I J))
is a theorem.
[ 0.0 0.1 0.0 ]
BSEARCH-INDUCT
(DEFN BSEARCH-STATEP
(S X A N LST)
(AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (MC-PC S) (MC-MEM S) 70)
(MCODE-ADDRP (MC-PC S)
(MC-MEM S)
(BSEARCH-CODE))
(RAM-ADDRP (SUB 32 12 (READ-SP S))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 12 (READ-SP S))
28 A
(TIMES 4 N))
(EQUAL A
(READ-MEM (ADD 32 (READ-SP S) 8)
(MC-MEM S)
4))
(EQUAL N
(IREAD-MEM (ADD 32 (READ-SP S) 12)
(MC-MEM S)
4))
(EQUAL X
(IREAD-MEM (ADD 32 (READ-SP S) 4)
(MC-MEM S)
4))
(INT-RANGEP (TIMES 2 N) 32)
(NUMBERP N)))
Note that:
(OR (FALSEP (BSEARCH-STATEP S X A N LST))
(TRUEP (BSEARCH-STATEP S X A N LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
BSEARCH-STATEP
(DEFN BSEARCH-S0P
(S X A N LST I J)
(AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
70)
(MCODE-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
(BSEARCH-CODE))
(RAM-ADDRP (SUB 32 8 (READ-AN 32 6 S))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 8 (READ-AN 32 6 S))
28 A
(TIMES 4 N))
(EQUAL A (READ-AN 32 0 S))
(EQUAL I
(NAT-TO-INT (READ-DN 32 1 S) 32))
(EQUAL J
(NAT-TO-INT (READ-DN 32 2 S) 32))
(EQUAL X
(NAT-TO-INT (READ-DN 32 3 S) 32))
(INT-RANGEP (TIMES 2 J) 32)
(NUMBERP I)
(NUMBERP J)
(NUMBERP N)
(LEQ I N)
(LEQ J N)))
Note that:
(OR (FALSEP (BSEARCH-S0P S X A N LST I J))
(TRUEP (BSEARCH-S0P S X A N LST I J)))
is a theorem.
[ 0.0 0.0 0.0 ]
BSEARCH-S0P
(PROVE-LEMMA BSEARCH-S-S0P NIL
(IMPLIES (BSEARCH-STATEP S X A N LST)
(BSEARCH-S0P (STEPN S 6)
X A N LST 0 N)))
This conjecture can be simplified, using the abbreviations SP, L, READ-AN,
READ-SP, BSEARCH-CODE, BSEARCH-STATEP, and IMPLIES, to the goal:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (MC-PC S) (MC-MEM S) 70)
(MCODE-ADDRP (MC-PC S)
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 12
(READ-RN 32 (PLUS 8 7) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 12
(READ-RN 32 (PLUS 8 7) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
8)
(MC-MEM S)
4))
(EQUAL N
(IREAD-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
12)
(MC-MEM S)
4))
(EQUAL X
(IREAD-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
4)
(MC-MEM S)
4))
(INT-RANGEP (TIMES 2 N) 32)
(NUMBERP N))
(BSEARCH-S0P (STEPN S 6)
X A N LST 0 N)).
This simplifies, using linear arithmetic, rewriting with SUB-NEG,
WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP,
MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1,
MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0,
PC-READ-MEMP-ROM0, READM-WRITE-RN, CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP,
CDR-CONS, READ-WRITE-RN, HEAD-LEMMA, WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM,
WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP,
WRITE-MEMP->READ-MEMP, READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2,
PC-READ-MEM-WRITEM-MEM, READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP,
READ-MEM-NAT-RANGEP, EXT-LEMMA, SET-CVZNX-NAT-RANGEP, SET-SET-CVZNX1,
SET-CVZNX-X, BITP-FIX-BIT, FIX-BIT-BITP, STEPN-REWRITER0, STEPN-REWRITER,
DISJOINT-6-UINT, WRITEM-ELSE-MEM-ILST, WRITE-ELSE-MEM-ILST, DISJOINT-6~,
RAM-ADDRP-LA2, PLUS-0, PLUS-COMMUTATIVITY, WRITEM-MEM-MAINTAIN-RAM-ADDRP,
WRITE-MEM-MAINTAIN-RAM-ADDRP, RAM-ADDRP-3, WRITEM-MEM-MCODE-ADDRP,
WRITE-MEM-MCODE-ADDRP, WRITEM-MEM-MAINTAIN-ROM-ADDRP,
WRITE-MEM-MAINTAIN-ROM-ADDRP, ROM-ADDRP-LA2, INDEX-N-X-X, ADD-0, and
MC-PC-RANGEP, and unfolding PLUS, NEG, TIMES, IREAD-MEM, EXECUTE-INS,
OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP,
READ-SP, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W,
LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN,
LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, EXT-SUBGROUP,
S_MODE, N-MEMBER, MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC, NUMBERP, OP-SZ, B,
PRE-EFFECT, MOVEM-LEN, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP, MOVE-INS,
MOVE-ADDR-MODEP, EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP, DISJOINT,
OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS,
DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEA-INS, MOVEA-ADDR-MODEP,
CLR-SUBGROUP, OP-LEN, Q, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS,
NAT-TO-INT, READ-DN, HEAD, BSEARCH-CODE, and BSEARCH-S0P, to the goal:
(IMPLIES
(AND
(EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (MC-PC S) (MC-MEM S) 70)
(MCODE-ADDRP (MC-PC S)
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0 12 66 129 36
46 0 16 180 129 111 32 32 1 208 130 106 2 82 128
226 128 182 176 12 0 108 4 36 0 96 232 182 176 12 0
111 8 34 0 82 129 96 220 112 255 76 238 0 12 255
248 78 94 78 117))
(RAM-ADDRP (ADD 32
(READ-RN 32 15 (MC-RFILE S))
4294967284)
(MC-MEM S)
28)
(RAM-ADDRP
(READ-MEM (ADD 32
(READ-RN 32 15 (MC-RFILE S))
8)
(MC-MEM S)
4)
(MC-MEM S)
(TIMES 4
(NAT-TO-INT (READ-MEM (ADD 32
(READ-RN 32 15 (MC-RFILE S))
12)
(MC-MEM S)
4)
32)))
(MEM-ILST 4
(READ-MEM (ADD 32
(READ-RN 32 15 (MC-RFILE S))
8)
(MC-MEM S)
4)
(MC-MEM S)
(NAT-TO-INT (READ-MEM (ADD 32
(READ-RN 32 15 (MC-RFILE S))
12)
(MC-MEM S)
4)
32)
LST)
(DISJOINT
(ADD 32
(READ-RN 32 15 (MC-RFILE S))
4294967284)
28
(READ-MEM (ADD 32
(READ-RN 32 15 (MC-RFILE S))
8)
(MC-MEM S)
4)
(TIMES 4
(NAT-TO-INT (READ-MEM (ADD 32
(READ-RN 32 15 (MC-RFILE S))
12)
(MC-MEM S)
4)
32)))
(INT-RANGEP
(TIMES 2
(NAT-TO-INT (READ-MEM (ADD 32
(READ-RN 32 15 (MC-RFILE S))
12)
(MC-MEM S)
4)
32))
32)
(NUMBERP (NAT-TO-INT (READ-MEM (ADD 32
(READ-RN 32 15 (MC-RFILE S))
12)
(MC-MEM S)
4)
32)))
(NOT (LESSP (NAT-TO-INT (READ-MEM (ADD 32
(READ-RN 32 15 (MC-RFILE S))
12)
(MC-MEM S)
4)
32)
(NAT-TO-INT (READ-MEM (ADD 32
(READ-RN 32 15 (MC-RFILE S))
12)
(MC-MEM S)
4)
32)))).
This again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.8 0.0 ]
BSEARCH-S-S0P
(PROVE-LEMMA BSEARCH-S-S0
(REWRITE)
(IMPLIES (BSEARCH-STATEP S X A N LST)
(AND (EQUAL (LINKED-RTS-ADDR (STEPN S 6))
(RTS-ADDR S))
(EQUAL (LINKED-A6 (STEPN S 6))
(READ-AN 32 6 S))
(EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6)))
(SUB 32 4 (READ-SP S)))
(EQUAL (MOVEM-SAVED (STEPN S 6) 4 8 2)
(READM-RN 32 '(2 3) (MC-RFILE S))))))
WARNING: Note that the rewrite rule BSEARCH-S-S0 will be stored so as to
apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR.
WARNING: Note that BSEARCH-S-S0 contains the free variables LST, N, A, and X
which will be chosen by instantiating the hypothesis:
(BSEARCH-STATEP S X A N LST).
WARNING: Note that the rewrite rule BSEARCH-S-S0 will be stored so as to
apply only to terms with the nonrecursive function symbol LINKED-A6.
WARNING: Note that BSEARCH-S-S0 contains the free variables LST, N, A, and X
which will be chosen by instantiating the hypothesis:
(BSEARCH-STATEP S X A N LST).
WARNING: Note that BSEARCH-S-S0 contains the free variables LST, N, A, and X
which will be chosen by instantiating the hypothesis:
(BSEARCH-STATEP S X A N LST).
WARNING: Note that the rewrite rule BSEARCH-S-S0 will be stored so as to
apply only to terms with the nonrecursive function symbol MOVEM-SAVED.
WARNING: Note that BSEARCH-S-S0 contains the free variables LST, N, A, and X
which will be chosen by instantiating the hypothesis:
(BSEARCH-STATEP S X A N LST).
WARNING: Note that the proposed lemma BSEARCH-S-S0 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
This formula can be simplified, using the abbreviations BSEARCH-CODE,
BSEARCH-STATEP, IMPLIES, SP, L, READ-SP, and READ-AN, to the new goal:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (MC-PC S) (MC-MEM S) 70)
(MCODE-ADDRP (MC-PC S)
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 12
(READ-RN 32 (PLUS 8 7) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 12
(READ-RN 32 (PLUS 8 7) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
8)
(MC-MEM S)
4))
(EQUAL N
(IREAD-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
12)
(MC-MEM S)
4))
(EQUAL X
(IREAD-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
4)
(MC-MEM S)
4))
(INT-RANGEP (TIMES 2 N) 32)
(NUMBERP N))
(AND (EQUAL (LINKED-RTS-ADDR (STEPN S 6))
(RTS-ADDR S))
(EQUAL (LINKED-A6 (STEPN S 6))
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
(EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6)))
(SUB 32 4
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))))
(EQUAL (MOVEM-SAVED (STEPN S 6) 4 8 2)
(READM-RN 32 '(2 3) (MC-RFILE S))))),
which simplifies, rewriting with SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE,
MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY,
PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE,
ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, READM-WRITE-RN,
CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, CDR-CONS, READ-WRITE-RN, HEAD-LEMMA,
WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP,
ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP, WRITE-MEMP->READ-MEMP,
READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITEM-MEM,
READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP, READ-MEM-NAT-RANGEP, EXT-LEMMA,
SET-CVZNX-NAT-RANGEP, SET-SET-CVZNX1, SET-CVZNX-X, BITP-FIX-BIT, FIX-BIT-BITP,
STEPN-REWRITER0, STEPN-REWRITER, DISJOINT-DEDUCTION1, ADD-0, HEAD-READ-RN,
READ-WRITE-MEM2, READM-WRITEM-MEM, and MODN-READM-RN, and expanding PLUS, NEG,
TIMES, IREAD-MEM, EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN,
LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, INDEX-N, UPDATE-RFILE, WRITE-AN,
WRITE-SP, UPDATE-MEM, ADD, EXT, W, LINK_W-INS, B0P, BITN, MISC-GROUP,
UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ,
PC-WORD-READP, WSZ, LESSP, STEPI, EXT-SUBGROUP, S_MODE, N-MEMBER,
MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC, NUMBERP, OP-SZ, B, PRE-EFFECT,
MOVEM-LEN, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP, MOVE-INS, MOVE-ADDR-MODEP,
EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR,
CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN,
MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEA-INS, MOVEA-ADDR-MODEP, CLR-SUBGROUP,
OP-LEN, Q, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, LINKED-RTS-ADDR,
RTS-ADDR, UINT-RANGEP, LINKED-A6, MOVEM-SAVED, and AND, to:
T.
Q.E.D.
[ 0.0 2.7 0.0 ]
BSEARCH-S-S0
(PROVE-LEMMA BSEARCH-S-S0-RFILE
(REWRITE)
(IMPLIES (AND (BSEARCH-STATEP S X A N LST)
(D4-7A2-5P RN))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 6)))
(READ-RN OPLEN RN (MC-RFILE S)))))
WARNING: Note that BSEARCH-S-S0-RFILE contains the free variables LST, N, A,
and X which will be chosen by instantiating the hypothesis:
(BSEARCH-STATEP S X A N LST).
This conjecture can be simplified, using the abbreviations D2-7A2-5P,
D4-7A2-5P, SP, L, READ-AN, READ-SP, BSEARCH-CODE, BSEARCH-STATEP, AND, and
IMPLIES, to:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (MC-PC S) (MC-MEM S) 70)
(MCODE-ADDRP (MC-PC S)
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 12
(READ-RN 32 (PLUS 8 7) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 12
(READ-RN 32 (PLUS 8 7) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
8)
(MC-MEM S)
4))
(EQUAL N
(IREAD-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
12)
(MC-MEM S)
4))
(EQUAL X
(IREAD-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
4)
(MC-MEM S)
4))
(INT-RANGEP (TIMES 2 N) 32)
(NUMBERP N)
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (EQUAL RN 2))
(NOT (EQUAL RN 3)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 6)))
(READ-RN OPLEN RN (MC-RFILE S)))).
This simplifies, appealing to the lemmas SUB-NEG, WRITE-MEMP-RAM3,
MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE,
ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE,
MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0,
READM-WRITE-RN, CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, CDR-CONS,
READ-WRITE-RN, HEAD-LEMMA, WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM,
WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP,
WRITE-MEMP->READ-MEMP, READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2,
PC-READ-MEM-WRITEM-MEM, READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP,
READ-MEM-NAT-RANGEP, EXT-LEMMA, SET-CVZNX-NAT-RANGEP, SET-SET-CVZNX1,
SET-CVZNX-X, BITP-FIX-BIT, FIX-BIT-BITP, STEPN-REWRITER0, and STEPN-REWRITER,
and unfolding PLUS, NEG, TIMES, IREAD-MEM, EXECUTE-INS, OPCODE-FIELD, EQUAL,
UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, INDEX-N,
UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, LINK_W-INS, B0P,
BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP,
PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, EXT-SUBGROUP, S_MODE, N-MEMBER,
MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC, NUMBERP, OP-SZ, B, PRE-EFFECT,
MOVEM-LEN, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP, MOVE-INS, MOVE-ADDR-MODEP,
EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR,
CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN,
MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEA-INS, MOVEA-ADDR-MODEP, CLR-SUBGROUP,
OP-LEN, Q, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, and CLR-INS, to:
T.
Q.E.D.
[ 0.0 0.8 0.0 ]
BSEARCH-S-S0-RFILE
(PROVE-LEMMA BSEARCH-S-S0-MEM
(REWRITE)
(IMPLIES (AND (BSEARCH-STATEP S X A N LST)
(DISJOINT X K
(SUB 32 12 (READ-SP S))
28))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) K)
(READ-MEM X (MC-MEM S) K))))
WARNING: Note that BSEARCH-S-S0-MEM contains the free variables LST, N, and A
which will be chosen by instantiating the hypothesis:
(BSEARCH-STATEP S X A N LST).
This formula can be simplified, using the abbreviations BSEARCH-CODE,
BSEARCH-STATEP, AND, IMPLIES, SP, L, READ-AN, and READ-SP, to the new goal:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (MC-PC S) (MC-MEM S) 70)
(MCODE-ADDRP (MC-PC S)
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 12
(READ-RN 32 (PLUS 8 7) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 12
(READ-RN 32 (PLUS 8 7) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
8)
(MC-MEM S)
4))
(EQUAL N
(IREAD-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
12)
(MC-MEM S)
4))
(EQUAL X
(IREAD-MEM (ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
4)
(MC-MEM S)
4))
(INT-RANGEP (TIMES 2 N) 32)
(NUMBERP N)
(DISJOINT X K
(SUB 32 12
(READ-RN 32 (PLUS 8 7) (MC-RFILE S)))
28))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) K)
(READ-MEM X (MC-MEM S) K))),
which simplifies, using linear arithmetic, appealing to the lemmas SUB-NEG,
WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP,
MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1,
MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0,
PC-READ-MEMP-ROM0, READM-WRITE-RN, CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP,
CDR-CONS, READ-WRITE-RN, HEAD-LEMMA, WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM,
WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP,
WRITE-MEMP->READ-MEMP, READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2,
PC-READ-MEM-WRITEM-MEM, READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP,
READ-MEM-NAT-RANGEP, EXT-LEMMA, SET-CVZNX-NAT-RANGEP, SET-SET-CVZNX1,
SET-CVZNX-X, BITP-FIX-BIT, FIX-BIT-BITP, STEPN-REWRITER0, STEPN-REWRITER, and
DISJOINT-10, and expanding the definitions of PLUS, NEG, TIMES, IREAD-MEM,
EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ,
READ-AN, SP, READ-SP, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM,
ADD, EXT, W, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS,
READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI,
EXT-SUBGROUP, S_MODE, N-MEMBER, MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC,
NUMBERP, OP-SZ, B, PRE-EFFECT, MOVEM-LEN, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP,
MOVE-INS, MOVE-ADDR-MODEP, EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP,
DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX,
CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEA-INS,
MOVEA-ADDR-MODEP, CLR-SUBGROUP, OP-LEN, Q, CLR-EFFECT, B1, CLR-CVZNX,
CLR-ADDR-MODEP, and CLR-INS, to:
T.
Q.E.D.
[ 0.0 0.8 0.0 ]
BSEARCH-S-S0-MEM
(PROVE-LEMMA BSEARCH-S0-SN-BASE1
(REWRITE)
(IMPLIES (AND (BSEARCH-S0P S X A N LST I J)
(NOT (LESSP I J)))
(AND (EQUAL (MC-STATUS (STEPN S 6))
'RUNNING)
(EQUAL (MC-PC (STEPN S 6))
(LINKED-RTS-ADDR S))
(EQUAL (IREAD-DN 32 0 (STEPN S 6)) -1)
(EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6)))
(LINKED-A6 S))
(EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 6)))
(ADD 32 (READ-AN 32 6 S) 8))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) L)
(READ-MEM X (MC-MEM S) L)))))
WARNING: Note that BSEARCH-S0-SN-BASE1 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN-BASE1 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the rewrite rule BSEARCH-S0-SN-BASE1 will be stored so as
to apply only to terms with the nonrecursive function symbol IREAD-DN.
WARNING: Note that BSEARCH-S0-SN-BASE1 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN-BASE1 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN-BASE1 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN-BASE1 contains the free variables J, I, LST,
N, and A which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the proposed lemma BSEARCH-S0-SN-BASE1 is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and six replacement rules.
This conjecture can be simplified, using the abbreviations NOT, READ-DN,
BSEARCH-CODE, BSEARCH-S0P, AND, IMPLIES, and READ-AN, to:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
70)
(MCODE-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-RN 32 (PLUS 8 0) (MC-RFILE S)))
(EQUAL I
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(EQUAL J
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(EQUAL X
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32))
(INT-RANGEP (TIMES 2 J) 32)
(NUMBERP I)
(NUMBERP J)
(NUMBERP N)
(NOT (LESSP N I))
(NOT (LESSP N J))
(NOT (LESSP I J)))
(AND (EQUAL (MC-STATUS (STEPN S 6))
'RUNNING)
(EQUAL (MC-PC (STEPN S 6))
(LINKED-RTS-ADDR S))
(EQUAL (IREAD-DN 32 0 (STEPN S 6)) -1)
(EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6)))
(LINKED-A6 S))
(EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 6)))
(ADD 32
(READ-RN 32 (PLUS 8 6) (MC-RFILE S))
8))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) L)
(READ-MEM X (MC-MEM S) L)))).
This simplifies, rewriting with SUB-NEG, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE,
MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE,
ADD-NAT-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, BLE-BGT, SUB-BGT,
ILESSP-LESSP, READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z,
SUB-Z-BITP, SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, SET-CVZNX-NAT-RANGEP,
ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP,
SET-SET-CVZNX1, SET-CVZNX-X, READ-MEMP-RAM3, READ-WRITE-RN, READ-MEMP-RAM2,
READ-WRITEM-RN, HEAD-LEMMA, STEPN-REWRITER0, STEPN-REWRITER, and
READ-MEM-NAT-RANGEP, and expanding the functions NEG, PLUS, EXECUTE-INS,
OPCODE-FIELD, EQUAL, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS,
DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, READ-DN, CDR, OPERAND, D_RN,
CMP-CVZNX, UPDATE-CCR, Q, B0P, BITN, CMP-GROUP, UPDATE-PC, L, CURRENT-INS,
READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N,
STEPI, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD,
EVENP, D-MAPPING, MOVE-EFFECT, MOVE-N, MOVE-Z, B0, MOVE-CVZNX, MOVEQ-INS,
MOVEM-EA-RN-SUBGROUP, UPDATE-RFILE, MOVEM-RNLST, READMP, OP-SZ, MOVEM-LEN,
TIMES, W, READ-AN, NUMBERP, ADDR-DISP, MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP,
MOVEM-EA-RN-INS, MISC-GROUP, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ,
LONG-READP, LSZ, N-MEMBER, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP,
RTS-INS, LINKED-RTS-ADDR, NAT-TO-INT, IREAD-DN, LINKED-A6, and AND, to:
T.
Q.E.D.
[ 0.0 0.8 0.0 ]
BSEARCH-S0-SN-BASE1
(PROVE-LEMMA BSEARCH-S0-SN-RFILE-BASE1
(REWRITE)
(IMPLIES (AND (BSEARCH-S0P S X A N LST I J)
(NOT (LESSP I J))
(D2-7A2-5P RN)
(LEQ OPLEN 32))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 6)))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN (MC-RFILE S))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED S 4 8 2))))))
WARNING: Note that BSEARCH-S0-SN-RFILE-BASE1 contains the free variables J, I,
LST, N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
This formula can be simplified, using the abbreviations D2-7A2-5P, NOT,
READ-DN, READ-AN, BSEARCH-CODE, BSEARCH-S0P, AND, and IMPLIES, to the new
conjecture:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
70)
(MCODE-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-RN 32 (PLUS 8 0) (MC-RFILE S)))
(EQUAL I
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(EQUAL J
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(EQUAL X
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32))
(INT-RANGEP (TIMES 2 J) 32)
(NUMBERP I)
(NUMBERP J)
(NUMBERP N)
(NOT (LESSP N I))
(NOT (LESSP N J))
(NOT (LESSP I J))
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (LESSP 32 OPLEN)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 6)))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN (MC-RFILE S))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED S 4 8 2))))),
which simplifies, applying SUB-NEG, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE,
MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE,
ADD-NAT-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, BLE-BGT, SUB-BGT,
ILESSP-LESSP, READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z,
SUB-Z-BITP, SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, SET-CVZNX-NAT-RANGEP,
ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP,
SET-SET-CVZNX1, SET-CVZNX-X, READ-MEMP-RAM3, READ-WRITE-RN, READ-MEMP-RAM2,
READ-WRITEM-RN, HEAD-LEMMA, STEPN-REWRITER0, and STEPN-REWRITER, and unfolding
the functions NEG, PLUS, EXECUTE-INS, OPCODE-FIELD, EQUAL, OP-LEN, CMP-INS,
CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE,
MC-HALTP, READ-DN, CDR, OPERAND, D_RN, CMP-CVZNX, UPDATE-CCR, Q, B0P, BITN,
CMP-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ,
PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, B-NOT,
BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, D-MAPPING, MOVE-EFFECT,
MOVE-N, MOVE-Z, B0, MOVE-CVZNX, MOVEQ-INS, MOVEM-EA-RN-SUBGROUP, UPDATE-RFILE,
MOVEM-RNLST, READMP, OP-SZ, MOVEM-LEN, TIMES, W, READ-AN, NUMBERP, ADDR-DISP,
MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, MISC-GROUP,
UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER,
UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LISTP, D2-7A2-5P,
D4-7A2-5P, and MOVEM-SAVED, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
BSEARCH-S0-SN-RFILE-BASE1
(ENABLE IPLUS)
[ 0.0 0.0 0.0 ]
IPLUS-ON
(ENABLE IQUOTIENT)
[ 0.0 0.0 0.0 ]
IQUOTIENT-ON
(DISABLE QUOTIENT)
[ 0.0 0.0 0.0 ]
QUOTIENT-OFF
(DISABLE REMAINDER)
[ 0.0 0.0 0.0 ]
REMAINDER-OFF
(DISABLE TIMES)
[ 0.0 0.0 0.0 ]
TIMES-OFF1
(PROVE-LEMMA BSEARCH-CROCK
(REWRITE)
(IMPLIES (AND (INT-RANGEP (TIMES 2 J) N)
(LESSP I J))
(INT-RANGEP (PLUS I J) N)))
This formula simplifies, using linear arithmetic, rewriting with the lemma
ABS-LESSP-INT-RANGEP, and expanding ABS and NEGP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
BSEARCH-CROCK
(PROVE-LEMMA BSEARCH-S0-SN-BASE2
(REWRITE)
(LET ((K (QUOTIENT (PLUS I J) 2)))
(IMPLIES (AND (BSEARCH-S0P S X A N LST I J)
(LESSP I J)
(NOT (ILESSP X (GET-NTH K LST)))
(NOT (ILESSP (GET-NTH K LST) X)))
(AND (EQUAL (MC-STATUS (STEPN S 13))
'RUNNING)
(EQUAL (MC-PC (STEPN S 13))
(LINKED-RTS-ADDR S))
(EQUAL (IREAD-DN 32 0 (STEPN S 13))
(QUOTIENT (PLUS I J) 2))
(EQUAL (READ-RN 32 14
(MC-RFILE (STEPN S 13)))
(LINKED-A6 S))
(EQUAL (READ-RN 32 15
(MC-RFILE (STEPN S 13)))
(ADD 32 (READ-AN 32 6 S) 8))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 13)) L)
(READ-MEM X (MC-MEM S) L))))))
WARNING: Note that BSEARCH-S0-SN-BASE2 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN-BASE2 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the rewrite rule BSEARCH-S0-SN-BASE2 will be stored so as
to apply only to terms with the nonrecursive function symbol IREAD-DN.
WARNING: Note that BSEARCH-S0-SN-BASE2 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN-BASE2 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN-BASE2 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN-BASE2 contains the free variables J, I, LST,
N, and A which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the proposed lemma BSEARCH-S0-SN-BASE2 is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and six replacement rules.
This conjecture can be simplified, using the abbreviations NOT, READ-DN,
BSEARCH-CODE, BSEARCH-S0P, AND, IMPLIES, and READ-AN, to the conjecture:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
70)
(MCODE-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-RN 32 (PLUS 8 0) (MC-RFILE S)))
(EQUAL I
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(EQUAL J
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(EQUAL X
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32))
(INT-RANGEP (TIMES 2 J) 32)
(NUMBERP I)
(NUMBERP J)
(NUMBERP N)
(NOT (LESSP N I))
(NOT (LESSP N J))
(LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(NOT (ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)))
(AND (EQUAL (MC-STATUS (STEPN S 13))
'RUNNING)
(EQUAL (MC-PC (STEPN S 13))
(LINKED-RTS-ADDR S))
(EQUAL (IREAD-DN 32 0 (STEPN S 13))
(QUOTIENT (PLUS I J) 2))
(EQUAL (READ-RN 32 14
(MC-RFILE (STEPN S 13)))
(LINKED-A6 S))
(EQUAL (READ-RN 32 15
(MC-RFILE (STEPN S 13)))
(ADD 32
(READ-RN 32 (PLUS 8 6) (MC-RFILE S))
8))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 13)) L)
(READ-MEM X (MC-MEM S) L)))).
This simplifies, using linear arithmetic, appealing to the lemmas SUB-NEG,
CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP,
MC-CCR-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP,
PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, BLE-BGT, SUB-BGT, ILESSP-LESSP,
READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP,
SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY,
PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X,
READ-WRITE-RN, HEAD-READ-RN, WRITE-WRITE-RN, ADD-BMI, BSEARCH-CROCK,
IPLUS-COMMUTATIVITY, ADD-N-BITP, HEAD-LEMMA, READ-MEMP-RAM1-ASL, ADD-INT,
ASR-INT, QUOTIENT-TIMES, MEAN-BOUNDS, ASR-NAT-RANGEP, ADD-0, ASR-C-BITP,
SUB-BGE, READ-MEM-ILST-ASL, READ-MEM-NAT-RANGEP, READ-MEMP-RAM3,
READ-MEMP-RAM2, READ-WRITEM-RN, STEPN-REWRITER0, and STEPN-REWRITER, and
expanding the functions NEG, PLUS, EXECUTE-INS, OPCODE-FIELD, EQUAL, OP-LEN,
CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE,
MC-INSTATE, MC-HALTP, READ-DN, CDR, OPERAND, D_RN, CMP-CVZNX, UPDATE-CCR, Q,
B0P, BITN, CMP-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP,
PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR,
B-NOT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, MOVE-INS,
MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, MOVE-MAPPING,
D_MODE, MOVE-GROUP, OPMODE-FIELD, ADD-INS1, ADD-ADDR-MODEP1, NUMBERP,
ADD-CVZNX, ADD-EFFECT, ADD-GROUP, IPLUS, NEGP, REGISTER-SHIFT-ROTATE,
ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA, REGISTER-ASR-INS, S&R-GROUP, EXP,
IQUOTIENT, OP-SZ, ADDR-INDEX1, IR-SCALED, INDEX-RN, INDEX-REGISTER, BITS,
READ-AN, ADDR-INDEX-DISP, ADDR-INDEX, TIMES, MOVEM-EA-RN-SUBGROUP,
UPDATE-RFILE, MOVEM-RNLST, READMP, MOVEM-LEN, W, ADDR-DISP,
MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, MISC-GROUP,
UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER,
UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LINKED-RTS-ADDR,
IREAD-DN, LINKED-A6, and AND, to:
T.
Q.E.D.
[ 0.0 5.0 0.0 ]
BSEARCH-S0-SN-BASE2
(PROVE-LEMMA BSEARCH1-S0-SN-RFILE-BASE2
(REWRITE)
(LET ((K (QUOTIENT (PLUS I J) 2)))
(IMPLIES (AND (BSEARCH-S0P S X A N LST I J)
(LESSP I J)
(NOT (ILESSP X (GET-NTH K LST)))
(NOT (ILESSP (GET-NTH K LST) X))
(D2-7A2-5P RN)
(LEQ OPLEN 32))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 13)))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN (MC-RFILE S))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED S 4 8 2)))))))
WARNING: Note that BSEARCH1-S0-SN-RFILE-BASE2 contains the free variables J,
I, LST, N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
This formula can be simplified, using the abbreviations D2-7A2-5P, NOT,
READ-DN, READ-AN, BSEARCH-CODE, BSEARCH-S0P, AND, and IMPLIES, to:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
70)
(MCODE-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-RN 32 (PLUS 8 0) (MC-RFILE S)))
(EQUAL I
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(EQUAL J
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(EQUAL X
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32))
(INT-RANGEP (TIMES 2 J) 32)
(NUMBERP I)
(NUMBERP J)
(NUMBERP N)
(NOT (LESSP N I))
(NOT (LESSP N J))
(LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(NOT (ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X))
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (LESSP 32 OPLEN)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 13)))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN (MC-RFILE S))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED S 4 8 2))))),
which simplifies, using linear arithmetic, rewriting with the lemmas SUB-NEG,
CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP,
MC-CCR-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP,
PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, BLE-BGT, SUB-BGT, ILESSP-LESSP,
READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP,
SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY,
PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X,
READ-WRITE-RN, HEAD-READ-RN, WRITE-WRITE-RN, ADD-BMI, BSEARCH-CROCK,
IPLUS-COMMUTATIVITY, ADD-N-BITP, HEAD-LEMMA, READ-MEMP-RAM1-ASL, ADD-INT,
ASR-INT, QUOTIENT-TIMES, MEAN-BOUNDS, ASR-NAT-RANGEP, ADD-0, ASR-C-BITP,
SUB-BGE, READ-MEM-ILST-ASL, READ-MEM-NAT-RANGEP, READ-MEMP-RAM3,
READ-MEMP-RAM2, READ-WRITEM-RN, STEPN-REWRITER0, and STEPN-REWRITER, and
unfolding the functions NEG, PLUS, EXECUTE-INS, OPCODE-FIELD, EQUAL, OP-LEN,
CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE,
MC-INSTATE, MC-HALTP, READ-DN, CDR, OPERAND, D_RN, CMP-CVZNX, UPDATE-CCR, Q,
B0P, BITN, CMP-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP,
PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR,
B-NOT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, MOVE-INS,
MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, MOVE-MAPPING,
D_MODE, MOVE-GROUP, OPMODE-FIELD, ADD-INS1, ADD-ADDR-MODEP1, NUMBERP,
ADD-CVZNX, ADD-EFFECT, ADD-GROUP, IPLUS, NEGP, REGISTER-SHIFT-ROTATE,
ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA, REGISTER-ASR-INS, S&R-GROUP, EXP,
IQUOTIENT, OP-SZ, ADDR-INDEX1, IR-SCALED, INDEX-RN, INDEX-REGISTER, BITS,
READ-AN, ADDR-INDEX-DISP, ADDR-INDEX, TIMES, MOVEM-EA-RN-SUBGROUP,
UPDATE-RFILE, MOVEM-RNLST, READMP, MOVEM-LEN, W, ADDR-DISP,
MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, MISC-GROUP,
UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER,
UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LISTP, D2-7A2-5P,
D4-7A2-5P, and MOVEM-SAVED, to:
T.
Q.E.D.
[ 0.0 0.8 0.0 ]
BSEARCH1-S0-SN-RFILE-BASE2
(PROVE-LEMMA BSEARCH-S0-S0-1
(REWRITE)
(LET ((K (QUOTIENT (PLUS I J) 2)))
(IMPLIES (AND (BSEARCH-S0P S X A N LST I J)
(LESSP I J)
(ILESSP X (GET-NTH K LST)))
(AND (BSEARCH-S0P (STEPN S 10)
X A N LST I K)
(EQUAL (READ-RN OPLEN 14
(MC-RFILE (STEPN S 10)))
(READ-RN OPLEN 14 (MC-RFILE S)))
(EQUAL (LINKED-A6 (STEPN S 10))
(LINKED-A6 S))
(EQUAL (LINKED-RTS-ADDR (STEPN S 10))
(LINKED-RTS-ADDR S))
(EQUAL (MOVEM-SAVED (STEPN S 10) 4 8 2)
(MOVEM-SAVED S 4 8 2))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 10)) L)
(READ-MEM X (MC-MEM S) L))))))
WARNING: Note that the rewrite rule BSEARCH-S0-S0-1 will be stored so as to
apply only to terms with the nonrecursive function symbol BSEARCH-S0P.
WARNING: Note that BSEARCH-S0-S0-1 contains the free variables J, I, LST, N,
A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the rewrite rule BSEARCH-S0-S0-1 will be stored so as to
apply only to terms with the nonrecursive function symbol LINKED-A6.
WARNING: Note that BSEARCH-S0-S0-1 contains the free variables J, I, LST, N,
A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the rewrite rule BSEARCH-S0-S0-1 will be stored so as to
apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR.
WARNING: Note that BSEARCH-S0-S0-1 contains the free variables J, I, LST, N,
A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the rewrite rule BSEARCH-S0-S0-1 will be stored so as to
apply only to terms with the nonrecursive function symbol MOVEM-SAVED.
WARNING: Note that BSEARCH-S0-S0-1 contains the free variables J, I, LST, N,
A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-S0-1 contains the free variables J, I, LST, N,
and A which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the proposed lemma BSEARCH-S0-S0-1 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and six replacement rules.
This conjecture can be simplified, using the abbreviations READ-DN, READ-AN,
BSEARCH-CODE, BSEARCH-S0P, AND, and IMPLIES, to:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
70)
(MCODE-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-RN 32 (PLUS 8 0) (MC-RFILE S)))
(EQUAL I
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(EQUAL J
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(EQUAL X
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32))
(INT-RANGEP (TIMES 2 J) 32)
(NUMBERP I)
(NUMBERP J)
(NUMBERP N)
(NOT (LESSP N I))
(NOT (LESSP N J))
(LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(AND (BSEARCH-S0P (STEPN S 10)
X A N LST I
(QUOTIENT (PLUS I J) 2))
(EQUAL (READ-RN OPLEN 14
(MC-RFILE (STEPN S 10)))
(READ-RN OPLEN 14 (MC-RFILE S)))
(EQUAL (LINKED-A6 (STEPN S 10))
(LINKED-A6 S))
(EQUAL (LINKED-RTS-ADDR (STEPN S 10))
(LINKED-RTS-ADDR S))
(EQUAL (MOVEM-SAVED (STEPN S 10) 4 8 2)
(MOVEM-SAVED S 4 8 2))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 10)) L)
(READ-MEM X (MC-MEM S) L)))).
This simplifies, using linear arithmetic, applying SUB-NEG, CDR-CONS, CAR-CONS,
MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE,
MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE2,
PC-READ-MEMP-ROM2, BLE-BGT, SUB-BGT, ILESSP-LESSP, READ-RN-NAT-RANGEP,
SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP, SET-CVZNX-V, BITP-FIX-BIT,
SUB-V-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3,
PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, READ-WRITE-RN,
HEAD-READ-RN, WRITE-WRITE-RN, ADD-BMI, BSEARCH-CROCK, IPLUS-COMMUTATIVITY,
ADD-N-BITP, HEAD-LEMMA, READ-MEMP-RAM1-ASL, ADD-INT, ASR-INT, QUOTIENT-TIMES,
MEAN-BOUNDS, ASR-NAT-RANGEP, ADD-0, ASR-C-BITP, SUB-BGE, READ-MEM-ILST-ASL,
READ-MEM-NAT-RANGEP, MC-PC-RANGEP, STEPN-REWRITER0, STEPN-REWRITER,
ABS-LESSP-INT-RANGEP, DISJOINT-6-UINT, RAM-ADDRP-LA2, INDEX-N-X-X, PLUS-0,
PLUS-COMMUTATIVITY, RAM-ADDRP-3, ROM-ADDRP-LA2, and INDEX-N-DEDUCTION2, and
opening up the functions NEG, PLUS, EXECUTE-INS, OPCODE-FIELD, EQUAL, OP-LEN,
CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE,
MC-INSTATE, MC-HALTP, READ-DN, CDR, OPERAND, D_RN, CMP-CVZNX, UPDATE-CCR, Q,
B0P, BITN, CMP-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP,
PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR,
B-NOT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, MOVE-INS,
MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, MOVE-MAPPING,
D_MODE, MOVE-GROUP, OPMODE-FIELD, ADD-INS1, ADD-ADDR-MODEP1, NUMBERP,
ADD-CVZNX, ADD-EFFECT, ADD-GROUP, IPLUS, NEGP, REGISTER-SHIFT-ROTATE,
ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA, REGISTER-ASR-INS, S&R-GROUP, EXP,
IQUOTIENT, OP-SZ, ADDR-INDEX1, IR-SCALED, INDEX-RN, INDEX-REGISTER, BITS,
READ-AN, ADDR-INDEX-DISP, ADDR-INDEX, TIMES, ABS, BSEARCH-CODE, BSEARCH-S0P,
LINKED-A6, LINKED-RTS-ADDR, MOVEM-SAVED, and AND, to the conjecture:
(IMPLIES
(AND
(EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (ADD 32 (MC-PC S) 4294967274)
(MC-MEM S)
70)
(MCODE-ADDRP (ADD 32 (MC-PC S) 4294967274)
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0 12 66 129 36
46 0 16 180 129 111 32 32 1 208 130 106 2 82 128
226 128 182 176 12 0 108 4 36 0 96 232 182 176 12 0
111 8 34 0 82 129 96 220 112 255 76 238 0 12 255
248 78 94 78 117))
(RAM-ADDRP (ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
28)
(RAM-ADDRP (READ-RN 32 8 (MC-RFILE S))
(MC-MEM S)
(TIMES 4 N))
(MEM-ILST 4
(READ-RN 32 8 (MC-RFILE S))
(MC-MEM S)
N LST)
(DISJOINT (ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
28
(READ-RN 32 8 (MC-RFILE S))
(TIMES 4 N))
(INT-RANGEP (TIMES 2
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
32)
(NUMBERP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(NUMBERP (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(NUMBERP N)
(NOT (LESSP N
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)))
(NOT (LESSP N
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32)))
(LESSP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(ILESSP
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32)
(GET-NTH (QUOTIENT (PLUS (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
2)
LST)))
(NOT (LESSP N
(QUOTIENT (PLUS (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
2)))).
But this again simplifies, using linear arithmetic and applying MEAN-BOUNDS,
to:
T.
Q.E.D.
[ 0.0 2.5 0.0 ]
BSEARCH-S0-S0-1
(PROVE-LEMMA BSEARCH-S0-S0-RFILE1
(REWRITE)
(LET ((K (QUOTIENT (PLUS I J) 2)))
(IMPLIES (AND (BSEARCH-S0P S X A N LST I J)
(LESSP I J)
(ILESSP X (GET-NTH K LST))
(D4-7A2-5P RN))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 10)))
(READ-RN OPLEN RN (MC-RFILE S))))))
WARNING: Note that BSEARCH-S0-S0-RFILE1 contains the free variables J, I, LST,
N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
This formula can be simplified, using the abbreviations D2-7A2-5P, D4-7A2-5P,
READ-DN, READ-AN, BSEARCH-CODE, BSEARCH-S0P, AND, and IMPLIES, to:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
70)
(MCODE-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-RN 32 (PLUS 8 0) (MC-RFILE S)))
(EQUAL I
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(EQUAL J
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(EQUAL X
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32))
(INT-RANGEP (TIMES 2 J) 32)
(NUMBERP I)
(NUMBERP J)
(NUMBERP N)
(NOT (LESSP N I))
(NOT (LESSP N J))
(LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (EQUAL RN 2))
(NOT (EQUAL RN 3)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 10)))
(READ-RN OPLEN RN (MC-RFILE S)))),
which simplifies, using linear arithmetic, rewriting with SUB-NEG, CDR-CONS,
CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE,
MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE2,
PC-READ-MEMP-ROM2, BLE-BGT, SUB-BGT, ILESSP-LESSP, READ-RN-NAT-RANGEP,
SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP, SET-CVZNX-V, BITP-FIX-BIT,
SUB-V-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3,
PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, READ-WRITE-RN,
HEAD-READ-RN, WRITE-WRITE-RN, ADD-BMI, BSEARCH-CROCK, IPLUS-COMMUTATIVITY,
ADD-N-BITP, HEAD-LEMMA, READ-MEMP-RAM1-ASL, ADD-INT, ASR-INT, QUOTIENT-TIMES,
MEAN-BOUNDS, ASR-NAT-RANGEP, ADD-0, ASR-C-BITP, SUB-BGE, READ-MEM-ILST-ASL,
READ-MEM-NAT-RANGEP, MC-PC-RANGEP, STEPN-REWRITER0, and STEPN-REWRITER, and
unfolding the functions NEG, PLUS, EXECUTE-INS, OPCODE-FIELD, EQUAL, OP-LEN,
CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE,
MC-INSTATE, MC-HALTP, READ-DN, CDR, OPERAND, D_RN, CMP-CVZNX, UPDATE-CCR, Q,
B0P, BITN, CMP-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP,
PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR,
B-NOT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, MOVE-INS,
MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, MOVE-MAPPING,
D_MODE, MOVE-GROUP, OPMODE-FIELD, ADD-INS1, ADD-ADDR-MODEP1, NUMBERP,
ADD-CVZNX, ADD-EFFECT, ADD-GROUP, IPLUS, NEGP, REGISTER-SHIFT-ROTATE,
ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA, REGISTER-ASR-INS, S&R-GROUP, EXP,
IQUOTIENT, OP-SZ, ADDR-INDEX1, IR-SCALED, INDEX-RN, INDEX-REGISTER, BITS,
READ-AN, ADDR-INDEX-DISP, ADDR-INDEX, and TIMES, to:
T.
Q.E.D.
[ 0.0 0.6 0.0 ]
BSEARCH-S0-S0-RFILE1
(PROVE-LEMMA BSEARCH-S0-S0-2
(REWRITE)
(LET ((K (QUOTIENT (PLUS I J) 2)))
(IMPLIES (AND (BSEARCH-S0P S X A N LST I J)
(LESSP I J)
(NOT (ILESSP X (GET-NTH K LST)))
(ILESSP (GET-NTH K LST) X))
(AND (BSEARCH-S0P (STEPN S 13)
X A N LST
(ADD1 K)
J)
(EQUAL (READ-RN OPLEN 14
(MC-RFILE (STEPN S 13)))
(READ-RN OPLEN 14 (MC-RFILE S)))
(EQUAL (LINKED-A6 (STEPN S 13))
(LINKED-A6 S))
(EQUAL (LINKED-RTS-ADDR (STEPN S 13))
(LINKED-RTS-ADDR S))
(EQUAL (MOVEM-SAVED (STEPN S 13) 4 8 2)
(MOVEM-SAVED S 4 8 2))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 13)) L)
(READ-MEM X (MC-MEM S) L))))))
WARNING: Note that the rewrite rule BSEARCH-S0-S0-2 will be stored so as to
apply only to terms with the nonrecursive function symbol BSEARCH-S0P.
WARNING: Note that BSEARCH-S0-S0-2 contains the free variables J, I, LST, N,
A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the rewrite rule BSEARCH-S0-S0-2 will be stored so as to
apply only to terms with the nonrecursive function symbol LINKED-A6.
WARNING: Note that BSEARCH-S0-S0-2 contains the free variables J, I, LST, N,
A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the rewrite rule BSEARCH-S0-S0-2 will be stored so as to
apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR.
WARNING: Note that BSEARCH-S0-S0-2 contains the free variables J, I, LST, N,
A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the rewrite rule BSEARCH-S0-S0-2 will be stored so as to
apply only to terms with the nonrecursive function symbol MOVEM-SAVED.
WARNING: Note that BSEARCH-S0-S0-2 contains the free variables J, I, LST, N,
A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-S0-2 contains the free variables J, I, LST, N,
and A which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
WARNING: Note that the proposed lemma BSEARCH-S0-S0-2 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and six replacement rules.
This formula can be simplified, using the abbreviations NOT, READ-DN, READ-AN,
BSEARCH-CODE, BSEARCH-S0P, AND, and IMPLIES, to:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
70)
(MCODE-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-RN 32 (PLUS 8 0) (MC-RFILE S)))
(EQUAL I
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(EQUAL J
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(EQUAL X
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32))
(INT-RANGEP (TIMES 2 J) 32)
(NUMBERP I)
(NUMBERP J)
(NUMBERP N)
(NOT (LESSP N I))
(NOT (LESSP N J))
(LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X))
(AND (BSEARCH-S0P (STEPN S 13)
X A N LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)
(EQUAL (READ-RN OPLEN 14
(MC-RFILE (STEPN S 13)))
(READ-RN OPLEN 14 (MC-RFILE S)))
(EQUAL (LINKED-A6 (STEPN S 13))
(LINKED-A6 S))
(EQUAL (LINKED-RTS-ADDR (STEPN S 13))
(LINKED-RTS-ADDR S))
(EQUAL (MOVEM-SAVED (STEPN S 13) 4 8 2)
(MOVEM-SAVED S 4 8 2))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 13)) L)
(READ-MEM X (MC-MEM S) L)))),
which simplifies, using linear arithmetic, applying SUB-NEG,
ILESSP-ENTAILS-ILEQ, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE,
MC-CCR-RANGEP, MC-CCR-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP,
PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, BLE-BGT, SUB-BGT, ILESSP-LESSP,
READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP,
SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY,
PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X,
READ-WRITE-RN, HEAD-READ-RN, WRITE-WRITE-RN, ADD-BMI, BSEARCH-CROCK,
IPLUS-COMMUTATIVITY, ADD-N-BITP, HEAD-LEMMA, READ-MEMP-RAM1-ASL, ADD-INT,
ASR-INT, QUOTIENT-TIMES, MEAN-BOUNDS, ASR-NAT-RANGEP, ADD-0, ASR-C-BITP,
SUB-BGE, READ-MEM-ILST-ASL, READ-MEM-NAT-RANGEP, MC-PC-RANGEP, STEPN-REWRITER0,
STEPN-REWRITER, SUB1-ADD1, ABS-LESSP-INT-RANGEP, PLUS-ADD1, DISJOINT-6-UINT,
RAM-ADDRP-LA2, INDEX-N-X-X, PLUS-0, PLUS-COMMUTATIVITY, RAM-ADDRP-3,
ROM-ADDRP-LA2, and INDEX-N-DEDUCTION2, and opening up the definitions of NEG,
PLUS, EXECUTE-INS, OPCODE-FIELD, EQUAL, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CAR,
EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, READ-DN, CDR,
OPERAND, D_RN, CMP-CVZNX, UPDATE-CCR, Q, B0P, BITN, CMP-GROUP, UPDATE-PC, L,
CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ,
LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, EXT, COND-FIELD,
BCC-GROUP, ADD, EVENP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, D-MAPPING,
MOVE-EFFECT, B0, MOVE-CVZNX, MOVE-MAPPING, D_MODE, MOVE-GROUP, OPMODE-FIELD,
ADD-INS1, ADD-ADDR-MODEP1, NUMBERP, ADD-CVZNX, ADD-EFFECT, ADD-GROUP, IPLUS,
NEGP, REGISTER-SHIFT-ROTATE, ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA,
REGISTER-ASR-INS, S&R-GROUP, EXP, IQUOTIENT, OP-SZ, ADDR-INDEX1, IR-SCALED,
INDEX-RN, INDEX-REGISTER, BITS, READ-AN, ADDR-INDEX-DISP, ADDR-INDEX, TIMES,
ADDQ-INS, ADDQ-ADDR-MODEP, AN-DIRECT-MODEP, ADD-MAPPING, SCC-GROUP, ABS,
NAT-TO-INT, NAT-RANGEP, BSEARCH-CODE, BSEARCH-S0P, LINKED-A6, LINKED-RTS-ADDR,
MOVEM-SAVED, and AND, to the following two new goals:
Case 2. (IMPLIES
(AND
(EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (ADD 32 (MC-PC S) 4294967274)
(MC-MEM S)
70)
(MCODE-ADDRP (ADD 32 (MC-PC S) 4294967274)
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0 12 66 129
36 46 0 16 180 129 111 32 32 1 208 130 106 2 82
128 226 128 182 176 12 0 108 4 36 0 96 232 182
176 12 0 111 8 34 0 82 129 96 220 112 255 76 238
0 12 255 248 78 94 78 117))
(RAM-ADDRP (ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
28)
(RAM-ADDRP (READ-RN 32 8 (MC-RFILE S))
(MC-MEM S)
(TIMES 4 N))
(MEM-ILST 4
(READ-RN 32 8 (MC-RFILE S))
(MC-MEM S)
N LST)
(DISJOINT (ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
28
(READ-RN 32 8 (MC-RFILE S))
(TIMES 4 N))
(INT-RANGEP (TIMES 2
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
32)
(NUMBERP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(NUMBERP (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(NUMBERP N)
(NOT (LESSP N
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)))
(NOT (LESSP N
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32)))
(LESSP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(ILESSP
(GET-NTH (QUOTIENT (PLUS (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
2)
LST)
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32)))
(NOT (EQUAL N 0))).
But this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES
(AND
(EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (ADD 32 (MC-PC S) 4294967274)
(MC-MEM S)
70)
(MCODE-ADDRP (ADD 32 (MC-PC S) 4294967274)
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0 12 66 129
36 46 0 16 180 129 111 32 32 1 208 130 106 2 82
128 226 128 182 176 12 0 108 4 36 0 96 232 182
176 12 0 111 8 34 0 82 129 96 220 112 255 76 238
0 12 255 248 78 94 78 117))
(RAM-ADDRP (ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
28)
(RAM-ADDRP (READ-RN 32 8 (MC-RFILE S))
(MC-MEM S)
(TIMES 4 N))
(MEM-ILST 4
(READ-RN 32 8 (MC-RFILE S))
(MC-MEM S)
N LST)
(DISJOINT (ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
28
(READ-RN 32 8 (MC-RFILE S))
(TIMES 4 N))
(INT-RANGEP (TIMES 2
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
32)
(NUMBERP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(NUMBERP (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(NUMBERP N)
(NOT (LESSP N
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)))
(NOT (LESSP N
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32)))
(LESSP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(ILESSP
(GET-NTH (QUOTIENT (PLUS (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
2)
LST)
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32)))
(NOT (LESSP (SUB1 N)
(QUOTIENT (PLUS (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32)
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
2)))),
which again simplifies, using linear arithmetic and rewriting with the lemma
MEAN-BOUNDS, to:
T.
Q.E.D.
[ 0.0 4.4 0.0 ]
BSEARCH-S0-S0-2
(PROVE-LEMMA BSEARCH1-S0-S0-RFILE2
(REWRITE)
(LET ((K (QUOTIENT (PLUS I J) 2)))
(IMPLIES (AND (BSEARCH-S0P S X A N LST I J)
(LESSP I J)
(NOT (ILESSP X (GET-NTH K LST)))
(ILESSP (GET-NTH K LST) X)
(D4-7A2-5P RN))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 13)))
(READ-RN OPLEN RN (MC-RFILE S))))))
WARNING: Note that BSEARCH1-S0-S0-RFILE2 contains the free variables J, I,
LST, N, A, and X which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
This conjecture can be simplified, using the abbreviations D2-7A2-5P,
D4-7A2-5P, NOT, READ-DN, READ-AN, BSEARCH-CODE, BSEARCH-S0P, AND, and IMPLIES,
to:
(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING)
(EVENP (MC-PC S))
(ROM-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
70)
(MCODE-ADDRP (SUB 32 22 (MC-PC S))
(MC-MEM S)
'(78 86 0 0 72 231 48 0 38 46 0 8 32 110 0
12 66 129 36 46 0 16 180 129 111 32 32
1 208 130 106 2 82 128 226 128 182 176
12 0 108 4 36 0 96 232 182 176 12 0 111
8 34 0 82 129 96 220 112 255 76 238 0
12 255 248 78 94 78 117))
(RAM-ADDRP (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
(MC-MEM S)
28)
(RAM-ADDRP A (MC-MEM S) (TIMES 4 N))
(MEM-ILST 4 A (MC-MEM S) N LST)
(DISJOINT (SUB 32 8
(READ-RN 32 (PLUS 8 6) (MC-RFILE S)))
28 A
(TIMES 4 N))
(EQUAL A
(READ-RN 32 (PLUS 8 0) (MC-RFILE S)))
(EQUAL I
(NAT-TO-INT (READ-RN 32 1 (MC-RFILE S))
32))
(EQUAL J
(NAT-TO-INT (READ-RN 32 2 (MC-RFILE S))
32))
(EQUAL X
(NAT-TO-INT (READ-RN 32 3 (MC-RFILE S))
32))
(INT-RANGEP (TIMES 2 J) 32)
(NUMBERP I)
(NUMBERP J)
(NUMBERP N)
(NOT (LESSP N I))
(NOT (LESSP N J))
(LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (EQUAL RN 2))
(NOT (EQUAL RN 3)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 13)))
(READ-RN OPLEN RN (MC-RFILE S)))).
This simplifies, using linear arithmetic, rewriting with SUB-NEG,
ILESSP-ENTAILS-ILEQ, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE,
MC-CCR-RANGEP, MC-CCR-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP,
PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, BLE-BGT, SUB-BGT, ILESSP-LESSP,
READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP,
SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY,
PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X,
READ-WRITE-RN, HEAD-READ-RN, WRITE-WRITE-RN, ADD-BMI, BSEARCH-CROCK,
IPLUS-COMMUTATIVITY, ADD-N-BITP, HEAD-LEMMA, READ-MEMP-RAM1-ASL, ADD-INT,
ASR-INT, QUOTIENT-TIMES, MEAN-BOUNDS, ASR-NAT-RANGEP, ADD-0, ASR-C-BITP,
SUB-BGE, READ-MEM-ILST-ASL, READ-MEM-NAT-RANGEP, MC-PC-RANGEP, STEPN-REWRITER0,
and STEPN-REWRITER, and opening up the definitions of NEG, PLUS, EXECUTE-INS,
OPCODE-FIELD, EQUAL, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS,
DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, READ-DN, CDR, OPERAND, D_RN,
CMP-CVZNX, UPDATE-CCR, Q, B0P, BITN, CMP-GROUP, UPDATE-PC, L, CURRENT-INS,
READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N,
STEPI, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD,
EVENP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, B0,
MOVE-CVZNX, MOVE-MAPPING, D_MODE, MOVE-GROUP, OPMODE-FIELD, ADD-INS1,
ADD-ADDR-MODEP1, NUMBERP, ADD-CVZNX, ADD-EFFECT, ADD-GROUP, IPLUS, NEGP,
REGISTER-SHIFT-ROTATE, ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA,
REGISTER-ASR-INS, S&R-GROUP, EXP, IQUOTIENT, OP-SZ, ADDR-INDEX1, IR-SCALED,
INDEX-RN, INDEX-REGISTER, BITS, READ-AN, ADDR-INDEX-DISP, ADDR-INDEX, TIMES,
ADDQ-INS, ADDQ-ADDR-MODEP, AN-DIRECT-MODEP, ADD-MAPPING, and SCC-GROUP, to:
T.
Q.E.D.
[ 0.0 0.8 0.0 ]
BSEARCH1-S0-S0-RFILE2
(DISABLE BSEARCH-STATEP)
[ 0.0 0.0 0.0 ]
BSEARCH-STATEP-OFF
(DISABLE BSEARCH-S0P)
[ 0.0 0.0 0.0 ]
BSEARCH-S0P-OFF
(PROVE-LEMMA BSEARCH-S0-SN
(REWRITE)
(LET ((SN (STEPN S (BSEARCH1-T X LST I J))))
(IMPLIES (BSEARCH-S0P S X A N LST I J)
(AND (EQUAL (MC-STATUS SN) 'RUNNING)
(EQUAL (MC-PC SN) (LINKED-RTS-ADDR S))
(EQUAL (IREAD-DN 32 0 SN)
(BSEARCH1 X LST I J))
(EQUAL (READ-RN 32 14 (MC-RFILE SN))
(LINKED-A6 S))
(EQUAL (READ-RN 32 15 (MC-RFILE SN))
(ADD 32 (READ-AN 32 6 S) 8))
(EQUAL (READ-MEM X (MC-MEM SN) K)
(READ-MEM X (MC-MEM S) K)))))
((INDUCT (BSEARCH-INDUCT S X LST I J))
(DISABLE LINKED-RTS-ADDR LINKED-A6)))
WARNING: Note that BSEARCH-S0-SN contains the free variables N and A which
will be chosen by instantiating the hypothesis (BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN contains the free variables N and A which
will be chosen by instantiating the hypothesis (BSEARCH-S0P S X A N LST I J).
WARNING: Note that the rewrite rule BSEARCH-S0-SN will be stored so as to
apply only to terms with the nonrecursive function symbol IREAD-DN.
WARNING: Note that BSEARCH-S0-SN contains the free variables N and A which
will be chosen by instantiating the hypothesis (BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN contains the free variables N and A which
will be chosen by instantiating the hypothesis (BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN contains the free variables N and A which
will be chosen by instantiating the hypothesis (BSEARCH-S0P S X A N LST I J).
WARNING: Note that BSEARCH-S0-SN contains the free variables N and A which
will be chosen by instantiating the hypothesis (BSEARCH-S0P S X A N LST I J).
WARNING: Note that the proposed lemma BSEARCH-S0-SN is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and six replacement rules.
This conjecture can be simplified, using the abbreviations IMPLIES, NOT, OR,
AND, and READ-AN, to four new formulas:
Case 4. (IMPLIES
(AND
(LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(IMPLIES
(BSEARCH-S0P (STEPN S 10)
X A N LST I
(QUOTIENT (PLUS I J) 2))
(AND
(EQUAL (MC-STATUS (STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2))))
'RUNNING)
(EQUAL (MC-PC (STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2))))
(LINKED-RTS-ADDR (STEPN S 10)))
(EQUAL (IREAD-DN 32 0
(STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2))))
(BSEARCH1 X LST I
(QUOTIENT (PLUS I J) 2)))
(EQUAL
(READ-RN 32 14
(MC-RFILE (STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))
(LINKED-A6 (STEPN S 10)))
(EQUAL
(READ-RN 32 15
(MC-RFILE (STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))
(ADD 32
(READ-RN 32
(PLUS 8 6)
(MC-RFILE (STEPN S 10)))
8))
(EQUAL
(READ-MEM X
(MC-MEM (STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2))))
K)
(READ-MEM X
(MC-MEM (STEPN S 10))
K))))
(BSEARCH-S0P S X A N LST I J))
(AND (EQUAL (MC-STATUS (STEPN S (BSEARCH1-T X LST I J)))
'RUNNING)
(EQUAL (MC-PC (STEPN S (BSEARCH1-T X LST I J)))
(LINKED-RTS-ADDR S))
(EQUAL (IREAD-DN 32 0
(STEPN S (BSEARCH1-T X LST I J)))
(BSEARCH1 X LST I J))
(EQUAL (READ-RN 32 14
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(LINKED-A6 S))
(EQUAL (READ-RN 32 15
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(ADD 32
(READ-RN 32 (PLUS 8 6) (MC-RFILE S))
8))
(EQUAL (READ-MEM X
(MC-MEM (STEPN S (BSEARCH1-T X LST I J)))
K)
(READ-MEM X (MC-MEM S) K)))),
which simplifies, rewriting with the lemmas BSEARCH-S0-S0-1 and STEPN-LEMMA,
and expanding the definitions of READ-DN, IREAD-DN, PLUS, AND, IMPLIES,
BSEARCH1-T, EQUAL, and BSEARCH1, to:
T.
Case 3. (IMPLIES
(AND
(LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(IMPLIES
(BSEARCH-S0P (STEPN S 13)
X A N LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)
(AND
(EQUAL (MC-STATUS (STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
'RUNNING)
(EQUAL (MC-PC (STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
(LINKED-RTS-ADDR (STEPN S 13)))
(EQUAL (IREAD-DN 32 0
(STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
(BSEARCH1 X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))
(EQUAL
(READ-RN 32 14
(MC-RFILE (STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))
(LINKED-A6 (STEPN S 13)))
(EQUAL
(READ-RN 32 15
(MC-RFILE (STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))
(ADD 32
(READ-RN 32
(PLUS 8 6)
(MC-RFILE (STEPN S 13)))
8))
(EQUAL
(READ-MEM X
(MC-MEM (STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
K)
(READ-MEM X
(MC-MEM (STEPN S 13))
K))))
(BSEARCH-S0P S X A N LST I J))
(AND (EQUAL (MC-STATUS (STEPN S (BSEARCH1-T X LST I J)))
'RUNNING)
(EQUAL (MC-PC (STEPN S (BSEARCH1-T X LST I J)))
(LINKED-RTS-ADDR S))
(EQUAL (IREAD-DN 32 0
(STEPN S (BSEARCH1-T X LST I J)))
(BSEARCH1 X LST I J))
(EQUAL (READ-RN 32 14
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(LINKED-A6 S))
(EQUAL (READ-RN 32 15
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(ADD 32
(READ-RN 32 (PLUS 8 6) (MC-RFILE S))
8))
(EQUAL (READ-MEM X
(MC-MEM (STEPN S (BSEARCH1-T X LST I J)))
K)
(READ-MEM X (MC-MEM S) K)))),
which simplifies, applying the lemmas ILESSP-ENTAILS-ILEQ, BSEARCH-S0-S0-2,
and STEPN-LEMMA, and opening up the functions READ-DN, IREAD-DN, PLUS, AND,
IMPLIES, BSEARCH1-T, EQUAL, and BSEARCH1, to:
T.
Case 2. (IMPLIES
(AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(NOT (ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X))
(BSEARCH-S0P S X A N LST I J))
(AND (EQUAL (MC-STATUS (STEPN S (BSEARCH1-T X LST I J)))
'RUNNING)
(EQUAL (MC-PC (STEPN S (BSEARCH1-T X LST I J)))
(LINKED-RTS-ADDR S))
(EQUAL (IREAD-DN 32 0
(STEPN S (BSEARCH1-T X LST I J)))
(BSEARCH1 X LST I J))
(EQUAL (READ-RN 32 14
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(LINKED-A6 S))
(EQUAL (READ-RN 32 15
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(ADD 32
(READ-RN 32 (PLUS 8 6) (MC-RFILE S))
8))
(EQUAL (READ-MEM X
(MC-MEM (STEPN S (BSEARCH1-T X LST I J)))
K)
(READ-MEM X (MC-MEM S) K)))),
which simplifies, rewriting with BSEARCH-S0-SN-BASE2, and opening up
BSEARCH1-T, EQUAL, BSEARCH1, PLUS, READ-AN, and AND, to:
T.
Case 1. (IMPLIES
(AND (NOT (LESSP I J))
(BSEARCH-S0P S X A N LST I J))
(AND (EQUAL (MC-STATUS (STEPN S (BSEARCH1-T X LST I J)))
'RUNNING)
(EQUAL (MC-PC (STEPN S (BSEARCH1-T X LST I J)))
(LINKED-RTS-ADDR S))
(EQUAL (IREAD-DN 32 0
(STEPN S (BSEARCH1-T X LST I J)))
(BSEARCH1 X LST I J))
(EQUAL (READ-RN 32 14
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(LINKED-A6 S))
(EQUAL (READ-RN 32 15
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(ADD 32
(READ-RN 32 (PLUS 8 6) (MC-RFILE S))
8))
(EQUAL (READ-MEM X
(MC-MEM (STEPN S (BSEARCH1-T X LST I J)))
K)
(READ-MEM X (MC-MEM S) K)))).
This simplifies, applying BSEARCH-S0-SN-BASE1, and expanding BSEARCH1-T,
EQUAL, BSEARCH1, PLUS, READ-AN, and AND, to:
T.
Q.E.D.
[ 0.0 0.5 0.0 ]
BSEARCH-S0-SN
(PROVE-LEMMA BSEARCH-S0-SN-RFILE
(REWRITE)
(IMPLIES (AND (BSEARCH-S0P S X A N LST I J)
(D2-7A2-5P RN)
(LEQ OPLEN 32))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN (MC-RFILE S))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED S 4 8 2)))))
((INDUCT (BSEARCH-INDUCT S X LST I J))))
WARNING: Note that BSEARCH-S0-SN-RFILE contains the free variables N and A
which will be chosen by instantiating the hypothesis:
(BSEARCH-S0P S X A N LST I J).
This conjecture can be simplified, using the abbreviations D2-7A2-5P, IMPLIES,
NOT, OR, and AND, to four new formulas:
Case 4. (IMPLIES
(AND
(LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(IMPLIES
(AND (BSEARCH-S0P (STEPN S 10)
X A N LST I
(QUOTIENT (PLUS I J) 2))
(D2-7A2-5P RN)
(IF (LESSP 32 OPLEN) F T))
(EQUAL
(READ-RN OPLEN RN
(MC-RFILE (STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN
(MC-RFILE (STEPN S 10)))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED (STEPN S 10) 4 8 2)))))
(BSEARCH-S0P S X A N LST I J)
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (LESSP 32 OPLEN)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN (MC-RFILE S))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED S 4 8 2))))),
which simplifies, applying the lemmas BSEARCH-S0-S0-1, SUB-NEG, STEPN-LEMMA,
and BSEARCH-S0-S0-RFILE1, and opening up D2-7A2-5P, AND, D4-7A2-5P, NEG,
READ-AN, PLUS, MOVEM-SAVED, IMPLIES, EQUAL, NUMBERP, and BSEARCH1-T, to two
new goals:
Case 4.2.
(IMPLIES
(AND
(LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(EQUAL RN 3)
(EQUAL
(READ-RN OPLEN RN
(MC-RFILE (STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))
(GET-VLST OPLEN 0 RN
'(2 3)
(READM-MEM 4
(ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
2)))
(BSEARCH-S0P S X A N LST I J)
(NOT (LESSP 32 OPLEN)))
(EQUAL
(READ-RN OPLEN 3
(MC-RFILE (STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))
(GET-VLST OPLEN 0 3
'(2 3)
(READM-MEM 4
(ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
2)))),
which again simplifies, obviously, to:
T.
Case 4.1.
(IMPLIES
(AND
(LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(EQUAL RN 2)
(EQUAL
(READ-RN OPLEN RN
(MC-RFILE (STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))
(GET-VLST OPLEN 0 RN
'(2 3)
(READM-MEM 4
(ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
2)))
(BSEARCH-S0P S X A N LST I J)
(NOT (LESSP 32 OPLEN)))
(EQUAL
(READ-RN OPLEN 2
(MC-RFILE (STEPN (STEPN S 10)
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))
(GET-VLST OPLEN 0 2
'(2 3)
(READM-MEM 4
(ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
2)))).
This again simplifies, obviously, to:
T.
Case 3. (IMPLIES
(AND
(LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(IMPLIES
(AND (BSEARCH-S0P (STEPN S 13)
X A N LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)
(D2-7A2-5P RN)
(IF (LESSP 32 OPLEN) F T))
(EQUAL
(READ-RN OPLEN RN
(MC-RFILE (STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN
(MC-RFILE (STEPN S 13)))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED (STEPN S 13) 4 8 2)))))
(BSEARCH-S0P S X A N LST I J)
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (LESSP 32 OPLEN)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN (MC-RFILE S))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED S 4 8 2))))).
This simplifies, applying ILESSP-ENTAILS-ILEQ, BSEARCH-S0-S0-2, SUB-NEG,
STEPN-LEMMA, and BSEARCH1-S0-S0-RFILE2, and expanding the functions
D2-7A2-5P, AND, D4-7A2-5P, NEG, READ-AN, PLUS, MOVEM-SAVED, IMPLIES, EQUAL,
NUMBERP, and BSEARCH1-T, to two new formulas:
Case 3.2.
(IMPLIES
(AND
(LESSP I J)
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(EQUAL RN 3)
(EQUAL
(READ-RN OPLEN RN
(MC-RFILE (STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))
(GET-VLST OPLEN 0 RN
'(2 3)
(READM-MEM 4
(ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
2)))
(BSEARCH-S0P S X A N LST I J)
(NOT (LESSP 32 OPLEN)))
(EQUAL
(READ-RN OPLEN 3
(MC-RFILE (STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))
(GET-VLST OPLEN 0 3
'(2 3)
(READM-MEM 4
(ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
2)))),
which again simplifies, obviously, to:
T.
Case 3.1.
(IMPLIES
(AND
(LESSP I J)
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(EQUAL RN 2)
(EQUAL
(READ-RN OPLEN RN
(MC-RFILE (STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))
(GET-VLST OPLEN 0 RN
'(2 3)
(READM-MEM 4
(ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
2)))
(BSEARCH-S0P S X A N LST I J)
(NOT (LESSP 32 OPLEN)))
(EQUAL
(READ-RN OPLEN 2
(MC-RFILE (STEPN (STEPN S 13)
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))
(GET-VLST OPLEN 0 2
'(2 3)
(READM-MEM 4
(ADD 32
(READ-RN 32 14 (MC-RFILE S))
4294967288)
(MC-MEM S)
2)))).
This again simplifies, trivially, to:
T.
Case 2. (IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(NOT (ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X))
(BSEARCH-S0P S X A N LST I J)
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (LESSP 32 OPLEN)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN (MC-RFILE S))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED S 4 8 2))))).
This simplifies, rewriting with SUB-NEG and BSEARCH1-S0-SN-RFILE-BASE2, and
opening up BSEARCH1-T, D2-7A2-5P, D4-7A2-5P, NEG, READ-AN, PLUS, and
MOVEM-SAVED, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP I J))
(BSEARCH-S0P S X A N LST I J)
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (LESSP 32 OPLEN)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S (BSEARCH1-T X LST I J))))
(IF (D4-7A2-5P RN)
(READ-RN OPLEN RN (MC-RFILE S))
(GET-VLST OPLEN 0 RN
'(2 3)
(MOVEM-SAVED S 4 8 2))))),
which simplifies, rewriting with the lemmas SUB-NEG and
BSEARCH-S0-SN-RFILE-BASE1, and opening up the definitions of BSEARCH1-T,
D2-7A2-5P, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
BSEARCH-S0-SN-RFILE
(PROVE-LEMMA BSEARCH-CORRECTNESS
(REWRITE)
(LET ((SN (STEPN S (BSEARCH-T X N LST))))
(IMPLIES (BSEARCH-STATEP S X A N LST)
(AND (EQUAL (MC-STATUS SN) 'RUNNING)
(EQUAL (MC-PC SN) (RTS-ADDR S))
(EQUAL (READ-RN 32 14 (MC-RFILE SN))
(READ-RN 32 14 (MC-RFILE S)))
(EQUAL (READ-RN 32 15 (MC-RFILE SN))
(ADD 32 (READ-SP S) 4))
(IMPLIES (AND (D2-7A2-5P RN) (LEQ OPLEN 32))
(EQUAL (READ-RN OPLEN RN (MC-RFILE SN))
(READ-RN OPLEN RN (MC-RFILE S))))
(IMPLIES (DISJOINT X K
(SUB 32 12 (READ-SP S))
28)
(EQUAL (READ-MEM X (MC-MEM SN) K)
(READ-MEM X (MC-MEM S) K)))
(EQUAL (IREAD-DN 32 0 SN)
(BSEARCH X N LST)))))
((USE (BSEARCH-S-S0P))
(DISABLE RTS-ADDR LINKED-RTS-ADDR LINKED-A6)))
WARNING: Note that BSEARCH-CORRECTNESS contains the free variable A which
will be chosen by instantiating the hypothesis (BSEARCH-STATEP S X A N LST).
WARNING: Note that BSEARCH-CORRECTNESS contains the free variable A which
will be chosen by instantiating the hypothesis (BSEARCH-STATEP S X A N LST).
WARNING: Note that BSEARCH-CORRECTNESS contains the free variable A which
will be chosen by instantiating the hypothesis (BSEARCH-STATEP S X A N LST).
WARNING: Note that BSEARCH-CORRECTNESS contains the free variable A which
will be chosen by instantiating the hypothesis (BSEARCH-STATEP S X A N LST).
WARNING: Note that BSEARCH-CORRECTNESS contains the free variable A which
will be chosen by instantiating the hypothesis (BSEARCH-STATEP S X A N LST).
WARNING: Note that BSEARCH-CORRECTNESS contains the free variable A which
will be chosen by instantiating the hypothesis (BSEARCH-STATEP S X A N LST).
WARNING: Note that the rewrite rule BSEARCH-CORRECTNESS will be stored so as
to apply only to terms with the nonrecursive function symbol IREAD-DN.
WARNING: Note that BSEARCH-CORRECTNESS contains the free variable A which
will be chosen by instantiating the hypothesis (BSEARCH-STATEP S X A N LST).
WARNING: Note that the proposed lemma BSEARCH-CORRECTNESS is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and seven replacement rules.
This conjecture can be simplified, using the abbreviations IMPLIES, BSEARCH,
SP, L, READ-AN, READ-SP, STEPN-LEMMA, and BSEARCH-T, to:
(IMPLIES
(AND (IMPLIES (BSEARCH-STATEP S X A N LST)
(BSEARCH-S0P (STEPN S 6)
X A N LST 0 N))
(BSEARCH-STATEP S X A N LST))
(AND (EQUAL (MC-STATUS (STEPN (STEPN S 6)
(BSEARCH1-T X LST 0 N)))
'RUNNING)
(EQUAL (MC-PC (STEPN (STEPN S 6)
(BSEARCH1-T X LST 0 N)))
(RTS-ADDR S))
(EQUAL (READ-RN 32 14
(MC-RFILE (STEPN (STEPN S 6)
(BSEARCH1-T X LST 0 N))))
(READ-RN 32 14 (MC-RFILE S)))
(EQUAL (READ-RN 32 15
(MC-RFILE (STEPN (STEPN S 6)
(BSEARCH1-T X LST 0 N))))
(ADD 32
(READ-RN 32 (PLUS 8 7) (MC-RFILE S))
4))
(IMPLIES (AND (D2-7A2-5P RN)
(IF (LESSP 32 OPLEN) F T))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN (STEPN S 6)
(BSEARCH1-T X LST 0 N))))
(READ-RN OPLEN RN (MC-RFILE S))))
(IMPLIES (DISJOINT X K
(SUB 32 12
(READ-RN 32 (PLUS 8 7) (MC-RFILE S)))
28)
(EQUAL (READ-MEM X
(MC-MEM (STEPN (STEPN S 6)
(BSEARCH1-T X LST 0 N)))
K)
(READ-MEM X (MC-MEM S) K)))
(EQUAL (IREAD-DN 32 0
(STEPN (STEPN S 6)
(BSEARCH1-T X LST 0 N)))
(BSEARCH1 X LST 0 N)))).
This simplifies, applying the lemmas BSEARCH-S0-SN, BSEARCH-S-S0, SUB-NEG, and
ADD-ASSOCIATIVITY, and expanding IMPLIES, EQUAL, PLUS, READ-AN, NEG, READ-SP,
L, SP, ADD, D2-7A2-5P, and AND, to the following two new conjectures:
Case 2. (IMPLIES (AND (BSEARCH-S0P (STEPN S 6)
X A N LST 0 N)
(BSEARCH-STATEP S X A N LST)
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (LESSP 32 OPLEN)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN (STEPN S 6)
(BSEARCH1-T X LST 0 N))))
(READ-RN OPLEN RN (MC-RFILE S)))).
But this again simplifies, applying BSEARCH-S-S0, GET-VLST-READM-RN, and
BSEARCH-S0-SN-RFILE, and expanding the functions D2-7A2-5P, D4-7A2-5P, CDR,
NUMBERP, CAR, LISTP, and N-MEMBER, to:
(IMPLIES (AND (BSEARCH-S0P (STEPN S 6)
X A N LST 0 N)
(BSEARCH-STATEP S X A N LST)
(NOT (EQUAL RN 0))
(NUMBERP RN)
(NOT (EQUAL RN 1))
(NOT (EQUAL RN 8))
(NOT (EQUAL RN 9))
(NOT (EQUAL RN 14))
(NOT (EQUAL RN 15))
(NOT (LESSP 32 OPLEN))
(NOT (EQUAL RN 2))
(NOT (EQUAL RN 3)))
(EQUAL (READ-RN OPLEN RN
(MC-RFILE (STEPN S 6)))
(READ-RN OPLEN RN (MC-RFILE S)))),
which again simplifies, applying BSEARCH-S-S0-RFILE, and opening up the
functions D4-7A2-5P and D2-7A2-5P, to:
T.
Case 1. (IMPLIES (AND (BSEARCH-S0P (STEPN S 6)
X A N LST 0 N)
(BSEARCH-STATEP S X A N LST)
(DISJOINT X K
(ADD 32
(READ-RN 32 15 (MC-RFILE S))
4294967284)
28))
(EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) K)
(READ-MEM X (MC-MEM S) K))).
However this again simplifies, using linear arithmetic, rewriting with the
lemmas DISJOINT-10, SUB-NEG, and BSEARCH-S-S0-MEM, and unfolding the
functions INDEX-N, LESSP, NEG, READ-SP, L, SP, PLUS, and READ-AN, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
BSEARCH-CORRECTNESS
(DISABLE BSEARCH-T)
[ 0.0 0.0 0.0 ]
BSEARCH-T-OFF
(DEFN MEMBER1
(X LST I J)
(IF (LESSP I J)
(IF (EQUAL X (GET-NTH I LST))
T
(MEMBER1 X LST (ADD1 I) J))
F)
((LESSP (DIFFERENCE J I))))
Linear arithmetic can be used to prove that the measure (DIFFERENCE J I)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, MEMBER1 is accepted under the principle of definition. Observe that:
(OR (FALSEP (MEMBER1 X LST I J))
(TRUEP (MEMBER1 X LST I J)))
is a theorem.
[ 0.0 0.0 0.0 ]
MEMBER1
(DEFN ORDEREDP
(LST)
(IF (NLISTP LST)
T
(IF (NLISTP (CDR LST))
T
(AND (ILEQ (CAR LST) (CADR LST))
(ORDEREDP (CDR LST))))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to show that the measure (COUNT LST)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, ORDEREDP is accepted under the definitional principle. Note that:
(OR (FALSEP (ORDEREDP LST))
(TRUEP (ORDEREDP LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
ORDEREDP
(PROVE-LEMMA LEQ-TRANS
(REWRITE)
(IMPLIES (AND (NOT (ILESSP X Y))
(NOT (ILESSP Y Z)))
(NOT (ILESSP X Z)))
((ENABLE ILESSP)))
WARNING: Note that LEQ-TRANS contains the free variable Y which will be
chosen by instantiating the hypothesis (NOT (ILESSP X Y)).
This simplifies, rewriting with ILESSP-ENTAILS-ILEQ, and opening up NEGP,
NEGATIVE-GUTS, ILESSP, LESSP, EQUAL, and NUMBERP, to nine new conjectures:
Case 9. (IMPLIES (AND (NEGATIVEP Y)
(NOT (EQUAL Y (MINUS 0)))
(NOT (LESSP (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS X)))
(NEGATIVEP Z)
(NOT (EQUAL Z (MINUS 0)))
(NOT (LESSP (NEGATIVE-GUTS Z)
(NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(NOT (EQUAL X (MINUS 0))))
(NOT (LESSP (NEGATIVE-GUTS Z)
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 8. (IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (LESSP X Y))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y Z))
(EQUAL Z (MINUS 0)))
(NOT (LESSP X Z))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (LESSP X Y))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y Z))
(NOT (NEGATIVEP Z)))
(NOT (LESSP X Z))),
which again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (LESSP X Y))
(EQUAL Y (MINUS 0))
(NOT (LESSP Y Z))
(EQUAL Z (MINUS 0)))
(NOT (LESSP X Z))),
which again simplifies, trivially, to:
T.
Case 5. (IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (LESSP X Y))
(EQUAL Y (MINUS 0))
(NOT (LESSP Y Z))
(NOT (NEGATIVEP Z)))
(NOT (LESSP X Z))).
However this again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (EQUAL X (MINUS 0))
(NOT (LESSP X Y))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y Z))
(EQUAL Z (MINUS 0))
(NOT (EQUAL Z 0)))
(NOT (NUMBERP Z))),
which again simplifies, clearly, to:
T.
Case 3. (IMPLIES (AND (EQUAL X (MINUS 0))
(NOT (LESSP X Y))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y Z))
(NOT (NEGATIVEP Z))
(NOT (EQUAL Z 0)))
(NOT (NUMBERP Z))).
However this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (EQUAL X (MINUS 0))
(NOT (LESSP X Y))
(EQUAL Y (MINUS 0))
(NOT (LESSP Y Z))
(EQUAL Z (MINUS 0))
(NOT (EQUAL Z 0)))
(NOT (NUMBERP Z))),
which again simplifies, trivially, to:
T.
Case 1. (IMPLIES (AND (EQUAL X (MINUS 0))
(NOT (LESSP X Y))
(EQUAL Y (MINUS 0))
(NOT (LESSP Y Z))
(NOT (NEGATIVEP Z))
(NOT (EQUAL Z 0)))
(NOT (NUMBERP Z))).
But this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
LEQ-TRANS
(PROVE-LEMMA INT-EQUAL
(REWRITE)
(IMPLIES (AND (INTEGERP X)
(INTEGERP Y)
(NOT (ILESSP X Y))
(NOT (ILESSP Y X)))
(EQUAL (EQUAL X Y) T))
((ENABLE ILESSP INTEGERP)))
This formula simplifies, rewriting with ILESSP-LESSP, and opening up the
functions NEGP, NEGATIVE-GUTS, INTEGERP, and ILESSP, to the following two new
goals:
Case 2. (IMPLIES (AND (NUMBERP X)
(NUMBERP Y)
(NOT (LESSP X Y))
(NOT (LESSP Y X)))
(EQUAL X Y)).
However this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NEGATIVEP X)
(NOT (EQUAL X (MINUS 0)))
(NEGATIVEP Y)
(NOT (EQUAL Y (MINUS 0)))
(NOT (LESSP (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS X)))
(NOT (LESSP (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))))
(EQUAL X Y)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS X))
(NEGATIVEP X)
(NOT (EQUAL X (MINUS 0)))
(NEGATIVEP Y)
(NOT (EQUAL Y (MINUS 0)))
(NOT (LESSP (NEGATIVE-GUTS X)
(NEGATIVE-GUTS X)))
(NOT (LESSP (NEGATIVE-GUTS X)
(NEGATIVE-GUTS X))))
(EQUAL X Y)).
But this again simplifies, applying NEGATIVEP-GUTS0, and expanding the
functions NEGATIVE-GUTS, INTEGERP, and NEGP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INT-EQUAL
(PROVE-LEMMA ORDEREDP-ORDERED
(REWRITE)
(IMPLIES (AND (ORDEREDP LST)
(LEQ I J)
(LESSP J (LEN LST)))
(EQUAL (ILESSP (GET-NTH J LST)
(GET-NTH I LST))
F))
((ENABLE GET-NTH)))
Name the conjecture *1.
We will appeal to induction. There are seven plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP LST) (p J LST I))
(IMPLIES (AND (NOT (NLISTP LST))
(NLISTP (CDR LST)))
(p J LST I))
(IMPLIES (AND (NOT (NLISTP LST))
(NOT (NLISTP (CDR LST)))
(p (SUB1 J) (CDR LST) (SUB1 I)))
(p J LST I))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT LST) decreases according to
the well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instances chosen for I and J. The above induction
scheme generates six new conjectures:
Case 6. (IMPLIES (AND (NLISTP LST)
(ORDEREDP LST)
(NOT (LESSP J I))
(LESSP J (LEN LST)))
(NOT (ILESSP (GET-NTH J LST)
(GET-NTH I LST)))),
which simplifies, opening up the functions NLISTP, ORDEREDP, LESSP, LEN, and
EQUAL, to:
T.
Case 5. (IMPLIES (AND (NOT (NLISTP LST))
(NLISTP (CDR LST))
(ORDEREDP LST)
(NOT (LESSP J I))
(LESSP J (LEN LST)))
(NOT (ILESSP (GET-NTH J LST)
(GET-NTH I LST)))),
which simplifies, applying the lemmas SUB1-ADD1 and ILESSP-REFLEX, and
unfolding the definitions of NLISTP, ORDEREDP, LESSP, LEN, EQUAL, and
GET-NTH, to nine new goals:
Case 5.9.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(EQUAL I 0)
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))),
which again simplifies, trivially, to:
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))),
which further simplifies, expanding the functions LEN, EQUAL, and LESSP,
to:
T.
Case 5.8.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(EQUAL I 0)
(LESSP (SUB1 J) (LEN (CDR LST)))
(EQUAL J 0))
(NOT (ILESSP (CAR LST) (CAR LST)))),
which again simplifies, rewriting with ILESSP-REFLEX, and unfolding the
functions SUB1, EQUAL, and LESSP, to:
T.
Case 5.7.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(EQUAL I 0)
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (NUMBERP J)))
(NOT (ILESSP (CAR LST) (CAR LST)))).
But this again simplifies, applying the lemma ILESSP-REFLEX, to:
T.
Case 5.6.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (NUMBERP I))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))),
which further simplifies, expanding the definitions of LEN, EQUAL, and
LESSP, to:
T.
Case 5.5.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (NUMBERP I))
(LESSP (SUB1 J) (LEN (CDR LST)))
(EQUAL J 0))
(NOT (ILESSP (CAR LST) (CAR LST)))),
which again simplifies, rewriting with ILESSP-REFLEX, and unfolding the
definitions of SUB1, EQUAL, and LESSP, to:
T.
Case 5.4.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (NUMBERP I))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (NUMBERP J)))
(NOT (ILESSP (CAR LST) (CAR LST)))).
However this again simplifies, appealing to the lemma ILESSP-REFLEX, to:
T.
Case 5.3.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (SUB1 J) (SUB1 I)))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (EQUAL I 0))
(NUMBERP I))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(GET-NTH (SUB1 I) (CDR LST))))),
which further simplifies, unfolding the functions LEN, EQUAL, and LESSP,
to:
T.
Case 5.2.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (SUB1 J) (SUB1 I)))
(LESSP (SUB1 J) (LEN (CDR LST)))
(EQUAL I 0))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))),
which again simplifies, opening up the definitions of SUB1, EQUAL, and
LESSP, to the formula:
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J)
(LESSP (SUB1 J) (LEN (CDR LST))))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))).
However this further simplifies, opening up LEN, EQUAL, and LESSP, to:
T.
Case 5.1.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (SUB1 J) (SUB1 I)))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (NUMBERP I)))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))),
which further simplifies, rewriting with the lemma SUB1-NNUMBERP, and
expanding the functions EQUAL, LESSP, and LEN, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP LST))
(NOT (NLISTP (CDR LST)))
(NOT (ORDEREDP (CDR LST)))
(ORDEREDP LST)
(NOT (LESSP J I))
(LESSP J (LEN LST)))
(NOT (ILESSP (GET-NTH J LST)
(GET-NTH I LST)))),
which simplifies, unfolding the definitions of NLISTP, ORDEREDP, and ILEQ,
to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP LST))
(NOT (NLISTP (CDR LST)))
(LESSP (SUB1 J) (SUB1 I))
(ORDEREDP LST)
(NOT (LESSP J I))
(LESSP J (LEN LST)))
(NOT (ILESSP (GET-NTH J LST)
(GET-NTH I LST)))),
which simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (LESSP I 1)
(NOT (NLISTP LST))
(NOT (NLISTP (CDR LST)))
(LESSP (SUB1 J) (SUB1 I))
(ORDEREDP LST)
(NOT (LESSP J I))
(LESSP J (LEN LST)))
(NOT (ILESSP (GET-NTH J LST)
(GET-NTH I LST)))).
However this again simplifies, applying LESSP-OF-1, SUB1-ADD1, and
ILESSP-REFLEX, and unfolding NLISTP, ORDEREDP, ILEQ, EQUAL, LESSP, LEN, and
GET-NTH, to the following six new goals:
Case 3.6.
(IMPLIES (AND (EQUAL I 0)
(LISTP LST)
(LISTP (CDR LST))
(LESSP (SUB1 J) (SUB1 I))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))).
However this again simplifies, expanding SUB1, EQUAL, and LESSP, to:
T.
Case 3.5.
(IMPLIES (AND (EQUAL I 0)
(LISTP LST)
(LISTP (CDR LST))
(LESSP (SUB1 J) (SUB1 I))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(LESSP (SUB1 J) (LEN (CDR LST)))
(EQUAL J 0))
(NOT (ILESSP (CAR LST) (CAR LST)))),
which again simplifies, opening up the definitions of SUB1 and LESSP, to:
T.
Case 3.4.
(IMPLIES (AND (EQUAL I 0)
(LISTP LST)
(LISTP (CDR LST))
(LESSP (SUB1 J) (SUB1 I))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (NUMBERP J)))
(NOT (ILESSP (CAR LST) (CAR LST)))),
which again simplifies, appealing to the lemma SUB1-NNUMBERP, and
expanding SUB1 and LESSP, to:
T.
Case 3.3.
(IMPLIES (AND (NOT (NUMBERP I))
(LISTP LST)
(LISTP (CDR LST))
(LESSP (SUB1 J) (SUB1 I))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))),
which further simplifies, rewriting with SUB1-NNUMBERP, and unfolding the
functions EQUAL and LESSP, to:
T.
Case 3.2.
(IMPLIES (AND (NOT (NUMBERP I))
(LISTP LST)
(LISTP (CDR LST))
(LESSP (SUB1 J) (SUB1 I))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(LESSP (SUB1 J) (LEN (CDR LST)))
(EQUAL J 0))
(NOT (ILESSP (CAR LST) (CAR LST)))).
But this again simplifies, appealing to the lemma SUB1-NNUMBERP, and
opening up the definitions of SUB1 and LESSP, to:
T.
Case 3.1.
(IMPLIES (AND (NOT (NUMBERP I))
(LISTP LST)
(LISTP (CDR LST))
(LESSP (SUB1 J) (SUB1 I))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (NUMBERP J)))
(NOT (ILESSP (CAR LST) (CAR LST)))),
which again simplifies, rewriting with the lemma ILESSP-REFLEX, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP LST))
(NOT (NLISTP (CDR LST)))
(NOT (LESSP (SUB1 J) (LEN (CDR LST))))
(ORDEREDP LST)
(NOT (LESSP J I))
(LESSP J (LEN LST)))
(NOT (ILESSP (GET-NTH J LST)
(GET-NTH I LST)))),
which simplifies, rewriting with the lemmas SUB1-ADD1 and ILESSP-REFLEX, and
expanding NLISTP, ORDEREDP, ILEQ, LESSP, LEN, EQUAL, and GET-NTH, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP LST))
(NOT (NLISTP (CDR LST)))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(GET-NTH (SUB1 I) (CDR LST))))
(ORDEREDP LST)
(NOT (LESSP J I))
(LESSP J (LEN LST)))
(NOT (ILESSP (GET-NTH J LST)
(GET-NTH I LST)))),
which simplifies, appealing to the lemmas SUB1-ADD1 and ILESSP-REFLEX, and
expanding the functions NLISTP, ORDEREDP, ILEQ, LESSP, LEN, EQUAL, and
GET-NTH, to eight new goals:
Case 1.8.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(GET-NTH (SUB1 I) (CDR LST))))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(EQUAL I 0)
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))),
which again simplifies, applying the lemma LEQ-TRANS, and unfolding the
functions SUB1, EQUAL, and GET-NTH, to:
T.
Case 1.7.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(GET-NTH (SUB1 I) (CDR LST))))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(EQUAL I 0)
(LESSP (SUB1 J) (LEN (CDR LST)))
(EQUAL J 0))
(NOT (ILESSP (CAR LST) (CAR LST)))),
which again simplifies, applying ILESSP-REFLEX, and expanding the
definitions of SUB1, EQUAL, GET-NTH, and LESSP, to:
T.
Case 1.6.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(GET-NTH (SUB1 I) (CDR LST))))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(EQUAL I 0)
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (NUMBERP J)))
(NOT (ILESSP (CAR LST) (CAR LST)))).
But this again simplifies, rewriting with ILESSP-REFLEX, and opening up
the definitions of SUB1, EQUAL, and GET-NTH, to:
T.
Case 1.5.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(GET-NTH (SUB1 I) (CDR LST))))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(NOT (NUMBERP I))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (EQUAL J 0))
(NUMBERP J))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))).
This further simplifies, rewriting with SUB1-NNUMBERP and LEQ-TRANS, and
unfolding the functions EQUAL and GET-NTH, to:
T.
Case 1.4.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(GET-NTH (SUB1 I) (CDR LST))))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(NOT (NUMBERP I))
(LESSP (SUB1 J) (LEN (CDR LST)))
(EQUAL J 0))
(NOT (ILESSP (CAR LST) (CAR LST)))).
However this again simplifies, rewriting with the lemma ILESSP-REFLEX, and
opening up the functions SUB1, EQUAL, GET-NTH, and LESSP, to:
T.
Case 1.3.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(GET-NTH (SUB1 I) (CDR LST))))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(NOT (NUMBERP I))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (NUMBERP J)))
(NOT (ILESSP (CAR LST) (CAR LST)))),
which again simplifies, applying the lemma ILESSP-REFLEX, to:
T.
Case 1.2.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(GET-NTH (SUB1 I) (CDR LST))))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (SUB1 J) (SUB1 I)))
(LESSP (SUB1 J) (LEN (CDR LST)))
(NOT (NUMBERP I)))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))),
which further simplifies, rewriting with SUB1-NNUMBERP and LEQ-TRANS, and
expanding the functions EQUAL, GET-NTH, and LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(GET-NTH (SUB1 I) (CDR LST))))
(NOT (ILESSP (CADR LST) (CAR LST)))
(ORDEREDP (CDR LST))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (SUB1 J) (SUB1 I)))
(LESSP (SUB1 J) (LEN (CDR LST)))
(EQUAL I 0))
(NOT (ILESSP (GET-NTH (SUB1 J) (CDR LST))
(CAR LST)))).
This again simplifies, rewriting with LEQ-TRANS, and expanding the
definitions of SUB1, EQUAL, GET-NTH, and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
ORDEREDP-ORDERED
(PROVE-LEMMA BSEARCH1-FOUND
(REWRITE)
(IMPLIES (AND (NOT (EQUAL (BSEARCH1 X LST I J) -1))
(LST-INTEGERP LST)
(INTEGERP X))
(EQUAL (GET-NTH (BSEARCH1 X LST I J) LST)
X))
((DISABLE QUOTIENT REMAINDER)))
Name the conjecture *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest two inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(p X LST I (QUOTIENT (PLUS I J) 2)))
(p X LST I J))
(IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(p X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))
(p X LST I J))
(IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(NOT (ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)))
(p X LST I J))
(IMPLIES (NOT (LESSP I J))
(p X LST I J))).
Linear arithmetic and the lemma MEAN-BOUNDS can be used to prove that the
measure (DIFFERENCE J I) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme leads
to the following six new goals:
Case 6. (IMPLIES (AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(EQUAL (BSEARCH1 X LST I
(QUOTIENT (PLUS I J) 2))
-1)
(NOT (EQUAL (BSEARCH1 X LST I J) -1))
(LST-INTEGERP LST)
(INTEGERP X))
(EQUAL (GET-NTH (BSEARCH1 X LST I J) LST)
X)).
This simplifies, expanding the functions BSEARCH1 and EQUAL, to:
T.
Case 5. (IMPLIES (AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(EQUAL (GET-NTH (BSEARCH1 X LST I
(QUOTIENT (PLUS I J) 2))
LST)
X)
(NOT (EQUAL (BSEARCH1 X LST I J) -1))
(LST-INTEGERP LST)
(INTEGERP X))
(EQUAL (GET-NTH (BSEARCH1 X LST I J) LST)
X)).
This simplifies, opening up BSEARCH1, to:
T.
Case 4. (IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(EQUAL (BSEARCH1 X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)
-1)
(NOT (EQUAL (BSEARCH1 X LST I J) -1))
(LST-INTEGERP LST)
(INTEGERP X))
(EQUAL (GET-NTH (BSEARCH1 X LST I J) LST)
X)).
This simplifies, applying ILESSP-ENTAILS-ILEQ, and unfolding the functions
BSEARCH1 and EQUAL, to:
T.
Case 3. (IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(EQUAL (GET-NTH (BSEARCH1 X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)
LST)
X)
(NOT (EQUAL (BSEARCH1 X LST I J) -1))
(LST-INTEGERP LST)
(INTEGERP X))
(EQUAL (GET-NTH (BSEARCH1 X LST I J) LST)
X)),
which simplifies, rewriting with ILESSP-ENTAILS-ILEQ, and expanding the
function BSEARCH1, to:
T.
Case 2. (IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(NOT (ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X))
(NOT (EQUAL (BSEARCH1 X LST I J) -1))
(LST-INTEGERP LST)
(INTEGERP X))
(EQUAL (GET-NTH (BSEARCH1 X LST I J) LST)
X)).
This simplifies, appealing to the lemmas LEQ-TRANS, GET-LST-INTEGERP, and
INT-EQUAL, and opening up the definition of BSEARCH1, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP I J))
(NOT (EQUAL (BSEARCH1 X LST I J) -1))
(LST-INTEGERP LST)
(INTEGERP X))
(EQUAL (GET-NTH (BSEARCH1 X LST I J) LST)
X)).
This simplifies, expanding the functions BSEARCH1 and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
BSEARCH1-FOUND
(PROVE-LEMMA BSEARCH1-NOT-FOUND-1
(REWRITE)
(IMPLIES (AND (ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(LEQ I K)
(LESSP K J)
(LEQ J (LEN LST)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST (ADD1 K) J))))
WARNING: Note that BSEARCH1-NOT-FOUND-1 contains the free variable K which
will be chosen by instantiating the hypothesis (ILESSP (GET-NTH K LST) X).
Call the conjecture *1.
We will appeal to induction. Two inductions are suggested by terms in
the conjecture. However, only one is unflawed. We will induct according to
the following scheme:
(AND (IMPLIES (AND (LESSP I J)
(EQUAL X (GET-NTH I LST)))
(p X LST I J K))
(IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(p X LST (ADD1 I) J K))
(p X LST I J K))
(IMPLIES (NOT (LESSP I J))
(p X LST I J K))).
Linear arithmetic establishes that the measure (DIFFERENCE J I) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme leads to the following four new formulas:
Case 4. (IMPLIES (AND (LESSP I J)
(EQUAL X (GET-NTH I LST))
(ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(NOT (LESSP K I))
(LESSP K J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST (ADD1 K) J))).
This simplifies, using linear arithmetic and appealing to the lemma
ORDEREDP-ORDERED, to:
T.
Case 3. (IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(LESSP K (ADD1 I))
(ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(NOT (LESSP K I))
(LESSP K J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST (ADD1 K) J))).
This simplifies, using linear arithmetic, to the following three new goals:
Case 3.3.
(IMPLIES (AND (NOT (NUMBERP K))
(LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(LESSP K (ADD1 I))
(ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(NOT (LESSP K I))
(LESSP K J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST (ADD1 K) J))).
But this again simplifies, applying SUB1-TYPE-RESTRICTION, and unfolding
the definitions of LESSP and MEMBER1, to the following two new goals:
Case 3.3.2.
(IMPLIES (AND (NOT (NUMBERP K))
(LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(EQUAL I 0)
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST 0 J)
(MEMBER1 X LST 1 J))).
However this again simplifies, expanding EQUAL, LESSP, ADD1, and MEMBER1,
to:
T.
Case 3.3.1.
(IMPLIES (AND (NOT (NUMBERP K))
(LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(NOT (NUMBERP I))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST (ADD1 I) J)
(MEMBER1 X LST 1 J))),
which again simplifies, expanding LESSP, to:
(IMPLIES (AND (NOT (NUMBERP K))
(NOT (EQUAL X (GET-NTH I LST)))
(ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(NOT (NUMBERP I))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST (ADD1 I) J)
(MEMBER1 X LST 1 J))).
But this further simplifies, appealing to the lemma
SUB1-TYPE-RESTRICTION, to:
T.
Case 3.2.
(IMPLIES (AND (NOT (NUMBERP I))
(LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(LESSP K (ADD1 I))
(ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(NOT (LESSP K I))
(LESSP K J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST (ADD1 K) J))),
which again simplifies, applying the lemmas SUB1-TYPE-RESTRICTION and
LESSP-OF-1, and opening up the definitions of LESSP, EQUAL, MEMBER1, and
ADD1, to two new goals:
Case 3.2.2.
(IMPLIES (AND (NOT (NUMBERP I))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (EQUAL X (GET-NTH I LST)))
(EQUAL K 0)
(ORDEREDP LST)
(ILESSP (GET-NTH 0 LST) X)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST (ADD1 I) J)
(MEMBER1 X LST 1 J))),
which again simplifies, obviously, to the new conjecture:
(IMPLIES (AND (NOT (NUMBERP I))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (EQUAL X (GET-NTH I LST)))
(ORDEREDP LST)
(ILESSP (GET-NTH 0 LST) X)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST (ADD1 I) J)
(MEMBER1 X LST 1 J))),
which further simplifies, applying SUB1-TYPE-RESTRICTION, to:
T.
Case 3.2.1.
(IMPLIES (AND (NOT (NUMBERP I))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (EQUAL X (GET-NTH I LST)))
(NOT (NUMBERP K))
(ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST (ADD1 I) J)
(MEMBER1 X LST 1 J))).
However this further simplifies, appealing to the lemma
SUB1-TYPE-RESTRICTION, to:
T.
Case 3.1.
(IMPLIES (AND (NUMBERP I)
(NUMBERP K)
(LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(LESSP I (ADD1 I))
(ORDEREDP LST)
(ILESSP (GET-NTH I LST) X)
(NOT (LESSP I I))
(LESSP I J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST (ADD1 I) J))),
which again simplifies, applying the lemmas LESSP-SUB1 and SUB1-ADD1, and
unfolding the functions LESSP and MEMBER1, to:
T.
Case 2. (IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(EQUAL (MEMBER1 X LST (ADD1 I) J)
(MEMBER1 X LST (ADD1 K) J))
(ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(NOT (LESSP K I))
(LESSP K J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST (ADD1 K) J))),
which simplifies, unfolding the function MEMBER1, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP I J))
(ORDEREDP LST)
(ILESSP (GET-NTH K LST) X)
(NOT (LESSP K I))
(LESSP K J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST (ADD1 K) J))),
which simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
BSEARCH1-NOT-FOUND-1
(PROVE-LEMMA BSEARCH1-NOT-FOUND-2-LEMMA
(REWRITE)
(IMPLIES (AND (ORDEREDP LST)
(ILESSP X (GET-NTH K LST))
(LEQ K I)
(LESSP J (LEN LST)))
(NOT (MEMBER1 X LST I J))))
WARNING: Note that BSEARCH1-NOT-FOUND-2-LEMMA contains the free variable K
which will be chosen by instantiating the hypothesis:
(ILESSP X (GET-NTH K LST)).
Call the conjecture *1.
Perhaps we can prove it by induction. The recursive terms in the
conjecture suggest two inductions. However, only one is unflawed. We will
induct according to the following scheme:
(AND (IMPLIES (AND (LESSP I J)
(EQUAL X (GET-NTH I LST)))
(p X LST I J K))
(IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(p X LST (ADD1 I) J K))
(p X LST I J K))
(IMPLIES (NOT (LESSP I J))
(p X LST I J K))).
Linear arithmetic informs us that the measure (DIFFERENCE J I) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme produces the following four new
conjectures:
Case 4. (IMPLIES (AND (LESSP I J)
(EQUAL X (GET-NTH I LST))
(ORDEREDP LST)
(ILESSP X (GET-NTH K LST))
(NOT (LESSP I K))
(LESSP J (LEN LST)))
(NOT (MEMBER1 X LST I J))).
This simplifies, using linear arithmetic and applying ORDEREDP-ORDERED, to:
T.
Case 3. (IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(LESSP (ADD1 I) K)
(ORDEREDP LST)
(ILESSP X (GET-NTH K LST))
(NOT (LESSP I K))
(LESSP J (LEN LST)))
(NOT (MEMBER1 X LST I J))),
which simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(NOT (MEMBER1 X LST (ADD1 I) J))
(ORDEREDP LST)
(ILESSP X (GET-NTH K LST))
(NOT (LESSP I K))
(LESSP J (LEN LST)))
(NOT (MEMBER1 X LST I J))),
which simplifies, opening up the definition of MEMBER1, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP I J))
(ORDEREDP LST)
(ILESSP X (GET-NTH K LST))
(NOT (LESSP I K))
(LESSP J (LEN LST)))
(NOT (MEMBER1 X LST I J))),
which simplifies, unfolding the definition of MEMBER1, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
BSEARCH1-NOT-FOUND-2-LEMMA
(PROVE-LEMMA BSEARCH1-NOT-FOUND-2
(REWRITE)
(IMPLIES (AND (ORDEREDP LST)
(ILESSP X (GET-NTH K LST))
(LESSP K J)
(LEQ J (LEN LST)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST I K))))
WARNING: Note that BSEARCH1-NOT-FOUND-2 contains the free variable K which
will be chosen by instantiating the hypothesis (ILESSP X (GET-NTH K LST)).
Call the conjecture *1.
We will appeal to induction. Three inductions are suggested by terms in
the conjecture. They merge into two likely candidate inductions. However,
only one is unflawed. We will induct according to the following scheme:
(AND (IMPLIES (AND (LESSP I J)
(EQUAL X (GET-NTH I LST)))
(p X LST I J K))
(IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(p X LST (ADD1 I) J K))
(p X LST I J K))
(IMPLIES (NOT (LESSP I J))
(p X LST I J K))).
Linear arithmetic establishes that the measure (DIFFERENCE J I) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme produces the following three new goals:
Case 3. (IMPLIES (AND (LESSP I J)
(EQUAL X (GET-NTH I LST))
(ORDEREDP LST)
(ILESSP X (GET-NTH K LST))
(LESSP K J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST I K))).
This simplifies, expanding MEMBER1, to:
(IMPLIES (AND (LESSP I J)
(ORDEREDP LST)
(ILESSP (GET-NTH I LST)
(GET-NTH K LST))
(LESSP K J)
(NOT (LESSP (LEN LST) J)))
(LESSP I K)),
which again simplifies, using linear arithmetic and rewriting with
ORDEREDP-ORDERED, to:
T.
Case 2. (IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(EQUAL (MEMBER1 X LST (ADD1 I) J)
(MEMBER1 X LST (ADD1 I) K))
(ORDEREDP LST)
(ILESSP X (GET-NTH K LST))
(LESSP K J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST I K))).
This simplifies, unfolding the definition of MEMBER1, to:
(IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(EQUAL (MEMBER1 X LST (ADD1 I) J)
(MEMBER1 X LST (ADD1 I) K))
(ORDEREDP LST)
(ILESSP X (GET-NTH K LST))
(LESSP K J)
(NOT (LESSP (LEN LST) J))
(NOT (LESSP I K)))
(EQUAL (MEMBER1 X LST (ADD1 I) J) F)),
which again simplifies, using linear arithmetic and applying the lemma
BSEARCH1-NOT-FOUND-2-LEMMA, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP I J))
(ORDEREDP LST)
(ILESSP X (GET-NTH K LST))
(LESSP K J)
(NOT (LESSP (LEN LST) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER1 X LST I K))),
which simplifies, using linear arithmetic, rewriting with
BSEARCH1-NOT-FOUND-2-LEMMA, and unfolding MEMBER1 and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
BSEARCH1-NOT-FOUND-2
(DISABLE BSEARCH1-NOT-FOUND-2-LEMMA)
[ 0.0 0.0 0.0 ]
BSEARCH1-NOT-FOUND-2-LEMMA-OFF
(PROVE-LEMMA BSEARCH1-NOT-FOUND
(REWRITE)
(IMPLIES (AND (EQUAL (BSEARCH1 X LST I J) -1)
(ORDEREDP LST)
(LST-INTEGERP LST)
(INTEGERP X)
(LEQ J (LEN LST)))
(NOT (MEMBER1 X LST I J)))
((INDUCT (BSEARCH1 X LST I J))))
This conjecture can be simplified, using the abbreviations IMPLIES, NOT, OR,
and AND, to four new formulas:
Case 4. (IMPLIES (AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(IMPLIES (AND (EQUAL (BSEARCH1 X LST I
(QUOTIENT (PLUS I J) 2))
-1)
(ORDEREDP LST)
(LST-INTEGERP LST)
(INTEGERP X)
(IF (LESSP (LEN LST)
(QUOTIENT (PLUS I J) 2))
F T))
(NOT (MEMBER1 X LST I
(QUOTIENT (PLUS I J) 2))))
(EQUAL (BSEARCH1 X LST I J) -1)
(ORDEREDP LST)
(LST-INTEGERP LST)
(INTEGERP X)
(NOT (LESSP (LEN LST) J)))
(NOT (MEMBER1 X LST I J))),
which simplifies, using linear arithmetic, appealing to the lemmas
MEAN-BOUNDS and BSEARCH1-NOT-FOUND-2, and opening up the definitions of AND,
NOT, IMPLIES, and BSEARCH1, to:
(IMPLIES (AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(LESSP (LEN LST)
(QUOTIENT (PLUS I J) 2))
(EQUAL (BSEARCH1 X LST I
(QUOTIENT (PLUS I J) 2))
-1)
(ORDEREDP LST)
(LST-INTEGERP LST)
(INTEGERP X)
(NOT (LESSP (LEN LST) J)))
(NOT (MEMBER1 X LST I
(QUOTIENT (PLUS I J) 2)))).
This again simplifies, using linear arithmetic and appealing to the lemma
MEAN-BOUNDS, to:
T.
Case 3. (IMPLIES
(AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(IMPLIES (AND (EQUAL (BSEARCH1 X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)
-1)
(ORDEREDP LST)
(LST-INTEGERP LST)
(INTEGERP X)
(IF (LESSP (LEN LST) J) F T))
(NOT (MEMBER1 X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
(EQUAL (BSEARCH1 X LST I J) -1)
(ORDEREDP LST)
(LST-INTEGERP LST)
(INTEGERP X)
(NOT (LESSP (LEN LST) J)))
(NOT (MEMBER1 X LST I J))),
which simplifies, using linear arithmetic, rewriting with the lemmas
ILESSP-ENTAILS-ILEQ, MEAN-BOUNDS, and BSEARCH1-NOT-FOUND-1, and opening up
the definitions of AND, NOT, IMPLIES, and BSEARCH1, to:
T.
Case 2. (IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(NOT (ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X))
(EQUAL (BSEARCH1 X LST I J) -1)
(ORDEREDP LST)
(LST-INTEGERP LST)
(INTEGERP X)
(NOT (LESSP (LEN LST) J)))
(NOT (MEMBER1 X LST I J))),
which simplifies, using linear arithmetic, rewriting with LEQ-TRANS,
MEAN-BOUNDS, and ORDEREDP-ORDERED, and expanding BSEARCH1, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP I J))
(EQUAL (BSEARCH1 X LST I J) -1)
(ORDEREDP LST)
(LST-INTEGERP LST)
(INTEGERP X)
(NOT (LESSP (LEN LST) J)))
(NOT (MEMBER1 X LST I J))).
This simplifies, unfolding the functions BSEARCH1, EQUAL, and MEMBER1, to:
T.
Q.E.D.
[ 0.0 3.3 0.0 ]
BSEARCH1-NOT-FOUND
(DEFN MEMBER2
(X LST I J)
(IF (LESSP I J)
(IF (EQUAL X (GET-NTH I LST))
T
(MEMBER2 X (CDR LST) I (SUB1 J)))
F)
((LESSP (DIFFERENCE J I))))
Linear arithmetic establishes that the measure (DIFFERENCE J I) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
MEMBER2 is accepted under the definitional principle. Observe that:
(OR (FALSEP (MEMBER2 X LST I J))
(TRUEP (MEMBER2 X LST I J)))
is a theorem.
[ 0.0 0.0 0.0 ]
MEMBER2
(PROVE-LEMMA MEMBER2-MEMBER NIL
(EQUAL (MEMBER2 X LST 0 (LEN LST))
(MEMBER X LST))
((ENABLE GET-NTH)))
Call the conjecture *1.
Perhaps we can prove it by induction. Two inductions are suggested by
terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP LST) (p X LST))
(IMPLIES (AND (NOT (NLISTP LST))
(EQUAL X (CAR LST)))
(p X LST))
(IMPLIES (AND (NOT (NLISTP LST))
(NOT (EQUAL X (CAR LST)))
(p X (CDR LST)))
(p X LST))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT LST) decreases according
to the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme leads to three new goals:
Case 3. (IMPLIES (NLISTP LST)
(EQUAL (MEMBER2 X LST 0 (LEN LST))
(MEMBER X LST))),
which simplifies, opening up the definitions of NLISTP, LEN, LESSP, MEMBER2,
MEMBER, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP LST))
(EQUAL X (CAR LST)))
(EQUAL (MEMBER2 X LST 0 (LEN LST))
(MEMBER X LST))),
which simplifies, expanding NLISTP, LEN, GET-NTH, LESSP, EQUAL, MEMBER2, and
MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP LST))
(NOT (EQUAL X (CAR LST)))
(EQUAL (MEMBER2 X
(CDR LST)
0
(LEN (CDR LST)))
(MEMBER X (CDR LST))))
(EQUAL (MEMBER2 X LST 0 (LEN LST))
(MEMBER X LST))),
which simplifies, applying the lemma SUB1-ADD1, and opening up the functions
NLISTP, LEN, GET-NTH, LESSP, EQUAL, MEMBER2, and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER2-MEMBER
(PROVE-LEMMA MEMBER2-LEMMA
(REWRITE)
(IMPLIES (NOT (EQUAL X (GET-NTH I LST)))
(EQUAL (MEMBER2 X LST (ADD1 I) J)
(MEMBER2 X LST I J)))
((ENABLE GET-NTH)))
Call the conjecture *1.
We will try to prove it by induction. The recursive terms in the
conjecture suggest three inductions. They merge into two likely candidate
inductions. However, only one is unflawed. We will induct according to the
following scheme:
(AND (IMPLIES (AND (LESSP (ADD1 I) J)
(EQUAL X (GET-NTH (ADD1 I) LST)))
(p X LST I J))
(IMPLIES (AND (LESSP (ADD1 I) J)
(NOT (EQUAL X (GET-NTH (ADD1 I) LST)))
(p X (CDR LST) I (SUB1 J)))
(p X LST I J))
(IMPLIES (NOT (LESSP (ADD1 I) J))
(p X LST I J))).
Linear arithmetic can be used to prove that the measure
(DIFFERENCE J (ADD1 I)) decreases according to the well-founded relation LESSP
in each induction step of the scheme. Note, however, the inductive instance
chosen for LST. The above induction scheme leads to the following four new
goals:
Case 4. (IMPLIES (AND (LESSP (ADD1 I) J)
(EQUAL X (GET-NTH (ADD1 I) LST))
(NOT (EQUAL X (GET-NTH I LST))))
(EQUAL (MEMBER2 X LST (ADD1 I) J)
(MEMBER2 X LST I J))).
This simplifies, applying the lemmas SUB1-ADD1 and SUB1-TYPE-RESTRICTION,
and expanding the functions LESSP, GET-NTH, EQUAL, NUMBERP, SUB1, and
MEMBER2, to the following two new formulas:
Case 4.2.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(LESSP 0 (SUB1 J))
(NOT (EQUAL (GET-NTH 1 LST) (CAR LST))))
(MEMBER2 (GET-NTH 1 LST) LST I J)).
However this again simplifies, rewriting with SUB1-OF-1, and unfolding
EQUAL and LESSP, to the new formula:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (GET-NTH 1 LST) (CAR LST))))
(MEMBER2 (GET-NTH 1 LST) LST I J)).
Applying the lemma CAR-CDR-ELIM, replace LST by (CONS Z V) to eliminate
(CAR LST) and (CDR LST). We would thus like to prove the following two
new goals:
Case 4.2.2.
(IMPLIES (AND (NOT (LISTP LST))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (GET-NTH 1 LST) (CAR LST))))
(MEMBER2 (GET-NTH 1 LST) LST I J)).
However this further simplifies, rewriting with the lemmas CDR-NLISTP
and CAR-NLISTP, and unfolding the definitions of GET-NTH, SUB1, NUMBERP,
and EQUAL, to:
T.
Case 4.2.1.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (GET-NTH 1 (CONS Z V)) Z)))
(MEMBER2 (GET-NTH 1 (CONS Z V))
(CONS Z V)
I J)),
which further simplifies, applying CDR-CONS, and expanding the functions
SUB1, NUMBERP, EQUAL, and GET-NTH, to:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (CAR V) Z)))
(MEMBER2 (CAR V) (CONS Z V) I J)),
which we will name *1.1.
Case 4.1.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NUMBERP I)
(LESSP I (SUB1 J))
(NOT (EQUAL (GET-NTH I (CDR LST))
(GET-NTH I LST))))
(MEMBER2 (GET-NTH I (CDR LST))
LST I J)).
Appealing to the lemma SUB1-ELIM, we now replace J by (ADD1 Z) to
eliminate (SUB1 J). We rely upon the type restriction lemma noted when
SUB1 was introduced to constrain the new variable. We must thus prove the
goal:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(NUMBERP I)
(LESSP I Z)
(NOT (EQUAL (GET-NTH I (CDR LST))
(GET-NTH I LST))))
(MEMBER2 (GET-NTH I (CDR LST))
LST I
(ADD1 Z))).
But this further simplifies, rewriting with SUB1-ADD1, and opening up the
functions LESSP and MEMBER2, to:
(IMPLIES (AND (NUMBERP Z)
(NUMBERP I)
(LESSP I Z)
(NOT (EQUAL (GET-NTH I (CDR LST))
(GET-NTH I LST)))
(NOT (EQUAL I 0)))
(LESSP (SUB1 I) Z)),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (LESSP (ADD1 I) J)
(NOT (EQUAL X (GET-NTH (ADD1 I) LST)))
(EQUAL X (GET-NTH I (CDR LST)))
(NOT (EQUAL X (GET-NTH I LST))))
(EQUAL (MEMBER2 X LST (ADD1 I) J)
(MEMBER2 X LST I J))),
which simplifies, rewriting with SUB1-ADD1 and SUB1-TYPE-RESTRICTION, and
opening up the functions LESSP and GET-NTH, to:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(LESSP 0 (SUB1 J))
(NOT (EQUAL (CADR LST) (GET-NTH 1 LST)))
(NOT (EQUAL (CADR LST) (CAR LST))))
(EQUAL (MEMBER2 (CADR LST) LST 1 J)
(MEMBER2 (CADR LST) LST I J))),
which again simplifies, rewriting with SUB1-OF-1, and opening up the
definitions of EQUAL and LESSP, to the new formula:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (CADR LST) (GET-NTH 1 LST)))
(NOT (EQUAL (CADR LST) (CAR LST))))
(EQUAL (MEMBER2 (CADR LST) LST 1 J)
(MEMBER2 (CADR LST) LST I J))).
Applying the lemma CAR-CDR-ELIM, replace LST by (CONS V Z) to eliminate
(CDR LST) and (CAR LST) and Z by (CONS W D) to eliminate (CAR Z) and (CDR Z).
We would thus like to prove the following three new formulas:
Case 3.3.
(IMPLIES (AND (NOT (LISTP LST))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (CADR LST) (GET-NTH 1 LST)))
(NOT (EQUAL (CADR LST) (CAR LST))))
(EQUAL (MEMBER2 (CADR LST) LST 1 J)
(MEMBER2 (CADR LST) LST I J))).
But this further simplifies, rewriting with CDR-NLISTP, and opening up the
definitions of CAR, GET-NTH, SUB1, NUMBERP, and EQUAL, to:
T.
Case 3.2.
(IMPLIES (AND (NOT (LISTP Z))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (CAR Z)
(GET-NTH 1 (CONS V Z))))
(NOT (EQUAL (CAR Z) V)))
(EQUAL (MEMBER2 (CAR Z) (CONS V Z) 1 J)
(MEMBER2 (CAR Z) (CONS V Z) I J))).
This further simplifies, applying CAR-NLISTP and CDR-CONS, and unfolding
the functions SUB1, NUMBERP, EQUAL, and GET-NTH, to:
T.
Case 3.1.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL W
(GET-NTH 1 (CONS V (CONS W D)))))
(NOT (EQUAL W V)))
(EQUAL (MEMBER2 W (CONS V (CONS W D)) 1 J)
(MEMBER2 W (CONS V (CONS W D)) I J))).
This further simplifies, rewriting with CDR-CONS and CAR-CONS, and
unfolding SUB1, NUMBERP, EQUAL, and GET-NTH, to:
T.
Case 2. (IMPLIES (AND (LESSP (ADD1 I) J)
(NOT (EQUAL X (GET-NTH (ADD1 I) LST)))
(EQUAL (MEMBER2 X
(CDR LST)
(ADD1 I)
(SUB1 J))
(MEMBER2 X (CDR LST) I (SUB1 J)))
(NOT (EQUAL X (GET-NTH I LST))))
(EQUAL (MEMBER2 X LST (ADD1 I) J)
(MEMBER2 X LST I J))).
This simplifies, rewriting with SUB1-ADD1 and SUB1-TYPE-RESTRICTION, and
expanding LESSP, GET-NTH, and MEMBER2, to two new goals:
Case 2.2.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(LESSP 0 (SUB1 J))
(NOT (EQUAL X (GET-NTH 1 LST)))
(EQUAL (MEMBER2 X
(CDR LST)
(ADD1 I)
(SUB1 J))
(MEMBER2 X (CDR LST) I (SUB1 J)))
(NOT (EQUAL X (CAR LST))))
(EQUAL (MEMBER2 X LST 1 J)
(MEMBER2 X (CDR LST) I (SUB1 J)))),
which again simplifies, applying SUB1-OF-1, and unfolding EQUAL and LESSP,
to:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL X (GET-NTH 1 LST)))
(EQUAL (MEMBER2 X
(CDR LST)
(ADD1 I)
(SUB1 J))
(MEMBER2 X (CDR LST) I (SUB1 J)))
(NOT (EQUAL X (CAR LST))))
(EQUAL (MEMBER2 X LST 1 J)
(MEMBER2 X (CDR LST) I (SUB1 J)))),
which further simplifies, applying SUB1-TYPE-RESTRICTION, to the new
formula:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL X (GET-NTH 1 LST)))
(EQUAL (MEMBER2 X (CDR LST) 1 (SUB1 J))
(MEMBER2 X (CDR LST) I (SUB1 J)))
(NOT (EQUAL X (CAR LST))))
(EQUAL (MEMBER2 X LST 1 J)
(MEMBER2 X (CDR LST) 1 (SUB1 J)))),
which again simplifies, opening up MEMBER2, to the goal:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL X (GET-NTH 1 LST)))
(EQUAL (MEMBER2 X (CDR LST) 1 (SUB1 J))
(MEMBER2 X (CDR LST) I (SUB1 J)))
(NOT (EQUAL X (CAR LST)))
(NOT (LESSP 1 J)))
(EQUAL F
(MEMBER2 X (CDR LST) 1 (SUB1 J)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NUMBERP I)
(LESSP I (SUB1 J))
(NOT (EQUAL X (GET-NTH I (CDR LST))))
(EQUAL (MEMBER2 X
(CDR LST)
(ADD1 I)
(SUB1 J))
(MEMBER2 X (CDR LST) I (SUB1 J)))
(NOT (EQUAL X (GET-NTH I LST)))
(NOT (LESSP I J)))
(EQUAL (MEMBER2 X (CDR LST) I (SUB1 J))
F)),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP (ADD1 I) J))
(NOT (EQUAL X (GET-NTH I LST))))
(EQUAL (MEMBER2 X LST (ADD1 I) J)
(MEMBER2 X LST I J))),
which simplifies, appealing to the lemmas SUB1-ADD1 and
SUB1-TYPE-RESTRICTION, and expanding the definitions of LESSP, EQUAL,
MEMBER2, GET-NTH, NUMBERP, and SUB1, to two new formulas:
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP I))
(NOT (LESSP 0 (SUB1 J)))
(NOT (EQUAL X (CAR LST)))
(NOT (EQUAL J 0))
(NUMBERP J))
(NOT (MEMBER2 X (CDR LST) I (SUB1 J)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (NUMBERP I))
(NOT (LESSP 0 (SUB1 1)))
(NOT (EQUAL X (CAR LST)))
(NOT (EQUAL 1 0))
(NUMBERP 1))
(NOT (MEMBER2 X (CDR LST) I (SUB1 1)))).
However this again simplifies, unfolding SUB1, LESSP, EQUAL, NUMBERP, and
MEMBER2, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP I)
(NOT (LESSP I (SUB1 J)))
(NOT (EQUAL X (GET-NTH I LST)))
(LESSP I J))
(NOT (MEMBER2 X (CDR LST) I (SUB1 J)))),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 1.1.2.
(IMPLIES (AND (NOT (NUMBERP J))
(NUMBERP I)
(NOT (LESSP I (SUB1 J)))
(NOT (EQUAL X (GET-NTH I LST)))
(LESSP I J))
(NOT (MEMBER2 X (CDR LST) I (SUB1 J)))),
which again simplifies, appealing to the lemma SUB1-NNUMBERP, and
expanding the definitions of EQUAL and LESSP, to:
T.
Case 1.1.1.
(IMPLIES (AND (NUMBERP J)
(NUMBERP I)
(NOT (LESSP I (SUB1 (PLUS 1 I))))
(NOT (EQUAL X (GET-NTH I LST)))
(LESSP I (PLUS 1 I)))
(NOT (MEMBER2 X
(CDR LST)
I
(SUB1 (PLUS 1 I))))),
which again simplifies, rewriting with PLUS-ADD1, SUB1-ADD1, and
LESSP-SUB1, and unfolding LESSP and MEMBER2, to:
T.
So we now return to:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (CAR V) Z)))
(MEMBER2 (CAR V) (CONS Z V) I J)),
which we named *1.1 above. We will appeal to induction. There is only one
plausible induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LESSP I J)
(EQUAL (CAR V)
(GET-NTH I (CONS Z V))))
(p V Z I J))
(IMPLIES (AND (LESSP I J)
(NOT (EQUAL (CAR V)
(GET-NTH I (CONS Z V))))
(p V Z I (SUB1 J)))
(p V Z I J))
(IMPLIES (NOT (LESSP I J))
(p V Z I J))).
Linear arithmetic establishes that the measure (DIFFERENCE J I) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme generates the following five new goals:
Case 5. (IMPLIES (AND (LESSP I J)
(EQUAL (CAR V) (GET-NTH I (CONS Z V)))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (CAR V) Z)))
(MEMBER2 (CAR V) (CONS Z V) I J)).
This simplifies, rewriting with CAR-CONS, and opening up the definitions of
LESSP and GET-NTH, to:
T.
Case 4. (IMPLIES (AND (LESSP I J)
(NOT (EQUAL (CAR V)
(GET-NTH I (CONS Z V))))
(EQUAL (SUB1 J) 0)
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (CAR V) Z)))
(MEMBER2 (CAR V) (CONS Z V) I J)),
which simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (LESSP I J)
(NOT (EQUAL (CAR V)
(GET-NTH I (CONS Z V))))
(EQUAL (SUB1 J) 1)
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (CAR V) Z)))
(MEMBER2 (CAR V) (CONS Z V) I J)),
which simplifies, appealing to the lemmas CAR-CONS, CDR-CONS, and LESSP-OF-1,
and unfolding the functions LESSP, GET-NTH, and MEMBER2, to:
T.
Case 2. (IMPLIES (AND (LESSP I J)
(NOT (EQUAL (CAR V)
(GET-NTH I (CONS Z V))))
(MEMBER2 (CAR V)
(CONS Z V)
I
(SUB1 J))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (CAR V) Z)))
(MEMBER2 (CAR V) (CONS Z V) I J)),
which simplifies, rewriting with CAR-CONS, CDR-CONS, and SUB1-OF-1, and
expanding the functions LESSP, GET-NTH, and MEMBER2, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP I J))
(NOT (EQUAL J 0))
(NUMBERP J)
(NOT (NUMBERP I))
(NOT (EQUAL J 1))
(NOT (EQUAL (CAR V) Z)))
(MEMBER2 (CAR V) (CONS Z V) I J)).
This simplifies, opening up the definition of LESSP, to:
T.
That finishes the proof of *1.1, which, consequently, also finishes the
proof of *1. Q.E.D.
[ 0.0 0.2 0.1 ]
MEMBER2-LEMMA
(PROVE-LEMMA MEMBER1-MEMBER2 NIL
(EQUAL (MEMBER1 X LST I J)
(MEMBER2 X LST I J)))
Name the conjecture *1.
We will appeal to induction. The recursive terms in the conjecture
suggest two inductions, both of which are flawed. So we will choose the one
suggested by the largest number of nonprimitive recursive functions. We will
induct according to the following scheme:
(AND (IMPLIES (AND (LESSP I J)
(EQUAL X (GET-NTH I LST)))
(p X LST I J))
(IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(p X LST (ADD1 I) J))
(p X LST I J))
(IMPLIES (NOT (LESSP I J))
(p X LST I J))).
Linear arithmetic establishes that the measure (DIFFERENCE J I) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme produces the following three new formulas:
Case 3. (IMPLIES (AND (LESSP I J)
(EQUAL X (GET-NTH I LST)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER2 X LST I J))).
This simplifies, expanding the definitions of MEMBER1, MEMBER2, and EQUAL,
to:
T.
Case 2. (IMPLIES (AND (LESSP I J)
(NOT (EQUAL X (GET-NTH I LST)))
(EQUAL (MEMBER1 X LST (ADD1 I) J)
(MEMBER2 X LST (ADD1 I) J)))
(EQUAL (MEMBER1 X LST I J)
(MEMBER2 X LST I J))).
This simplifies, applying MEMBER2-LEMMA, and expanding the definition of
MEMBER1, to:
T.
Case 1. (IMPLIES (NOT (LESSP I J))
(EQUAL (MEMBER1 X LST I J)
(MEMBER2 X LST I J))),
which simplifies, opening up MEMBER1, MEMBER2, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.4 0.0 ]
MEMBER1-MEMBER2
(PROVE-LEMMA BSEARCH-FOUND
(REWRITE)
(IMPLIES (AND (NOT (EQUAL (BSEARCH X N LST) -1))
(LST-INTEGERP LST)
(INTEGERP X))
(EQUAL (GET-NTH (BSEARCH X N LST) LST)
X)))
This conjecture can be simplified, using the abbreviations NOT, AND, IMPLIES,
and BSEARCH, to:
(IMPLIES (AND (NOT (EQUAL (BSEARCH1 X LST 0 N) -1))
(LST-INTEGERP LST)
(INTEGERP X))
(EQUAL (GET-NTH (BSEARCH1 X LST 0 N) LST)
X)).
This simplifies, appealing to the lemma BSEARCH1-FOUND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
BSEARCH-FOUND
(PROVE-LEMMA BSEARCH-NOT-FOUND
(REWRITE)
(IMPLIES (AND (EQUAL (BSEARCH X (LEN LST) LST) -1)
(ORDEREDP LST)
(LST-INTEGERP LST)
(INTEGERP X))
(NOT (MEMBER X LST)))
((USE (MEMBER1-MEMBER2 (I 0) (J (LEN LST)))
(MEMBER2-MEMBER))))
This formula can be simplified, using the abbreviations NOT, IMPLIES, AND, and
BSEARCH, to:
(IMPLIES (AND (EQUAL (MEMBER1 X LST 0 (LEN LST))
(MEMBER2 X LST 0 (LEN LST)))
(EQUAL (MEMBER2 X LST 0 (LEN LST))
(MEMBER X LST))
(EQUAL (BSEARCH1 X LST 0 (LEN LST))
-1)
(ORDEREDP LST)
(LST-INTEGERP LST)
(INTEGERP X))
(NOT (MEMBER X LST))),
which simplifies, using linear arithmetic and applying BSEARCH1-NOT-FOUND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
BSEARCH-NOT-FOUND
(PROVE-LEMMA BSEARCH1-T-0
(REWRITE)
(EQUAL (BSEARCH1-T X LST I I) 6)
((EXPAND (BSEARCH1-T X LST I I))))
This simplifies, rewriting with QUOTIENT-2X, and unfolding BSEARCH1-T, to the
following six new conjectures:
Case 6. (IMPLIES (AND (LESSP I I)
(NUMBERP I)
(NOT (ILESSP X (GET-NTH I LST))))
(EQUAL (SPLUS 13
(BSEARCH1-T X LST (ADD1 I) I))
6)).
However this again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (LESSP I I)
(NUMBERP I)
(ILESSP X (GET-NTH I LST)))
(EQUAL (SPLUS 10 (BSEARCH1-T X LST I I))
6)),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (LESSP I I)
(NOT (NUMBERP I))
(NOT (ILESSP X (GET-NTH 0 LST))))
(EQUAL (SPLUS 13 (BSEARCH1-T X LST 1 I))
6)),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (LESSP I I)
(NOT (NUMBERP I))
(ILESSP X (GET-NTH 0 LST)))
(EQUAL (SPLUS 10 (BSEARCH1-T X LST I 0))
6)),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (LESSP I I)
(NOT (NUMBERP I))
(NOT (ILESSP X (GET-NTH 0 LST))))
(ILESSP (GET-NTH 0 LST) X)),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (LESSP I I)
(NUMBERP I)
(NOT (ILESSP X (GET-NTH I LST))))
(ILESSP (GET-NTH I LST) X)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
BSEARCH1-T-0
(PROVE-LEMMA BSEARCH1-T-CROCK
(REWRITE)
(IMPLIES
(AND (LESSP I J)
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))
(EQUAL (LESSP (PLUS 26
(TIMES 13 (LOG 2 (DIFFERENCE J I))))
(PLUS 13
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
F))
((USE (LOG-LEQ (B 2)
(X (DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))
(Y (QUOTIENT (DIFFERENCE J I) 2)))
(MEAN-DIFFERENCE-2))))
This formula simplifies, applying the lemmas QUOTIENT-TIMES-LESSP,
DIFFERENCE=0, DIFFERENCE-IS-1, SUB1-OF-1, and LESSP-OF-1, and expanding the
definitions of EQUAL, NUMBERP, NOT, IMPLIES, LESSP, SUB1, and LOG, to the
following six new goals:
Case 6. (IMPLIES
(AND
(LESSP (DIFFERENCE J I)
(TIMES 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2))))
(LESSP J I)
(LESSP I J)
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
(NOT (EQUAL J (ADD1 I))))
(NOT (LESSP (PLUS 26
(TIMES 13
(ADD1 (LOG 2
(QUOTIENT (DIFFERENCE J I) 2)))))
(PLUS 13
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))).
This again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES
(AND
(LESSP (DIFFERENCE J I)
(TIMES 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2))))
(LESSP J I)
(LESSP I J)
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
(EQUAL J (ADD1 I)))
(NOT (LESSP (PLUS 26 (TIMES 13 0))
(PLUS 13
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES
(AND
(NOT (LESSP (LOG 2 (QUOTIENT (DIFFERENCE J I) 2))
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(LESSP J I)
(LESSP I J)
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
(NOT (EQUAL J (ADD1 I))))
(NOT (LESSP (PLUS 26
(TIMES 13
(ADD1 (LOG 2
(QUOTIENT (DIFFERENCE J I) 2)))))
(PLUS 13
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES
(AND
(NOT (LESSP (LOG 2 (QUOTIENT (DIFFERENCE J I) 2))
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(LESSP J I)
(LESSP I J)
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
(EQUAL J (ADD1 I)))
(NOT (LESSP (PLUS 26 (TIMES 13 0))
(PLUS 13
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES
(AND
(NOT (LESSP (LOG 2 (QUOTIENT (DIFFERENCE J I) 2))
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(NOT (LESSP (DIFFERENCE J I)
(TIMES 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(LESSP I J)
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
(NOT (EQUAL J (ADD1 I))))
(NOT (LESSP (PLUS 26
(TIMES 13
(ADD1 (LOG 2
(QUOTIENT (DIFFERENCE J I) 2)))))
(PLUS 13
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))),
which again simplifies, rewriting with TIMES-ADD1, PLUS-COMMUTATIVITY1, and
CORRECTNESS-OF-CANCEL-LESSP-PLUS, and expanding FIX, to:
(IMPLIES
(AND
(NOT (LESSP (LOG 2 (QUOTIENT (DIFFERENCE J I) 2))
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(NOT (LESSP (DIFFERENCE J I)
(TIMES 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(LESSP I J)
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
(NOT (EQUAL J (ADD1 I))))
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(QUOTIENT (DIFFERENCE J I) 2))))
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES
(AND
(NOT (LESSP (LOG 2 (QUOTIENT (DIFFERENCE J I) 2))
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(NOT (LESSP (DIFFERENCE J I)
(TIMES 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(LESSP I J)
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(DIFFERENCE (SUB1 J)
(QUOTIENT (PLUS I J) 2)))))
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J)))
(EQUAL J (ADD1 I)))
(NOT (LESSP (PLUS 26 (TIMES 13 0))
(PLUS 13
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))),
which again simplifies, rewriting with SUB1-ADD1, SUB1-TYPE-RESTRICTION,
QUOTIENT-2X-ADD1, DIFFERENCE-X-X, LESSP-SUB1, PLUS-ADD1, PLUS-COMMUTATIVITY,
and BSEARCH1-T-0, and opening up the functions DIFFERENCE, ADD1, LOG, EQUAL,
LESSP, TIMES, PLUS, and QUOTIENT, to:
T.
Q.E.D.
[ 0.0 7.1 0.0 ]
BSEARCH1-T-CROCK
(PROVE-LEMMA BSEARCH1-T-UBOUND
(REWRITE)
(NOT (LESSP (PLUS 26
(TIMES 13 (LOG 2 (DIFFERENCE J I))))
(BSEARCH1-T X LST I J)))
((ENABLE SPLUS)))
WARNING: Note that the proposed lemma BSEARCH1-T-UBOUND is to be stored as
zero type prescription rules, zero compound recognizer rules, one linear rule,
and zero replacement rules.
Give the conjecture the name *1.
Let us appeal to the induction principle. There are three plausible
inductions. They merge into two likely candidate inductions, both of which
are unflawed. So we will choose the one suggested by the largest number of
nonprimitive recursive functions. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(p (QUOTIENT (PLUS I J) 2) I X LST))
(p J I X LST))
(IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(p J
(ADD1 (QUOTIENT (PLUS I J) 2))
X LST))
(p J I X LST))
(IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(NOT (ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)))
(p J I X LST))
(IMPLIES (NOT (LESSP I J))
(p J I X LST))).
Linear arithmetic and the lemma MEAN-BOUNDS establish that the measure
(DIFFERENCE J I) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme produces four
new goals:
Case 4. (IMPLIES
(AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(DIFFERENCE (QUOTIENT (PLUS I J) 2)
I))))
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))
(NOT (LESSP (PLUS 26
(TIMES 13 (LOG 2 (DIFFERENCE J I))))
(BSEARCH1-T X LST I J)))),
which simplifies, using linear arithmetic, rewriting with the lemma
MEAN-DIFFERENCE-1, and unfolding the functions BSEARCH1-T and SPLUS, to:
(IMPLIES
(AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(QUOTIENT (DIFFERENCE J I) 2))))
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))
(NOT (LESSP (PLUS 26
(TIMES 13 (LOG 2 (DIFFERENCE J I))))
(PLUS 10
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))).
But this again simplifies, rewriting with DIFFERENCE=0, DIFFERENCE-IS-1,
SUB1-OF-1, and LESSP-OF-1, and expanding the functions LESSP, SUB1, NUMBERP,
EQUAL, and LOG, to the following two new formulas:
Case 4.2.
(IMPLIES
(AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(QUOTIENT (DIFFERENCE J I) 2))))
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2))))
(NOT (EQUAL J (ADD1 I))))
(NOT
(LESSP (PLUS 26
(TIMES 13
(ADD1 (LOG 2
(QUOTIENT (DIFFERENCE J I) 2)))))
(PLUS 10
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))).
However this again simplifies, applying the lemmas TIMES-ADD1 and
PLUS-COMMUTATIVITY1, to:
(IMPLIES
(AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(QUOTIENT (DIFFERENCE J I) 2))))
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2))))
(NOT (EQUAL J (ADD1 I))))
(NOT (LESSP (PLUS 13 26
(TIMES 13
(LOG 2
(QUOTIENT (DIFFERENCE J I) 2))))
(PLUS 10
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 4.1.
(IMPLIES
(AND (LESSP I J)
(ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2) LST))
(NOT (LESSP (PLUS 26
(TIMES 13
(LOG 2
(QUOTIENT (DIFFERENCE J I) 2))))
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2))))
(EQUAL J (ADD1 I)))
(NOT (LESSP (PLUS 26 (TIMES 13 0))
(PLUS 10
(BSEARCH1-T X LST I
(QUOTIENT (PLUS I J) 2)))))),
which again simplifies, rewriting with the lemmas LESSP-SUB1, SUB1-ADD1,
QUOTIENT-2X-ADD1, SUB1-TYPE-RESTRICTION, PLUS-ADD1, PLUS-COMMUTATIVITY,
and BSEARCH1-T-0, and expanding the functions LESSP, NUMBERP, EQUAL,
DIFFERENCE, QUOTIENT, LOG, TIMES, PLUS, BSEARCH1-T, and ADD1, to:
T.
Case 3. (IMPLIES
(AND
(LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)
(NOT
(LESSP
(PLUS 26
(TIMES 13
(LOG 2
(DIFFERENCE J
(ADD1 (QUOTIENT (PLUS I J) 2))))))
(BSEARCH1-T X LST
(ADD1 (QUOTIENT (PLUS I J) 2))
J))))
(NOT (LESSP (PLUS 26
(TIMES 13 (LOG 2 (DIFFERENCE J I))))
(BSEARCH1-T X LST I J)))),
which simplifies, using linear arithmetic, applying ILESSP-ENTAILS-ILEQ,
SUB1-ADD1, BSEARCH1-T-CROCK, and DIFFERENCE-0, and opening up the
definitions of DIFFERENCE, BSEARCH1-T, SPLUS, LOG, TIMES, PLUS, LESSP, and
EQUAL, to:
T.
Case 2. (IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(NOT (ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)))
(NOT (LESSP (PLUS 26
(TIMES 13 (LOG 2 (DIFFERENCE J I))))
(BSEARCH1-T X LST I J)))).
This simplifies, rewriting with the lemma LEQ-TRANS, and unfolding the
definition of BSEARCH1-T, to the new conjecture:
(IMPLIES (AND (LESSP I J)
(NOT (ILESSP X
(GET-NTH (QUOTIENT (PLUS I J) 2)
LST)))
(NOT (ILESSP (GET-NTH (QUOTIENT (PLUS I J) 2) LST)
X)))
(NOT (LESSP (PLUS 26
(TIMES 13 (LOG 2 (DIFFERENCE J I))))
13))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (NOT (LESSP I J))
(NOT (LESSP (PLUS 26
(TIMES 13 (LOG 2 (DIFFERENCE J I))))
(BSEARCH1-T X LST I J)))),
which simplifies, applying DIFFERENCE-0, and opening up the functions LOG,
TIMES, PLUS, BSEARCH1-T, and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 1.1 0.0 ]
BSEARCH1-T-UBOUND
(DISABLE BSEARCH1-T-CROCK)
[ 0.0 0.0 0.0 ]
BSEARCH1-T-CROCK-OFF
(PROVE-LEMMA BSEARCH-T-UBOUND-LA NIL
(LEQ (BSEARCH-T X N LST)
(PLUS 32 (TIMES 13 (LOG 2 N))))
((ENABLE SPLUS BSEARCH-T)))
This conjecture can be simplified, using the abbreviations NOT, SPLUS, and
BSEARCH-T, to the formula:
(NOT (LESSP (PLUS 32 (TIMES 13 (LOG 2 N)))
(PLUS 6 (BSEARCH1-T X LST 0 N)))).
Name the above subgoal *1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (OR (ZEROP 2) (EQUAL 2 1))
(p N X LST))
(IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1)))
(LESSP N 2))
(p N X LST))
(IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1)))
(NOT (LESSP N 2))
(p (QUOTIENT N 2) X LST))
(p N X LST))).
Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP,
COUNT-NOT-LESSP, and COUNT-NUMBERP, and the definitions of OR and ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme leads
to the following three new goals:
Case 3. (IMPLIES (OR (ZEROP 2) (EQUAL 2 1))
(NOT (LESSP (PLUS 32 (TIMES 13 (LOG 2 N)))
(PLUS 6 (BSEARCH1-T X LST 0 N))))).
This simplifies, opening up the functions ZEROP, EQUAL, and OR, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1)))
(LESSP N 2))
(NOT (LESSP (PLUS 32 (TIMES 13 (LOG 2 N)))
(PLUS 6 (BSEARCH1-T X LST 0 N))))).
This simplifies, rewriting with LESSP-OF-1, SUB1-OF-1, and BSEARCH1-T-0, and
unfolding the definitions of ZEROP, EQUAL, OR, SUB1, NUMBERP, LESSP, LOG,
TIMES, PLUS, BSEARCH1-T, ADD1, SPLUS, and QUOTIENT, to three new formulas:
Case 2.3.
(IMPLIES (AND (EQUAL N 1)
(NOT (ILESSP X (GET-NTH 0 LST)))
(ILESSP (GET-NTH 0 LST) X))
(NOT (LESSP 32 (PLUS 6 19)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES (AND (EQUAL N 1)
(NOT (ILESSP X (GET-NTH 0 LST)))
(NOT (ILESSP (GET-NTH 0 LST) X)))
(NOT (LESSP 32 (PLUS 6 13)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (EQUAL N 1)
(ILESSP X (GET-NTH 0 LST)))
(NOT (LESSP 32 (PLUS 6 16)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1)))
(NOT (LESSP N 2))
(NOT (LESSP (PLUS 32
(TIMES 13 (LOG 2 (QUOTIENT N 2))))
(PLUS 6
(BSEARCH1-T X LST 0
(QUOTIENT N 2))))))
(NOT (LESSP (PLUS 32 (TIMES 13 (LOG 2 N)))
(PLUS 6 (BSEARCH1-T X LST 0 N))))),
which simplifies, applying LESSP-OF-1, SUB1-OF-1, TIMES-ADD1, and
PLUS-COMMUTATIVITY1, and unfolding the functions ZEROP, EQUAL, OR, SUB1,
NUMBERP, LESSP, and LOG, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL N 1))
(NOT (LESSP (PLUS 32
(TIMES 13 (LOG 2 (QUOTIENT N 2))))
(PLUS 6
(BSEARCH1-T X LST 0
(QUOTIENT N 2))))))
(NOT (LESSP (PLUS 13 32
(TIMES 13 (LOG 2 (QUOTIENT N 2))))
(PLUS 6 (BSEARCH1-T X LST 0 N))))),
which again simplifies, using linear arithmetic, applying BSEARCH1-T-UBOUND,
PLUS-COMMUTATIVITY1, TIMES-ADD1, SUB1-OF-1, and LESSP-OF-1, and opening up
LESSP, SUB1, NUMBERP, LOG, DIFFERENCE, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.2 0.0 ]
BSEARCH-T-UBOUND-LA
(PROVE-LEMMA BSEARCH-T-UBOUND NIL
(IMPLIES (LESSP N (EXP 2 31))
(LEQ (BSEARCH-T X N LST) 435))
((USE (TA-LEMMA-1 (X 32)
(Y 13)
(A N)
(A1 (EXP 2 31)))
(BSEARCH-T-UBOUND-LA))))
This conjecture can be simplified, using the abbreviations IMPLIES, AND, and
PLUS-LESSP-CANCEL-1, to:
(IMPLIES (AND (IMPLIES (IF (LESSP (EXP 2 31) N) F T)
(IF (LESSP (TIMES 13 (LOG 2 (EXP 2 31)))
(TIMES 13 (LOG 2 N)))
F T))
(NOT (LESSP (PLUS 32 (TIMES 13 (LOG 2 N)))
(BSEARCH-T X N LST)))
(LESSP N (EXP 2 31)))
(NOT (LESSP 435 (BSEARCH-T X N LST)))).
This simplifies, rewriting with the lemma SUB1-ADD1, and unfolding the
definitions of EXP, LOG, TIMES, IMPLIES, SUB1, NUMBERP, EQUAL, PLUS, and LESSP,
to the following two new conjectures:
Case 2. (IMPLIES (AND (LESSP 2147483648 N)
(NOT (LESSP (PLUS 31 (TIMES 13 (LOG 2 N)))
(SUB1 (BSEARCH-T X N LST))))
(LESSP N 2147483648))
(NOT (LESSP 435 (BSEARCH-T X N LST)))).
This again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP 403 (TIMES 13 (LOG 2 N))))
(NOT (LESSP (PLUS 31 (TIMES 13 (LOG 2 N)))
(SUB1 (BSEARCH-T X N LST))))
(LESSP N 2147483648))
(NOT (LESSP 435 (BSEARCH-T X N LST)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
BSEARCH-T-UBOUND