(FILECREATED "19-Nov-85 16:20:00" {ERIS}<LISPUSERS>BOYERMOOREDATA.;1 244225
changes to: (VARS BOYERMOOREDATACOMS))
(* Copyright (c) 1985 by Xerox Corporation. All rights reserved.)
(PRETTYCOMPRINT BOYERMOOREDATACOMS)
(RPAQQ BOYERMOOREDATACOMS ((COMS (FNS PROVEALL1)
(PROP DEFN)
(PROP PROVE-LEMMA))
(COMS (FNS PROVEALL2)
(PROP DEFN APPEND DELETE SUBBAGP BAGDIFF BAGINT PLUS-FRINGE PLUS-TREE CANCEL REVERSE
PLISTP EXPRESSIONP EVAL OPTIMIZE CODEGEN COMPILE EXEC EQP FLATTEN MC-FLATTEN
INTERSECT UNION NTH GREATEREQP ORDERED ADDTOLIST SORT ASSOC BOOLEAN IFF ODD EVEN1
EVEN2 DOUBLE HALF EXP COUNT-LIST NUMBER-LISTP XOR SUBST OCCUR COUNTPS-LOOP
COUNTPS- COUNTPS FACT FACT-LOOP FACT- REVERSE-LOOP REVERSE- SORT-LP POWER-EVAL
BIG-PLUS1 BIG-PLUS POWER-REP GCD DIVIDES ASSIGNMENT VALUE IF-DEPTH IF-COMPLEXITY
NORMALIZE NORMALIZED-IF-EXPRP ASSIGNEDP ASSUME-TRUE ASSUME-FALSE TAUTOLOGYP
TAUTOLOGY-CHECKER FALSIFY1 FALSIFY LEFTCOUNT GOPHER SAMEFRINGE PRIME1 PRIME
GREATEST-FACTOR PRIME-FACTORS PRIME-LIST TIMES-LIST GREATEREQPR PERM MAXIMUM
ORDERED2 DSORT ADDTOLIST2 SORT2 SIGMA PROG-TRANS-OF-SIGMA SET GET EXECUTE1
EXECUTE GET-SIMPLIFIER SET-SIMPLIFIER H-PR H-AC F0 EVEN SQUARE EVAL2 SUBST2)
(PROP PROVE-LEMMA PLUS-RIGHT-ID2 PLUS-ADD1 COMMUTATIVITY2-OF-PLUS COMMUTATIVITY-OF-PLUS
ASSOCIATIVITY-OF-PLUS PLUS-EQUAL-0 DIFFERENCE-X-X DIFFERENCE-PLUS
PLUS-CANCELLATION DIFFERENCE-0 EQUAL-DIFFERENCE-0 DIFFERENCE-CANCELLATION-0
DIFFERENCE-CANCELLATION-1 DELETE-NON-MEMBER MEMBER-DELETE COMMUTATIVITY-OF-DELETE
SUBBAGP-DELETE SUBBAGP-CDR1 SUBBAGP-CDR2 SUBBAGP-BAGINT1 SUBBAGP-BAGINT2
FORM-LSTP-APPEND FORM-LSTP-PLUS-FRINGE FORM-LSTP-DELETE FORM-LSTP-BAGDIFF
FORMP-PLUS-TREE NUMBERP-MEANING-PLUS NUMBERP-MEANING-PLUS-TREE
MEMBER-IMPLIES-PLUS-TREE-GREATEREQP PLUS-TREE-DELETE
SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP PLUS-TREE-BAGDIFF NUMBERP-MEANING-BRIDGE
BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP MEANING-PLUS-TREE-APPEND
PLUS-TREE-PLUS-FRINGE MEMBER-IMPLIES-NUMBERP CORRECTNESS-OF-CANCEL
ASSOCIATIVITY-OF-APPEND APPEND-RIGHT-ID PLISTP-REVERSE APPEND-REVERSE TIMES-ZERO2
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS TIMES-ADD1 COMMUTATIVITY-OF-TIMES
COMMUTATIVITY2-OF-TIMES ASSOCIATIVITY-OF-TIMES EQUAL-TIMES-0 CADR-CROCK
FORMP-OPTIMIZE CORRECTNESS-OF-OPTIMIZE SEQUENTIAL-EXECUTION
CORRECTNESS-OF-CODEGEN CORRECTNESS-OF-OPTIMIZING-COMPILER TRANSITIVITY-OF-LESSP
LESSP-NOT-REFLEXIVE TRICHOTOMY-OF-LESSP REVERSE-REVERSE FLATTEN-MC-FLATTEN
MEMBER-APPEND MEMBER-REVERSE LENGTH-REVERSE MEMBER-INTERSECT MEMBER-UNION
SUBSETP-UNION SUBSETP-INTERSECT TRANSITIVITY-OF-LEQ IFF-EQUAL-EQUAL NTH-0 NTH-NIL
NTH-APPEND1 ASSOCIATIVITY-OF-EQUAL EVEN1-DOUBLE HALF-DOUBLE DOUBLE-HALF
DOUBLE-TIMES-2 SUBSETP-CONS LAST-APPEND LAST-REVERSE EXP-PLUS EVEN1-EVEN2 LEQ-NTH
MEMBER-SORT LENGTH-SORT COUNT-LIST-SORT ORDERED-APPEND LEQ-HALF ORDERED-SORT
ADDTOLIST-OF-ORDERED-NUMBER-LIST SORT-OF-ORDERED-NUMBER-LIST
CROCK-DUE-TO-LACK-OF-BOUNCE SORT-ORDERED SUBST-A-A OCCUR-SUBST COUNTPS-COUNTPS
FACT-LOOP-FACT FACT-FACT REVERSE-LOOP-APPEND-REVERSE REVERSE-LOOP-REVERSE
REVERSE-APPEND REVERSE-REVERSE- ORDERED-ADDTOLIST ORDERED-SORT-LP COUNT-SORT-LP
APPEND-CANCELLATION EQUAL-LESSP DIFFERENCE-ELIM REMAINDER-QUOTIENT
POWER-EVAL-BIG-PLUS1 POWER-EVAL-BIG-PLUS REMAINDER-WRT-1 REMAINDER-WRT-12
LESSP-REMAINDER2 REMAINDER-X-X REMAINDER-QUOTIENT-ELIM LESSP-TIMES-1
LESSP-TIMES-2 LESSP-QUOTIENT1 LESSP-REMAINDER1 POWER-EVAL-POWER-REP
CORRECTNESS-OF-BIG-PLUS NUMBERP-GCD GCD-EQUAL-0 GCD-0 COMMUTATIVITY-OF-GCD
NTH-APPEND DIFFERENCE-PLUS1 DIFFERENCE-PLUS2 DIFFERENCE-PLUS-CANCELATION
TIMES-DIFFERENCE DIVIDES-TIMES DIFFERENCE-PLUS3 DIFFERENCE-ADD1-CANCELLATION
REMAINDER-ADD1 DIVIDES-PLUS-REWRITE1 DIVIDES-PLUS-REWRITE2 DIVIDES-PLUS-REWRITE
LESSP-PLUS-CANCELATION DIVIDES-PLUS-REWRITE-COMMUTED EUCLID
LESSP-TIMES-CANCELLATION LESSP-PLUS-CANCELLATION3
DISTRIBUTIVITY-OF-TIMES-OVER-GCD GCD-DIVIDES-BOTH GCD-IS-THE-GREATEST
IF-COMPLEXITY-NOT-0 IF-COMPLEXITY-GOES-DOWN1 IF-COMPLEXITY-GOES-DOWN2
ASSIGNMENT-APPEND VALUE-CAN-IGNORE-REDUNDANT-ASSIGNMENTS VALUE-SHORT-CUT
ASSIGNMENT-IMPLIES-ASSIGNED TAUTOLOGYP-IS-SOUND FALSIFY1-EXTENDS-MODELS
FALSIFY1-FALSIFIES TAUTOLOGYP-FAILS-MEANS-FALSIFY1-WINS NORMALIZE-IS-SOUND
NORMALIZE-NORMALIZES TAUTOLOGY-CHECKER-COMPLETENESS-BRIDGE
TAUTOLOGY-CHECKER-IS-COMPLETE TAUTOLOGY-CHECKER-SOUNDNESS-BRIDGE
TAUTOLOGY-CHECKER-IS-SOUND FLATTEN-SINGLETON GOPHER-PRESERVES-COUNT LISTP-GOPHER
GOPHER-RETURNS-LEFTMOST-ATOM GOPHER-RETURNS-CORRECT-STATE
CORRECTNESS-OF-SAMEFRINGE GREATEST-FACTOR-LESSP GREATEST-FACTOR-DIVIDES
GREATEST-FACTOR-0 REMAINDER-0-CROCK GREATEST-FACTOR-1 NUMBERP-GREATEST-FACTOR
TIMES-LIST-APPEND PRIME-LIST-APPEND PRIME-LIST-PRIME-FACTORS QUOTIENT-TIMES1
QUOTIENT-LESSP ENOUGH-FACTORS PRIME-FACTORIZATION-EXISTENCE TIMES-ID-IFF-1
PRIME1-BASIC GREATEREQPR-LESSP GREATEREQPR-REMAINDER PRIME-BASIC REMAINDER-GCD
REMAINDER-GCD-1 DIVIDES-TIMES1 TIMES-IDENTITY1 TIMES-IDENTITY KLUDGE-BRIDGE HACK1
PRIME-GCD GCD-DISTRIBUTES-OVER-AN-OPENED-UP-TIMES PRIME-KEY QUOTIENT-DIVIDES
LITTLE-STEP LESSP-COUNT-DELETE REMAINDER-TIMES PRIME-LIST-DELETE
DIVIDES-TIMES-LIST QUOTIENT-TIMES DISTRIBUTIVITY-OF-DIVIDES TIMES-LIST-DELETE
PRIME-LIST-TIMES-LIST IF-TIMES-THEN-DIVIDES TIMES-EQUAL-1 PRIME-MEMBER
DIVIDES-IMPLIES-TIMES PRIME-FACTORIZATION-UNIQUENESS MEMBER-MAXIMUM
LESSP-DELETE-REWRITE SORT2-GEN-1 SORT2-GEN-2 SORT2-GEN ADDTOLIST2-DELETE
DELETE-ADDTOLIST2 ADDTOLIST2-KLUDGE LESSP-MAXIMUM-ADDTOLIST2 SORT2-DELETE-CONS
SORT2-DELETE DSORT-SORT2 COUNT-LIST-SORT2 DIFFERENCE-1 FUNCTIONAL-LOOP-INVRT
CORRECTNESS-OF-FUNCTIONAL-SIGMA SIGMA-INPUT-PATH SIGMA-LOOP-INVRT
SIGMA-OUTPUT-PATH GET-SET CORRECTNESS-OF-GET-SIMPLIFIER
CORRECTNESS-OF-SET-SIMPLIFIER LENGTH-5 LENGTH-CONS6 EXECUTE1-1 EXECUTE1-3
EXECUTE1-4 EXECUTE1-OPENED-UP EXECUTE-OPENED-UP INTERPRETER-LOOP-INVRT
INTERPRETER-INPUT-PATH CORRECTNESS-OF-INTERPRETED-SIGMA DIFFERENCE-2 HALF-PLUS
SIGMA-IS-HALF-PRODUCT H-LEMMA H-EQ F0-SATISFIES-F91-EQUATION F91-IS-F0 TIMES-1
TIMES-2 EXP-OF-0 EXP-OF-1 EXP-BY-0 EXP-TIMES EXP-EXP REMAINDER-PLUS-TIMES-1
REMAINDER-PLUS-TIMES-2 REMAINDER-TIMES-1 REMAINDER-OF-1 EQUAL-LENGTH-0
LENGTH-DELETE REMAINDER-DIFFERENCE-TIMES PRIME-KEY-REWRITE
TIMES-TIMES-LIST-DELETE LESSP-REMAINDER-DIVISOR SUBST2-OK))
(COMS (FNS PROVEALL3)
(PROP DEFN CRYPT PDIFFERENCE ALL-DISTINCT ALL-LESSEQP ALL-NON-ZEROP POSITIVES
PIGEON-HOLE-INDUCTION S)
(PROP PROVE-LEMMA TIMES-MOD-1 TIMES-MOD-2 CRYPT-CORRECT TIMES-MOD-3 REMAINDER-EXP-LEMMA
REMAINDER-EXP EXP-MOD-IS-1 TIMES-DISTRIBUTES-OVER-PDIFFERENCE EQUAL-MODS-TRICK-1
EQUAL-MODS-TRICK-2 PRIME-KEY-TRICK PRODUCT-DIVIDES-LEMMA PRODUCT-DIVIDES
THM-53-SPECIALIZED-TO-PRIMES COROLLARY-53 THM-55-SPECIALIZED-TO-PRIMES
COROLLARY-55 LISTP-POSITIVES CAR-POSITIVES MEMBER-POSITIVES ALL-NON-ZEROP-DELETE
ALL-DISTINCT-DELETE PIGEON-HOLE-PRINCIPLE-LEMMA-1 PIGEON-HOLE-PRINCIPLE-LEMMA-2
PERM-MEMBER PIGEON-HOLE-PRINCIPLE PERM-TIMES-LIST TIMES-LIST-POSITIVES
TIMES-LIST-EQUAL-FACT PRIME-FACT REMAINDER-TIMES-LIST-S ALL-DISTINCT-S-LEMMA
ALL-DISTINCT-S ALL-NON-ZEROP-S ALL-LESSEQP-S LENGTH-S FERMAT-THM
CRYPT-INVERTS-STEP-1 CRYPT-INVERTS-STEP-1A CRYPT-INVERTS-STEP-1B
CRYPT-INVERTS-STEP-2 CRYPT-INVERTS))
(COMS (FNS PROVEALL4)
(PROP DEFN INVERSE INVERSE-LIST PIGEONHOLE2-INDUCTION)
(PROP PROVE-LEMMA INVERSE-INVERTS-LEMMA INVERSE-INVERTS INVERSE-IS-UNIQUE
S-P-I-I-LEMMA1 S-P-I-I-LEMMA2 SUB1-P-IS-INVOLUTION N-O-I-LEMMA1 N-O-I-LEMMA2
N-O-I-LEMMA3 N-O-I-LEMMA4 NO-OTHER-INVOLUTIONS I-O-I-LEMMA INVERSE-OF-INVERSE
N-Z-I-LEMMA NON-ZEROP-INVERSE B-I-LEMMA2 B-I-LEMMA1 BOUNDED-INVERSE
ALL-NON-ZEROP-INVERSE-LIST BOUNDED-INVERSE-LIST SUBSETP-POSITIVES INVERSE-1
A-D-I-L-LEMMA1 A-D-I-L-LEMMA2 A-D-I-L-LEMMA3 ALL-DISTINCT-INVERSE-LIST
T-I-L-LEMMA1 T-I-L-LEMMA T-I-L-LEMMA3 T-I-L-LEMMA4 TIMES-INVERSE-LIST
DELETE-X-LEAVE-A DELETE-MEMBER-LEAVE-SUBSET ALL-LESSEQP-DELETE POSITIVES-BOUNDED
SUBSETP-POSITIVES-DELETE NONZEROP-LESSEQP-ZERO PIGEONHOLE2
PERM-POSITIVES-INVERSE-LIST INVERSE-LIST-FACT W-T-LEMMA WILSON-THM))
(COMS (FNS PROVEALL5)
(PROP DEFN SQUARES RESIDUE COMPLEMENT COMP-LIST RES1 REFLECT REFLECT-LIST PLUS-LIST
QUOT-LIST REM-LIST EVEN3 WINS1 WINS LOSSES1 LOSSES MULTS QUOT-QUOT-INDUCTION
MONOTONE-QUOT-INDUCTION WINS2)
(PROP PROVE-LEMMA ALL-SQUARES-1 ALL-SQUARES-2 ALL-SQUARES EULER-1-1 EULER-1-2 EULER-1-3
EULER-1-4 EULER-1-5 EULER-1-6 EULER-1-7 EULER-1 COMPLEMENT-WORKS
BOUNDED-COMPLEMENT NON-ZEROP-COMPLEMENT COMPLEMENT-IS-UNIQUE NO-SELF-COMPLEMENT
COMPLEMENT-OF-COMPLEMENT ALL-NON-ZEROP-COMP-LIST BOUNDED-COMP-LIST
SUBSETP-POSITIVES-COMP-LIST COMP-LIST-CLOSED-1 COMP-LIST-CLOSED-2
ALL-DISTINCT-COMP-LIST-1 ALL-DISTINCT-COMP-LIST PERM-POSITIVES-COMP-LIST
COMP-LIST-FACT TIMES-MOD-4 TIMES-COMP-LIST-1 TIMES-COMP-LIST-2 QUOTIENT-PLUS-1
TIMES-COMP-LIST-3 TIMES-COMP-LIST-4 TIMES-COMP-LIST-5 TIMES-COMP-LIST
SUB1-LENGTH-DELETE EQUAL-LENGTH-PERM LENGTH-POSITIVES EULER-2-1 EULER-2-2
EULER-2-3 EULER-2-4 EULER-2 DIFF-MOD-1 REM-DIFF-TIMES
REFLECT-COMMUTES-WITH-TIMES-1 REFLECT-COMMUTES-WITH-TIMES-2 TIMES-EXP-FACT
REM-REFLECT-LIST-1 REM-REFLECT-LIST-2 REM-REFLECT-LIST-3 DOUBLE-REFLECT
REM-REFLECT-LIST-4 REM-REFLECT-LIST-BASE-CASE REM-REFLECT-LIST
LENGTH-REFLECT-LIST ALL-LESSEQP-REFLECT-LIST-1 ALL-LESSEQP-REFLECT-LIST
ALL-NON-ZEROP-REFLECT-LIST ALL-DISTINCT-REFLECT-LIST-1
ALL-DISTINCT-REFLECT-LIST-2 NUMBERP-REMAINDER ALL-DISTINCT-REFLECT-LIST-3
PLUS-MOD-1 PLUS-MOD-2 ALL-DISTINCT-REFLECT-LIST-4 ALL-DISTINCT-REFLECT-LIST-5
ALL-DISTINCT-REFLECT-LIST-6 ALL-DISTINCT-REFLECT-LIST-7
ALL-DISTINCT-REFLECT-LIST-8 ALL-DISTINCT-REFLECT-LIST-9
ALL-DISTINCT-REFLECT-LIST-10 ALL-DISTINCT-REFLECT-LIST TIMES-REFLECT-LIST
PLUS-X-X-EVEN RES1-REM-1-1 RES1-REM-1 REMAINDER-LESSP RES1-REM-2 TWO-EVEN
GAUSS-LEMMA REM-QUOT-LIST EVEN3-PLUS EVEN3-DIFF EVEN3-TIMES EVEN3-REM
EVEN3-REM-REFLECT PERM-PLUS-LIST-1 PERM-PLUS-LIST EVEN3-EVEN PLUS-REFLECT-LIST
EQUALS-HAVE-SAME-PARITY RES1-QUOT-LIST WIN-SOME-LOSE-SOME-1 WIN-SOME-LOSE-SOME-2
EQUAL-LOSSES-WINS A-WINNER-EVERY-TIME LENGTH-MULTS LEQ-N-WINS1 MONOTONE-WINS1
LEQ-TIMES-QUOT LEQ-QUOT-TIMES MONOTONE-QUOT LEQ-QUOT-TIMES-2 LEQ-QUOT-WINS1-1
LEQ-QUOT-WINS1-2 LEQ-QUOT-WINS1 LEQ-WINS2 LEQ-WINS1-N LEQ-WINS1-WINS2 LEQ-WINS1
LEQ-WINS1-QUOT EQUAL-QUOT-WINS1 EQUAL-WINS-PLUS-QUOT-LIST GAUSS-COROLLARY
RESIDUE-QUOT-LIST ALL-NON-ZEROP-MULTS EMPTY-INTERSECT-MULTS-1
EMPTY-INTERSECT-MULTS EQUAL-PLUS-QUOT-LIST-WINS LAW-OF-QUADRATIC-RECIPROCITY))
(COMS (FNS PROVEALL6)
(PROP DEFN LOGICALP EXPT ZNUMBERP ZZERO ZPLUS ZDIFFERENCE ZTIMES ZQUOTIENT ZEXPTZ
ZNORMALIZE ZEQP ZNEQP ZLESSP ZLESSEQP ZGREATERP ZGREATEREQP EXPRESSIBLE-ZNUMBERP
IABS MOD MAX0 MIN0 ISIGN IDIM DEFINEDP LEX ALMOST-EQUAL1)
(PROP PROVE-LEMMA PLUS-0 PLUS-NON-NUMBERP PLUS-ADD1 COMMUTATIVITY2-OF-PLUS
COMMUTATIVITY-OF-PLUS ASSOCIATIVITY-OF-PLUS TIMES-0 TIMES-NON-NUMBERP
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS TIMES-ADD1 COMMUTATIVITY2-OF-TIMES
COMMUTATIVITY-OF-TIMES ASSOCIATIVITY-OF-TIMES EQUAL-TIMES-0 EQUAL-LESSP
ALMOST-EQUAL1-IN-RANGE ALMOST-EQUAL1-IN-RANGE-OPENED-UP ALMOST-EQUAL1-CONTRACTS))
(COMS (FNS PROVEALL7)
(PROP DEFN HD TL EMPTY RANDOM-DELTA-WS CONTROLLER SGN NEXT-STATE FINAL-STATE-OF-VEHICLE
GOOD-STATEP ZERO-DELTA-WS APPEND FSV)
(PROP PROVE-LEMMA ZPLUS-COMM1 ZPLUS-COMM2 ZPLUS-ASSOC TL-REWRITE DOWN-ON-TL
NEXT-GOOD-STATE LENGTH-0 DECOMPOSE-LIST-OF-LENGTH-4 DRIFT-TO-0-IN-4
CANCEL-WIND-IN-4 ONCE-0-ALWAYS-0 FINAL-STATE-OF-VEHICLE-APPEND
ZERO-DELTA-WS-APPEND GOOD-STATEP-BOUNDED-ABOVE GOOD-STATEP-BOUNDED-BELOW
ZLESSP-IS-LESSP ALL-GOOD-STATES VEHICLE-STAYS-WITHIN-3-OF-COURSE
ZERO-DELTA-WS-CDDDDR GOOD-STATES-FIND-AND-STAY-AT-0
VEHICLE-GETS-ON-COURSE-IN-STEADY-WIND))
(COMS (FNS PROVEALL8)
(PROP DEFN RT NCAR NCDR NCONS NCADR NCADDR PR-APPLY NON-PR-FN COUNTER-EXAMPLE-FOR MAX
MAX2 MAX1 EXCEED EXCEED-AT)
(PROP PROVE-LEMMA TIMES-ADD1 PLUS-ADD1 SQUARE-0 SQUARE-MONOTONIC SPEC-FOR-RT
RT-IS-UNIQUE NCONS-LEMMA NCAR-NCONS NCDR-NCONS RT-LESSP RT-LESSEQP DIFFERENCE-0
LESSP-DIFFERENCE-1 NCAR-LESSEQP CROCK NCDR-LESSEQP NCDR-LESSP
NON-PR-FUNCTIONS-EXIST COUNTER-EXAMPLE-FOR-NUMERIC MAX2-GTE MAX1-GTE1 MAX1-GTE2
EXCEED-IS-BIGGER))
(COMS (FNS PROVEALL9)
(PROP DEFN GET PAIRLIST SUBRP APPLY-SUBR EV EVAL EVLIST APPEND ASSOC SUBLIS X FA VA K
OCCUR OCCUR-IN-DEFNS)
(PROP PROVE-LEMMA OCCUR-OCCUR-IN-DEFNS LEMMA1 COUNT-OCCUR COUNT-GET
COUNT-OCCUR-IN-DEFNS COROLLARY1 LEMMA2 COROLLARY2 LEMMA3 EXPAND-CIRC
UNSOLVABILITY-OF-THE-HALTING-PROBLEM))
(COMS (FNS PROVEALL10)
(PROP DEFN SYMBOL HALF-TAPE TAPE OPERATION STATE TURING-4TUPLE TURING-MACHINE INSTR
NEW-TAPE TMI INSTR-DEFN NEW-TAPE-DEFN TMI-DEFN KWOTE TMI-FA TMI-X TMI-K TMI-N CNB
INSTRN EVAL-INSTR-INDUCTION-SCHEME TMIN EVAL-TMI-INDUCTION-SCHEME)
(PROP PROVE-LEMMA LENGTH-0 PLUS-EQUAL-0 PLUS-DIFFERENCE EVAL-FN-0 EVAL-FN-1 EVAL-SUBRP
EVAL-IF EVAL-QUOTE EVAL-NLISTP EVLIST-NIL EVLIST-CONS CNB-NBTM CNB-CONS
CNB-LITATOM CNB-NUMBERP GET-TMI-FA EVAL-INSTR EVAL-NEW-TAPE CNB-INSTRN
CNB-NEW-TAPE EVAL-TMI EVAL-TMI-X INSTRN-INSTR NBTMP-INSTR INSTRN-NON-F TMIN-BTM
TMIN-TMI SYMBOL-CNB HALF-TAPE-CNB TAPE-CNB OPERATION-CNB TURING-MACHINE-CNB
TURING-COMPLETENESS-OF-LISP))
(COMS (FNS PROVEALL11)
(PROP DEFN ZLESSP ZLESSEQP ZMAX ZMIN ZSUB1 PZDIFFERENCE M1 M2 M3 TAK0 M)
(PROP PROVE-LEMMA TAK0-SATISFIES-TAK-EQUATION M1-LESSEQP-0 M1-LESSEQP-1 M1-LESSEQP-2
M1-LESSEQP-3 M2-LESSEQP-0 M2-LESSEQP-1 M2-LESSEQP-2 M2-LESSEQP-3 M3-LESSP-0
M3-LESSP-1 M3-LESSP-2 M3-LESSP-3 M-GOES-DOWN-1 M-GOES-DOWN-2 M-GOES-DOWN-3
M-GOES-DOWN-0))))
(DEFINEQ
(PROVEALL1
(LAMBDA NIL (* kbr: " 8-Nov-85 16:04")
(PROVEALL (QUOTE ((BOOT-STRAP)))
NIL
(QUOTE BOOTSTRAP))))
)
(DEFINEQ
(PROVEALL2
(LAMBDA NIL (* kbr: " 8-Nov-85 16:01")
(PROVEALL (QUOTE ((NOTE-LIB BOOTSTRAP)
(PROVE-LEMMA& PLUS-RIGHT-ID2)
(PROVE-LEMMA& PLUS-ADD1)
(PROVE-LEMMA& COMMUTATIVITY2-OF-PLUS)
(PROVE-LEMMA& COMMUTATIVITY-OF-PLUS)
(PROVE-LEMMA& ASSOCIATIVITY-OF-PLUS)
(PROVE-LEMMA& PLUS-EQUAL-0)
(PROVE-LEMMA& DIFFERENCE-X-X)
(PROVE-LEMMA& DIFFERENCE-PLUS)
(PROVE-LEMMA& PLUS-CANCELLATION)
(PROVE-LEMMA& DIFFERENCE-0)
(PROVE-LEMMA& EQUAL-DIFFERENCE-0)
(PROVE-LEMMA& DIFFERENCE-CANCELLATION-0)
(PROVE-LEMMA& DIFFERENCE-CANCELLATION-1)
(DEFN& APPEND)
(DEFN& DELETE)
(DEFN& SUBBAGP)
(DEFN& BAGDIFF)
(DEFN& BAGINT)
(PROVE-LEMMA& DELETE-NON-MEMBER)
(PROVE-LEMMA& MEMBER-DELETE)
(PROVE-LEMMA& COMMUTATIVITY-OF-DELETE)
(PROVE-LEMMA& SUBBAGP-DELETE)
(PROVE-LEMMA& SUBBAGP-CDR1)
(PROVE-LEMMA& SUBBAGP-CDR2)
(PROVE-LEMMA& SUBBAGP-BAGINT1)
(PROVE-LEMMA& SUBBAGP-BAGINT2)
(DEFN& PLUS-FRINGE)
(DEFN& PLUS-TREE)
(DEFN& CANCEL)
(PROVE-LEMMA& FORM-LSTP-APPEND)
(PROVE-LEMMA& FORM-LSTP-PLUS-FRINGE)
(PROVE-LEMMA& FORM-LSTP-DELETE)
(PROVE-LEMMA& FORM-LSTP-BAGDIFF)
(PROVE-LEMMA& FORMP-PLUS-TREE)
(PROVE-LEMMA& NUMBERP-MEANING-PLUS)
(PROVE-LEMMA& NUMBERP-MEANING-PLUS-TREE)
(PROVE-LEMMA& MEMBER-IMPLIES-PLUS-TREE-GREATEREQP)
(PROVE-LEMMA& PLUS-TREE-DELETE)
(PROVE-LEMMA& SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP)
(PROVE-LEMMA& PLUS-TREE-BAGDIFF)
(PROVE-LEMMA& NUMBERP-MEANING-BRIDGE)
(PROVE-LEMMA& BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP)
(PROVE-LEMMA& MEANING-PLUS-TREE-APPEND)
(PROVE-LEMMA& PLUS-TREE-PLUS-FRINGE)
(PROVE-LEMMA& MEMBER-IMPLIES-NUMBERP)
(PROVE-LEMMA& CORRECTNESS-OF-CANCEL)
(DEFN& REVERSE)
(PROVE-LEMMA& ASSOCIATIVITY-OF-APPEND)
(DEFN& PLISTP)
(PROVE-LEMMA& APPEND-RIGHT-ID)
(PROVE-LEMMA& PLISTP-REVERSE)
(PROVE-LEMMA& APPEND-REVERSE)
(PROVE-LEMMA& TIMES-ZERO2)
(PROVE-LEMMA& DISTRIBUTIVITY-OF-TIMES-OVER-PLUS)
(PROVE-LEMMA& TIMES-ADD1)
(PROVE-LEMMA& COMMUTATIVITY-OF-TIMES)
(PROVE-LEMMA& COMMUTATIVITY2-OF-TIMES)
(PROVE-LEMMA& ASSOCIATIVITY-OF-TIMES)
(PROVE-LEMMA& EQUAL-TIMES-0)
(ADD-SHELL PUSH NIL STACKP ((TOP (NONE-OF)
ZERO)
(POP (NONE-OF)
ZERO)))
(DCL CALL (FN X Y))
(DCL GETVALUE (VAR ENVRN))
(ADD-AXIOM NUMBERP-CALL (REWRITE)
(NUMBERP (CALL FN X Y)))
(DEFN& EXPRESSIONP)
(PROVE-LEMMA& CADR-CROCK)
(DEFN& EVAL)
(DEFN& OPTIMIZE)
(DEFN& CODEGEN)
(DEFN& COMPILE)
(PROVE-LEMMA& FORMP-OPTIMIZE)
(PROVE-LEMMA& CORRECTNESS-OF-OPTIMIZE)
(DEFN& EXEC)
(PROVE-LEMMA& SEQUENTIAL-EXECUTION)
(PROVE-LEMMA& CORRECTNESS-OF-CODEGEN)
(PROVE-LEMMA& CORRECTNESS-OF-OPTIMIZING-COMPILER)
(PROVE-LEMMA& TRANSITIVITY-OF-LESSP)
(PROVE-LEMMA& LESSP-NOT-REFLEXIVE)
(DEFN& EQP)
(PROVE-LEMMA& TRICHOTOMY-OF-LESSP)
(PROVE-LEMMA& REVERSE-REVERSE)
(DEFN& FLATTEN)
(DEFN& MC-FLATTEN)
(PROVE-LEMMA& FLATTEN-MC-FLATTEN)
(PROVE-LEMMA& MEMBER-APPEND)
(PROVE-LEMMA& MEMBER-REVERSE)
(PROVE-LEMMA& LENGTH-REVERSE)
(DEFN& INTERSECT)
(PROVE-LEMMA& MEMBER-INTERSECT)
(DEFN& UNION)
(PROVE-LEMMA& MEMBER-UNION)
(PROVE-LEMMA& SUBSETP-UNION)
(PROVE-LEMMA& SUBSETP-INTERSECT)
(DEFN& NTH)
(DEFN& GREATEREQP)
(PROVE-LEMMA& TRANSITIVITY-OF-LEQ)
(DEFN& ORDERED)
(DEFN& ADDTOLIST)
(DEFN& SORT)
(DEFN& ASSOC)
(DEFN& BOOLEAN)
(DEFN& IFF)
(PROVE-LEMMA& IFF-EQUAL-EQUAL)
(PROVE-LEMMA& NTH-0)
(PROVE-LEMMA& NTH-NIL)
(PROVE-LEMMA& NTH-APPEND1)
(PROVE-LEMMA& ASSOCIATIVITY-OF-EQUAL)
(DEFN& ODD)
(DEFN& EVEN1)
(DEFN& EVEN2)
(DEFN& DOUBLE)
(PROVE-LEMMA& EVEN1-DOUBLE)
(DEFN& HALF)
(PROVE-LEMMA& HALF-DOUBLE)
(PROVE-LEMMA& DOUBLE-HALF)
(PROVE-LEMMA& DOUBLE-TIMES-2)
(PROVE-LEMMA& SUBSETP-CONS)
(PROVE-LEMMA& LAST-APPEND)
(PROVE-LEMMA& LAST-REVERSE)
(DEFN& EXP)
(PROVE-LEMMA& EXP-PLUS)
(PROVE-LEMMA& EVEN1-EVEN2)
(PROVE-LEMMA& LEQ-NTH)
(PROVE-LEMMA& MEMBER-SORT)
(PROVE-LEMMA& LENGTH-SORT)
(DEFN& COUNT-LIST)
(PROVE-LEMMA& COUNT-LIST-SORT)
(PROVE-LEMMA& ORDERED-APPEND)
(PROVE-LEMMA& LEQ-HALF)
(DEFN& NUMBER-LISTP)
(PROVE-LEMMA& ORDERED-SORT)
(PROVE-LEMMA& ADDTOLIST-OF-ORDERED-NUMBER-LIST)
(PROVE-LEMMA& SORT-OF-ORDERED-NUMBER-LIST)
(DEFN& XOR)
(PROVE-LEMMA& CROCK-DUE-TO-LACK-OF-BOUNCE)
(PROVE-LEMMA& SORT-ORDERED)
(DEFN& SUBST)
(PROVE-LEMMA& SUBST-A-A)
(DEFN& OCCUR)
(PROVE-LEMMA& OCCUR-SUBST)
(DEFN& COUNTPS-LOOP)
(DEFN& COUNTPS-)
(DEFN& COUNTPS)
(PROVE-LEMMA& COUNTPS-COUNTPS)
(DEFN& FACT)
(DEFN& FACT-LOOP)
(DEFN& FACT-)
(PROVE-LEMMA& FACT-LOOP-FACT)
(PROVE-LEMMA& FACT-FACT)
(DEFN& REVERSE-LOOP)
(DEFN& REVERSE-)
(PROVE-LEMMA& REVERSE-LOOP-APPEND-REVERSE)
(PROVE-LEMMA& REVERSE-LOOP-REVERSE)
(PROVE-LEMMA& REVERSE-APPEND)
(PROVE-LEMMA& REVERSE-REVERSE-)
(DEFN& SORT-LP)
(PROVE-LEMMA& ORDERED-ADDTOLIST)
(PROVE-LEMMA& ORDERED-SORT-LP)
(PROVE-LEMMA& COUNT-SORT-LP)
(PROVE-LEMMA& APPEND-CANCELLATION)
(PROVE-LEMMA& EQUAL-LESSP)
(PROVE-LEMMA& DIFFERENCE-ELIM)
(DEFN& POWER-EVAL)
(DEFN& BIG-PLUS1)
(PROVE-LEMMA& REMAINDER-QUOTIENT)
(PROVE-LEMMA& POWER-EVAL-BIG-PLUS1)
(DEFN& BIG-PLUS)
(PROVE-LEMMA& POWER-EVAL-BIG-PLUS)
(PROVE-LEMMA& REMAINDER-WRT-1)
(PROVE-LEMMA& REMAINDER-WRT-12)
(PROVE-LEMMA& LESSP-REMAINDER2)
(PROVE-LEMMA& REMAINDER-X-X)
(PROVE-LEMMA& REMAINDER-QUOTIENT-ELIM)
(PROVE-LEMMA& LESSP-TIMES-1)
(PROVE-LEMMA& LESSP-TIMES-2)
(PROVE-LEMMA& LESSP-QUOTIENT1)
(PROVE-LEMMA& LESSP-REMAINDER1)
(DEFN& POWER-REP)
(PROVE-LEMMA& POWER-EVAL-POWER-REP)
(PROVE-LEMMA& CORRECTNESS-OF-BIG-PLUS)
(DEFN& GCD)
(PROVE-LEMMA& NUMBERP-GCD)
(PROVE-LEMMA& GCD-EQUAL-0)
(PROVE-LEMMA& GCD-0)
(PROVE-LEMMA& COMMUTATIVITY-OF-GCD)
(PROVE-LEMMA& NTH-APPEND)
(PROVE-LEMMA& DIFFERENCE-PLUS1)
(PROVE-LEMMA& DIFFERENCE-PLUS2)
(PROVE-LEMMA& DIFFERENCE-PLUS-CANCELATION)
(PROVE-LEMMA& TIMES-DIFFERENCE)
(DEFN& DIVIDES)
(PROVE-LEMMA& DIVIDES-TIMES)
(PROVE-LEMMA& DIFFERENCE-PLUS3)
(PROVE-LEMMA& DIFFERENCE-ADD1-CANCELLATION)
(PROVE-LEMMA& REMAINDER-ADD1)
(PROVE-LEMMA& DIVIDES-PLUS-REWRITE1)
(PROVE-LEMMA& DIVIDES-PLUS-REWRITE2)
(PROVE-LEMMA& DIVIDES-PLUS-REWRITE)
(PROVE-LEMMA& LESSP-PLUS-CANCELATION)
(PROVE-LEMMA& DIVIDES-PLUS-REWRITE-COMMUTED)
(PROVE-LEMMA& EUCLID)
(PROVE-LEMMA& LESSP-TIMES-CANCELLATION)
(PROVE-LEMMA& LESSP-PLUS-CANCELLATION3)
(PROVE-LEMMA& DISTRIBUTIVITY-OF-TIMES-OVER-GCD)
(PROVE-LEMMA& GCD-DIVIDES-BOTH)
(PROVE-LEMMA& GCD-IS-THE-GREATEST)
(ADD-SHELL CONS-IF NIL IF-EXPRP ((TEST (NONE-OF)
ZERO)
(LEFT-BRANCH (NONE-OF)
ZERO)
(RIGHT-BRANCH (NONE-OF)
ZERO)))
(DEFN& ASSIGNMENT)
(DEFN& VALUE)
(DEFN& IF-DEPTH)
(DEFN& IF-COMPLEXITY)
(PROVE-LEMMA& IF-COMPLEXITY-NOT-0)
(PROVE-LEMMA& IF-COMPLEXITY-GOES-DOWN1)
(PROVE-LEMMA& IF-COMPLEXITY-GOES-DOWN2)
(DEFN& NORMALIZE)
(DEFN& NORMALIZED-IF-EXPRP)
(DEFN& ASSIGNEDP)
(DEFN& ASSUME-TRUE)
(DEFN& ASSUME-FALSE)
(DEFN& TAUTOLOGYP)
(PROVE-LEMMA& ASSIGNMENT-APPEND)
(PROVE-LEMMA& VALUE-CAN-IGNORE-REDUNDANT-ASSIGNMENTS)
(PROVE-LEMMA& VALUE-SHORT-CUT)
(PROVE-LEMMA& ASSIGNMENT-IMPLIES-ASSIGNED)
(PROVE-LEMMA& TAUTOLOGYP-IS-SOUND)
(DEFN& TAUTOLOGY-CHECKER)
(DEFN& FALSIFY1)
(DEFN& FALSIFY)
(PROVE-LEMMA& FALSIFY1-EXTENDS-MODELS)
(PROVE-LEMMA& FALSIFY1-FALSIFIES)
(PROVE-LEMMA& TAUTOLOGYP-FAILS-MEANS-FALSIFY1-WINS)
(PROVE-LEMMA& NORMALIZE-IS-SOUND)
(PROVE-LEMMA& NORMALIZE-NORMALIZES)
(PROVE-LEMMA& TAUTOLOGY-CHECKER-COMPLETENESS-BRIDGE)
(PROVE-LEMMA& TAUTOLOGY-CHECKER-IS-COMPLETE)
(PROVE-LEMMA& TAUTOLOGY-CHECKER-SOUNDNESS-BRIDGE)
(PROVE-LEMMA& TAUTOLOGY-CHECKER-IS-SOUND)
(SWAP-OUT BASICS-TEMP)
(PROVE-LEMMA& FLATTEN-SINGLETON)
(DEFN& LEFTCOUNT)
(DEFN& GOPHER)
(PROVE-LEMMA& GOPHER-PRESERVES-COUNT)
(PROVE-LEMMA& LISTP-GOPHER)
(DEFN& SAMEFRINGE)
(PROVE-LEMMA& GOPHER-RETURNS-LEFTMOST-ATOM)
(PROVE-LEMMA& GOPHER-RETURNS-CORRECT-STATE)
(PROVE-LEMMA& CORRECTNESS-OF-SAMEFRINGE)
(DEFN& PRIME1)
(DEFN& PRIME)
(DEFN& GREATEST-FACTOR)
(PROVE-LEMMA& GREATEST-FACTOR-LESSP)
(PROVE-LEMMA& GREATEST-FACTOR-DIVIDES)
(PROVE-LEMMA& GREATEST-FACTOR-0)
(PROVE-LEMMA& REMAINDER-0-CROCK)
(PROVE-LEMMA& GREATEST-FACTOR-1)
(PROVE-LEMMA& NUMBERP-GREATEST-FACTOR)
(DEFN& PRIME-FACTORS)
(DEFN& PRIME-LIST)
(DEFN& TIMES-LIST)
(PROVE-LEMMA& TIMES-LIST-APPEND)
(PROVE-LEMMA& PRIME-LIST-APPEND)
(PROVE-LEMMA& PRIME-LIST-PRIME-FACTORS)
(PROVE-LEMMA& QUOTIENT-TIMES1)
(PROVE-LEMMA& QUOTIENT-LESSP)
(PROVE-LEMMA& ENOUGH-FACTORS)
(PROVE-LEMMA& PRIME-FACTORIZATION-EXISTENCE)
(DEFN& GREATEREQPR)
(PROVE-LEMMA& TIMES-ID-IFF-1)
(PROVE-LEMMA& PRIME1-BASIC)
(PROVE-LEMMA& GREATEREQPR-LESSP)
(PROVE-LEMMA& GREATEREQPR-REMAINDER)
(PROVE-LEMMA& PRIME-BASIC)
(PROVE-LEMMA& REMAINDER-GCD)
(PROVE-LEMMA& REMAINDER-GCD-1)
(PROVE-LEMMA& DIVIDES-TIMES1)
(PROVE-LEMMA& TIMES-IDENTITY1)
(PROVE-LEMMA& TIMES-IDENTITY)
(PROVE-LEMMA& KLUDGE-BRIDGE)
(PROVE-LEMMA& HACK1)
(PROVE-LEMMA& PRIME-GCD)
(PROVE-LEMMA& GCD-DISTRIBUTES-OVER-AN-OPENED-UP-TIMES)
(PROVE-LEMMA& PRIME-KEY)
(PROVE-LEMMA& QUOTIENT-DIVIDES)
(PROVE-LEMMA& LITTLE-STEP)
(PROVE-LEMMA& LESSP-COUNT-DELETE)
(DEFN& PERM)
(PROVE-LEMMA& REMAINDER-TIMES)
(PROVE-LEMMA& PRIME-LIST-DELETE)
(PROVE-LEMMA& DIVIDES-TIMES-LIST)
(PROVE-LEMMA& QUOTIENT-TIMES)
(PROVE-LEMMA& DISTRIBUTIVITY-OF-DIVIDES)
(PROVE-LEMMA& TIMES-LIST-DELETE)
(PROVE-LEMMA& PRIME-LIST-TIMES-LIST)
(PROVE-LEMMA& IF-TIMES-THEN-DIVIDES)
(PROVE-LEMMA& TIMES-EQUAL-1)
(PROVE-LEMMA& PRIME-MEMBER)
(PROVE-LEMMA& DIVIDES-IMPLIES-TIMES)
(PROVE-LEMMA& PRIME-FACTORIZATION-UNIQUENESS)
(DEFN& MAXIMUM)
(PROVE-LEMMA& MEMBER-MAXIMUM)
(PROVE-LEMMA& LESSP-DELETE-REWRITE)
(DEFN& ORDERED2)
(DEFN& DSORT)
(DEFN& ADDTOLIST2)
(DEFN& SORT2)
(PROVE-LEMMA& SORT2-GEN-1)
(PROVE-LEMMA& SORT2-GEN-2)
(PROVE-LEMMA& SORT2-GEN)
(PROVE-LEMMA& ADDTOLIST2-DELETE)
(PROVE-LEMMA& DELETE-ADDTOLIST2)
(PROVE-LEMMA& ADDTOLIST2-KLUDGE)
(PROVE-LEMMA& LESSP-MAXIMUM-ADDTOLIST2)
(PROVE-LEMMA& SORT2-DELETE-CONS)
(PROVE-LEMMA& SORT2-DELETE)
(PROVE-LEMMA& DSORT-SORT2)
(PROVE-LEMMA& COUNT-LIST-SORT2)
(* The next segment of this XXX illustrates three different program verification methods: the functional approach,
the inductive assertion approach, and the interpreter approach. The program considered is a simple loop for summing
the numbers from I down to 0 *)
(DEFN& SIGMA)
(PROVE-LEMMA& DIFFERENCE-1)
(DEFN& PROG-TRANS-OF-SIGMA)
(PROVE-LEMMA& FUNCTIONAL-LOOP-INVRT)
(PROVE-LEMMA& CORRECTNESS-OF-FUNCTIONAL-SIGMA)
(PROVE-LEMMA& SIGMA-INPUT-PATH)
(PROVE-LEMMA& SIGMA-LOOP-INVRT)
(PROVE-LEMMA& SIGMA-OUTPUT-PATH)
(* The interpreter we consider fetches instructions out of the same memory being modified by the execution.
Earlier we proved a simpler version in which the program was in read-only memory. The new approach is almost
identical but we have to force the opening up of certain functions because instead of doing CDR recursion the
interpreter EXECUTE1 has to count the PC up and the theorem prover doesn't handle counting up very well yet.
*)
(DEFN& SET)
(DEFN& GET)
(PROVE-LEMMA& GET-SET)
(DEFN& EXECUTE1)
(DEFN& EXECUTE)
(DEFN& GET-SIMPLIFIER)
(PROVE-LEMMA& CORRECTNESS-OF-GET-SIMPLIFIER)
(DEFN& SET-SIMPLIFIER)
(PROVE-LEMMA& CORRECTNESS-OF-SET-SIMPLIFIER)
(PROVE-LEMMA& LENGTH-5)
(PROVE-LEMMA& LENGTH-CONS6)
(PROVE-LEMMA& EXECUTE1-1)
(PROVE-LEMMA& EXECUTE1-3)
(PROVE-LEMMA& EXECUTE1-4)
(PROVE-LEMMA& EXECUTE1-OPENED-UP)
(PROVE-LEMMA& EXECUTE-OPENED-UP)
(PROVE-LEMMA& INTERPRETER-LOOP-INVRT)
(PROVE-LEMMA& INTERPRETER-INPUT-PATH)
(PROVE-LEMMA& CORRECTNESS-OF-INTERPRETED-SIGMA)
(PROVE-LEMMA& DIFFERENCE-2)
(PROVE-LEMMA& HALF-PLUS)
(PROVE-LEMMA& SIGMA-IS-HALF-PRODUCT)
(DCL H (X Y))
(ADD-AXIOM H-COMMUTIVITY2 (REWRITE)
(EQUAL (H X (H Y Z))
(H Y (H X Z))))
(DEFN& H-PR)
(DEFN& H-AC)
(PROVE-LEMMA& H-LEMMA)
(PROVE-LEMMA& H-EQ)
(DEFN& F0)
(PROVE-LEMMA& F0-SATISFIES-F91-EQUATION)
(REFLECT F91 F0-SATISFIES-F91-EQUATION ((LESSP (DIFFERENCE 101 X))))
(PROVE-LEMMA& F91-IS-F0)
(DEFN& EVEN)
(DEFN& SQUARE)
(PROVE-LEMMA& TIMES-1)
(PROVE-LEMMA& TIMES-2)
(PROVE-LEMMA& EXP-OF-0)
(PROVE-LEMMA& EXP-OF-1)
(PROVE-LEMMA& EXP-BY-0)
(PROVE-LEMMA& EXP-TIMES)
(PROVE-LEMMA& EXP-EXP)
(PROVE-LEMMA& REMAINDER-PLUS-TIMES-1)
(PROVE-LEMMA& REMAINDER-PLUS-TIMES-2)
(PROVE-LEMMA& REMAINDER-TIMES-1)
(PROVE-LEMMA& REMAINDER-OF-1)
(PROVE-LEMMA& EQUAL-LENGTH-0)
(PROVE-LEMMA& LENGTH-DELETE)
(PROVE-LEMMA& REMAINDER-DIFFERENCE-TIMES)
(PROVE-LEMMA& PRIME-KEY-REWRITE)
(PROVE-LEMMA& TIMES-TIMES-LIST-DELETE)
(PROVE-LEMMA& LESSP-REMAINDER-DIVISOR)
(DCL APPLY2 (FN X Y))
(DEFN& EVAL2)
(DEFN& SUBST2)
(PROVE-LEMMA& SUBST2-OK)))
NIL
(QUOTE BASICS))))
)
(PUTPROPS APPEND DEFN ((X Y)
(IF (LISTP X)
(CONS (CAR X)
(APPEND (CDR X)
Y))
Y)))
(PUTPROPS DELETE DEFN ((X Y)
(IF (LISTP Y)
(IF (EQUAL X (CAR Y))
(CDR Y)
(CONS (CAR Y)
(DELETE X (CDR Y))))
Y)))
(PUTPROPS SUBBAGP DEFN ((X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X)
Y)
(SUBBAGP (CDR X)
(DELETE (CAR X)
Y))
F)
T)))
(PUTPROPS BAGDIFF DEFN ((X Y)
(IF (LISTP Y)
(IF (MEMBER (CAR Y)
X)
(BAGDIFF (DELETE (CAR Y)
X)
(CDR Y))
(BAGDIFF X (CDR Y)))
X)))
(PUTPROPS BAGINT DEFN ((X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X)
Y)
(CONS (CAR X)
(BAGINT (CDR X)
(DELETE (CAR X)
Y)))
(BAGINT (CDR X)
Y))
NIL)))
(PUTPROPS PLUS-FRINGE DEFN ((X)
(IF (AND (LISTP X)
(EQUAL (CAR X)
(QUOTE PLUS)))
(APPEND (PLUS-FRINGE (CADR X))
(PLUS-FRINGE (CADDR X)))
(CONS X NIL))))
(PUTPROPS PLUS-TREE DEFN ((L)
(IF (NLISTP L)
(QUOTE (QUOTE 0))
(IF (NLISTP (CDR L))
(LIST (QUOTE FIX)
(CAR L))
(IF (NLISTP (CDDR L))
(LIST (QUOTE PLUS)
(CAR L)
(CADR L))
(LIST (QUOTE PLUS)
(CAR L)
(PLUS-TREE (CDR L))))))))
(PUTPROPS CANCEL DEFN ((X)
(IF (AND (LISTP X)
(EQUAL (CAR X)
(QUOTE EQUAL)))
(IF (AND (LISTP (CADR X))
(EQUAL (CAADR X)
(QUOTE PLUS))
(LISTP (CADDR X))
(EQUAL (CAADDR X)
(QUOTE PLUS)))
(LIST (QUOTE EQUAL)
(PLUS-TREE (BAGDIFF (PLUS-FRINGE (CADR X))
(BAGINT (PLUS-FRINGE (CADR X))
(PLUS-FRINGE (CADDR X)))))
(PLUS-TREE (BAGDIFF (PLUS-FRINGE (CADDR X))
(BAGINT (PLUS-FRINGE (CADR X))
(PLUS-FRINGE (CADDR X))))))
(IF (AND (LISTP (CADR X))
(EQUAL (CAADR X)
(QUOTE PLUS))
(MEMBER (CADDR X)
(PLUS-FRINGE (CADR X))))
(LIST (QUOTE IF)
(LIST (QUOTE NUMBERP)
(CADDR X))
(LIST (QUOTE EQUAL)
(PLUS-TREE (DELETE (CADDR X)
(PLUS-FRINGE (CADR X))))
(QUOTE (QUOTE 0)))
(LIST (QUOTE QUOTE)
F))
(IF (AND (LISTP (CADDR X))
(EQUAL (CAADDR X)
(QUOTE PLUS))
(MEMBER (CADR X)
(PLUS-FRINGE (CADDR X))))
(LIST (QUOTE IF)
(LIST (QUOTE NUMBERP)
(CADR X))
(LIST (QUOTE EQUAL)
(QUOTE (QUOTE 0))
(PLUS-TREE (DELETE (CADR X)
(PLUS-FRINGE (CADDR X)))))
(LIST (QUOTE QUOTE)
F))
X)))
X)))
(PUTPROPS REVERSE DEFN ((X)
(IF (LISTP X)
(APPEND (REVERSE (CDR X))
(CONS (CAR X)
NIL))
NIL)))
(PUTPROPS PLISTP DEFN ((X)
(IF (LISTP X)
(PLISTP (CDR X))
(EQUAL X NIL))))
(PUTPROPS EXPRESSIONP DEFN ((X)
(IF (LISTP X)
(IF (LISTP (CAR X))
F
(IF (LISTP (CDR X))
(IF (LISTP (CDDR X))
(IF (EXPRESSIONP (CADR X))
(EXPRESSIONP (CADDR X))
F)
F)
F))
T)))
(PUTPROPS EVAL DEFN ((FORM ENVRN)
(IF (NUMBERP FORM)
FORM
(IF (LISTP (CDDR FORM))
(CALL (CAR FORM)
(EVAL (CADR FORM)
ENVRN)
(EVAL (CADDR FORM)
ENVRN))
(GETVALUE FORM ENVRN)))))
(PUTPROPS OPTIMIZE DEFN ((FORM)
(IF (LISTP (CDDR FORM))
(IF (NUMBERP (OPTIMIZE (CADR FORM)))
(IF (NUMBERP (OPTIMIZE (CADDR FORM)))
(CALL (CAR FORM)
(OPTIMIZE (CADR FORM))
(OPTIMIZE (CADDR FORM)))
(LIST (CAR FORM)
(OPTIMIZE (CADR FORM))
(OPTIMIZE (CADDR FORM))))
(LIST (CAR FORM)
(OPTIMIZE (CADR FORM))
(OPTIMIZE (CADDR FORM))))
FORM)))
(PUTPROPS CODEGEN DEFN ((FORM INS)
(IF (NUMBERP FORM)
(CONS (LIST (QUOTE PUSHI)
FORM)
INS)
(IF (LISTP (CDDR FORM))
(CONS (CAR FORM)
(CODEGEN (CADDR FORM)
(CODEGEN (CADR FORM)
INS)))
(CONS (LIST (QUOTE PUSHV)
FORM)
INS)))))
(PUTPROPS COMPILE DEFN ((FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
NIL))))
(PUTPROPS EXEC DEFN ((PC PDS ENVRN)
(IF (NLISTP PC)
PDS
(IF (LISTP (CAR PC))
(IF (EQUAL (CAAR PC)
(QUOTE PUSHI))
(EXEC (CDR PC)
(PUSH (CADAR PC)
PDS)
ENVRN)
(EXEC (CDR PC)
(PUSH (GETVALUE (CADAR PC)
ENVRN)
PDS)
ENVRN))
(EXEC (CDR PC)
(PUSH (CALL (CAR PC)
(TOP (POP PDS))
(TOP PDS))
(POP (POP PDS)))
ENVRN)))))
(PUTPROPS EQP DEFN ((X Y)
(EQUAL (FIX X)
(FIX Y))))
(PUTPROPS FLATTEN DEFN ((X)
(IF (LISTP X)
(APPEND (FLATTEN (CAR X))
(FLATTEN (CDR X)))
(CONS X NIL))))
(PUTPROPS MC-FLATTEN DEFN ((X Y)
(IF (LISTP X)
(MC-FLATTEN (CAR X)
(MC-FLATTEN (CDR X)
Y))
(CONS X Y))))
(PUTPROPS INTERSECT DEFN ((X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X)
Y)
(CONS (CAR X)
(INTERSECT (CDR X)
Y))
(INTERSECT (CDR X)
Y))
NIL)))
(PUTPROPS UNION DEFN ((X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X)
Y)
(UNION (CDR X)
Y)
(CONS (CAR X)
(UNION (CDR X)
Y)))
Y)))
(PUTPROPS NTH DEFN ((X N)
(IF (ZEROP N)
X
(NTH (CDR X)
(SUB1 N)))))
(PUTPROPS GREATEREQP DEFN ((X Y)
(NOT (LESSP X Y))))
(PUTPROPS ORDERED DEFN ((L)
(IF (LISTP L)
(IF (LISTP (CDR L))
(IF (LESSP (CADR L)
(CAR L))
F
(ORDERED (CDR L)))
T)
T)))
(PUTPROPS ADDTOLIST DEFN ((X L)
(IF (LISTP L)
(IF (LESSP X (CAR L))
(CONS X L)
(CONS (CAR L)
(ADDTOLIST X (CDR L))))
(CONS X NIL))))
(PUTPROPS SORT DEFN ((L)
(IF (LISTP L)
(ADDTOLIST (CAR L)
(SORT (CDR L)))
NIL)))
(PUTPROPS ASSOC DEFN ((X Y)
(IF (LISTP Y)
(IF (EQUAL X (CAAR Y))
(CAR Y)
(ASSOC X (CDR Y)))
NIL)))
(PUTPROPS BOOLEAN DEFN ((X)
(OR (EQUAL X T)
(EQUAL X F))))
(PUTPROPS IFF DEFN ((X Y)
(AND (IMPLIES X Y)
(IMPLIES Y X))))
(PUTPROPS ODD DEFN ((X)
(IF (ZEROP X)
F
(IF (ZEROP (SUB1 X))
T
(ODD (SUB1 (SUB1 X)))))))
(PUTPROPS EVEN1 DEFN ((X)
(IF (ZEROP X)
T
(ODD (SUB1 X)))))
(PUTPROPS EVEN2 DEFN ((X)
(IF (ZEROP X)
T
(IF (ZEROP (SUB1 X))
F
(EVEN2 (SUB1 (SUB1 X)))))))
(PUTPROPS DOUBLE DEFN ((I)
(IF (ZEROP I)
0
(ADD1 (ADD1 (DOUBLE (SUB1 I)))))))
(PUTPROPS HALF DEFN ((I)
(IF (ZEROP I)
0
(IF (ZEROP (SUB1 I))
0
(ADD1 (HALF (SUB1 (SUB1 I))))))))
(PUTPROPS EXP DEFN ((I J)
(IF (ZEROP J)
1
(TIMES I (EXP I (SUB1 J))))))
(PUTPROPS COUNT-LIST DEFN ((A L)
(IF (LISTP L)
(IF (EQUAL A (CAR L))
(ADD1 (COUNT-LIST A (CDR L)))
(COUNT-LIST A (CDR L)))
0)))
(PUTPROPS NUMBER-LISTP DEFN ((L)
(IF (LISTP L)
(IF (NUMBERP (CAR L))
(NUMBER-LISTP (CDR L))
F)
(EQUAL L NIL))))
(PUTPROPS XOR DEFN ((P Q)
(IF Q (IF P F T)
(EQUAL P T))))
(PUTPROPS SUBST DEFN ((X Y Z)
(IF (EQUAL Y Z)
X
(IF (LISTP Z)
(CONS (SUBST X Y (CAR Z))
(SUBST X Y (CDR Z)))
Z))))
(PUTPROPS OCCUR DEFN ((X Y)
(IF (EQUAL X Y)
T
(IF (LISTP Y)
(IF (OCCUR X (CAR Y))
T
(OCCUR X (CDR Y)))
F))))
(PUTPROPS COUNTPS-LOOP DEFN ((L PRED ANS)
(IF (LISTP L)
(IF (CALL PRED (CAR L)
NIL)
(COUNTPS-LOOP (CDR L)
PRED
(ADD1 ANS))
(COUNTPS-LOOP (CDR L)
PRED ANS))
ANS)))
(PUTPROPS COUNTPS- DEFN ((L PRED)
(COUNTPS-LOOP L PRED 0)))
(PUTPROPS COUNTPS DEFN ((L PRED)
(IF (LISTP L)
(IF (CALL PRED (CAR L)
NIL)
(ADD1 (COUNTPS (CDR L)
PRED))
(COUNTPS (CDR L)
PRED))
0)))
(PUTPROPS FACT DEFN ((I)
(IF (ZEROP I)
1
(TIMES I (FACT (SUB1 I))))))
(PUTPROPS FACT-LOOP DEFN ((I ANS)
(IF (ZEROP I)
ANS
(FACT-LOOP (SUB1 I)
(TIMES I ANS)))))
(PUTPROPS FACT- DEFN ((I)
(FACT-LOOP I 1)))
(PUTPROPS REVERSE-LOOP DEFN ((X ANS)
(IF (LISTP X)
(REVERSE-LOOP (CDR X)
(CONS (CAR X)
ANS))
ANS)))
(PUTPROPS REVERSE- DEFN ((X)
(REVERSE-LOOP X NIL)))
(PUTPROPS SORT-LP DEFN ((X Y)
(IF (LISTP X)
(SORT-LP (CDR X)
(ADDTOLIST (CAR X)
Y))
Y)))
(PUTPROPS POWER-EVAL DEFN ((L BASE)
(IF (LISTP L)
(PLUS (CAR L)
(TIMES BASE (POWER-EVAL (CDR L)
BASE)))
0)))
(PUTPROPS BIG-PLUS1 DEFN ((L I BASE)
(IF (LISTP L)
(IF (ZEROP I)
L
(CONS (REMAINDER (PLUS (CAR L)
I)
BASE)
(BIG-PLUS1 (CDR L)
(QUOTIENT (PLUS (CAR L)
I)
BASE)
BASE)))
(CONS I NIL))))
(PUTPROPS BIG-PLUS DEFN ((X Y I BASE)
(IF (LISTP X)
(IF (LISTP Y)
(CONS (REMAINDER (PLUS I (PLUS (CAR X)
(CAR Y)))
BASE)
(BIG-PLUS (CDR X)
(CDR Y)
(QUOTIENT (PLUS I (PLUS (CAR X)
(CAR Y)))
BASE)
BASE))
(BIG-PLUS1 X I BASE))
(BIG-PLUS1 Y I BASE))))
(PUTPROPS POWER-REP DEFN ((I BASE)
(IF (ZEROP I)
NIL
(IF (ZEROP BASE)
(CONS I NIL)
(IF (EQUAL BASE 1)
(CONS I NIL)
(CONS (REMAINDER I BASE)
(POWER-REP (QUOTIENT I BASE)
BASE)))))))
(PUTPROPS GCD DEFN ((X Y)
(IF (ZEROP X)
(FIX Y)
(IF (ZEROP Y)
X
(IF (LESSP X Y)
(GCD X (DIFFERENCE Y X))
(GCD (DIFFERENCE X Y)
Y))))
((LEX2 (LIST (COUNT X)
(COUNT Y))))))
(PUTPROPS DIVIDES DEFN ((X Y)
(ZEROP (REMAINDER Y X))))
(PUTPROPS ASSIGNMENT DEFN ((VAR ALIST)
(IF (EQUAL VAR T)
T
(IF (EQUAL VAR F)
F
(IF (NLISTP ALIST)
F
(IF (EQUAL VAR (CAAR ALIST))
(CDAR ALIST)
(ASSIGNMENT VAR (CDR ALIST))))))))
(PUTPROPS VALUE DEFN ((X ALIST)
(IF (IF-EXPRP X)
(IF (VALUE (TEST X)
ALIST)
(VALUE (LEFT-BRANCH X)
ALIST)
(VALUE (RIGHT-BRANCH X)
ALIST))
(ASSIGNMENT X ALIST))))
(PUTPROPS IF-DEPTH DEFN ((X)
(IF (IF-EXPRP X)
(ADD1 (IF-DEPTH (TEST X)))
0)))
(PUTPROPS IF-COMPLEXITY DEFN ((X)
(IF (IF-EXPRP X)
(TIMES (IF-COMPLEXITY (TEST X))
(PLUS (IF-COMPLEXITY (LEFT-BRANCH X))
(IF-COMPLEXITY (RIGHT-BRANCH X))))
1)))
(PUTPROPS NORMALIZE DEFN ((X)
(IF (IF-EXPRP X)
(IF (IF-EXPRP (TEST X))
(NORMALIZE (CONS-IF (TEST (TEST X))
(CONS-IF (LEFT-BRANCH (TEST X))
(LEFT-BRANCH X)
(RIGHT-BRANCH X))
(CONS-IF (RIGHT-BRANCH (TEST X))
(LEFT-BRANCH X)
(RIGHT-BRANCH X))))
(CONS-IF (TEST X)
(NORMALIZE (LEFT-BRANCH X))
(NORMALIZE (RIGHT-BRANCH X))))
X)
((LEX2 (LIST (IF-COMPLEXITY X)
(IF-DEPTH X))))))
(PUTPROPS NORMALIZED-IF-EXPRP DEFN ((X)
(IF (IF-EXPRP X)
(AND (NOT (IF-EXPRP (TEST X)))
(NORMALIZED-IF-EXPRP (LEFT-BRANCH X))
(NORMALIZED-IF-EXPRP (RIGHT-BRANCH X)))
T)))
(PUTPROPS ASSIGNEDP DEFN ((VAR ALIST)
(IF (EQUAL VAR T)
T
(IF (EQUAL VAR F)
T
(IF (NLISTP ALIST)
F
(IF (EQUAL VAR (CAAR ALIST))
T
(ASSIGNEDP VAR (CDR ALIST))))))))
(PUTPROPS ASSUME-TRUE DEFN ((VAR ALIST)
(CONS (CONS VAR T)
ALIST)))
(PUTPROPS ASSUME-FALSE DEFN ((VAR ALIST)
(CONS (CONS VAR F)
ALIST)))
(PUTPROPS TAUTOLOGYP DEFN ((X ALIST)
(IF (IF-EXPRP X)
(IF (ASSIGNEDP (TEST X)
ALIST)
(IF (ASSIGNMENT (TEST X)
ALIST)
(TAUTOLOGYP (LEFT-BRANCH X)
ALIST)
(TAUTOLOGYP (RIGHT-BRANCH X)
ALIST))
(AND (TAUTOLOGYP (LEFT-BRANCH X)
(ASSUME-TRUE (TEST X)
ALIST))
(TAUTOLOGYP (RIGHT-BRANCH X)
(ASSUME-FALSE (TEST X)
ALIST))))
(ASSIGNMENT X ALIST))))
(PUTPROPS TAUTOLOGY-CHECKER DEFN ((X)
(TAUTOLOGYP (NORMALIZE X)
NIL)))
(PUTPROPS FALSIFY1 DEFN ((X ALIST)
(IF (IF-EXPRP X)
(IF (ASSIGNEDP (TEST X)
ALIST)
(IF (ASSIGNMENT (TEST X)
ALIST)
(FALSIFY1 (LEFT-BRANCH X)
ALIST)
(FALSIFY1 (RIGHT-BRANCH X)
ALIST))
(IF (FALSIFY1 (LEFT-BRANCH X)
(ASSUME-TRUE (TEST X)
ALIST))
(FALSIFY1 (LEFT-BRANCH X)
(ASSUME-TRUE (TEST X)
ALIST))
(FALSIFY1 (RIGHT-BRANCH X)
(ASSUME-FALSE (TEST X)
ALIST))))
(IF (ASSIGNEDP X ALIST)
(IF (ASSIGNMENT X ALIST)
F ALIST)
(CONS (CONS X F)
ALIST)))))
(PUTPROPS FALSIFY DEFN ((X)
(FALSIFY1 (NORMALIZE X)
NIL)))
(PUTPROPS LEFTCOUNT DEFN ((X)
(IF (NLISTP X)
0
(ADD1 (LEFTCOUNT (CAR X))))))
(PUTPROPS GOPHER DEFN ((X)
(IF (OR (NLISTP X)
(NLISTP (CAR X)))
X
(GOPHER (CONS (CAAR X)
(CONS (CDAR X)
(CDR X)))))
((LESSP (LEFTCOUNT X)))))
(PUTPROPS SAMEFRINGE DEFN ((X Y)
(IF (OR (NLISTP X)
(NLISTP Y))
(EQUAL X Y)
(AND (EQUAL (CAR (GOPHER X))
(CAR (GOPHER Y)))
(SAMEFRINGE (CDR (GOPHER X))
(CDR (GOPHER Y)))))))
(PUTPROPS PRIME1 DEFN ((X Y)
(IF (ZEROP Y)
F
(IF (EQUAL Y 1)
T
(AND (NOT (DIVIDES Y X))
(PRIME1 X (SUB1 Y)))))))
(PUTPROPS PRIME DEFN ((X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X 1))
(PRIME1 X (SUB1 X)))))
(PUTPROPS GREATEST-FACTOR DEFN ((X Y)
(IF (OR (ZEROP Y)
(EQUAL Y 1))
X
(IF (DIVIDES Y X)
Y
(GREATEST-FACTOR X (SUB1 Y))))))
(PUTPROPS PRIME-FACTORS DEFN ((X)
(IF (OR (ZEROP X)
(EQUAL (SUB1 X)
0))
NIL
(IF (PRIME1 X (SUB1 X))
(CONS X NIL)
(APPEND (PRIME-FACTORS (GREATEST-FACTOR X (SUB1 X)))
(PRIME-FACTORS (QUOTIENT X (GREATEST-FACTOR
X
(SUB1 X)))))))))
(PUTPROPS PRIME-LIST DEFN ((L)
(IF (NLISTP L)
T
(AND (PRIME (CAR L))
(PRIME-LIST (CDR L))))))
(PUTPROPS TIMES-LIST DEFN ((L)
(IF (NLISTP L)
1
(TIMES (CAR L)
(TIMES-LIST (CDR L))))))
(PUTPROPS GREATEREQPR DEFN ((W Z)
(IF (ZEROP W)
(ZEROP Z)
(IF (EQUAL W Z)
T
(GREATEREQPR (SUB1 W)
Z)))))
(PUTPROPS PERM DEFN ((A B)
(IF (NLISTP A)
(NLISTP B)
(IF (MEMBER (CAR A)
B)
(PERM (CDR A)
(DELETE (CAR A)
B))
F))))
(PUTPROPS MAXIMUM DEFN ((L)
(IF (NLISTP L)
0
(IF (LESSP (CAR L)
(MAXIMUM (CDR L)))
(MAXIMUM (CDR L))
(CAR L)))))
(PUTPROPS ORDERED2 DEFN ((L)
(IF (LISTP L)
(IF (LISTP (CDR L))
(IF (LESSP (CAR L)
(CADR L))
F
(ORDERED2 (CDR L)))
T)
T)))
(PUTPROPS DSORT DEFN ((L)
(IF (NLISTP L)
NIL
(CONS (MAXIMUM L)
(DSORT (DELETE (MAXIMUM L)
L))))))
(PUTPROPS ADDTOLIST2 DEFN ((X L)
(IF (LISTP L)
(IF (LESSP X (CAR L))
(CONS (CAR L)
(ADDTOLIST2 X (CDR L)))
(CONS X L))
(CONS X NIL))))
(PUTPROPS SORT2 DEFN ((L)
(IF (NLISTP L)
NIL
(ADDTOLIST2 (CAR L)
(SORT2 (CDR L))))))
(PUTPROPS SIGMA DEFN ((M N)
(IF (LESSP M N)
(PLUS N (SIGMA M (SUB1 N)))
0)
NIL
(* " With each program verification method we will prove that the program"
*)
(*
" computes (SIGMA 0 I) at the end of this exercise we prove that (SIGMA 0 I)"
*)
(* " is I*I+1/2." *)))
(PUTPROPS PROG-TRANS-OF-SIGMA DEFN ((I AC)
(IF (ZEROP I)
AC
(PROG-TRANS-OF-SIGMA (DIFFERENCE I 1)
(PLUS AC I)))))
(PUTPROPS SET DEFN ((ADDR VAL MEM)
(IF (ZEROP ADDR)
(CONS VAL (CDR MEM))
(CONS (CAR MEM)
(SET (SUB1 ADDR)
VAL
(CDR MEM))))))
(PUTPROPS GET DEFN ((ADDR MEM)
(IF (ZEROP ADDR)
(CAR MEM)
(GET (SUB1 ADDR)
(CDR MEM)))))
(PUTPROPS EXECUTE1 DEFN ((PC MEM MAX)
(IF
(NOT (LESSP PC MAX))
(LIST F MEM)
(IF (EQUAL (GET PC MEM)
(QUOTE (STOP)))
(LIST F MEM)
(IF (EQUAL (CAR (GET PC MEM))
(QUOTE JUMPA))
(LIST (CADR (GET PC MEM))
MEM)
(IF (EQUAL (CAR (GET PC MEM))
(QUOTE SKIPNE))
(IF (ZEROP (GET (CADR (GET PC MEM))
MEM))
(EXECUTE1 (ADD1 PC)
MEM MAX)
(EXECUTE1 (ADD1 (ADD1 PC))
MEM MAX))
(IF (EQUAL (CAR (GET PC MEM))
(QUOTE SUBI))
(EXECUTE1 (ADD1 PC)
(SET (CADR (GET PC MEM))
(DIFFERENCE (GET (CADR (GET PC MEM))
MEM)
(CADDR (GET PC MEM)))
MEM)
MAX)
(IF (EQUAL (CAR (GET PC MEM))
(QUOTE ADDI))
(EXECUTE1 (ADD1 PC)
(SET (CADR (GET PC MEM))
(PLUS (CADDR (GET PC MEM))
(GET (CADR (GET PC MEM))
MEM))
MEM)
MAX)
(IF (EQUAL (CAR (GET PC MEM))
(QUOTE ADD))
(EXECUTE1 (ADD1 PC)
(SET (CADR (GET PC MEM))
(PLUS (GET (CADDR (GET PC MEM))
MEM)
(GET (CADR (GET PC MEM))
MEM))
MEM)
MAX)
(IF (EQUAL (CAR (GET PC MEM))
(QUOTE MOVEI))
(EXECUTE1 (ADD1 PC)
(SET (CADR (GET PC MEM))
(CADDR (GET PC MEM))
MEM)
MAX)
(LIST F MEM)))))))))
((LESSP (DIFFERENCE MAX PC)))))
(PUTPROPS EXECUTE DEFN ((PC MEM CLK)
(IF (ZEROP CLK)
MEM
(IF (NUMBERP PC)
(EXECUTE (CAR (EXECUTE1 PC MEM (LENGTH MEM)))
(CADR (EXECUTE1 PC MEM (LENGTH MEM)))
(SUB1 CLK))
MEM))))
(PUTPROPS GET-SIMPLIFIER DEFN ((X)
(IF (AND (LISTP X)
(EQUAL (CAR X)
(QUOTE GET))
(LISTP (CADR X))
(EQUAL (CAR (CADR X))
(QUOTE QUOTE)))
(IF (ZEROP (CADR (CADR X)))
(LIST (QUOTE CAR)
(CADDR X))
(LIST (QUOTE GET)
(LIST (QUOTE QUOTE)
(SUB1 (CADR (CADR X))))
(LIST (QUOTE CDR)
(CADDR X))))
X)))
(PUTPROPS SET-SIMPLIFIER DEFN ((X)
(IF (AND (LISTP X)
(EQUAL (CAR X)
(QUOTE SET))
(LISTP (CADR X))
(EQUAL (CAR (CADR X))
(QUOTE QUOTE)))
(IF (ZEROP (CADR (CADR X)))
(LIST (QUOTE CONS)
(CADDR X)
(LIST (QUOTE CDR)
(CADDDR X)))
(LIST (QUOTE CONS)
(LIST (QUOTE CAR)
(CADDDR X))
(LIST (QUOTE SET)
(LIST (QUOTE QUOTE)
(SUB1 (CADR (CADR X))))
(CADDR X)
(LIST (QUOTE CDR)
(CADDDR X)))))
X)))
(PUTPROPS H-PR DEFN ((L AC)
(IF (NLISTP L)
AC
(H (CAR L)
(H-PR (CDR L)
AC)))))
(PUTPROPS H-AC DEFN ((L AC)
(IF (NLISTP L)
AC
(H-AC (CDR L)
(H (CAR L)
AC)))))
(PUTPROPS F0 DEFN ((X)
(IF (LESSP 100 X)
(DIFFERENCE X 10)
91)))
(PUTPROPS EVEN DEFN ((X)
(EQUAL 0 (REMAINDER X 2))))
(PUTPROPS SQUARE DEFN ((X)
(TIMES X X)))
(PUTPROPS EVAL2 DEFN ((FORM ENVRN)
(IF (NUMBERP FORM)
FORM
(IF (LITATOM FORM)
(CDR (ASSOC FORM ENVRN))
(IF (LISTP FORM)
(APPLY2 (CAR FORM)
(EVAL2 (CADR FORM)
ENVRN)
(EVAL2 (CADDR FORM)
ENVRN))
FORM)))))
(PUTPROPS SUBST2 DEFN ((NEW OLD TERM)
(IF (NUMBERP TERM)
TERM
(IF (LITATOM TERM)
(IF (EQUAL OLD TERM)
NEW TERM)
(IF (LISTP TERM)
(LIST (CAR TERM)
(SUBST2 NEW OLD (CADR TERM))
(SUBST2 NEW OLD (CADDR TERM)))
TERM)))))
(PUTPROPS PLUS-RIGHT-ID2 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (NUMBERP Y))
(EQUAL (PLUS X Y)
(FIX X)))))
(PUTPROPS PLUS-ADD1 PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))))
(PUTPROPS COMMUTATIVITY2-OF-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS X (PLUS Y Z))
(PLUS Y (PLUS X Z)))))
(PUTPROPS COMMUTATIVITY-OF-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS X Y)
(PLUS Y X))))
(PUTPROPS ASSOCIATIVITY-OF-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))))
(PUTPROPS PLUS-EQUAL-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (PLUS A B)
0)
(AND (ZEROP A)
(ZEROP B)))))
(PUTPROPS DIFFERENCE-X-X PROVE-LEMMA ((REWRITE)
(EQUAL (DIFFERENCE X X)
0)))
(PUTPROPS DIFFERENCE-PLUS PROVE-LEMMA ((REWRITE)
(AND (EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y)))))
(PUTPROPS PLUS-CANCELLATION PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B)
(FIX C)))))
(PUTPROPS DIFFERENCE-0 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (LESSP Y X))
(EQUAL (DIFFERENCE X Y)
0))))
(PUTPROPS EQUAL-DIFFERENCE-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL 0 (DIFFERENCE X Y))
(NOT (LESSP Y X)))))
(PUTPROPS DIFFERENCE-CANCELLATION-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X 0)
(ZEROP Y))))))
(PUTPROPS DIFFERENCE-CANCELLATION-1 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z)))))))
(PUTPROPS DELETE-NON-MEMBER PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (MEMBER X Y))
(EQUAL (DELETE X Y)
Y))))
(PUTPROPS MEMBER-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (MEMBER X (DELETE U V))
(MEMBER X V))))
(PUTPROPS COMMUTATIVITY-OF-DELETE PROVE-LEMMA ((REWRITE)
(EQUAL (DELETE X (DELETE Y Z))
(DELETE Y (DELETE X Z)))))
(PUTPROPS SUBBAGP-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (SUBBAGP X (DELETE U Y))
(SUBBAGP X Y))))
(PUTPROPS SUBBAGP-CDR1 PROVE-LEMMA ((REWRITE)
(IMPLIES (SUBBAGP X Y)
(SUBBAGP (CDR X)
Y))))
(PUTPROPS SUBBAGP-CDR2 PROVE-LEMMA ((REWRITE)
(IMPLIES (SUBBAGP X (CDR Y))
(SUBBAGP X Y))))
(PUTPROPS SUBBAGP-BAGINT1 PROVE-LEMMA ((REWRITE)
(SUBBAGP (BAGINT X Y)
X)))
(PUTPROPS SUBBAGP-BAGINT2 PROVE-LEMMA ((REWRITE)
(SUBBAGP (BAGINT X Y)
Y)))
(PUTPROPS FORM-LSTP-APPEND PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (FORM-LSTP A)
(FORM-LSTP B))
(FORM-LSTP (APPEND A B)))))
(PUTPROPS FORM-LSTP-PLUS-FRINGE PROVE-LEMMA ((REWRITE)
(IMPLIES (FORMP X)
(FORM-LSTP (PLUS-FRINGE X)))))
(PUTPROPS FORM-LSTP-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (FORM-LSTP X)
(FORM-LSTP (DELETE Y X)))))
(PUTPROPS FORM-LSTP-BAGDIFF PROVE-LEMMA ((REWRITE)
(IMPLIES (FORM-LSTP X)
(FORM-LSTP (BAGDIFF X Y)))))
(PUTPROPS FORMP-PLUS-TREE PROVE-LEMMA ((REWRITE)
(IMPLIES (FORM-LSTP X)
(FORMP (PLUS-TREE X)))))
(PUTPROPS NUMBERP-MEANING-PLUS PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (LISTP X)
(EQUAL (CAR X)
(QUOTE PLUS)))
(NUMBERP (MEANING X A)))))
(PUTPROPS NUMBERP-MEANING-PLUS-TREE PROVE-LEMMA ((REWRITE)
(NUMBERP (MEANING (PLUS-TREE L)
A))))
(PUTPROPS MEMBER-IMPLIES-PLUS-TREE-GREATEREQP PROVE-LEMMA ((REWRITE)
(IMPLIES (MEMBER X Y)
(NOT (LESSP (MEANING (PLUS-TREE Y)
A)
(MEANING X A))))))
(PUTPROPS PLUS-TREE-DELETE PROVE-LEMMA ((REWRITE)
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A)))))
(PUTPROPS SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP PROVE-LEMMA ((REWRITE)
(IMPLIES (SUBBAGP X Y)
(NOT (LESSP (MEANING (PLUS-TREE Y)
A)
(MEANING (PLUS-TREE X)
A))))))
(PUTPROPS PLUS-TREE-BAGDIFF PROVE-LEMMA ((REWRITE)
(IMPLIES (SUBBAGP X Y)
(EQUAL (MEANING (PLUS-TREE (BAGDIFF Y X))
A)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING (PLUS-TREE X)
A))))))
(PUTPROPS NUMBERP-MEANING-BRIDGE PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (MEANING Z A)
(MEANING (PLUS-TREE X)
A))
(NUMBERP (MEANING Z A)))))
(PUTPROPS BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (SUBBAGP Y (PLUS-FRINGE Z))
(EQUAL (MEANING Z A)
(MEANING (PLUS-TREE (PLUS-FRINGE Z))
A)))
(EQUAL (LESSP (MEANING Z A)
(MEANING (PLUS-TREE Y)
A))
F))))
(PUTPROPS MEANING-PLUS-TREE-APPEND PROVE-LEMMA ((REWRITE)
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A)))))
(PUTPROPS PLUS-TREE-PLUS-FRINGE PROVE-LEMMA ((REWRITE)
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A)))))
(PUTPROPS MEMBER-IMPLIES-NUMBERP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (MEMBER C (PLUS-FRINGE X))
(NUMBERP (MEANING C A)))
(NUMBERP (MEANING X A)))))
(PUTPROPS CORRECTNESS-OF-CANCEL PROVE-LEMMA (((META EQUAL))
(IMPLIES (FORMP X)
(AND (EQUAL (MEANING X A)
(MEANING (CANCEL X)
A))
(FORMP (CANCEL X))))))
(PUTPROPS ASSOCIATIVITY-OF-APPEND PROVE-LEMMA ((REWRITE)
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z)))))
(PUTPROPS APPEND-RIGHT-ID PROVE-LEMMA ((REWRITE)
(IMPLIES (PLISTP X)
(EQUAL (APPEND X NIL)
X))))
(PUTPROPS PLISTP-REVERSE PROVE-LEMMA ((GENERALIZE REWRITE)
(PLISTP (REVERSE X))))
(PUTPROPS APPEND-REVERSE PROVE-LEMMA ((REWRITE)
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A)))))
(PUTPROPS TIMES-ZERO2 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (NUMBERP Y))
(EQUAL (TIMES X Y)
0))))
(PUTPROPS DISTRIBUTIVITY-OF-TIMES-OVER-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))))
(PUTPROPS TIMES-ADD1 PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))))
(PUTPROPS COMMUTATIVITY-OF-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X Y)
(TIMES Y X))))
(PUTPROPS COMMUTATIVITY2-OF-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X (TIMES Y Z))
(TIMES Y (TIMES X Z)))))
(PUTPROPS ASSOCIATIVITY-OF-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))))
(PUTPROPS EQUAL-TIMES-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (TIMES X Y)
0)
(OR (ZEROP X)
(ZEROP Y)))))
(PUTPROPS CADR-CROCK PROVE-LEMMA ((REWRITE)
(IMPLIES (LISTP (CDDR X))
(LESSP (COUNT (CADR X))
(COUNT X)))))
(PUTPROPS FORMP-OPTIMIZE PROVE-LEMMA ((REWRITE)
(IMPLIES (EXPRESSIONP X)
(EXPRESSIONP (OPTIMIZE X)))))
(PUTPROPS CORRECTNESS-OF-OPTIMIZE PROVE-LEMMA ((REWRITE)
(IMPLIES (EXPRESSIONP X)
(EQUAL (EVAL (OPTIMIZE X)
ENVRN)
(EVAL X ENVRN)))))
(PUTPROPS SEQUENTIAL-EXECUTION PROVE-LEMMA ((REWRITE)
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN))))
(PUTPROPS CORRECTNESS-OF-CODEGEN PROVE-LEMMA ((REWRITE)
(IMPLIES (EXPRESSIONP X)
(EQUAL (EXEC (REVERSE (CODEGEN X INS))
PDS ENVRN)
(PUSH (EVAL X ENVRN)
(EXEC (REVERSE INS)
PDS ENVRN))))))
(PUTPROPS CORRECTNESS-OF-OPTIMIZING-COMPILER PROVE-LEMMA (NIL (IMPLIES (EXPRESSIONP X)
(EQUAL (EXEC (COMPILE X)
PDS ENVRN)
(PUSH (EVAL X ENVRN)
PDS)))))
(PUTPROPS TRANSITIVITY-OF-LESSP PROVE-LEMMA (NIL (IMPLIES (AND (LESSP X Y)
(LESSP Y Z))
(LESSP X Z))))
(PUTPROPS LESSP-NOT-REFLEXIVE PROVE-LEMMA (NIL (NOT (LESSP X X))))
(PUTPROPS TRICHOTOMY-OF-LESSP PROVE-LEMMA (NIL (IMPLIES (AND (NOT (EQP X Y))
(NOT (LESSP Y X)))
(LESSP X Y))))
(PUTPROPS REVERSE-REVERSE PROVE-LEMMA ((REWRITE)
(IMPLIES (PLISTP X)
(EQUAL (REVERSE (REVERSE X))
X))))
(PUTPROPS FLATTEN-MC-FLATTEN PROVE-LEMMA ((REWRITE)
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y))))
(PUTPROPS MEMBER-APPEND PROVE-LEMMA ((REWRITE)
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B)))))
(PUTPROPS MEMBER-REVERSE PROVE-LEMMA ((REWRITE)
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y))))
(PUTPROPS LENGTH-REVERSE PROVE-LEMMA ((REWRITE)
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))))
(PUTPROPS MEMBER-INTERSECT PROVE-LEMMA ((REWRITE)
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C)))))
(PUTPROPS MEMBER-UNION PROVE-LEMMA (NIL (EQUAL (MEMBER A (UNION B C))
(OR (MEMBER A B)
(MEMBER A C)))))
(PUTPROPS SUBSETP-UNION PROVE-LEMMA (NIL (IMPLIES (SUBSETP A B)
(EQUAL (UNION A B)
B))))
(PUTPROPS SUBSETP-INTERSECT PROVE-LEMMA (NIL (IMPLIES (AND (PLISTP A)
(SUBSETP A B))
(EQUAL (INTERSECT A B)
A))))
(PUTPROPS TRANSITIVITY-OF-LEQ PROVE-LEMMA (NIL (IMPLIES (AND (LEQ X Y)
(LEQ Y Z))
(LEQ X Z))))
(PUTPROPS IFF-EQUAL-EQUAL PROVE-LEMMA (NIL (IMPLIES (AND (BOOLEAN P)
(BOOLEAN Q))
(EQUAL (IFF P Q)
(EQUAL P Q)))))
(PUTPROPS NTH-0 PROVE-LEMMA ((REWRITE)
(EQUAL (NTH 0 I)
0)))
(PUTPROPS NTH-NIL PROVE-LEMMA ((REWRITE)
(EQUAL (NTH NIL I)
(IF (ZEROP I)
NIL 0))))
(PUTPROPS NTH-APPEND1 PROVE-LEMMA ((REWRITE)
(EQUAL (NTH A (PLUS I J))
(NTH (NTH A I)
J))))
(PUTPROPS ASSOCIATIVITY-OF-EQUAL PROVE-LEMMA (NIL (IMPLIES (AND (BOOLEAN A)
(AND (BOOLEAN B)
(BOOLEAN C)))
(EQUAL (EQUAL (EQUAL A B)
C)
(EQUAL A (EQUAL B C))))))
(PUTPROPS EVEN1-DOUBLE PROVE-LEMMA ((REWRITE)
(EVEN1 (DOUBLE I))))
(PUTPROPS HALF-DOUBLE PROVE-LEMMA ((REWRITE)
(IMPLIES (NUMBERP I)
(EQUAL (HALF (DOUBLE I))
I))))
(PUTPROPS DOUBLE-HALF PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NUMBERP I)
(EVEN1 I))
(EQUAL (DOUBLE (HALF I))
I))))
(PUTPROPS DOUBLE-TIMES-2 PROVE-LEMMA (NIL (EQUAL (DOUBLE I)
(TIMES 2 I))))
(PUTPROPS SUBSETP-CONS PROVE-LEMMA ((REWRITE)
(IMPLIES (SUBSETP X Y)
(SUBSETP X (CONS Z Y)))))
(PUTPROPS LAST-APPEND PROVE-LEMMA ((REWRITE)
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B)))))
(PUTPROPS LAST-REVERSE PROVE-LEMMA (NIL (IMPLIES (LISTP A)
(EQUAL (LAST (REVERSE A))
(CONS (CAR A)
NIL)))))
(PUTPROPS EXP-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K)))))
(PUTPROPS EVEN1-EVEN2 PROVE-LEMMA (NIL (EQUAL (EVEN1 X)
(EVEN2 X))))
(PUTPROPS LEQ-NTH PROVE-LEMMA (NIL (LEQ (LENGTH (NTH L I))
(LENGTH L))))
(PUTPROPS MEMBER-SORT PROVE-LEMMA (NIL (EQUAL (MEMBER A (SORT B))
(MEMBER A B))))
(PUTPROPS LENGTH-SORT PROVE-LEMMA (NIL (EQUAL (LENGTH (SORT A))
(LENGTH A))))
(PUTPROPS COUNT-LIST-SORT PROVE-LEMMA (NIL (EQUAL (COUNT-LIST A (SORT L))
(COUNT-LIST A L))))
(PUTPROPS ORDERED-APPEND PROVE-LEMMA (NIL (IMPLIES (ORDERED (APPEND A B))
(ORDERED A))))
(PUTPROPS LEQ-HALF PROVE-LEMMA (NIL (LEQ (HALF I)
I)))
(PUTPROPS ORDERED-SORT PROVE-LEMMA ((REWRITE)
(ORDERED (SORT X))))
(PUTPROPS ADDTOLIST-OF-ORDERED-NUMBER-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (ORDERED X)
(NUMBER-LISTP X)
(NUMBERP I)
(NOT (LESSP (CAR X)
I)))
(EQUAL (ADDTOLIST I X)
(CONS I X)))))
(PUTPROPS SORT-OF-ORDERED-NUMBER-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (ORDERED X)
(NUMBER-LISTP X))
(EQUAL (SORT X)
X))))
(PUTPROPS CROCK-DUE-TO-LACK-OF-BOUNCE PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL X (SORT L))
(ORDERED X))))
(PUTPROPS SORT-ORDERED PROVE-LEMMA ((REWRITE)
(IMPLIES (NUMBER-LISTP L)
(EQUAL (EQUAL (SORT L)
L)
(ORDERED L)))))
(PUTPROPS SUBST-A-A PROVE-LEMMA (NIL (EQUAL (SUBST A A B)
B)))
(PUTPROPS OCCUR-SUBST PROVE-LEMMA (NIL (IMPLIES (NOT (OCCUR A B))
(EQUAL (SUBST C A B)
B))))
(PUTPROPS COUNTPS-COUNTPS PROVE-LEMMA ((REWRITE)
(IMPLIES (NUMBERP N)
(EQUAL (COUNTPS-LOOP L PRED N)
(PLUS N (COUNTPS L PRED))))))
(PUTPROPS FACT-LOOP-FACT PROVE-LEMMA ((REWRITE)
(IMPLIES (NUMBERP I)
(EQUAL (FACT-LOOP J I)
(TIMES I (FACT J))))))
(PUTPROPS FACT-FACT PROVE-LEMMA (NIL (EQUAL (FACT- I)
(FACT I))))
(PUTPROPS REVERSE-LOOP-APPEND-REVERSE PROVE-LEMMA ((REWRITE)
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y))))
(PUTPROPS REVERSE-LOOP-REVERSE PROVE-LEMMA ((REWRITE)
(EQUAL (REVERSE-LOOP X NIL)
(REVERSE X))))
(PUTPROPS REVERSE-APPEND PROVE-LEMMA (NIL (EQUAL (REVERSE- (APPEND A B))
(APPEND (REVERSE- B)
(REVERSE- A)))))
(PUTPROPS REVERSE-REVERSE- PROVE-LEMMA (NIL (IMPLIES (PLISTP X)
(EQUAL (REVERSE- (REVERSE- X))
X))))
(PUTPROPS ORDERED-ADDTOLIST PROVE-LEMMA ((REWRITE)
(IMPLIES (ORDERED Y)
(ORDERED (ADDTOLIST X Y)))))
(PUTPROPS ORDERED-SORT-LP PROVE-LEMMA ((REWRITE)
(IMPLIES (ORDERED Y)
(ORDERED (SORT-LP X Y)))))
(PUTPROPS COUNT-SORT-LP PROVE-LEMMA ((REWRITE)
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y)))))
(PUTPROPS APPEND-CANCELLATION PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C))))
(PUTPROPS EQUAL-LESSP PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))))
(PUTPROPS DIFFERENCE-ELIM PROVE-LEMMA ((ELIM)
(IMPLIES (AND (NUMBERP Y)
(NOT (LESSP Y X)))
(EQUAL (PLUS X (DIFFERENCE Y X))
Y))))
(PUTPROPS REMAINDER-QUOTIENT PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X))))
(PUTPROPS POWER-EVAL-BIG-PLUS1 PROVE-LEMMA ((REWRITE)
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I))))
(PUTPROPS POWER-EVAL-BIG-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE))))))
(PUTPROPS REMAINDER-WRT-1 PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER Y 1)
0)))
(PUTPROPS REMAINDER-WRT-12 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (NUMBERP X))
(EQUAL (REMAINDER Y X)
(FIX Y)))))
(PUTPROPS LESSP-REMAINDER2 PROVE-LEMMA ((REWRITE GENERALIZE)
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y)))))
(PUTPROPS REMAINDER-X-X PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER X X)
0)))
(PUTPROPS REMAINDER-QUOTIENT-ELIM PROVE-LEMMA ((ELIM)
(IMPLIES (AND (NOT (ZEROP Y))
(NUMBERP X))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
X))))
(PUTPROPS LESSP-TIMES-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZEROP I))
(NOT (LESSP (TIMES I J)
J)))))
(PUTPROPS LESSP-TIMES-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZEROP I))
(NOT (LESSP (TIMES J I)
J)))))
(PUTPROPS LESSP-QUOTIENT1 PROVE-LEMMA ((REWRITE)
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1)))))))
(PUTPROPS LESSP-REMAINDER1 PROVE-LEMMA ((REWRITE)
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y))))))
(PUTPROPS POWER-EVAL-POWER-REP PROVE-LEMMA ((REWRITE)
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I))))
(PUTPROPS CORRECTNESS-OF-BIG-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
0 BASE)
BASE)
(PLUS I J))))
(PUTPROPS NUMBERP-GCD PROVE-LEMMA ((REWRITE)
(NUMBERP (GCD X Y))))
(PUTPROPS GCD-EQUAL-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (GCD X Y)
0)
(AND (ZEROP X)
(ZEROP Y)))))
(PUTPROPS GCD-0 PROVE-LEMMA ((REWRITE)
(EQUAL (GCD 0 Y)
(FIX Y))))
(PUTPROPS COMMUTATIVITY-OF-GCD PROVE-LEMMA ((REWRITE)
(EQUAL (GCD X Y)
(GCD Y X))))
(PUTPROPS NTH-APPEND PROVE-LEMMA ((REWRITE)
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A)))))))
(PUTPROPS DIFFERENCE-PLUS1 PROVE-LEMMA ((REWRITE)
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))))
(PUTPROPS DIFFERENCE-PLUS2 PROVE-LEMMA ((REWRITE)
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))))
(PUTPROPS DIFFERENCE-PLUS-CANCELATION PROVE-LEMMA ((REWRITE)
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z))))
(PUTPROPS TIMES-DIFFERENCE PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X)))))
(PUTPROPS DIVIDES-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (TIMES X Z)
Z)
0)))
(PUTPROPS DIFFERENCE-PLUS3 PROVE-LEMMA ((REWRITE)
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C))))
(PUTPROPS DIFFERENCE-ADD1-CANCELLATION PROVE-LEMMA ((REWRITE)
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y))))
(PUTPROPS REMAINDER-ADD1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP Y))
(NOT (EQUAL Y 1)))
(NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y))
Y)
0)))))
(PUTPROPS DIVIDES-PLUS-REWRITE1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER X Z)
0)
(EQUAL (REMAINDER Y Z)
0))
(EQUAL (REMAINDER (PLUS X Y)
Z)
0))))
(PUTPROPS DIVIDES-PLUS-REWRITE2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER X Z)
0)
(NOT (EQUAL (REMAINDER Y Z)
0)))
(NOT (EQUAL (REMAINDER (PLUS X Y)
Z)
0)))))
(PUTPROPS DIVIDES-PLUS-REWRITE PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (REMAINDER X Z)
0)
(EQUAL (EQUAL (REMAINDER (PLUS X Y)
Z)
0)
(EQUAL (REMAINDER Y Z)
0)))))
(PUTPROPS LESSP-PLUS-CANCELATION PROVE-LEMMA ((REWRITE)
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z))))
(PUTPROPS DIVIDES-PLUS-REWRITE-COMMUTED PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (REMAINDER X Z)
0)
(EQUAL (EQUAL (REMAINDER (PLUS Y X)
Z)
0)
(EQUAL (REMAINDER Y Z)
0)))))
(PUTPROPS EUCLID PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (REMAINDER X Z)
0)
(EQUAL (EQUAL (REMAINDER (DIFFERENCE Y X)
Z)
0)
(IF (LESSP X Y)
(EQUAL (REMAINDER Y Z)
0)
T)))))
(PUTPROPS LESSP-TIMES-CANCELLATION PROVE-LEMMA ((REWRITE)
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y)))))
(PUTPROPS LESSP-PLUS-CANCELLATION3 PROVE-LEMMA ((REWRITE)
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X)))))
(PUTPROPS DISTRIBUTIVITY-OF-TIMES-OVER-GCD PROVE-LEMMA ((REWRITE)
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y)))))
(PUTPROPS GCD-DIVIDES-BOTH PROVE-LEMMA ((REWRITE)
(AND (EQUAL (REMAINDER X (GCD X Y))
0)
(EQUAL (REMAINDER Y (GCD X Y))
0))))
(PUTPROPS GCD-IS-THE-GREATEST PROVE-LEMMA (NIL (IMPLIES (AND (NOT (ZEROP X))
(NOT (ZEROP Y))
(DIVIDES Z X)
(DIVIDES Z Y))
(LEQ Z (GCD X Y)))))
(PUTPROPS IF-COMPLEXITY-NOT-0 PROVE-LEMMA ((REWRITE)
(NOT (EQUAL (IF-COMPLEXITY X)
0))))
(PUTPROPS IF-COMPLEXITY-GOES-DOWN1 PROVE-LEMMA ((REWRITE)
(IMPLIES (IF-EXPRP X)
(LESSP (IF-COMPLEXITY (LEFT-BRANCH X))
(IF-COMPLEXITY X)))))
(PUTPROPS IF-COMPLEXITY-GOES-DOWN2 PROVE-LEMMA ((REWRITE)
(IMPLIES (IF-EXPRP X)
(LESSP (IF-COMPLEXITY (RIGHT-BRANCH X))
(IF-COMPLEXITY X)))))
(PUTPROPS ASSIGNMENT-APPEND PROVE-LEMMA ((REWRITE)
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B)))))
(PUTPROPS VALUE-CAN-IGNORE-REDUNDANT-ASSIGNMENTS PROVE-LEMMA ((REWRITE)
(AND (IMPLIES (AND (IFF VAL (ASSIGNMENT VAR A))
(VALUE X A))
(VALUE X (CONS (CONS VAR VAL)
A)))
(IMPLIES (AND (IFF VAL (ASSIGNMENT VAR A))
(NOT (VALUE X A)))
(NOT (VALUE X (CONS (CONS VAR VAL)
A)))))))
(PUTPROPS VALUE-SHORT-CUT PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (IF-EXPRP X)
(NORMALIZED-IF-EXPRP X))
(EQUAL (VALUE (TEST X)
A)
(ASSIGNMENT (TEST X)
A)))))
(PUTPROPS ASSIGNMENT-IMPLIES-ASSIGNED PROVE-LEMMA ((REWRITE)
(IMPLIES (ASSIGNMENT X A)
(ASSIGNEDP X A))))
(PUTPROPS TAUTOLOGYP-IS-SOUND PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NORMALIZED-IF-EXPRP X)
(TAUTOLOGYP X A1))
(VALUE X (APPEND A1 A2)))))
(PUTPROPS FALSIFY1-EXTENDS-MODELS PROVE-LEMMA ((REWRITE)
(IMPLIES (ASSIGNEDP X A)
(EQUAL (ASSIGNMENT X (FALSIFY1 Y A))
(IF (FALSIFY1 Y A)
(ASSIGNMENT X A)
(EQUAL X T))))))
(PUTPROPS FALSIFY1-FALSIFIES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NORMALIZED-IF-EXPRP X)
(FALSIFY1 X A))
(EQUAL (VALUE X (FALSIFY1 X A))
F))))
(PUTPROPS TAUTOLOGYP-FAILS-MEANS-FALSIFY1-WINS PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NORMALIZED-IF-EXPRP X)
(NOT (TAUTOLOGYP X A))
A)
(FALSIFY1 X A))))
(PUTPROPS NORMALIZE-IS-SOUND PROVE-LEMMA ((REWRITE)
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A))))
(PUTPROPS NORMALIZE-NORMALIZES PROVE-LEMMA ((REWRITE)
(NORMALIZED-IF-EXPRP (NORMALIZE X))))
(PUTPROPS TAUTOLOGY-CHECKER-COMPLETENESS-BRIDGE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (EQUAL (VALUE Y (FALSIFY1 X A))
(VALUE X (FALSIFY1 X A)))
(FALSIFY1 X A)
(NORMALIZED-IF-EXPRP X))
(EQUAL (VALUE Y (FALSIFY1 X A))
F))))
(PUTPROPS TAUTOLOGY-CHECKER-IS-COMPLETE PROVE-LEMMA (NIL (IMPLIES (NOT (TAUTOLOGY-CHECKER X))
(EQUAL (VALUE X (FALSIFY X))
F))))
(PUTPROPS TAUTOLOGY-CHECKER-SOUNDNESS-BRIDGE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (TAUTOLOGYP Y A1)
(NORMALIZED-IF-EXPRP Y)
(EQUAL (VALUE X A2)
(VALUE Y (APPEND A1 A2))))
(VALUE X A2))))
(PUTPROPS TAUTOLOGY-CHECKER-IS-SOUND PROVE-LEMMA (NIL (IMPLIES (TAUTOLOGY-CHECKER X)
(VALUE X A))))
(PUTPROPS FLATTEN-SINGLETON PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (FLATTEN X)
(CONS Y NIL))
(AND (NLISTP X)
(EQUAL X Y)))))
(PUTPROPS GOPHER-PRESERVES-COUNT PROVE-LEMMA ((REWRITE)
(NOT (LESSP (COUNT X)
(COUNT (GOPHER X))))))
(PUTPROPS LISTP-GOPHER PROVE-LEMMA ((REWRITE)
(EQUAL (LISTP (GOPHER X))
(LISTP X))))
(PUTPROPS GOPHER-RETURNS-LEFTMOST-ATOM PROVE-LEMMA ((REWRITE)
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
0))))
(PUTPROPS GOPHER-RETURNS-CORRECT-STATE PROVE-LEMMA ((REWRITE)
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS 0 NIL)))))
(PUTPROPS CORRECTNESS-OF-SAMEFRINGE PROVE-LEMMA ((REWRITE)
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y)))))
(PUTPROPS GREATEST-FACTOR-LESSP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (LESSP Y X)
(NOT (PRIME1 X Y))
(NOT (ZEROP X))
(NOT (EQUAL (SUB1 X)
0))
(NOT (ZEROP Y)))
(LESSP (GREATEST-FACTOR X Y)
X))))
(PUTPROPS GREATEST-FACTOR-DIVIDES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (LESSP Y X)
(NOT (PRIME1 X Y))
(NOT (ZEROP X))
(NOT (EQUAL X 1))
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X (GREATEST-FACTOR X Y))
0))))
(PUTPROPS GREATEST-FACTOR-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
0)
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X 0)))))
(PUTPROPS REMAINDER-0-CROCK PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER 0 Y)
0)
NIL
(*
" We have to prove this to get (REMAINDER 1 Y) to open in GREATEST-FACTOR-1."
*)
(* " If CURRENT-CL moved we wouldn't have to do it." *)))
(PUTPROPS GREATEST-FACTOR-1 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1))))
(PUTPROPS NUMBERP-GREATEST-FACTOR PROVE-LEMMA ((REWRITE)
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X)))))))
(PUTPROPS TIMES-LIST-APPEND PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y)))))
(PUTPROPS PRIME-LIST-APPEND PROVE-LEMMA ((REWRITE)
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y)))))
(PUTPROPS PRIME-LIST-PRIME-FACTORS PROVE-LEMMA ((REWRITE)
(PRIME-LIST (PRIME-FACTORS X))))
(PUTPROPS QUOTIENT-TIMES1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NUMBERP Y)
(NUMBERP X)
(NOT (EQUAL X 0))
(DIVIDES X Y))
(EQUAL (TIMES X (QUOTIENT Y X))
Y))))
(PUTPROPS QUOTIENT-LESSP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP X))
(LESSP X Y))
(NOT (EQUAL (QUOTIENT Y X)
0)))))
(PUTPROPS ENOUGH-FACTORS PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZEROP X))
(EQUAL (TIMES-LIST (PRIME-FACTORS X))
X))))
(PUTPROPS PRIME-FACTORIZATION-EXISTENCE PROVE-LEMMA (NIL (IMPLIES
(NOT (ZEROP X))
(AND (EQUAL (TIMES-LIST (PRIME-FACTORS
X))
X)
(PRIME-LIST (PRIME-FACTORS X))))))
(PUTPROPS TIMES-ID-IFF-1 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z 0)
(EQUAL W 1))))))
(PUTPROPS PRIME1-BASIC PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (EQUAL Z 1))
(NOT (EQUAL Z 0))
(NUMBERP Z)
(GREATEREQPR U Z))
(NOT (PRIME1 (TIMES W Z)
U)))))
(PUTPROPS GREATEREQPR-LESSP PROVE-LEMMA ((REWRITE)
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y)))))
(PUTPROPS GREATEREQPR-REMAINDER PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (EQUAL Z (ADD1 V)))
(DIVIDES Z (ADD1 V)))
(GREATEREQPR V Z))))
(PUTPROPS PRIME-BASIC PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (EQUAL Z 1))
(NOT (EQUAL Z X))
(NOT (ZEROP X))
(NOT (EQUAL X 1))
(DIVIDES Z X))
(NOT (PRIME1 X (SUB1 X))))))
(PUTPROPS REMAINDER-GCD PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (GCD B X)
Y)
(EQUAL (REMAINDER B Y)
0))))
(PUTPROPS REMAINDER-GCD-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (EQUAL (REMAINDER B X)
0))
(NOT (EQUAL (GCD B X)
X)))))
(PUTPROPS DIVIDES-TIMES1 PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL A (TIMES Z Y))
(EQUAL (REMAINDER A Z)
0))))
(PUTPROPS TIMES-IDENTITY1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 1))
(NOT (EQUAL Y 0))
(NOT (EQUAL X 0)))
(NOT (EQUAL X (TIMES X Y))))))
(PUTPROPS TIMES-IDENTITY PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X 0)
(AND (NUMBERP X)
(EQUAL Y 1))))))
(PUTPROPS KLUDGE-BRIDGE PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL Y (TIMES K X))
(EQUAL (GCD Y (TIMES A X))
(TIMES X (GCD A K))))))
(PUTPROPS HACK1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (DIVIDES X A))
(EQUAL A (GCD (TIMES X A)
(TIMES B A))))
(NOT (EQUAL (TIMES K X)
(TIMES B A))))))
(PUTPROPS PRIME-GCD PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (DIVIDES X B))
(NOT (ZEROP X))
(NOT (EQUAL (SUB1 X)
0))
(PRIME1 X (SUB1 X)))
(EQUAL (EQUAL (GCD B X)
1)
T))
NIL
(*
" The third hyp is that X is not 1 we have phrased it oddly on purpose. The"
*)
(*
" more natural phrasing causes us to fail to prove this theorem. The problem"
*)
(*
" is that the proof requires an appeal to PRIME-BASIC in which the free var Z"
*)
(*
" is instantiated to be (GCD B X) -- which is guessed by instantiating the"
*)
(*
" hyp (NOT (EQUAL Z 1)) and that instantiation is screwed if we put among our"
*)
(* " hyps (NOT (EQUAL X 1))." *)))
(PUTPROPS GCD-DISTRIBUTES-OVER-AN-OPENED-UP-TIMES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL X 0))
(EQUAL FREE (TIMES X Z)))
(EQUAL (GCD (TIMES B Z)
FREE)
(TIMES Z (GCD B X))))
NIL
(* " As is evident from the name, this stupid lemma is necessary because of a" *)
(* " Knuth-Bendix type problem. Had X*Z not been expanded we could have used the" *)
(* " more elegant DISTRIBUTIVITY-OF-TIMES-OVER-GCD. This lemma has a further" *)
(* " twist. X is a free var. to cut down on the frequency with which this lemma" *)
(* " is tried. Once, (NOT (EQUAL X 0)) was the first hyp. It happened that in" *)
(* " there were three possibly choices for X from the TYPE-ALIST at run time," *)
(* " but that the first one was correct. Unfortunately, when we changed the
" *)
(* " order of evaluation of the lits in a clause, the correct choice was" *)
(* " obscured. Luckily, by keying on the NUMBERP hyp we can still get the tp to" *)
(* " chose the right X. The other two choices are both numeric -- they are" *)
(* " REMAINDER expressions -- but the fact that they are numeric is not stored" *)
(* " on the TYPE-ALIST, thank goodness! Isn't that dreadful?" *)))
(PUTPROPS PRIME-KEY PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NUMBERP Z)
(PRIME X)
(NOT (DIVIDES X Z))
(NOT (DIVIDES X B)))
(NOT (EQUAL (TIMES X K)
(TIMES B Z))))))
(PUTPROPS QUOTIENT-DIVIDES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL (TIMES X (QUOTIENT Y X))
Y)))
(NOT (EQUAL (REMAINDER Y X)
0)))))
(PUTPROPS LITTLE-STEP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME X)
(NOT (EQUAL Y 1))
(NOT (EQUAL X Y)))
(NOT (EQUAL (REMAINDER X Y)
0)))))
(PUTPROPS LESSP-COUNT-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (MEMBER N L)
(LESSP (COUNT (DELETE N L))
(COUNT L)))))
(PUTPROPS REMAINDER-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (TIMES Y X)
Y)
0)))
(PUTPROPS PRIME-LIST-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (PRIME-LIST L2)
(PRIME-LIST (DELETE X L2)))))
(PUTPROPS DIVIDES-TIMES-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP C))
(MEMBER C L))
(EQUAL (REMAINDER (TIMES-LIST L)
C)
0))))
(PUTPROPS QUOTIENT-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
0
(FIX X)))))
(PUTPROPS DISTRIBUTIVITY-OF-DIVIDES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP A))
(DIVIDES A W))
(EQUAL (TIMES C (QUOTIENT W A))
(QUOTIENT (TIMES C W)
A)))))
(PUTPROPS TIMES-LIST-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP C))
(MEMBER C L))
(EQUAL (TIMES-LIST (DELETE C L))
(QUOTIENT (TIMES-LIST L)
C)))))
(PUTPROPS PRIME-LIST-TIMES-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME C)
(PRIME-LIST L2)
(NOT (MEMBER C L2)))
(NOT (EQUAL (REMAINDER (TIMES-LIST L2)
C)
0)))))
(PUTPROPS IF-TIMES-THEN-DIVIDES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP C))
(NOT (DIVIDES C X)))
(NOT (EQUAL (TIMES C Y)
X)))))
(PUTPROPS TIMES-EQUAL-1 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A 0))
(NOT (EQUAL B 0))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
0)
(EQUAL (SUB1 B)
0)))))
(PUTPROPS PRIME-MEMBER PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (EQUAL (TIMES C (TIMES-LIST L1))
(TIMES-LIST L2))
(PRIME C)
(PRIME-LIST L2))
(MEMBER C L2))
((DISABLE TIMES))))
(PUTPROPS DIVIDES-IMPLIES-TIMES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP A))
(NUMBERP C)
(EQUAL (TIMES A C)
B))
(EQUAL (EQUAL C (QUOTIENT B A))
T))))
(PUTPROPS PRIME-FACTORIZATION-UNIQUENESS PROVE-LEMMA (NIL (IMPLIES (AND (PRIME-LIST L1)
(PRIME-LIST L2)
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2)))
(PERM L1 L2))))
(PUTPROPS MEMBER-MAXIMUM PROVE-LEMMA ((REWRITE)
(IMPLIES (LISTP X)
(MEMBER (MAXIMUM X)
X))))
(PUTPROPS LESSP-DELETE-REWRITE PROVE-LEMMA ((REWRITE)
(EQUAL (LESSP (COUNT (DELETE X L))
(COUNT L))
(MEMBER X L))))
(PUTPROPS SORT2-GEN-1 PROVE-LEMMA ((REWRITE)
(PLISTP (SORT2 X))))
(PUTPROPS SORT2-GEN-2 PROVE-LEMMA ((REWRITE)
(ORDERED2 (SORT2 X))))
(PUTPROPS SORT2-GEN PROVE-LEMMA ((GENERALIZE)
(AND (PLISTP (SORT2 X))
(ORDERED2 (SORT2 X)))))
(PUTPROPS ADDTOLIST2-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PLISTP Y)
(ORDERED2 Y)
(NOT (EQUAL X V)))
(EQUAL (ADDTOLIST2 V (DELETE X Y))
(DELETE X (ADDTOLIST2 V Y))))))
(PUTPROPS DELETE-ADDTOLIST2 PROVE-LEMMA ((REWRITE)
(IMPLIES (PLISTP Y)
(EQUAL (DELETE V (ADDTOLIST2 V Y))
Y))))
(PUTPROPS ADDTOLIST2-KLUDGE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (LESSP V W))
(EQUAL (ADDTOLIST2 V Y)
(CONS V Y)))
(EQUAL (ADDTOLIST2 V (ADDTOLIST2 W Y))
(CONS V (ADDTOLIST2 W Y))))))
(PUTPROPS LESSP-MAXIMUM-ADDTOLIST2 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (LESSP V (MAXIMUM Z)))
(EQUAL (ADDTOLIST2 V (SORT2 Z))
(CONS V (SORT2 Z))))))
(PUTPROPS SORT2-DELETE-CONS PROVE-LEMMA ((REWRITE)
(IMPLIES (LISTP X)
(EQUAL (CONS (MAXIMUM X)
(DELETE (MAXIMUM X)
(SORT2 X)))
(SORT2 X)))))
(PUTPROPS SORT2-DELETE PROVE-LEMMA ((REWRITE)
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L)))))
(PUTPROPS DSORT-SORT2 PROVE-LEMMA ((REWRITE)
(EQUAL (DSORT X)
(SORT2 X))))
(PUTPROPS COUNT-LIST-SORT2 PROVE-LEMMA (NIL (EQUAL (COUNT-LIST A (SORT2 L))
(COUNT-LIST A L))))
(PUTPROPS DIFFERENCE-1 PROVE-LEMMA ((REWRITE)
(EQUAL (DIFFERENCE X 1)
(SUB1 X))))
(PUTPROPS FUNCTIONAL-LOOP-INVRT PROVE-LEMMA ((REWRITE)
(IMPLIES (NUMBERP AC)
(EQUAL (PROG-TRANS-OF-SIGMA I AC)
(PLUS AC (SIGMA 0 I))))))
(PUTPROPS CORRECTNESS-OF-FUNCTIONAL-SIGMA PROVE-LEMMA (NIL (EQUAL (PROG-TRANS-OF-SIGMA I 0)
(SIGMA 0 I))))
(PUTPROPS SIGMA-INPUT-PATH PROVE-LEMMA (NIL (AND (EQUAL 0 (SIGMA K K))
(LEQ K K))))
(PUTPROPS SIGMA-LOOP-INVRT PROVE-LEMMA (NIL (IMPLIES (AND (NOT (ZEROP I))
(LEQ I K))
(AND (EQUAL (PLUS (SIGMA I K)
I)
(SIGMA (SUB1 I)
K))
(LEQ (SUB1 I)
K)))))
(PUTPROPS SIGMA-OUTPUT-PATH PROVE-LEMMA (NIL (IMPLIES (AND (ZEROP I)
(LEQ I K))
(EQUAL (SIGMA I K)
(SIGMA 0 K)))))
(PUTPROPS GET-SET PROVE-LEMMA ((REWRITE)
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM)))))
(PUTPROPS CORRECTNESS-OF-GET-SIMPLIFIER PROVE-LEMMA (((META GET))
(IMPLIES (FORMP X)
(AND (EQUAL (MEANING X A)
(MEANING (GET-SIMPLIFIER
X)
A))
(FORMP (GET-SIMPLIFIER X))))))
(PUTPROPS CORRECTNESS-OF-SET-SIMPLIFIER PROVE-LEMMA (((META SET))
(IMPLIES (FORMP X)
(AND (EQUAL (MEANING X A)
(MEANING (SET-SIMPLIFIER
X)
A))
(FORMP (SET-SIMPLIFIER X))))))
(PUTPROPS LENGTH-5 PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (CADDDDR X)
(QUOTE (JUMPA 1)))
(EQUAL (LENGTH X)
(PLUS 5 (LENGTH (CDDDDDR X)))))
NIL
(*
" To relieve the hyp that MAX is greater than 6 in EXECUTE1-OPENED-UP, we"
*)
(*
" need to know that (LENGTH MEM) there is greater than six. We have an"
*)
(*
" explicit picture of the first 6 elements of MEM, so it suffices just to"
*)
(*
" expand (LENGTH MEM) into 6 + (LENGTH ...). This rather clear picture of"
*)
(*
" things is messed up slightly because the tp expands LENGTH once on its own."
*)
(* " So this lemma forces the other five." *)))
(PUTPROPS LENGTH-CONS6 PROVE-LEMMA ((REWRITE)
(EQUAL (LENGTH (CONS X1 (CONS X2 (CONS X3 (CONS X4 (CONS X5 (CONS X6 X7)))))))
(PLUS 6 (LENGTH X7)))))
(PUTPROPS EXECUTE1-1 PROVE-LEMMA ((REWRITE)
(IMPLIES
(NOT (LESSP MAX 6))
(EQUAL (EXECUTE1 1 (CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
L))))))
MAX)
(IF (ZEROP (CAR L))
(EXECUTE1 2 (CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
L))))))
MAX)
(EXECUTE1 3 (CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
L))))))
MAX))))
NIL
(* " This and the next few lemmas are required to force EXECUTE1 to open up when" *)
(* " given explicit PCs. Without these lemmas the stupid theorem prover refused" *)
(* " to expand (EXECUTE1 3 --) to (EXECUTE 4 --) because it doesn't think" *)
(* " anything has improved since MEM is more complicated." *)))
(PUTPROPS EXECUTE1-3 PROVE-LEMMA ((REWRITE)
(IMPLIES
(NOT (LESSP MAX 6))
(EQUAL
(EXECUTE1 3 (CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
L))))))
MAX)
(EXECUTE1 4
(CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
(CONS (CAR L)
(CONS (PLUS (CAR L)
(CADR L))
(CDDR L)))))))))
MAX)))))
(PUTPROPS EXECUTE1-4 PROVE-LEMMA ((REWRITE)
(IMPLIES
(NOT (LESSP MAX 6))
(EQUAL (EXECUTE1 4 (CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
L))))))
MAX)
(EXECUTE1 5 (CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
(CONS (DIFFERENCE (CAR L)
1)
(CDR L))))))))
MAX)))))
(PUTPROPS EXECUTE1-OPENED-UP PROVE-LEMMA ((REWRITE)
(IMPLIES
(AND (NOT (LESSP MAX 6))
(EQUAL (CAR MEM)
(QUOTE (MOVEI 7 0)))
(EQUAL (CADR MEM)
(QUOTE (SKIPNE 6)))
(EQUAL (CADDR MEM)
(QUOTE (STOP)))
(EQUAL (CADDDR MEM)
(QUOTE (ADD 7 6)))
(EQUAL (CADDDDR MEM)
(QUOTE (SUBI 6 1)))
(EQUAL (CADDDDDR MEM)
(QUOTE (JUMPA 1))))
(EQUAL
(EXECUTE1 1 MEM MAX)
(IF
(ZEROP (CADDDDDDR MEM))
(LIST F (CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
(CDDDDDDR MEM))))))))
(LIST 1 (CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
(CONS (SUB1 (CADDDDDDR MEM))
(CONS (PLUS (CADDDDDDR MEM)
(CADDDDDDDR MEM))
(CDDDDDDDDR MEM))))))))))))))
)
(PUTPROPS EXECUTE-OPENED-UP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NUMBERP PC)
(NOT (ZEROP CLK)))
(EQUAL (EXECUTE PC MEM CLK)
(EXECUTE (CAR (EXECUTE1 PC MEM
(LENGTH MEM)))
(CADR (EXECUTE1 PC MEM
(LENGTH MEM)))
(SUB1 CLK))))
NIL
(*
" This lemma forces EXECUTE to open even though it has calls of EXECUTE1 in"
*)
(*
" it that might not occur in the thm. Without this lemma we don't expand"
*)
(*
" EXECUTE even when we have (SUB1 CLK) in the problem because of the"
*)
(*
" EXECUTE1s. What is so maddening is that after an ELIM on CLK we do expand"
*)
(*
" it. But in some of the cases things get messy because some other elims"
*)
(*
" happen first. I am not sure if we could prove it without this lemma, but if
"
*)
(* " so it takes an awfully long time." *)))
(PUTPROPS INTERPRETER-LOOP-INVRT PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (LESSP CLK (CADDDDDDR MEM)))
(EQUAL (CAR MEM)
(QUOTE (MOVEI 7 0)))
(EQUAL (CADR MEM)
(QUOTE (SKIPNE 6)))
(EQUAL (CADDR MEM)
(QUOTE (STOP)))
(EQUAL (CADDDR MEM)
(QUOTE (ADD 7 6)))
(EQUAL (CADDDDR MEM)
(QUOTE (SUBI 6 1)))
(EQUAL (CADDDDDR MEM)
(QUOTE (JUMPA 1))))
(EQUAL (CADDDDDDDR (EXECUTE 1 MEM CLK))
(IF (ZEROP (CADDDDDDR MEM))
(CADDDDDDDR MEM)
(PLUS (CADDDDDDDR MEM)
(SIGMA 0 (CADDDDDDR MEM)))))
)
NIL
(*
" Note the careful way I phrased that so that (EXECUTE & MEM CLK) appears so"
*)
(*
" we pick MEM up in the induction hyps. Had I phrased the hyps as an equation"
*)
(*
" between MEM and a half-constant APPEND the induction wouldn't go through."
*)))
(PUTPROPS INTERPRETER-INPUT-PATH PROVE-LEMMA ((REWRITE)
(EQUAL (EXECUTE 0 (CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
MEM))))))
CLK)
(IF (ZEROP CLK)
(CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
MEM))))))
(EXECUTE 1
(CONS (QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
(CONS (CAR MEM)
(CONS 0 (CDDR MEM)))))))))
CLK)))
NIL
(* " This one is necessary because we don't open up (EXECUTE 0 & &) so as to hit" *)
(* " it with the INTERPRETER-LOOP-INVRT unless we have the target in the theorem" *)
(* " already." *)))
(PUTPROPS CORRECTNESS-OF-INTERPRETED-SIGMA PROVE-LEMMA (NIL
(IMPLIES (AND (EQUAL MEM (APPEND (QUOTE ((MOVEI 7 0)
(SKIPNE 6)
(STOP)
(ADD 7 6)
(SUBI 6 1)
(JUMPA 1)))
TL))
(EQUAL I (GET 6 MEM))
(NOT (LESSP CLK I)))
(EQUAL (GET 7 (EXECUTE 0 MEM CLK))
(IF (ZEROP CLK)
(GET 7 MEM)
(SIGMA 0 I))))))
(PUTPROPS DIFFERENCE-2 PROVE-LEMMA ((REWRITE)
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X))))
(PUTPROPS HALF-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2)))))
(PUTPROPS SIGMA-IS-HALF-PRODUCT PROVE-LEMMA ((REWRITE)
(EQUAL (SIGMA 0 I)
(QUOTIENT (TIMES I (ADD1 I))
2))))
(PUTPROPS H-LEMMA PROVE-LEMMA ((REWRITE)
(EQUAL (H-PR X (H Z A))
(H Z (H-PR X A)))))
(PUTPROPS H-EQ PROVE-LEMMA ((REWRITE)
(EQUAL (H-AC L AC)
(H-PR L AC))
((INDUCT (H-AC L AC)))))
(PUTPROPS F0-SATISFIES-F91-EQUATION PROVE-LEMMA (NIL (EQUAL (F0 X)
(IF (LESSP 100 X)
(DIFFERENCE X 10)
(F0 (F0 (PLUS X 11)))))))
(PUTPROPS F91-IS-F0 PROVE-LEMMA ((REWRITE)
(EQUAL (F91 X)
(F0 X))))
(PUTPROPS TIMES-1 PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES 1 X)
(FIX X))))
(PUTPROPS TIMES-2 PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES 2 X)
(PLUS X X))))
(PUTPROPS EXP-OF-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EXP 0 K)
(IF (ZEROP K)
1 0))))
(PUTPROPS EXP-OF-1 PROVE-LEMMA ((REWRITE)
(EQUAL (EXP 1 K)
1)))
(PUTPROPS EXP-BY-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EXP X 0)
1)))
(PUTPROPS EXP-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (EXP (TIMES I J)
K)
(TIMES (EXP I K)
(EXP J K)))))
(PUTPROPS EXP-EXP PROVE-LEMMA ((REWRITE)
(EQUAL (EXP (EXP I J)
K)
(EXP I (TIMES J K)))))
(PUTPROPS REMAINDER-PLUS-TIMES-1 PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (PLUS X (TIMES I J))
J)
(REMAINDER X J))))
(PUTPROPS REMAINDER-PLUS-TIMES-2 PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (PLUS X (TIMES J I))
J)
(REMAINDER X J))))
(PUTPROPS REMAINDER-TIMES-1 PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (TIMES B (TIMES A C))
A)
0)))
(PUTPROPS REMAINDER-OF-1 PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER 1 X)
(IF (EQUAL X 1)
0 1))))
(PUTPROPS EQUAL-LENGTH-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (LENGTH X)
0)
(NLISTP X))))
(PUTPROPS LENGTH-DELETE PROVE-LEMMA ((REWRITE)
(EQUAL (LENGTH (DELETE X L))
(IF (MEMBER X L)
(LENGTH (CDR L))
(LENGTH L)))))
(PUTPROPS REMAINDER-DIFFERENCE-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (DIFFERENCE (TIMES P X)
(TIMES P Y))
P)
0)
((USE (DIVIDES-TIMES (X (DIFFERENCE X Y))
(Z P)))
(DISABLE DIVIDES-TIMES))))
(PUTPROPS PRIME-KEY-REWRITE PROVE-LEMMA ((REWRITE)
(IMPLIES (PRIME P)
(EQUAL (EQUAL (REMAINDER (TIMES A B)
P)
0)
(OR (EQUAL (REMAINDER A P)
0)
(EQUAL (REMAINDER B P)
0))))
((USE (PRIME-KEY (X P)
(B A)
(Z B)
(K (QUOTIENT (TIMES A B)
P)))
(REMAINDER-QUOTIENT (X (TIMES A B))
(Y P)))
(DISABLE PRIME-KEY REMAINDER-QUOTIENT))))
(PUTPROPS TIMES-TIMES-LIST-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (MEMBER X L)
(EQUAL (TIMES X (TIMES-LIST (DELETE X L)))
(TIMES-LIST L)))))
(PUTPROPS LESSP-REMAINDER-DIVISOR PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZEROP Y))
(LESSP (REMAINDER X Y)
Y))))
(PUTPROPS SUBST2-OK PROVE-LEMMA (NIL (EQUAL (EVAL2 (SUBST2 NEW OLD TERM)
A)
(EVAL2 TERM (CONS (CONS OLD (EVAL2 NEW A))
A)))
NIL))
(DEFINEQ
(PROVEALL3
(LAMBDA NIL (* kbr: " 8-Nov-85 16:02")
(PROVEALL (QUOTE ((NOTE-LIB BASICS)
(DISABLE EUCLID)
(DISABLE QUOTIENT-DIVIDES)
(DISABLE IF-TIMES-THEN-DIVIDES)
(DISABLE TIMES)
(DEFN& CRYPT)
(PROVE-LEMMA& TIMES-MOD-1)
(PROVE-LEMMA& TIMES-MOD-2)
(PROVE-LEMMA& CRYPT-CORRECT)
(PROVE-LEMMA& TIMES-MOD-3)
(PROVE-LEMMA& REMAINDER-EXP-LEMMA)
(PROVE-LEMMA& REMAINDER-EXP)
(PROVE-LEMMA& EXP-MOD-IS-1)
(DEFN& PDIFFERENCE)
(PROVE-LEMMA& TIMES-DISTRIBUTES-OVER-PDIFFERENCE)
(PROVE-LEMMA& EQUAL-MODS-TRICK-1)
(PROVE-LEMMA& EQUAL-MODS-TRICK-2)
(DISABLE PDIFFERENCE)
(PROVE-LEMMA& PRIME-KEY-TRICK)
(PROVE-LEMMA& PRODUCT-DIVIDES-LEMMA)
(PROVE-LEMMA& PRODUCT-DIVIDES)
(PROVE-LEMMA& THM-53-SPECIALIZED-TO-PRIMES)
(PROVE-LEMMA& COROLLARY-53)
(PROVE-LEMMA& THM-55-SPECIALIZED-TO-PRIMES)
(PROVE-LEMMA& COROLLARY-55)
(DEFN& ALL-DISTINCT)
(DEFN& ALL-LESSEQP)
(DEFN& ALL-NON-ZEROP)
(DEFN& POSITIVES)
(PROVE-LEMMA& LISTP-POSITIVES)
(PROVE-LEMMA& CAR-POSITIVES)
(PROVE-LEMMA& MEMBER-POSITIVES)
(PROVE-LEMMA& ALL-NON-ZEROP-DELETE)
(PROVE-LEMMA& ALL-DISTINCT-DELETE)
(PROVE-LEMMA& PIGEON-HOLE-PRINCIPLE-LEMMA-1)
(PROVE-LEMMA& PIGEON-HOLE-PRINCIPLE-LEMMA-2)
(PROVE-LEMMA& PERM-MEMBER)
(DEFN& PIGEON-HOLE-INDUCTION)
(PROVE-LEMMA& PIGEON-HOLE-PRINCIPLE)
(PROVE-LEMMA& PERM-TIMES-LIST)
(PROVE-LEMMA& TIMES-LIST-POSITIVES)
(PROVE-LEMMA& TIMES-LIST-EQUAL-FACT)
(PROVE-LEMMA& PRIME-FACT)
(DEFN& S)
(PROVE-LEMMA& REMAINDER-TIMES-LIST-S)
(PROVE-LEMMA& ALL-DISTINCT-S-LEMMA)
(PROVE-LEMMA& ALL-DISTINCT-S)
(PROVE-LEMMA& ALL-NON-ZEROP-S)
(PROVE-LEMMA& ALL-LESSEQP-S)
(PROVE-LEMMA& LENGTH-S)
(PROVE-LEMMA& FERMAT-THM)
(PROVE-LEMMA& CRYPT-INVERTS-STEP-1)
(PROVE-LEMMA& CRYPT-INVERTS-STEP-1A)
(PROVE-LEMMA& CRYPT-INVERTS-STEP-1B)
(PROVE-LEMMA& CRYPT-INVERTS-STEP-2)
(PROVE-LEMMA& CRYPT-INVERTS)))
NIL RSA)))
)
(PUTPROPS CRYPT DEFN ((M E N)
(IF (ZEROP E)
1
(IF (EVEN E)
(REMAINDER (SQUARE (CRYPT M (QUOTIENT E 2)
N))
N)
(REMAINDER (TIMES M (REMAINDER (SQUARE (CRYPT M (QUOTIENT E 2)
N))
N))
N)))))
(PUTPROPS PDIFFERENCE DEFN ((A B)
(IF (LESSP A B)
(DIFFERENCE B A)
(DIFFERENCE A B))
NIL
(*
" We wish to teach the system the trick of proving that A mod p = B mod p by"
*)
(*
" considering whether p A-B. If we used DIFFERENCE we would have to split on"
*)
(*
" whether A<B. So we introduce PDIFFERENCE that contains that split. Then"
*)
(*
" we prove the necessary facts about TIMES, REMAINDER and PDIFFERENCE. During"
*)
(*
" these proofs the case splits on A<B arise. But the case splits do not arise"
*)
(*
" in the statements of the lemmas and so don't arise when we try to apply"
*)
(*
" them. After proving what we need about PDIFFERENCE we disable it."
*)))
(PUTPROPS ALL-DISTINCT DEFN ((L)
(IF (NLISTP L)
T
(AND (NOT (MEMBER (CAR L)
(CDR L)))
(ALL-DISTINCT (CDR L))))))
(PUTPROPS ALL-LESSEQP DEFN ((L N)
(IF (NLISTP L)
T
(AND (NOT (LESSP N (CAR L)))
(ALL-LESSEQP (CDR L)
N)))))
(PUTPROPS ALL-NON-ZEROP DEFN ((L)
(IF (NLISTP L)
T
(AND (NOT (ZEROP (CAR L)))
(ALL-NON-ZEROP (CDR L))))))
(PUTPROPS POSITIVES DEFN ((N)
(IF (ZEROP N)
NIL
(CONS N (POSITIVES (SUB1 N))))))
(PUTPROPS PIGEON-HOLE-INDUCTION DEFN ((L)
(IF (LISTP L)
(IF (MEMBER (LENGTH L)
L)
(PIGEON-HOLE-INDUCTION (DELETE (LENGTH L)
L))
(PIGEON-HOLE-INDUCTION (CDR L)))
T)))
(PUTPROPS S DEFN ((N M P)
(IF (ZEROP N)
NIL
(CONS (REMAINDER (TIMES M N)
P)
(S (SUB1 N)
M P)))))
(PUTPROPS TIMES-MOD-1 PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
N)
(REMAINDER (TIMES X Y)
N))))
(PUTPROPS TIMES-MOD-2 PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (TIMES A (TIMES B (REMAINDER Y N)))
N)
(REMAINDER (TIMES A B Y)
N))
((USE (TIMES-MOD-1 (X (TIMES A B))))
(DISABLE TIMES-MOD-1))))
(PUTPROPS CRYPT-CORRECT PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (EQUAL N 1))
(EQUAL (CRYPT M E N)
(REMAINDER (EXP M E)
N)))))
(PUTPROPS TIMES-MOD-3 PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (TIMES (REMAINDER A N)
B)
N)
(REMAINDER (TIMES A B)
N))))
(PUTPROPS REMAINDER-EXP-LEMMA PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (REMAINDER Y A)
(REMAINDER Z A))
(EQUAL (EQUAL (REMAINDER (TIMES X Y)
A)
(REMAINDER (TIMES X Z)
A))
T))))
(PUTPROPS REMAINDER-EXP PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (EXP (REMAINDER A N)
I)
N)
(REMAINDER (EXP A I)
N))))
(PUTPROPS EXP-MOD-IS-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (REMAINDER (EXP M J)
P)
1)
(EQUAL (REMAINDER (EXP M (TIMES I J))
P)
1))
((USE (EXP-EXP (I M)
(J J)
(K I))
(REMAINDER-EXP (A (EXP M J))
(N P)))
(DISABLE EXP-EXP REMAINDER-EXP))))
(PUTPROPS TIMES-DISTRIBUTES-OVER-PDIFFERENCE PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES M (PDIFFERENCE A B))
(PDIFFERENCE (TIMES M A)
(TIMES M B)))))
(PUTPROPS EQUAL-MODS-TRICK-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (REMAINDER (PDIFFERENCE A B)
P)
0)
(EQUAL (EQUAL (REMAINDER A P)
(REMAINDER B P))
T))))
(PUTPROPS EQUAL-MODS-TRICK-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER (PDIFFERENCE A B)
P)
0))
((DISABLE DIFFERENCE-ELIM))))
(PUTPROPS PRIME-KEY-TRICK PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER (TIMES M A)
P)
(REMAINDER (TIMES M B)
P))
(NOT (EQUAL (REMAINDER M P)
0))
(PRIME P))
(EQUAL (EQUAL (REMAINDER A P)
(REMAINDER B P))
T))
((USE (PRIME-KEY-REWRITE (A M)
(B (PDIFFERENCE A B)))
(EQUAL-MODS-TRICK-2 (A (TIMES M A))
(B (TIMES M B))))
(DISABLE PRIME-KEY-REWRITE EQUAL-MODS-TRICK-2))))
(PUTPROPS PRODUCT-DIVIDES-LEMMA PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (REMAINDER X Z)
0)
(EQUAL (REMAINDER (TIMES Y X)
(TIMES Y Z))
0))))
(PUTPROPS PRODUCT-DIVIDES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER X P)
0)
(EQUAL (REMAINDER X Q)
0)
(PRIME P)
(PRIME Q)
(NOT (EQUAL P Q)))
(EQUAL (REMAINDER X (TIMES P Q))
0))))
(PUTPROPS THM-53-SPECIALIZED-TO-PRIMES PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q)))
(EQUAL (REMAINDER A
(TIMES P Q))
(REMAINDER B
(TIMES P Q))))
NIL
(*
" The proof of this consists merely of applying trick 1 to backwards chain"
*)
(*
" from A mod PQ = B mod PQ to PQ A-B, then use PRODUCT-DIVIDES to back up to"
*)
(*
" P A-B and Q A-B, and then use trick 2 to come back to A mod P = B mod P.
"
*)))
(PUTPROPS COROLLARY-53 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q))
(NUMBERP B)
(LESSP B (TIMES P Q)))
(EQUAL (EQUAL (REMAINDER A (TIMES P Q))
B)
T))
((USE (THM-53-SPECIALIZED-TO-PRIMES))
(DISABLE THM-53-SPECIALIZED-TO-PRIMES))))
(PUTPROPS THM-55-SPECIALIZED-TO-PRIMES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P)
0)))
(EQUAL (EQUAL (REMAINDER (TIMES M X)
P)
(REMAINDER (TIMES M Y)
P))
(EQUAL (REMAINDER X P)
(REMAINDER Y P))))))
(PUTPROPS COROLLARY-55 PROVE-LEMMA ((REWRITE)
(IMPLIES (PRIME P)
(EQUAL (EQUAL (REMAINDER (TIMES M X)
P)
(REMAINDER M P))
(OR (EQUAL (REMAINDER M P)
0)
(EQUAL (REMAINDER X P)
1))))
((USE (THM-55-SPECIALIZED-TO-PRIMES (Y 1)))
(DISABLE THM-55-SPECIALIZED-TO-PRIMES))))
(PUTPROPS LISTP-POSITIVES PROVE-LEMMA ((REWRITE)
(EQUAL (LISTP (POSITIVES N))
(NOT (ZEROP N)))))
(PUTPROPS CAR-POSITIVES PROVE-LEMMA ((REWRITE)
(EQUAL (CAR (POSITIVES N))
(IF (ZEROP N)
0 N))))
(PUTPROPS MEMBER-POSITIVES PROVE-LEMMA ((REWRITE)
(EQUAL (MEMBER X (POSITIVES N))
(IF (ZEROP X)
F
(LESSP X (ADD1 N))))))
(PUTPROPS ALL-NON-ZEROP-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (ALL-NON-ZEROP L)
(ALL-NON-ZEROP (DELETE X L)))))
(PUTPROPS ALL-DISTINCT-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (ALL-DISTINCT L)
(ALL-DISTINCT (DELETE X L)))))
(PUTPROPS PIGEON-HOLE-PRINCIPLE-LEMMA-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N)
L)
N))))
(PUTPROPS PIGEON-HOLE-PRINCIPLE-LEMMA-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (MEMBER (ADD1 N)
X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N))))
(PUTPROPS PERM-MEMBER PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PERM A B)
(MEMBER X A))
(MEMBER X B))))
(PUTPROPS PIGEON-HOLE-PRINCIPLE PROVE-LEMMA (NIL (IMPLIES (AND (ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L))
L))
((INDUCT (PIGEON-HOLE-INDUCTION L)))
(*
" We have proved this theorem without this induction hint, but that proof"
*)
(*
" requires many more lemmas. This is a good example of a theorem whose"
*)
(*
" induction is not suggested by any term in the theorem."
*)))
(PUTPROPS PERM-TIMES-LIST PROVE-LEMMA (NIL (IMPLIES (PERM L1 L2)
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2)))))
(PUTPROPS TIMES-LIST-POSITIVES PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES-LIST (POSITIVES N))
(FACT N))))
(PUTPROPS TIMES-LIST-EQUAL-FACT PROVE-LEMMA ((REWRITE)
(IMPLIES (PERM (POSITIVES N)
L)
(EQUAL (TIMES-LIST L)
(FACT N)))
((USE (PERM-TIMES-LIST (L1 (POSITIVES N))
(L2 L)))
(DISABLE PERM-TIMES-LIST))))
(PUTPROPS PRIME-FACT PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP N P))
(NOT (EQUAL (REMAINDER (FACT N)
P)
0)))
((INDUCT (FACT N)))))
(PUTPROPS REMAINDER-TIMES-LIST-S PROVE-LEMMA (NIL (EQUAL (REMAINDER (TIMES-LIST (S N M P))
P)
(REMAINDER (TIMES (FACT N)
(EXP M N))
P))))
(PUTPROPS ALL-DISTINCT-S-LEMMA PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P)
0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1)
P)
(S N2 M P))))
((INDUCT (S N2 M P)))))
(PUTPROPS ALL-DISTINCT-S PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P)
0))
(LESSP N P))
(ALL-DISTINCT (S N M P)))))
(PUTPROPS ALL-NON-ZEROP-S PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P)
0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P)))))
(PUTPROPS ALL-LESSEQP-S PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZEROP P))
(ALL-LESSEQP (S N M P)
(SUB1 P)))))
(PUTPROPS LENGTH-S PROVE-LEMMA ((REWRITE)
(EQUAL (LENGTH (S N M P))
(FIX N))))
(PUTPROPS FERMAT-THM PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P)
0)))
(EQUAL (REMAINDER (EXP M (SUB1 P))
P)
1))
((USE (PIGEON-HOLE-PRINCIPLE (L (S (SUB1 P)
M P)))
(REMAINDER-TIMES-LIST-S (N (SUB1 P))))
(DISABLE PIGEON-HOLE-PRINCIPLE REMAINDER-TIMES-LIST-S))))
(PUTPROPS CRYPT-INVERTS-STEP-1 PROVE-LEMMA (NIL
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (TIMES M (EXP M (TIMES K (SUB1 P))))
P)
(REMAINDER M P)))))
(PUTPROPS CRYPT-INVERTS-STEP-1A PROVE-LEMMA ((REWRITE)
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (TIMES M (EXP M (TIMES K (SUB1 P)
(SUB1 Q))))
P)
(REMAINDER M P)))
((USE (CRYPT-INVERTS-STEP-1 (K (TIMES K (SUB1 Q)))))
(DISABLE CRYPT-INVERTS-STEP-1))))
(PUTPROPS CRYPT-INVERTS-STEP-1B PROVE-LEMMA ((REWRITE)
(IMPLIES (PRIME Q)
(EQUAL (REMAINDER (TIMES M (EXP M (TIMES K (SUB1 P)
(SUB1 Q))))
Q)
(REMAINDER M Q)))
((USE (CRYPT-INVERTS-STEP-1 (P Q)
(K (TIMES K (SUB1 P)))))
(DISABLE CRYPT-INVERTS-STEP-1))))
(PUTPROPS CRYPT-INVERTS-STEP-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED (TIMES (SUB1 P)
(SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED)
(TIMES P Q))
M))))
(PUTPROPS CRYPT-INVERTS PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL N (TIMES P Q))
(NUMBERP M)
(LESSP M N)
(EQUAL (REMAINDER (TIMES E D)
(TIMES (SUB1 P)
(SUB1 Q)))
1))
(EQUAL (CRYPT (CRYPT M E N)
D N)
M))
NIL))
(DEFINEQ
(PROVEALL4
(LAMBDA NIL (* kbr: "19-Oct-85 16:31")
(PROVEALL (QUOTE ((NOTE-LIB RSA)
(DEFN& INVERSE)
(PROVE-LEMMA& INVERSE-INVERTS-LEMMA)
(PROVE-LEMMA& INVERSE-INVERTS)
(PROVE-LEMMA& INVERSE-IS-UNIQUE)
(PROVE-LEMMA& S-P-I-I-LEMMA1)
(PROVE-LEMMA& S-P-I-I-LEMMA2)
(PROVE-LEMMA& SUB1-P-IS-INVOLUTION)
(PROVE-LEMMA& N-O-I-LEMMA1)
(PROVE-LEMMA& N-O-I-LEMMA2)
(PROVE-LEMMA& N-O-I-LEMMA3)
(PROVE-LEMMA& N-O-I-LEMMA4)
(PROVE-LEMMA& NO-OTHER-INVOLUTIONS)
(PROVE-LEMMA& I-O-I-LEMMA)
(PROVE-LEMMA& INVERSE-OF-INVERSE)
(PROVE-LEMMA& N-Z-I-LEMMA)
(PROVE-LEMMA& NON-ZEROP-INVERSE)
(PROVE-LEMMA& B-I-LEMMA2)
(PROVE-LEMMA& B-I-LEMMA1)
(PROVE-LEMMA& BOUNDED-INVERSE)
(DEFN& INVERSE-LIST)
(PROVE-LEMMA& ALL-NON-ZEROP-INVERSE-LIST)
(PROVE-LEMMA& BOUNDED-INVERSE-LIST)
(PROVE-LEMMA& SUBSETP-POSITIVES)
(PROVE-LEMMA& INVERSE-1)
(PROVE-LEMMA& A-D-I-L-LEMMA1)
(PROVE-LEMMA& A-D-I-L-LEMMA2)
(PROVE-LEMMA& A-D-I-L-LEMMA3)
(PROVE-LEMMA& ALL-DISTINCT-INVERSE-LIST)
(PROVE-LEMMA& T-I-L-LEMMA1)
(PROVE-LEMMA& T-I-L-LEMMA)
(PROVE-LEMMA& T-I-L-LEMMA3)
(PROVE-LEMMA& T-I-L-LEMMA4)
(PROVE-LEMMA& TIMES-INVERSE-LIST)
(PROVE-LEMMA& DELETE-X-LEAVE-A)
(PROVE-LEMMA& DELETE-MEMBER-LEAVE-SUBSET)
(PROVE-LEMMA& ALL-LESSEQP-DELETE)
(PROVE-LEMMA& POSITIVES-BOUNDED)
(PROVE-LEMMA& SUBSETP-POSITIVES-DELETE)
(PROVE-LEMMA& NONZEROP-LESSEQP-ZERO)
(DEFN& PIGEONHOLE2-INDUCTION)
(PROVE-LEMMA& PIGEONHOLE2)
(PROVE-LEMMA& PERM-POSITIVES-INVERSE-LIST)
(PROVE-LEMMA& INVERSE-LIST-FACT)
(PROVE-LEMMA& W-T-LEMMA)
(PROVE-LEMMA& WILSON-THM)))
NIL WILSON)))
)
(PUTPROPS INVERSE DEFN ((J P)
(IF (EQUAL P 2)
(REMAINDER J 2)
(REMAINDER (EXP J (DIFFERENCE P 2))
P))))
(PUTPROPS INVERSE-LIST DEFN ((I P)
(IF (ZEROP I)
NIL
(IF (EQUAL I 1)
(CONS 1 NIL)
(IF (MEMBER I (INVERSE-LIST (SUB1 I)
P))
(INVERSE-LIST (SUB1 I)
P)
(CONS I (CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I)
P))))))))
(PUTPROPS PIGEONHOLE2-INDUCTION DEFN ((L N)
(IF (ZEROP N)
T
(PIGEONHOLE2-INDUCTION (DELETE N L)
(SUB1 N)))))
(PUTPROPS INVERSE-INVERTS-LEMMA PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZEROP P))
(EQUAL (REMAINDER (TIMES (INVERSE J P)
J)
P)
(REMAINDER (EXP J (SUB1 P))
P)))))
(PUTPROPS INVERSE-INVERTS PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P)
0)))
(EQUAL (REMAINDER (TIMES (INVERSE J P)
J)
P)
1))
((USE (INVERSE-INVERTS-LEMMA))
(DISABLE INVERSE))))
(PUTPROPS INVERSE-IS-UNIQUE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL 1 (REMAINDER (TIMES M X)
P)))
(EQUAL (INVERSE M P)
(REMAINDER X P)))
((USE (INVERSE-INVERTS (J M))
(THM-55-SPECIALIZED-TO-PRIMES (Y (INVERSE M P)))))))
(PUTPROPS S-P-I-I-LEMMA1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1)))
(EQUAL (TIMES (SUB1 N)
(SUB1 N))
(PLUS 1 (TIMES N (SUB1 (SUB1 N))))))))
(PUTPROPS S-P-I-I-LEMMA2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (SUB1 N)
(SUB1 N))
N)
1))
((USE (S-P-I-I-LEMMA1)
(REMAINDER-PLUS-TIMES-2 (J N)
(X 1)
(I (SUB1 (SUB1 N)))))
(DISABLE S-P-I-I-LEMMA1 REMAINDER-PLUS-TIMES-2))))
(PUTPROPS SUB1-P-IS-INVOLUTION PROVE-LEMMA ((REWRITE)
(IMPLIES (PRIME P)
(EQUAL (INVERSE (SUB1 P)
P)
(SUB1 P)))
((USE (INVERSE-IS-UNIQUE (M (SUB1 P))
(X (SUB1 P))))
(DISABLE INVERSE))))
(PUTPROPS N-O-I-LEMMA1 PROVE-LEMMA ((REWRITE)
(EQUAL (DIFFERENCE (TIMES X X)
1)
(TIMES (ADD1 X)
(SUB1 X)))))
(PUTPROPS N-O-I-LEMMA2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL (REMAINDER (DIFFERENCE (TIMES J J)
1)
P)
0))
(OR (EQUAL (REMAINDER (ADD1 J)
P)
0)
(EQUAL (REMAINDER (SUB1 J)
P)
0)))))
(PUTPROPS N-O-I-LEMMA3 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (LESSP A 1))
(EQUAL (REMAINDER A P)
1))
(EQUAL (REMAINDER (SUB1 A)
P)
0))
((USE (EQUAL-MODS-TRICK-2 (B 1)))
(DISABLE N-O-I-LEMMA1))))
(PUTPROPS N-O-I-LEMMA4 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P)
0))
(EQUAL (INVERSE J P)
J))
(OR (EQUAL (REMAINDER (ADD1 J)
P)
0)
(EQUAL (REMAINDER (SUB1 J)
P)
0)))
((USE (INVERSE-INVERTS)
(N-O-I-LEMMA2))
(DISABLE INVERSE N-O-I-LEMMA1))))
(PUTPROPS NO-OTHER-INVOLUTIONS PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP J (SUB1 P))
(LESSP 1 J))
(NOT (EQUAL (INVERSE J P)
J)))
((USE (N-O-I-LEMMA4))
(DISABLE INVERSE))))
(PUTPROPS I-O-I-LEMMA PROVE-LEMMA (NIL (EQUAL (SUB1 (TIMES (DIFFERENCE P 2)
(DIFFERENCE P 2)))
(TIMES (DIFFERENCE P 3)
(SUB1 P)))))
(PUTPROPS INVERSE-OF-INVERSE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P)
0)))
(EQUAL (INVERSE (INVERSE J P)
P)
(REMAINDER J P)))
((USE (I-O-I-LEMMA)
(EXP-MOD-IS-1 (M J)
(J (SUB1 P))
(I (DIFFERENCE P 3)))))))
(PUTPROPS N-Z-I-LEMMA PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P)
0))))
(PUTPROPS NON-ZEROP-INVERSE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P)
0)))
(NOT (ZEROP (INVERSE J P))))
((USE (N-Z-I-LEMMA (I (INVERSE J P)))
(INVERSE-OF-INVERSE))
(DISABLE INVERSE))))
(PUTPROPS B-I-LEMMA2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P)
0))
(EQUAL (INVERSE J P)
(SUB1 P)))
(EQUAL (REMAINDER J P)
(SUB1 P)))
((USE (INVERSE-OF-INVERSE))
(DISABLE INVERSE))))
(PUTPROPS B-I-LEMMA1 PROVE-LEMMA (NIL (IMPLIES (LESSP 1 P)
(LEQ (INVERSE J P)
(SUB1 P)))))
(PUTPROPS BOUNDED-INVERSE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP J (SUB1 P)))
(LESSP (INVERSE J P)
(SUB1 P)))
((USE (B-I-LEMMA1)
(B-I-LEMMA2))
(DISABLE INVERSE))))
(PUTPROPS ALL-NON-ZEROP-INVERSE-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP (INVERSE-LIST I P)))
((USE (NON-ZEROP-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE))))
(PUTPROPS BOUNDED-INVERSE-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P))
(EQUAL J (DIFFERENCE P 2)))
(ALL-LESSEQP (INVERSE-LIST I P)
J))
((USE (BOUNDED-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE))))
(PUTPROPS SUBSETP-POSITIVES PROVE-LEMMA ((REWRITE)
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P))))
(PUTPROPS INVERSE-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (LESSP 1 P)
(EQUAL (INVERSE 1 P)
1))))
(PUTPROPS A-D-I-L-LEMMA1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P)
0))
(LESSP I P)
(MEMBER J (INVERSE-LIST I P)))
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
((USE (INVERSE-OF-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE))))
(PUTPROPS A-D-I-L-LEMMA2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P)
0))
(NOT (EQUAL (REMAINDER J P)
0))
(LESSP I P)
(LESSP J P)
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
(MEMBER J (INVERSE-LIST I P)))
((USE (INVERSE-OF-INVERSE)
(A-D-I-L-LEMMA1 (J (INVERSE J P))))
(DISABLE INVERSE INVERSE-LIST INVERSE-OF-INVERSE
A-D-I-L-LEMMA1))))
(PUTPROPS A-D-I-L-LEMMA3 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I)
P)))
(ALL-DISTINCT (INVERSE-LIST I P)))
((USE (A-D-I-L-LEMMA2 (J I)
(I (SUB1 I)))
(NO-OTHER-INVOLUTIONS (J I)))
(DISABLE INVERSE))))
(PUTPROPS ALL-DISTINCT-INVERSE-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P)))
(ALL-DISTINCT (INVERSE-LIST I P)))
((USE (A-D-I-L-LEMMA3))
(INDUCT (POSITIVES I))
(DISABLE INVERSE))))
(PUTPROPS T-I-L-LEMMA1 PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (REMAINDER (TIMES A B)
P)
1)
(EQUAL (REMAINDER (TIMES A (TIMES B C))
P)
(REMAINDER C P)))
((USE (TIMES-MOD-3 (A (TIMES A B))
(B C)
(N P)))
(DISABLE TIMES-MOD-3))))
(PUTPROPS T-I-L-LEMMA PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (REMAINDER (TIMES I (INVERSE I P))
P)
1)
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST
(SUB1 I)
P))
P)))
((USE (T-I-L-LEMMA1 (A I)
(B (INVERSE I P))
(C (TIMES-LIST (INVERSE-LIST (SUB1 I)
P)))))
(DISABLE T-I-L-LEMMA1 INVERSE INVERSE-INVERTS))))
(PUTPROPS T-I-L-LEMMA3 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P)
0)))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST
(SUB1 I)
P))
P)))
((USE (INVERSE-INVERTS (J I)))
(DISABLE INVERSE INVERSE-LIST TIMES-LIST REMAINDER PRIME))))
(PUTPROPS T-I-L-LEMMA4 PROVE-LEMMA ((REWRITE)
(IMPLIES (LEQ I 1)
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1))))
(PUTPROPS TIMES-INVERSE-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST
I P))
P)
1))
((USE (T-I-L-LEMMA3)
(T-I-L-LEMMA4))
(INDUCT (POSITIVES I))
(DISABLE INVERSE INVERSE-LIST TIMES-LIST T-I-L-LEMMA3
T-I-L-LEMMA4))))
(PUTPROPS DELETE-X-LEAVE-A PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (MEMBER A S)
(NOT (EQUAL A X)))
(MEMBER A (DELETE X S)))))
(PUTPROPS DELETE-MEMBER-LEAVE-SUBSET PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S)))))
(PUTPROPS ALL-LESSEQP-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L)
(SUB1 N)))))
(PUTPROPS POSITIVES-BOUNDED PROVE-LEMMA ((REWRITE)
(IMPLIES (LESSP N M)
(NOT (MEMBER M (POSITIVES N))))))
(PUTPROPS SUBSETP-POSITIVES-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (SUBSETP (POSITIVES N)
L)
(SUBSETP (POSITIVES (SUB1 N))
(DELETE N L)))))
(PUTPROPS NONZEROP-LESSEQP-ZERO PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L)))))
(PUTPROPS PIGEONHOLE2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N)
(SUBSETP (POSITIVES N)
L))
(PERM (POSITIVES N)
L))
((INDUCT (PIGEONHOLE2-INDUCTION L N)))))
(PUTPROPS PERM-POSITIVES-INVERSE-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2)))
(PERM (POSITIVES I)
(INVERSE-LIST I P)))))
(PUTPROPS INVERSE-LIST-FACT PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
(FACT I)))
((USE (TIMES-LIST-EQUAL-FACT (N I)
(L (INVERSE-LIST I P))))
(DISABLE INVERSE-LIST))))
(PUTPROPS W-T-LEMMA PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2)))
(EQUAL (REMAINDER (FACT I)
P)
1))
((USE (TIMES-INVERSE-LIST)))))
(PUTPROPS WILSON-THM PROVE-LEMMA (NIL (IMPLIES (PRIME P)
(EQUAL (REMAINDER (FACT (SUB1 P))
P)
(SUB1 P)))
((USE (W-T-LEMMA (I (SUB1 (SUB1 P))))
(THM-55-SPECIALIZED-TO-PRIMES
(M (SUB1 P))
(X (FACT (SUB1 (SUB1 P))))
(Y 1)))
(DISABLE W-T-LEMMA THM-55-SPECIALIZED-TO-PRIMES))))
(DEFINEQ
(PROVEALL5
(LAMBDA NIL (* kbr: "19-Oct-85 16:31")
(PROVEALL (QUOTE ((NOTE-LIB WILSON)
(DEFN& SQUARES)
(DEFN& RESIDUE)
(PROVE-LEMMA& ALL-SQUARES-1)
(PROVE-LEMMA& ALL-SQUARES-2)
(PROVE-LEMMA& ALL-SQUARES)
(PROVE-LEMMA& EULER-1-1)
(PROVE-LEMMA& EULER-1-2)
(PROVE-LEMMA& EULER-1-3)
(PROVE-LEMMA& EULER-1-4)
(PROVE-LEMMA& EULER-1-5)
(PROVE-LEMMA& EULER-1-6)
(PROVE-LEMMA& EULER-1-7)
(PROVE-LEMMA& EULER-1)
(DEFN& COMPLEMENT)
(TOGGLE G0219 INVERSE T)
(PROVE-LEMMA& COMPLEMENT-WORKS)
(PROVE-LEMMA& BOUNDED-COMPLEMENT)
(TOGGLE COMPLEMENT-OFF COMPLEMENT T)
(PROVE-LEMMA& NON-ZEROP-COMPLEMENT)
(PROVE-LEMMA& COMPLEMENT-IS-UNIQUE)
(TOGGLE SQUARES-OFF SQUARES T)
(PROVE-LEMMA& NO-SELF-COMPLEMENT)
(PROVE-LEMMA& COMPLEMENT-OF-COMPLEMENT)
(DEFN& COMP-LIST)
(PROVE-LEMMA& ALL-NON-ZEROP-COMP-LIST)
(PROVE-LEMMA& BOUNDED-COMP-LIST)
(PROVE-LEMMA& SUBSETP-POSITIVES-COMP-LIST)
(PROVE-LEMMA& COMP-LIST-CLOSED-1)
(PROVE-LEMMA& COMP-LIST-CLOSED-2)
(PROVE-LEMMA& ALL-DISTINCT-COMP-LIST-1)
(PROVE-LEMMA& ALL-DISTINCT-COMP-LIST)
(PROVE-LEMMA& PERM-POSITIVES-COMP-LIST)
(PROVE-LEMMA& COMP-LIST-FACT)
(PROVE-LEMMA& TIMES-MOD-4)
(PROVE-LEMMA& TIMES-COMP-LIST-1)
(PROVE-LEMMA& TIMES-COMP-LIST-2)
(PROVE-LEMMA& QUOTIENT-PLUS-1)
(PROVE-LEMMA& TIMES-COMP-LIST-3)
(PROVE-LEMMA& TIMES-COMP-LIST-4)
(PROVE-LEMMA& TIMES-COMP-LIST-5)
(PROVE-LEMMA& TIMES-COMP-LIST)
(PROVE-LEMMA& SUB1-LENGTH-DELETE)
(PROVE-LEMMA& EQUAL-LENGTH-PERM)
(PROVE-LEMMA& LENGTH-POSITIVES)
(PROVE-LEMMA& EULER-2-1)
(PROVE-LEMMA& EULER-2-2)
(PROVE-LEMMA& EULER-2-3)
(PROVE-LEMMA& EULER-2-4)
(PROVE-LEMMA& EULER-2)
(DEFN& RES1)
(DEFN& REFLECT)
(DEFN& REFLECT-LIST)
(PROVE-LEMMA& DIFF-MOD-1)
(PROVE-LEMMA& REM-DIFF-TIMES)
(PROVE-LEMMA& REFLECT-COMMUTES-WITH-TIMES-1)
(PROVE-LEMMA& REFLECT-COMMUTES-WITH-TIMES-2)
(PROVE-LEMMA& TIMES-EXP-FACT)
(PROVE-LEMMA& REM-REFLECT-LIST-1)
(PROVE-LEMMA& REM-REFLECT-LIST-2)
(PROVE-LEMMA& REM-REFLECT-LIST-3)
(PROVE-LEMMA& DOUBLE-REFLECT)
(PROVE-LEMMA& REM-REFLECT-LIST-4)
(PROVE-LEMMA& REM-REFLECT-LIST-BASE-CASE)
(PROVE-LEMMA& REM-REFLECT-LIST)
(PROVE-LEMMA& LENGTH-REFLECT-LIST)
(PROVE-LEMMA& ALL-LESSEQP-REFLECT-LIST-1)
(PROVE-LEMMA& ALL-LESSEQP-REFLECT-LIST)
(PROVE-LEMMA& ALL-NON-ZEROP-REFLECT-LIST)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST-1)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST-2)
(PROVE-LEMMA& NUMBERP-REMAINDER)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST-3)
(PROVE-LEMMA& PLUS-MOD-1)
(PROVE-LEMMA& PLUS-MOD-2)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST-4)
(SWAP-OUT GAUSS-TEMP-LIB-1)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST-5)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST-6)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST-7)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST-8)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST-9)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST-10)
(PROVE-LEMMA& ALL-DISTINCT-REFLECT-LIST)
(PROVE-LEMMA& TIMES-REFLECT-LIST)
(PROVE-LEMMA& PLUS-X-X-EVEN)
(PROVE-LEMMA& RES1-REM-1-1)
(PROVE-LEMMA& RES1-REM-1)
(PROVE-LEMMA& REMAINDER-LESSP)
(PROVE-LEMMA& RES1-REM-2)
(PROVE-LEMMA& TWO-EVEN)
(PROVE-LEMMA& GAUSS-LEMMA)
(DEFN& PLUS-LIST)
(DEFN& QUOT-LIST)
(DEFN& REM-LIST)
(PROVE-LEMMA& REM-QUOT-LIST)
(DEFN& EVEN3)
(PROVE-LEMMA& EVEN3-PLUS)
(PROVE-LEMMA& EVEN3-DIFF)
(PROVE-LEMMA& EVEN3-TIMES)
(PROVE-LEMMA& EVEN3-REM)
(PROVE-LEMMA& EVEN3-REM-REFLECT)
(PROVE-LEMMA& PERM-PLUS-LIST-1)
(PROVE-LEMMA& PERM-PLUS-LIST)
(PROVE-LEMMA& EVEN3-EVEN)
(PROVE-LEMMA& PLUS-REFLECT-LIST)
(PROVE-LEMMA& EQUALS-HAVE-SAME-PARITY)
(PROVE-LEMMA& RES1-QUOT-LIST)
(DEFN& WINS1)
(DEFN& WINS)
(DEFN& LOSSES1)
(DEFN& LOSSES)
(PROVE-LEMMA& WIN-SOME-LOSE-SOME-1)
(PROVE-LEMMA& WIN-SOME-LOSE-SOME-2)
(PROVE-LEMMA& EQUAL-LOSSES-WINS)
(PROVE-LEMMA& A-WINNER-EVERY-TIME)
(DEFN& MULTS)
(PROVE-LEMMA& LENGTH-MULTS)
(PROVE-LEMMA& LEQ-N-WINS1)
(PROVE-LEMMA& MONOTONE-WINS1)
(DEFN& QUOT-QUOT-INDUCTION)
(PROVE-LEMMA& LEQ-TIMES-QUOT)
(PROVE-LEMMA& LEQ-QUOT-TIMES)
(DEFN& MONOTONE-QUOT-INDUCTION)
(PROVE-LEMMA& MONOTONE-QUOT)
(PROVE-LEMMA& LEQ-QUOT-TIMES-2)
(PROVE-LEMMA& LEQ-QUOT-WINS1-1)
(PROVE-LEMMA& LEQ-QUOT-WINS1-2)
(PROVE-LEMMA& LEQ-QUOT-WINS1)
(DEFN& WINS2)
(PROVE-LEMMA& LEQ-WINS2)
(PROVE-LEMMA& LEQ-WINS1-N)
(PROVE-LEMMA& LEQ-WINS1-WINS2)
(PROVE-LEMMA& LEQ-WINS1)
(PROVE-LEMMA& LEQ-WINS1-QUOT)
(PROVE-LEMMA& EQUAL-QUOT-WINS1)
(PROVE-LEMMA& EQUAL-WINS-PLUS-QUOT-LIST)
(PROVE-LEMMA& GAUSS-COROLLARY)
(PROVE-LEMMA& RESIDUE-QUOT-LIST)
(PROVE-LEMMA& ALL-NON-ZEROP-MULTS)
(SWAP-OUT GAUSS-TEMP-LIB-2)
(PROVE-LEMMA& EMPTY-INTERSECT-MULTS-1)
(PROVE-LEMMA& EMPTY-INTERSECT-MULTS)
(PROVE-LEMMA& EQUAL-PLUS-QUOT-LIST-WINS)
(PROVE-LEMMA& LAW-OF-QUADRATIC-RECIPROCITY)))
NIL GAUSS)))
)
(PUTPROPS SQUARES DEFN ((N P)
(IF (ZEROP N)
(LIST 0)
(CONS (REMAINDER (TIMES N N)
P)
(SQUARES (SUB1 N)
P)))))
(PUTPROPS RESIDUE DEFN ((A P)
(AND (NOT (DIVIDES P A))
(MEMBER (REMAINDER A P)
(SQUARES P P)))))
(PUTPROPS COMPLEMENT DEFN ((J A P)
(REMAINDER (TIMES (INVERSE J P)
A)
P)))
(PUTPROPS COMP-LIST DEFN ((I A P)
(IF (ZEROP I)
NIL
(IF (MEMBER I (COMP-LIST (SUB1 I)
A P))
(COMP-LIST (SUB1 I)
A P)
(CONS I (CONS (COMPLEMENT I A P)
(COMP-LIST (SUB1 I)
A P)))))))
(PUTPROPS RES1 DEFN ((N A P)
(IF (ZEROP N)
T
(IF (LESSP (QUOTIENT P 2)
(REMAINDER (TIMES A N)
P))
(NOT (RES1 (SUB1 N)
A P))
(RES1 (SUB1 N)
A P)))))
(PUTPROPS REFLECT DEFN ((X P)
(DIFFERENCE P X)))
(PUTPROPS REFLECT-LIST DEFN ((N A P)
(IF (ZEROP N)
NIL
(IF (LESSP (QUOTIENT P 2)
(REMAINDER (TIMES A N)
P))
(CONS (REFLECT (REMAINDER (TIMES A N)
P)
P)
(REFLECT-LIST (SUB1 N)
A P))
(CONS (REMAINDER (TIMES A N)
P)
(REFLECT-LIST (SUB1 N)
A P))))))
(PUTPROPS PLUS-LIST DEFN ((L)
(IF (NLISTP L)
0
(PLUS (CAR L)
(PLUS-LIST (CDR L))))))
(PUTPROPS QUOT-LIST DEFN ((N A P)
(IF (ZEROP N)
NIL
(CONS (QUOTIENT (TIMES A N)
P)
(QUOT-LIST (SUB1 N)
A P)))))
(PUTPROPS REM-LIST DEFN ((N A P)
(IF (ZEROP N)
NIL
(CONS (REMAINDER (TIMES A N)
P)
(REM-LIST (SUB1 N)
A P)))))
(PUTPROPS EVEN3 DEFN ((X)
(IF (ZEROP X)
T
(NOT (EVEN3 (SUB1 X))))))
(PUTPROPS WINS1 DEFN ((X L)
(IF (NLISTP L)
0
(IF (LESSP (CAR L)
X)
(ADD1 (WINS1 X (CDR L)))
(WINS1 X (CDR L))))))
(PUTPROPS WINS DEFN ((K L)
(IF (NLISTP K)
0
(PLUS (WINS1 (CAR K)
L)
(WINS (CDR K)
L)))))
(PUTPROPS LOSSES1 DEFN ((X L)
(IF (NLISTP L)
0
(IF (LESSP X (CAR L))
(ADD1 (LOSSES1 X (CDR L)))
(LOSSES1 X (CDR L))))))
(PUTPROPS LOSSES DEFN ((K L)
(IF (NLISTP K)
0
(PLUS (LOSSES1 (CAR K)
L)
(LOSSES (CDR K)
L)))))
(PUTPROPS MULTS DEFN ((N P)
(IF (ZEROP N)
NIL
(CONS (TIMES N P)
(MULTS (SUB1 N)
P)))))
(PUTPROPS QUOT-QUOT-INDUCTION DEFN ((A B C D)
(IF (ZEROP B)
T
(IF (ZEROP D)
T
(IF (LESSP A D)
T
(IF (LESSP C B)
T
(QUOT-QUOT-INDUCTION (DIFFERENCE A D)
B
(DIFFERENCE C B)
D)))))))
(PUTPROPS MONOTONE-QUOT-INDUCTION DEFN ((I J P)
(IF (ZEROP P)
T
(IF (LESSP I P)
T
(IF (LESSP J P)
T
(MONOTONE-QUOT-INDUCTION (DIFFERENCE I P)
(DIFFERENCE J P)
P))))))
(PUTPROPS WINS2 DEFN ((A N P)
(IF (ZEROP N)
0
(IF (LESSP (TIMES N P)
A)
N
(WINS2 A (SUB1 N)
P)))))
(PUTPROPS ALL-SQUARES-1 PROVE-LEMMA (NIL (IMPLIES (AND (NOT (ZEROP P))
(LEQ M N))
(MEMBER (REMAINDER (TIMES M M)
P)
(SQUARES N P)))))
(PUTPROPS ALL-SQUARES-2 PROVE-LEMMA (NIL (EQUAL (REMAINDER (TIMES Y Y)
P)
(REMAINDER (TIMES (REMAINDER Y P)
(REMAINDER Y P))
P))
((USE (TIMES-MOD-1 (X Y)
(N P))
(TIMES-MOD-3 (B (REMAINDER Y P))
(A Y)
(N P)))
(DISABLE TIMES-MOD-1 TIMES-MOD-3))))
(PUTPROPS ALL-SQUARES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP P))
(NOT (MEMBER X (SQUARES P P))))
(NOT (EQUAL X (REMAINDER (TIMES Y Y)
P))))
((USE (ALL-SQUARES-1 (N P)
(M (REMAINDER Y P)))
(ALL-SQUARES-2))
(DISABLE TIMES-MOD-1 TIMES-MOD-3))))
(PUTPROPS EULER-1-1 PROVE-LEMMA (NIL (IMPLIES (NOT (DIVIDES 2 P))
(EQUAL (TIMES 2 (QUOTIENT P 2))
(SUB1 P)))))
(PUTPROPS EULER-1-2 PROVE-LEMMA (NIL (IMPLIES (NOT (DIVIDES 2 P))
(EQUAL (EXP (TIMES I I)
(QUOTIENT P 2))
(EXP I (SUB1 P))))
((USE (EXP-EXP (J 2)
(K (QUOTIENT P 2)))
(EULER-1-1))
(DISABLE EXP-EXP))))
(PUTPROPS EULER-1-3 PROVE-LEMMA (NIL (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER (EXP A C)
P)
(REMAINDER (EXP B C)
P)))
((USE (REMAINDER-EXP (I C)
(N P))
(REMAINDER-EXP (A B)
(I C)
(N P)))
(DISABLE REMAINDER-EXP))))
(PUTPROPS EULER-1-4 PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P I)))
(EQUAL (REMAINDER (EXP (TIMES I I)
(QUOTIENT P 2))
P)
1))
((USE (EULER-1-2))
(DISABLE LESSP-REMAINDER-DIVISOR PRIME))))
(PUTPROPS EULER-1-5 PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(EQUAL (REMAINDER A P)
(REMAINDER (TIMES I I)
P)))
(NOT (DIVIDES P I)))
((USE (PRIME-KEY-REWRITE (A I)
(B I)))
(DISABLE PRIME-KEY-REWRITE PRIME))))
(PUTPROPS EULER-1-6 PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(EQUAL (REMAINDER A P)
(REMAINDER (TIMES I I)
P)))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2))
P)
1))
((USE (EULER-1-4)
(EULER-1-5)
(EULER-1-3 (B (TIMES I I))
(C (QUOTIENT P 2))))
(DISABLE PRIME LESSP-REMAINDER-DIVISOR B-ILEMMA2 LESSP
SUB1-NNUMBERP REMAINDER-0-CROCK REMAINDER))))
(PUTPROPS EULER-1-7 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(MEMBER (REMAINDER A P)
(SQUARES I P)))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2))
P)
1))
((USE (EULER-1-6))
(INDUCT (SQUARES I P))
(DISABLE PRIME REMAINDER LESSP-REMAINDER-DIVISOR))))
(PUTPROPS EULER-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(RESIDUE A P))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2))
P)
1))
((DISABLE PRIME))))
(PUTPROPS COMPLEMENT-WORKS PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P J)))
(EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P))
P)
(REMAINDER A P)))
((USE (INVERSE-INVERTS)
(TIMES-MOD-3 (A (TIMES J (INVERSE J P)))
(B A)
(N P)))
(DISABLE INVERSE-INVERTS TIMES-MOD-3 PRIME))))
(PUTPROPS BOUNDED-COMPLEMENT PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZEROP P))
(LESSP (COMPLEMENT J A P)
P))))
(PUTPROPS NON-ZEROP-COMPLEMENT PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P J))
(NOT (DIVIDES P A)))
(NOT (ZEROP (COMPLEMENT J A P))))
((USE (COMPLEMENT-WORKS))
(DISABLE COMPLEMENT-WORKS PRIME))))
(PUTPROPS COMPLEMENT-IS-UNIQUE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(EQUAL (REMAINDER (TIMES J X)
P)
(REMAINDER A P)))
(EQUAL (COMPLEMENT J A P)
(REMAINDER X P)))
((USE (COMPLEMENT-WORKS)
(THM-55-SPECIALIZED-TO-PRIMES
(M J)
(Y (COMPLEMENT J A P))))
(DISABLE COMPLEMENT-WORKS THM-55-SPECIALIZED-TO-PRIMES
PRIME))))
(PUTPROPS NO-SELF-COMPLEMENT PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P J))
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(NOT (EQUAL J (COMPLEMENT J A P))))
((USE (COMPLEMENT-WORKS)
(ALL-SQUARES (X (REMAINDER A P))
(Y J)))
(DISABLE COMPLEMENT-WORKS ALL-SQUARES PRIME1))))
(PUTPROPS COMPLEMENT-OF-COMPLEMENT PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P J))
(NOT (DIVIDES P A)))
(EQUAL (COMPLEMENT (COMPLEMENT J A P)
A P)
(REMAINDER J P)))
((USE (COMPLEMENT-WORKS)
(COMPLEMENT-IS-UNIQUE (J (COMPLEMENT J A P))
(X J)))
(DISABLE COMPLEMENT-WORKS COMPLEMENT-IS-UNIQUE))))
(PUTPROPS ALL-NON-ZEROP-COMP-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I P)
(NOT (DIVIDES P A)))
(ALL-NON-ZEROP (COMP-LIST I A P)))
((USE (NON-ZEROP-COMPLEMENT (J I)))
(INDUCT (COMP-LIST I A P)))))
(PUTPROPS BOUNDED-COMP-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (LESSP I P)
(ALL-LESSEQP (COMP-LIST I A P)
(SUB1 P)))
((USE (BOUNDED-COMPLEMENT (J I)))
(INDUCT (COMP-LIST I A P)))))
(PUTPROPS SUBSETP-POSITIVES-COMP-LIST PROVE-LEMMA ((REWRITE)
(SUBSETP (POSITIVES N)
(COMP-LIST N A P))))
(PUTPROPS COMP-LIST-CLOSED-1 PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(NOT (ZEROP I))
(LESSP I P)
(NOT (DIVIDES P A))
(MEMBER J (COMP-LIST I A P)))
(MEMBER (COMPLEMENT J A P)
(COMP-LIST I A P)))
((USE (COMPLEMENT-OF-COMPLEMENT (J I)))
(INDUCT (COMP-LIST I A P))
(DISABLE COMPLEMENT-OF-COMPLEMENT))))
(PUTPROPS COMP-LIST-CLOSED-2 PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(NOT (ZEROP I))
(NOT (ZEROP J))
(LESSP I P)
(LESSP J P)
(NOT (DIVIDES P A))
(MEMBER (COMPLEMENT J A P)
(COMP-LIST I A P)))
(MEMBER J (COMP-LIST I A P)))
((USE (COMPLEMENT-OF-COMPLEMENT)
(COMP-LIST-CLOSED-1 (J (COMPLEMENT J A P))))
(DISABLE COMPLEMENT-OF-COMPLEMENT COMP-LIST))))
(PUTPROPS ALL-DISTINCT-COMP-LIST-1 PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(LESSP I P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P))
(ALL-DISTINCT
(COMP-LIST (SUB1 I)
A P)))
(ALL-DISTINCT (COMP-LIST I A P)))
((USE (COMP-LIST-CLOSED-2 (J I)
(I (SUB1 I)))
(NO-SELF-COMPLEMENT (J I)))
(DISABLE PRIME))))
(PUTPROPS ALL-DISTINCT-COMP-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(ALL-DISTINCT (COMP-LIST I A P)))
((USE (ALL-DISTINCT-COMP-LIST-1))
(INDUCT (POSITIVES I))
(DISABLE PRIME))))
(PUTPROPS PERM-POSITIVES-COMP-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(PERM (POSITIVES (SUB1 P))
(COMP-LIST (SUB1 P)
A P)))))
(PUTPROPS COMP-LIST-FACT PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(EQUAL (TIMES-LIST (COMP-LIST (SUB1 P)
A P))
(FACT (SUB1 P))))
((USE (TIMES-LIST-EQUAL-FACT (N (SUB1 P))
(L (COMP-LIST (SUB1 P)
A P))))
(DISABLE TIMES-LIST-EQUAL-FACT COMP-LIST))))
(PUTPROPS TIMES-MOD-4 PROVE-LEMMA (NIL (IMPLIES (EQUAL (REMAINDER (TIMES I J)
P)
(REMAINDER A P))
(EQUAL (REMAINDER (TIMES I (TIMES J K))
P)
(REMAINDER (TIMES A (REMAINDER K P))
P)))
((USE (TIMES-MOD-3 (A (TIMES I J))
(B K)
(N P)))
(DISABLE TIMES-MOD-3))))
(PUTPROPS TIMES-COMP-LIST-1 PROVE-LEMMA (NIL
(IMPLIES (AND (EQUAL (REMAINDER (TIMES I (COMPLEMENT I A P))
P)
(REMAINDER A P))
(NOT (ZEROP I))
(NOT (MEMBER I (COMP-LIST (SUB1 I)
A P))))
(EQUAL (REMAINDER (TIMES-LIST (COMP-LIST I A P))
P)
(REMAINDER (TIMES A (REMAINDER (TIMES-LIST (COMP-LIST (SUB1 I)
A P))
P))
P)))
((USE (TIMES-MOD-4 (J (COMPLEMENT I A P))
(K (TIMES-LIST (COMP-LIST (SUB1 I)
A P)))))
(DISABLE COMPLEMENT-WORKS))))
(PUTPROPS TIMES-COMP-LIST-2 PROVE-LEMMA (NIL
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P I))
(NOT (MEMBER I (COMP-LIST (SUB1 I)
A P))))
(EQUAL (REMAINDER (TIMES-LIST (COMP-LIST I A P))
P)
(REMAINDER (TIMES A (REMAINDER (TIMES-LIST (COMP-LIST (SUB1 I)
A P))
P))
P)))
((USE (TIMES-COMP-LIST-1)
(COMPLEMENT-WORKS (J I)))
(DISABLE COMPLEMENT-WORKS COMP-LIST TIMES-LIST PRIME))))
(PUTPROPS QUOTIENT-PLUS-1 PROVE-LEMMA (NIL (IMPLIES (AND (NOT (ZEROP N))
(NUMBERP X)
(EQUAL Y (PLUS X N)))
(EQUAL (QUOTIENT Y N)
(ADD1 (QUOTIENT X N))))))
(PUTPROPS TIMES-COMP-LIST-3 PROVE-LEMMA (NIL
(IMPLIES (AND (NOT (ZEROP I))
(NOT (MEMBER I (COMP-LIST (SUB1 I)
A P))))
(EQUAL (QUOTIENT (LENGTH (COMP-LIST I A P))
2)
(ADD1 (QUOTIENT (LENGTH (COMP-LIST (SUB1 I)
A P))
2))))
((USE (QUOTIENT-PLUS-1 (X (LENGTH (COMP-LIST (SUB1 I)
A P)))
(Y (LENGTH (COMP-LIST I A P)))
(N 2))))))
(PUTPROPS TIMES-COMP-LIST-4 PROVE-LEMMA (NIL
(IMPLIES (AND (PRIME P)
(NOT (ZEROP I))
(LESSP I P)
(EQUAL (REMAINDER (TIMES-LIST (COMP-LIST (SUB1 I)
A P))
P)
(REMAINDER (EXP A (QUOTIENT (LENGTH (COMP-LIST (SUB1 I)
A P))
2))
P)))
(EQUAL (REMAINDER (TIMES-LIST (COMP-LIST I A P))
P)
(REMAINDER (EXP A (QUOTIENT (LENGTH (COMP-LIST I A P))
2))
P)))
((USE (TIMES-COMP-LIST-2)
(TIMES-COMP-LIST-3)
(TIMES-MOD-1 (X A)
(Y (EXP A (QUOTIENT (LENGTH (COMP-LIST (SUB1 I)
A P))
2)))
(N P)))
(DISABLE PRIME TIMES-MOD-1 TIMES-LIST))))
(PUTPROPS TIMES-COMP-LIST-5 PROVE-LEMMA (NIL
(IMPLIES (ZEROP I)
(EQUAL (REMAINDER (TIMES-LIST (COMP-LIST I A P))
P)
(REMAINDER (EXP A (QUOTIENT (LENGTH (COMP-LIST I A P))
2))
P)))))
(PUTPROPS TIMES-COMP-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (COMP-LIST I A P))
P)
(REMAINDER (EXP A (QUOTIENT (LENGTH (COMP-LIST I A P))
2))
P)))
((USE (TIMES-COMP-LIST-4)
(TIMES-COMP-LIST-5))
(INDUCT (POSITIVES I))
(DISABLE PRIME REMAINDER TIMES-LIST COMP-LIST QUOTIENT LENGTH))))
(PUTPROPS SUB1-LENGTH-DELETE PROVE-LEMMA ((REWRITE)
(IMPLIES (MEMBER X B)
(EQUAL (LENGTH (DELETE X B))
(SUB1 (LENGTH B))))))
(PUTPROPS EQUAL-LENGTH-PERM PROVE-LEMMA (NIL (IMPLIES (PERM A B)
(EQUAL (LENGTH A)
(LENGTH B)))
((INDUCT (PERM A B)))))
(PUTPROPS LENGTH-POSITIVES PROVE-LEMMA ((REWRITE)
(EQUAL (LENGTH (POSITIVES N))
(FIX N))
((INDUCT (POSITIVES N)))))
(PUTPROPS EULER-2-1 PROVE-LEMMA (NIL (IMPLIES
(AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(EQUAL (REMAINDER (EXP A (QUOTIENT
(LENGTH (COMP-LIST (SUB1 P)
A P))
2))
P)
(SUB1 P)))
((USE (TIMES-COMP-LIST (I (SUB1 P)))
(COMP-LIST-FACT)
(WILSON-THM))
(DISABLE TIMES-COMP-LIST COMP-LIST-FACT))))
(PUTPROPS EULER-2-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(EQUAL (LENGTH (COMP-LIST (SUB1 P)
A P))
(SUB1 P)))
((USE (EQUAL-LENGTH-PERM (A (POSITIVES (SUB1 P)))
(B (COMP-LIST (SUB1 P)
A P)))
(PERM-POSITIVES-COMP-LIST))
(DISABLE EQUAL-LENGTH-PERM PERM-POSITIVES-COMP-LIST))))
(PUTPROPS EULER-2-3 PROVE-LEMMA (NIL (IMPLIES (NOT (ZEROP P))
(EQUAL (DIVIDES 2 P)
(NOT (DIVIDES 2 (SUB1 P)))))
((INDUCT (ODD P)))))
(PUTPROPS EULER-2-4 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (DIVIDES 2 P))
(EQUAL (QUOTIENT (SUB1 P)
2)
(QUOTIENT P 2)))
((USE (EULER-2-3)
(REMAINDER-QUOTIENT (X P)
(Y 2))
(REMAINDER-QUOTIENT (X (SUB1 P))
(Y 2)))
(DISABLE RES-REM-2LEMMA3 REMAINDER-QUOTIENT))))
(PUTPROPS EULER-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2))
P)
(SUB1 P)))
((USE (EULER-2-1))
(DISABLE EULER-2-1 PRIME DIVIDES RESIDUE EXP QUOTIENT LENGTH
COMP-LIST))))
(PUTPROPS DIFF-MOD-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (LEQ B A)
(EQUAL (REMAINDER (DIFFERENCE A (REMAINDER B P))
P)
(REMAINDER (DIFFERENCE A B)
P)))
((USE (REMAINDER-QUOTIENT (X B)
(Y P))
(REMAINDER-PLUS-TIMES-1 (X (DIFFERENCE A B))
(I (QUOTIENT B P))
(J P)))
(DISABLE REMAINDER-QUOTIENT REMAINDER-PLUS-TIMES-1
REMAINDER-PLUS-TIMES-2))))
(PUTPROPS REM-DIFF-TIMES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (LESSP X P)
(NOT (ZEROP X))
(NOT (ZEROP B)))
(EQUAL (REMAINDER (DIFFERENCE (TIMES B P)
X)
P)
(DIFFERENCE P X)))
((USE (REMAINDER-PLUS-TIMES-1 (X (DIFFERENCE P X))
(I (SUB1 B))
(J P)))
(DISABLE REMAINDER-PLUS-TIMES-1 REMAINDER-PLUS-TIMES-2))))
(PUTPROPS REFLECT-COMMUTES-WITH-TIMES-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (LEQ Y P)
(EQUAL (REMAINDER (TIMES (REFLECT Y P)
X)
P)
(REMAINDER (REFLECT (REMAINDER (TIMES Y X)
P)
P)
P)))
((USE (DIFF-MOD-1 (A (TIMES P X))
(B (TIMES Y X)))
(LESSP-TIMES-CANCELLATION (Z X)
(X Y)
(Y P))
(REM-DIFF-TIMES (B X)
(X (REMAINDER (TIMES Y X)
P))))
(DISABLE LESSP-TIMES-CANCELLATION REM-DIFF-TIMES DIFF-MOD-1))))
(PUTPROPS REFLECT-COMMUTES-WITH-TIMES-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (LEQ Y P)
(EQUAL (REMAINDER (TIMES X (REFLECT Y P))
P)
(REMAINDER (REFLECT (REMAINDER (TIMES X Y)
P)
P)
P)))
((USE (REFLECT-COMMUTES-WITH-TIMES-1))
(DISABLE REFLECT-COMMUTES-WITH-TIMES-1 REFLECT))))
(PUTPROPS TIMES-EXP-FACT PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZEROP N))
(EQUAL (REMAINDER (TIMES (TIMES A N)
(TIMES (EXP A (SUB1 N))
(FACT (SUB1 N))))
P)
(REMAINDER (TIMES (EXP A N)
(FACT N))
P)))))
(PUTPROPS REM-REFLECT-LIST-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP P))
(NOT (ZEROP N))
(NOT (LESSP (QUOTIENT P 2)
(REMAINDER (TIMES A N)
P)))
(EQUAL (REMAINDER
(TIMES-LIST (REFLECT-LIST
(SUB1 N)
A P))
P)
(REMAINDER
(TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST
N A P))
P)
(REMAINDER (TIMES (EXP A N)
(FACT N))
P)))
((USE (REMAINDER-EXP-LEMMA
(A P)
(X (TIMES A N))
(Y (TIMES-LIST (REFLECT-LIST (SUB1 N)
A P)))
(Z (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N))))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA REFLECT))))
(PUTPROPS REM-REFLECT-LIST-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP P))
(NOT (ZEROP N))
(LESSP (QUOTIENT P 2)
(REMAINDER (TIMES A N)
P))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST (SUB1 N)
A P))
P)
(REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P))
P)
(REMAINDER (REFLECT (REMAINDER (TIMES (EXP A N)
(FACT N))
P)
P)
P)))
((USE (REMAINDER-EXP-LEMMA (A P)
(X (TIMES A N))
(Y (TIMES-LIST (REFLECT-LIST (SUB1 N)
A P)))
(Z (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N))))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA REFLECT))))
(PUTPROPS REM-REFLECT-LIST-3 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP P))
(NOT (ZEROP N))
(NOT (LESSP (QUOTIENT P 2)
(REMAINDER (TIMES A N)
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST (SUB1 N)
A P))
P)
(REMAINDER (REFLECT (REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P)
P)
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P))
P)
(REMAINDER (REFLECT (REMAINDER (TIMES (EXP A N)
(FACT N))
P)
P)
P)))
((USE (REMAINDER-EXP-LEMMA (A P)
(X (TIMES A N))
(Y (TIMES-LIST (REFLECT-LIST (SUB1 N)
A P)))
(Z (REFLECT (REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P)
P))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA REFLECT))))
(PUTPROPS DOUBLE-REFLECT PROVE-LEMMA ((REWRITE)
(IMPLIES (LEQ A P)
(EQUAL (REMAINDER (REFLECT (REMAINDER (REFLECT
A P)
P)
P)
P)
(REMAINDER A P)))))
(PUTPROPS REM-REFLECT-LIST-4 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP P))
(NOT (ZEROP N))
(LESSP (QUOTIENT P 2)
(REMAINDER (TIMES A N)
P))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST (SUB1 N)
A P))
P)
(REMAINDER (REFLECT (REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P)
P)
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P))
P)
(REMAINDER (TIMES (EXP A N)
(FACT N))
P)))
((USE (REMAINDER-EXP-LEMMA (A P)
(X (TIMES A N))
(Y (TIMES-LIST (REFLECT-LIST (SUB1 N)
A P)))
(Z (REFLECT (REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P)
P))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA REFLECT))))
(PUTPROPS REM-REFLECT-LIST-BASE-CASE PROVE-LEMMA ((REWRITE)
(IMPLIES (ZEROP N)
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P))
P)
(REMAINDER (TIMES (EXP A N)
(FACT N))
P)))))
(PUTPROPS REM-REFLECT-LIST PROVE-LEMMA (NIL
(IMPLIES (NOT (ZEROP P))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P))
P)
(IF (RES1 N A P)
(REMAINDER (TIMES (EXP A N)
(FACT N))
P)
(REMAINDER (REFLECT (REMAINDER (TIMES (EXP A N)
(FACT N))
P)
P)
P))))
((HANDS-OFF TIMES-LIST REFLECT-LIST QUOTIENT EXP FACT TIMES)
(DISABLE REFLECT))))
(PUTPROPS LENGTH-REFLECT-LIST PROVE-LEMMA ((REWRITE)
(EQUAL (LENGTH (REFLECT-LIST N A P))
(FIX N))
((INDUCT (POSITIVES N)))))
(PUTPROPS ALL-LESSEQP-REFLECT-LIST-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (LESSP (QUOTIENT P 2)
X)
(NOT (LESSP (QUOTIENT P 2)
(REFLECT X P))))))
(PUTPROPS ALL-LESSEQP-REFLECT-LIST PROVE-LEMMA ((REWRITE)
(ALL-LESSEQP (REFLECT-LIST N A P)
(QUOTIENT P 2))
((DISABLE REFLECT))))
(PUTPROPS ALL-NON-ZEROP-REFLECT-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(LESSP B P))
(ALL-NON-ZEROP (REFLECT-LIST B A P)))
((INDUCT (REFLECT-LIST B A P))
(DISABLE PRIME1))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP J I)
(LESSP I P)
(NOT (DIVIDES P A)))
(NOT (EQUAL (REMAINDER (TIMES A I)
P)
(REMAINDER (TIMES A J)
P))))
((DISABLE PRIME))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NUMBERP X)
(NUMBERP Y)
(LESSP X P)
(LESSP Y P))
(EQUAL (EQUAL (DIFFERENCE P X)
(DIFFERENCE P Y))
(EQUAL X Y)))))
(PUTPROPS NUMBERP-REMAINDER PROVE-LEMMA ((REWRITE)
(NUMBERP (REMAINDER A P))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST-3 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP J I)
(LESSP I P)
(NOT (DIVIDES P A)))
(NOT (EQUAL (REFLECT (REMAINDER (TIMES A I)
P)
P)
(REFLECT (REMAINDER (TIMES A J)
P)
P))))
((USE (ALL-DISTINCT-REFLECT-LIST-1))
(HANDS-OFF DIFFERENCE REMAINDER TIMES)
(DISABLE ALL-DISTINCT-REFLECT-LIST-1 PRIME))))
(PUTPROPS PLUS-MOD-1 PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (PLUS (REMAINDER X P)
Y)
P)
(REMAINDER (PLUS X Y)
P))
((USE (REMAINDER-QUOTIENT (Y P))
(REMAINDER-PLUS-TIMES-1 (J P)
(X (PLUS (REMAINDER X P)
Y))
(I (QUOTIENT X P))))
(DISABLE REMAINDER-QUOTIENT REMAINDER-QUOTIENT-ELIM
REMAINDER-PLUS-TIMES-1))))
(PUTPROPS PLUS-MOD-2 PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (PLUS Y (REMAINDER X P))
P)
(REMAINDER (PLUS X Y)
P))
((USE (PLUS-MOD-1))
(DISABLE PLUS-MOD-1))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST-4 PROVE-LEMMA (NIL (IMPLIES (AND (EQUAL X (DIFFERENCE P Y))
(LESSP Y P))
(EQUAL (REMAINDER (PLUS X Y)
P)
0))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST-5 PROVE-LEMMA (NIL
(IMPLIES (AND (EQUAL (REMAINDER (TIMES A I)
P)
(DIFFERENCE P (REMAINDER (TIMES A J)
P)))
(NOT (ZEROP P)))
(EQUAL (REMAINDER (TIMES A (PLUS I J))
P)
0))
((USE (ALL-DISTINCT-REFLECT-LIST-4 (X (REMAINDER (TIMES A I)
P))
(Y (REMAINDER (TIMES A J)
P)))))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST-6 PROVE-LEMMA (NIL (IMPLIES (AND (LEQ I (QUOTIENT P 2))
(LESSP J I))
(AND (NOT (ZEROP (PLUS I J)))
(LESSP (PLUS I J)
P)))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST-7 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2))
(LESSP J I))
(NOT (EQUAL (REMAINDER (TIMES A I)
P)
(REFLECT (REMAINDER (TIMES A J)
P)
P))))
((USE (ALL-DISTINCT-REFLECT-LIST-5)
(ALL-DISTINCT-REFLECT-LIST-6))
(HANDS-OFF DIFFERENCE TIMES PLUS)
(DISABLE PRIME1))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST-8 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2))
(LESSP J I))
(NOT (EQUAL (REFLECT (REMAINDER (TIMES A I)
P)
P)
(REMAINDER (TIMES A J)
P))))
((USE (ALL-DISTINCT-REFLECT-LIST-5 (J I)
(I J))
(ALL-DISTINCT-REFLECT-LIST-6))
(HANDS-OFF TIMES DIFFERENCE)
(DISABLE PRIME1))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST-9 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2))
(LESSP J I))
(NOT (MEMBER (REMAINDER (TIMES A I)
P)
(REFLECT-LIST J A P))))
((USE (ALL-DISTINCT-REFLECT-LIST-1))
(INDUCT (REFLECT-LIST J A P))
(HANDS-OFF QUOTIENT REMAINDER TIMES)
(DISABLE PRIME1 REFLECT
ALL-DISTINCT-REFLECT-LIST-1))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST-10 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2))
(LESSP J I))
(NOT (MEMBER (REFLECT (REMAINDER (TIMES A I)
P)
P)
(REFLECT-LIST J A P))))
((USE (ALL-DISTINCT-REFLECT-LIST-3))
(INDUCT (REFLECT-LIST J A P))
(HANDS-OFF QUOTIENT REMAINDER TIMES)
(DISABLE PRIME1 REFLECT ALL-DISTINCT-REFLECT-LIST-3))))
(PUTPROPS ALL-DISTINCT-REFLECT-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2)))
(ALL-DISTINCT (REFLECT-LIST I A P)))
((USE (ALL-DISTINCT-REFLECT-LIST-9
(J (SUB1 I)))
(ALL-DISTINCT-REFLECT-LIST-10
(J (SUB1 I))))
(INDUCT (REFLECT-LIST I A P))
(HANDS-OFF QUOTIENT REMAINDER TIMES)
(DISABLE ALL-DISTINCT-REFLECT-LIST-9
ALL-DISTINCT-REFLECT-LIST-10 PRIME
DIVIDES REFLECT))))
(PUTPROPS TIMES-REFLECT-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A)))
(EQUAL (TIMES-LIST (REFLECT-LIST (QUOTIENT
P 2)
A P))
(FACT (QUOTIENT P 2))))
((USE (PIGEON-HOLE-PRINCIPLE (L (REFLECT-LIST
(QUOTIENT P 2)
A P))))
(HANDS-OFF QUOTIENT REMAINDER)
(DISABLE PRIME1 REFLECT-LIST TIMES-LIST FACT))))
(PUTPROPS PLUS-X-X-EVEN PROVE-LEMMA ((REWRITE)
(EQUAL (REMAINDER (PLUS X X)
2)
0)))
(PUTPROPS RES1-REM-1-1 PROVE-LEMMA (NIL (IMPLIES (AND (NOT (ZEROP X))
(NOT (DIVIDES 2 P)))
(NOT (EQUAL (REMAINDER (DIFFERENCE P X)
P)
X)))
((USE (DIFFERENCE-ELIM (Y P))))))
(PUTPROPS RES1-REM-1 PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(RES1 (QUOTIENT P 2)
A P))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2))
P)
1))
((USE (REM-REFLECT-LIST (N (QUOTIENT P 2)))
(PRIME-KEY-TRICK (M (FACT (QUOTIENT P 2)))
(A (EXP A (QUOTIENT P 2)))
(B 1)))
(DISABLE PRIME-KEY-TRICK LESSP-REMAINDER-DIVISOR PRIME1))))
(PUTPROPS REMAINDER-LESSP PROVE-LEMMA (NIL (IMPLIES (LESSP A P)
(EQUAL (REMAINDER A P)
(FIX A)))))
(PUTPROPS RES1-REM-2 PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(NOT (RES1 (QUOTIENT P 2)
A P)))
(NOT (EQUAL (REMAINDER (EXP A (QUOTIENT P 2))
P)
1)))
((USE (REM-REFLECT-LIST (N (QUOTIENT P 2)))
(REMAINDER-EXP-LEMMA (A P)
(Y (EXP A (QUOTIENT P 2)))
(Z 1)
(X (FACT (QUOTIENT P 2))))
(RES1-REM-1-1 (X (REMAINDER (FACT (QUOTIENT P 2))
P)))
(REMAINDER-LESSP (A 1)))
(HANDS-OFF FACT EXP QUOTIENT REMAINDER REFLECT-LIST)
(DISABLE LESSP-REMAINDER-DIVISOR PRIME1 DIFFERENCE
COROLLARY-55 REMAINDER-EXP-LEMMA))))
(PUTPROPS TWO-EVEN PROVE-LEMMA (NIL (IMPLIES (NOT (DIVIDES 2 P))
(NOT (EQUAL (SUB1 P)
1)))
((INDUCT (ODD P)))))
(PUTPROPS GAUSS-LEMMA PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (DIVIDES 2 P)))
(EQUAL (RES1 (QUOTIENT P 2)
A P)
(RESIDUE A P)))
((USE (EULER-1)
(EULER-2)
(RES1-REM-1)
(RES1-REM-2)
(TWO-EVEN))
(DISABLE EULER-1 EULER-2 QUOTIENT EXP RESIDUE RES1 PRIME
DIVIDES))))
(PUTPROPS REM-QUOT-LIST PROVE-LEMMA (NIL (EQUAL (TIMES A (PLUS-LIST (POSITIVES N)))
(PLUS (TIMES P (PLUS-LIST (QUOT-LIST N A P)))
(PLUS-LIST (REM-LIST N A P))))))
(PUTPROPS EVEN3-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (EVEN3 (PLUS A B))
(EQUAL (EVEN3 A)
(EVEN3 B)))))
(PUTPROPS EVEN3-DIFF PROVE-LEMMA ((REWRITE)
(IMPLIES (LEQ X P)
(EQUAL (EVEN3 (DIFFERENCE P X))
(EQUAL (EVEN3 P)
(EVEN3 X))))))
(PUTPROPS EVEN3-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (EVEN3 (TIMES A B))
(OR (EVEN3 A)
(EVEN3 B)))))
(PUTPROPS EVEN3-REM PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (EVEN3 P))
(EQUAL (EVEN3 (DIFFERENCE P (REMAINDER X P)))
(NOT (EVEN3 (REMAINDER X P)))))))
(PUTPROPS EVEN3-REM-REFLECT PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (EVEN3 P))
(EQUAL (RES1 N A P)
(IFF (EVEN3 (PLUS-LIST (REM-LIST N A P)))
(EVEN3 (PLUS-LIST (REFLECT-LIST N A P))))))))
(PUTPROPS PERM-PLUS-LIST-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (MEMBER X M)
(EQUAL (PLUS X (PLUS-LIST (DELETE X M)))
(PLUS-LIST M)))))
(PUTPROPS PERM-PLUS-LIST PROVE-LEMMA (NIL (IMPLIES (PERM L M)
(EQUAL (PLUS-LIST L)
(PLUS-LIST M)))))
(PUTPROPS EVEN3-EVEN PROVE-LEMMA (NIL (EQUAL (DIVIDES 2 P)
(EVEN3 P))))
(PUTPROPS PLUS-REFLECT-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (EVEN3 P)))
(EQUAL (PLUS-LIST (REFLECT-LIST (QUOTIENT P 2)
A P))
(PLUS-LIST (POSITIVES (QUOTIENT P 2)))))
((USE (PERM-PLUS-LIST (M (REFLECT-LIST (QUOTIENT P 2)
A P))
(L (POSITIVES (QUOTIENT P 2))))
(PIGEON-HOLE-PRINCIPLE (L (REFLECT-LIST
(QUOTIENT P 2)
A P)))
(EVEN3-EVEN)
(ALL-NON-ZEROP-REFLECT-LIST (B (QUOTIENT P 2))))
(DISABLE PRIME))))
(PUTPROPS EQUALS-HAVE-SAME-PARITY PROVE-LEMMA (NIL (IMPLIES (EQUAL X Y)
(EQUAL (EVEN3 X)
(EVEN3 Y)))))
(PUTPROPS RES1-QUOT-LIST PROVE-LEMMA (NIL
(IMPLIES (AND (PRIME P)
(NOT (EVEN3 P))
(NOT (EVEN3 A))
(NOT (DIVIDES P A)))
(EQUAL (RES1 (QUOTIENT P 2)
A P)
(EVEN3 (PLUS-LIST (QUOT-LIST (QUOTIENT P 2)
A P)))))
((USE (REM-QUOT-LIST (N (QUOTIENT P 2)))
(EQUALS-HAVE-SAME-PARITY (X (TIMES A (PLUS-LIST (POSITIVES (QUOTIENT P 2)))))
(Y (PLUS (TIMES P (PLUS-LIST (QUOT-LIST (QUOTIENT P 2)
A P)))
(PLUS-LIST (REM-LIST (QUOTIENT P 2)
A P))))))
(DISABLE PRIME))))
(PUTPROPS WIN-SOME-LOSE-SOME-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (MEMBER X L))
(ALL-NON-ZEROP L))
(EQUAL (PLUS (LOSSES1 X L)
(WINS1 X L))
(LENGTH L)))))
(PUTPROPS WIN-SOME-LOSE-SOME-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NLISTP (INTERSECT L M))
(ALL-NON-ZEROP L)
(ALL-NON-ZEROP M))
(EQUAL (PLUS (WINS L M)
(LOSSES L M))
(TIMES (LENGTH L)
(LENGTH M))))))
(PUTPROPS EQUAL-LOSSES-WINS PROVE-LEMMA ((REWRITE)
(EQUAL (LOSSES L M)
(WINS M L))))
(PUTPROPS A-WINNER-EVERY-TIME PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NLISTP (INTERSECT L M))
(ALL-NON-ZEROP L)
(ALL-NON-ZEROP M))
(EQUAL (PLUS (WINS L M)
(WINS M L))
(TIMES (LENGTH L)
(LENGTH M))))
((USE (WIN-SOME-LOSE-SOME-2))
(DISABLE WIN-SOME-LOSE-SOME-2))))
(PUTPROPS LENGTH-MULTS PROVE-LEMMA ((REWRITE)
(EQUAL (LENGTH (MULTS N P))
(FIX N))))
(PUTPROPS LEQ-N-WINS1 PROVE-LEMMA (NIL (IMPLIES (LESSP (TIMES N P)
A)
(LEQ N (WINS1 A (MULTS N P))))
((INDUCT (MULTS N P)))))
(PUTPROPS MONOTONE-WINS1 PROVE-LEMMA (NIL (IMPLIES (LEQ N M)
(LEQ (WINS1 A (MULTS N P))
(WINS1 A (MULTS M P))))
((INDUCT (MULTS M P)))))
(PUTPROPS LEQ-TIMES-QUOT PROVE-LEMMA (NIL (IMPLIES (AND (NOT (ZEROP B))
(LEQ (TIMES A B)
(TIMES C D)))
(LEQ (QUOTIENT A D)
(QUOTIENT C B)))
((INDUCT (QUOT-QUOT-INDUCTION A B C D)))))
(PUTPROPS LEQ-QUOT-TIMES PROVE-LEMMA (NIL (LEQ (QUOTIENT (TIMES (QUOTIENT P 2)
Q)
P)
(QUOTIENT Q 2))
((USE (LEQ-TIMES-QUOT (A (TIMES (QUOTIENT P 2)
Q))
(D P)
(C Q)
(B 2))))))
(PUTPROPS MONOTONE-QUOT PROVE-LEMMA (NIL (IMPLIES (LEQ J I)
(LEQ (QUOTIENT J P)
(QUOTIENT I P)))
((INDUCT (MONOTONE-QUOT-INDUCTION I J P)))))
(PUTPROPS LEQ-QUOT-TIMES-2 PROVE-LEMMA (NIL (IMPLIES (LEQ J (QUOTIENT P 2))
(LEQ (QUOTIENT (TIMES J Q)
P)
(QUOTIENT Q 2)))
((USE (LEQ-QUOT-TIMES)
(MONOTONE-QUOT (J (TIMES J Q))
(I (TIMES (QUOTIENT P 2)
Q)))
(LESSP-TIMES-CANCELLATION (X J)
(Y (QUOTIENT P 2))
(Z Q)))
(DISABLE LESSP-TIMES-CANCELLATION))))
(PUTPROPS LEQ-QUOT-WINS1-1 PROVE-LEMMA (NIL (IMPLIES (NOT (DIVIDES P X))
(LESSP (TIMES (QUOTIENT X P)
P)
X))))
(PUTPROPS LEQ-QUOT-WINS1-2 PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(NOT (DIVIDES P Q))
(NOT (ZEROP Q))
(NOT (ZEROP J))
(LESSP J P))
(LESSP (TIMES (QUOTIENT (TIMES J Q)
P)
P)
(TIMES J Q)))
((USE (LEQ-QUOT-WINS1-1 (X (TIMES J Q))))
(DISABLE PRIME QUOTIENT TIMES))))
(PUTPROPS LEQ-QUOT-WINS1 PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(NOT (DIVIDES P Q))
(LEQ J (QUOTIENT P 2))
(NOT (ZEROP J))
(NOT (ZEROP Q)))
(LEQ (QUOTIENT (TIMES J Q)
P)
(WINS1 (TIMES J Q)
(MULTS (QUOTIENT Q 2)
P))))
((USE (LEQ-QUOT-TIMES-2)
(MONOTONE-WINS1 (A (TIMES J Q))
(N (QUOTIENT (TIMES J Q)
P))
(M (QUOTIENT Q 2)))
(LEQ-N-WINS1 (A (TIMES J Q))
(N (QUOTIENT (TIMES J Q)
P)))
(LEQ-QUOT-WINS1-2))
(DISABLE PRIME))))
(PUTPROPS LEQ-WINS2 PROVE-LEMMA (NIL (LEQ (TIMES (WINS2 A N P)
P)
A)))
(PUTPROPS LEQ-WINS1-N PROVE-LEMMA (NIL (LEQ (WINS1 A (MULTS N P))
N)))
(PUTPROPS LEQ-WINS1-WINS2 PROVE-LEMMA (NIL (LEQ (WINS1 A (MULTS N P))
(WINS2 A N P))
((USE (LEQ-WINS1-N))
(INDUCT (WINS2 A N P)))))
(PUTPROPS LEQ-WINS1 PROVE-LEMMA (NIL (LEQ (TIMES (WINS1 A (MULTS N P))
P)
A)
((USE (LEQ-WINS2)
(LEQ-WINS1-WINS2)
(LESSP-TIMES-CANCELLATION (X (WINS1 A (MULTS N P)))
(Y (WINS2 A N P))
(Z P)))
(DISABLE LESSP-TIMES-CANCELLATION))))
(PUTPROPS LEQ-WINS1-QUOT PROVE-LEMMA (NIL (IMPLIES (NOT (ZEROP P))
(LEQ (WINS1 A (MULTS N P))
(QUOTIENT A P)))
((USE (MONOTONE-QUOT (I A)
(J (TIMES (WINS1 A (MULTS N P))
P)))
(LEQ-WINS1)))))
(PUTPROPS EQUAL-QUOT-WINS1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P Q))
(LEQ J (QUOTIENT P 2))
(NOT (ZEROP J))
(NOT (ZEROP Q)))
(EQUAL (WINS1 (TIMES J Q)
(MULTS (QUOTIENT Q 2)
P))
(QUOTIENT (TIMES J Q)
P)))
((USE (LEQ-QUOT-WINS1)
(LEQ-WINS1-QUOT (A (TIMES J Q))
(N (QUOTIENT Q 2)))))))
(PUTPROPS EQUAL-WINS-PLUS-QUOT-LIST PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P Q))
(NOT (ZEROP Q))
(NOT (ZEROP J))
(LEQ J (QUOTIENT P 2)))
(EQUAL (WINS (MULTS J Q)
(MULTS (QUOTIENT Q 2)
P))
(PLUS-LIST (QUOT-LIST J Q P))))
((INDUCT (MULTS J Q)))))
(PUTPROPS GAUSS-COROLLARY PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P 2))
(NOT (EQUAL Q 2))
(NOT (EQUAL P Q)))
(EQUAL (RES1 (QUOTIENT P 2)
Q P)
(RESIDUE Q P)))
((USE (GAUSS-LEMMA (A Q)))
(DISABLE RES1 RESIDUE QUOTIENT PRIME1 REMAINDER))))
(PUTPROPS RESIDUE-QUOT-LIST PROVE-LEMMA (NIL
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(NOT (EQUAL P 2))
(NOT (EQUAL Q 2)))
(EQUAL (EQUAL (RESIDUE Q P)
(RESIDUE P Q))
(EVEN3 (PLUS (PLUS-LIST (QUOT-LIST (QUOTIENT P 2)
Q P))
(PLUS-LIST (QUOT-LIST (QUOTIENT Q 2)
P Q))))))
((USE (RES1-QUOT-LIST (A Q))
(RES1-QUOT-LIST (A P)
(P Q))
(EVEN3-EVEN)
(EVEN3-EVEN (P Q)))
(DISABLE RESIDUE RES1 QUOTIENT QUOT-LIST PLUS-LIST LESSP-REMAINDER-DIVISOR DIFFERENCE
LESSP))))
(PUTPROPS ALL-NON-ZEROP-MULTS PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZEROP P))
(ALL-NON-ZEROP (MULTS N P)))))
(PUTPROPS EMPTY-INTERSECT-MULTS-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(LESSP I Q)
(LESSP J P))
(NOT (MEMBER (TIMES I P)
(MULTS J Q))))
((INDUCT (MULTS J Q)))))
(PUTPROPS EMPTY-INTERSECT-MULTS PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(LESSP I Q))
(NOT (LISTP (INTERSECT (MULTS I P)
(MULTS (QUOTIENT
P 2)
Q)))))
((USE (EMPTY-INTERSECT-MULTS-1 (J (QUOTIENT P 2))))
(INDUCT (MULTS I P))
(DISABLE PRIME1 QUOTIENT EMPTY-INTERSECT-MULTS-1
LESSP-REMAINDER-DIVISOR))))
(PUTPROPS EQUAL-PLUS-QUOT-LIST-WINS PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q)))
(EQUAL (PLUS-LIST (QUOT-LIST
(QUOTIENT P 2)
Q P))
(WINS (MULTS (QUOTIENT P 2)
Q)
(MULTS (QUOTIENT Q 2)
P))))
((USE (EQUAL-WINS-PLUS-QUOT-LIST
(J (QUOTIENT P 2))))
(DISABLE EQUAL-WINS-PLUS-QUOT-LIST MULTS
QUOT-LIST WINS PLUS-LIST PRIME1))))
(PUTPROPS LAW-OF-QUADRATIC-RECIPROCITY PROVE-LEMMA (NIL (IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(NOT (EQUAL P 2))
(NOT (EQUAL Q 2)))
(EQUAL (EQUAL (RESIDUE Q P)
(RESIDUE P Q))
(EVEN (TIMES (QUOTIENT
P 2)
(QUOTIENT
Q 2)))))
((USE (RESIDUE-QUOT-LIST)
(EVEN3-EVEN
(P (TIMES (QUOTIENT P 2)
(QUOTIENT Q 2)))))
(HANDS-OFF QUOTIENT QUOT-LIST EVEN3
RESIDUE TIMES)
(DISABLE RESIDUE PRIME1 QUOT-LIST
PLUS-LIST EVEN3-PLUS
LESSP-REMAINDER-DIVISOR))))
(DEFINEQ
(PROVEALL6
(LAMBDA NIL (* kbr: "19-Oct-85 16:31")
(PROVEALL (QUOTE ((NOTE-LIB BOOTSTRAP)
(DEFN& LOGICALP)
(DEFN& EXPT)
(DEFN& ZNUMBERP)
(DEFN& ZZERO)
(DEFN& ZPLUS)
(DEFN& ZDIFFERENCE)
(DEFN& ZTIMES)
(DEFN& ZQUOTIENT)
(DEFN& ZEXPTZ)
(DEFN& ZNORMALIZE)
(DEFN& ZEQP)
(DEFN& ZNEQP)
(DEFN& ZLESSP)
(DEFN& ZLESSEQP)
(DEFN& ZGREATERP)
(DEFN& ZGREATEREQP)
(DCL GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER NIL)
(DCL LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
(DEFN& EXPRESSIBLE-ZNUMBERP)
(DEFN& IABS)
(DEFN& MOD)
(DEFN& MAX0)
(DEFN& MIN0)
(DEFN& ISIGN)
(DEFN& IDIM)
(ADD-SHELL UNDEF NIL UNDEFINED ((UNDEF-GUTS (NONE-OF)
ZERO)))
(DEFN& DEFINEDP)
(DCL ELT1 (A I))
(DCL ELT2 (A I J))
(DCL ELT3 (A I J K))
(DEFN& LEX)
(DCL RNUMBERP (X))
(DCL DNUMBERP (X))
(DCL CNUMBERP (X))
(DCL RZERO NIL)
(DCL DZERO NIL)
(DCL CZERO NIL)
(DCL EXPRESSIBLE-RNUMBERP (X))
(DCL EXPRESSIBLE-DNUMBERP (X))
(DCL EXPRESSIBLE-CNUMBERP (X))
(DCL RPLUS (X Y))
(DCL RTIMES (X Y))
(DCL RDIFFERENCE (X Y))
(DCL RQUOTIENT (X Y))
(DCL RLESSP (X Y))
(DCL RLESSEQP (X Y))
(DCL REQP (X Y))
(DCL RNEQP (X Y))
(DCL RGREATEREQP (X Y))
(DCL RGREATERP (X Y))
(DCL DPLUS (X Y))
(DCL DTIMES (X Y))
(DCL DDIFFERENCE (X Y))
(DCL DQUOTIENT (X Y))
(DCL DLESSP (X Y))
(DCL DLESSEQP (X Y))
(DCL DEQP (X Y))
(DCL DNEQP (X Y))
(DCL DGREATEREQP (X Y))
(DCL DGREATERP (X Y))
(DCL CPLUS (X Y))
(DCL CTIMES (X Y))
(DCL CDIFFERENCE (X Y))
(DCL CQUOTIENT (X Y))
(DCL CEQP (X Y))
(DCL CNEQP (X Y))
(DCL REXPTZ (X Y))
(DCL DEXPTZ (X Y))
(DCL CEXPTZ (X Y))
(DCL REXPTR (X Y))
(DCL REXPTD (X Y))
(DCL DEXPTR (X Y))
(DCL DEXPTD (X Y))
(DCL ABS (I))
(DCL DABS (I))
(DCL AINT (I))
(DCL INT (I))
(DCL IDINT (I))
(DCL AMOD (I J))
(DCL AMAX0 (I J))
(DCL AMAX1 (I J))
(DCL MAX1 (I J))
(DCL DMAX1 (I J))
(DCL AMIN0 (I J))
(DCL AMIN1 (I J))
(DCL MIN1 (I J))
(DCL DMIN1 (I J))
(DCL FLOAT (I))
(DCL IFIX (I))
(DCL SIGN (I J))
(DCL DSIGN (I J))
(DCL DIM (I J))
(DCL SNGL (I))
(DCL REAL (I))
(DCL AIMAG (I))
(DCL DBLE (I))
(DCL CMPLX (I J))
(DCL CONJG (I))
(DCL EXP (I))
(DCL DEXP (I))
(DCL CEXP (I))
(DCL ALOG (I))
(DCL DLOG (I))
(DCL CLOG (I))
(DCL ALOG10 (I))
(DCL DLOG10 (I))
(DCL SIN (I))
(DCL DSIN (I))
(DCL CSIN (I))
(DCL COS (I))
(DCL DCOS (I))
(DCL CCOS (I))
(DCL TANH (I))
(DCL SQRT (I))
(DCL DSQRT (I))
(DCL CSQRT (I))
(DCL CL:ATAN (I))
(DCL DATAN (I))
(DCL ATAN2 (I J))
(DCL DATAN2 (I J))
(DCL DMOD (I J))
(DCL CABS (I))
(ADD-AXIOM INTEGER-SIZE (REWRITE)
(AND (NUMBERP (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NEGATIVEP (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
(LESSP 200 (NEGATIVE-GUTS (
GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER)))
(LESSP 200 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))))
(DEFN& ALMOST-EQUAL1)
(PROVE-LEMMA& PLUS-0)
(PROVE-LEMMA& PLUS-NON-NUMBERP)
(PROVE-LEMMA& PLUS-ADD1)
(PROVE-LEMMA& COMMUTATIVITY2-OF-PLUS)
(PROVE-LEMMA& COMMUTATIVITY-OF-PLUS)
(PROVE-LEMMA& ASSOCIATIVITY-OF-PLUS)
(PROVE-LEMMA& TIMES-0)
(PROVE-LEMMA& TIMES-NON-NUMBERP)
(PROVE-LEMMA& DISTRIBUTIVITY-OF-TIMES-OVER-PLUS)
(PROVE-LEMMA& TIMES-ADD1)
(PROVE-LEMMA& COMMUTATIVITY2-OF-TIMES)
(PROVE-LEMMA& COMMUTATIVITY-OF-TIMES)
(PROVE-LEMMA& ASSOCIATIVITY-OF-TIMES)
(PROVE-LEMMA& EQUAL-TIMES-0)
(PROVE-LEMMA& EQUAL-LESSP)
(PROVE-LEMMA& ALMOST-EQUAL1-IN-RANGE)
(PROVE-LEMMA& ALMOST-EQUAL1-IN-RANGE-OPENED-UP)
(PROVE-LEMMA& ALMOST-EQUAL1-CONTRACTS)))
NIL FORTRAN)))
)
(PUTPROPS LOGICALP DEFN ((X)
(OR (EQUAL X (TRUE))
(EQUAL X (FALSE)))))
(PUTPROPS EXPT DEFN ((I J)
(IF (ZEROP J)
1
(TIMES I (EXPT I (SUB1 J))))))
(PUTPROPS ZNUMBERP DEFN ((X)
(OR (NEGATIVEP X)
(NUMBERP X))))
(PUTPROPS ZZERO DEFN (NIL (ZERO)))
(PUTPROPS ZPLUS DEFN ((X Y)
(IF (NEGATIVEP X)
(IF (NEGATIVEP Y)
(MINUS (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))
(IF (LESSP Y (NEGATIVE-GUTS X))
(MINUS (DIFFERENCE (NEGATIVE-GUTS X)
Y))
(DIFFERENCE Y (NEGATIVE-GUTS X))))
(IF (NEGATIVEP Y)
(IF (LESSP X (NEGATIVE-GUTS Y))
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y)
X))
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(PLUS X Y)))))
(PUTPROPS ZDIFFERENCE DEFN ((X Y)
(IF (NEGATIVEP X)
(IF (NEGATIVEP Y)
(IF (LESSP (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS X))
(MINUS (DIFFERENCE (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))
(DIFFERENCE (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS X)))
(MINUS (PLUS (NEGATIVE-GUTS X)
Y)))
(IF (NEGATIVEP Y)
(PLUS X (NEGATIVE-GUTS Y))
(IF (LESSP X Y)
(MINUS (DIFFERENCE Y X))
(DIFFERENCE X Y))))))
(PUTPROPS ZTIMES DEFN ((X Y)
(IF (NEGATIVEP X)
(IF (NEGATIVEP Y)
(TIMES (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
(MINUS (TIMES (NEGATIVE-GUTS X)
Y)))
(IF (NEGATIVEP Y)
(MINUS (TIMES X (NEGATIVE-GUTS Y)))
(TIMES X Y)))))
(PUTPROPS ZQUOTIENT DEFN ((X Y)
(IF (NEGATIVEP X)
(IF (NEGATIVEP Y)
(QUOTIENT (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
(MINUS (QUOTIENT (NEGATIVE-GUTS X)
Y)))
(IF (NEGATIVEP Y)
(MINUS (QUOTIENT X (NEGATIVE-GUTS Y)))
(QUOTIENT X Y)))))
(PUTPROPS ZEXPTZ DEFN ((I J)
(IF (ZEROP J)
1
(ZTIMES I (ZEXPTZ I (SUB1 J))))))
(PUTPROPS ZNORMALIZE DEFN ((X)
(IF (NEGATIVEP X)
(IF (EQUAL (NEGATIVE-GUTS X)
0)
0 X)
(FIX X))))
(PUTPROPS ZEQP DEFN ((X Y)
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE Y))))
(PUTPROPS ZNEQP DEFN ((X Y)
(NOT (ZEQP X Y))))
(PUTPROPS ZLESSP DEFN ((X Y)
(LESSP (PLUS (POS X)
(NEG Y))
(PLUS (NEG X)
(POS Y)))))
(PUTPROPS ZLESSEQP DEFN ((X Y)
(NOT (ZLESSP Y X))))
(PUTPROPS ZGREATERP DEFN ((X Y)
(ZLESSP Y X)))
(PUTPROPS ZGREATEREQP DEFN ((X Y)
(NOT (ZLESSP X Y))))
(PUTPROPS EXPRESSIBLE-ZNUMBERP DEFN ((X)
(AND (ZLESSP (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER)
X)
(ZLESSP X (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))))
(PUTPROPS IABS DEFN ((I)
(IF (NEGATIVEP I)
(NEGATIVE-GUTS I)
(FIX I))))
(PUTPROPS MOD DEFN ((X Y)
(ZDIFFERENCE X (ZTIMES Y (ZQUOTIENT X Y)))))
(PUTPROPS MAX0 DEFN ((I J)
(IF (ZLESSP I J)
J I)))
(PUTPROPS MIN0 DEFN ((I J)
(IF (ZLESSP I J)
I J)))
(PUTPROPS ISIGN DEFN ((I J)
(IF (NEGATIVEP J)
(ZTIMES -1 (IABS I))
(IABS I))))
(PUTPROPS IDIM DEFN ((I J)
(ZDIFFERENCE I (MIN0 I J))))
(PUTPROPS DEFINEDP DEFN ((X)
(NOT (UNDEFINED X))))
(PUTPROPS LEX DEFN ((L1 L2)
(IF (OR (NLISTP L1)
(NLISTP L2))
F
(OR (LESSP (CAR L1)
(CAR L2))
(AND (EQUAL (CAR L1)
(CAR L2))
(LEX (CDR L1)
(CDR L2)))))))
(PUTPROPS ALMOST-EQUAL1 DEFN ((A1 A2 U V I E)
(IF (OR (ZEROP V)
(LESSP V U))
T
(AND (IF (EQUAL V I)
(EQUAL (ELT1 A2 V)
E)
(EQUAL (ELT1 A2 V)
(ELT1 A1 V)))
(ALMOST-EQUAL1 A1 A2 U (SUB1 V)
I E)))))
(PUTPROPS PLUS-0 PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS X 0)
(FIX X))))
(PUTPROPS PLUS-NON-NUMBERP PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (NUMBERP Y))
(EQUAL (PLUS X Y)
(FIX X)))))
(PUTPROPS PLUS-ADD1 PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))))
(PUTPROPS COMMUTATIVITY2-OF-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS X (PLUS Y Z))
(PLUS Y (PLUS X Z)))))
(PUTPROPS COMMUTATIVITY-OF-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS X Y)
(PLUS Y X))))
(PUTPROPS ASSOCIATIVITY-OF-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))))
(PUTPROPS TIMES-0 PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X 0)
0)))
(PUTPROPS TIMES-NON-NUMBERP PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (NUMBERP Y))
(EQUAL (TIMES X Y)
0))))
(PUTPROPS DISTRIBUTIVITY-OF-TIMES-OVER-PLUS PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))))
(PUTPROPS TIMES-ADD1 PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))))
(PUTPROPS COMMUTATIVITY2-OF-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X (TIMES Y Z))
(TIMES Y (TIMES X Z)))))
(PUTPROPS COMMUTATIVITY-OF-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X Y)
(TIMES Y X))))
(PUTPROPS ASSOCIATIVITY-OF-TIMES PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))))
(PUTPROPS EQUAL-TIMES-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (TIMES X Y)
0)
(OR (ZEROP X)
(ZEROP Y)))))
(PUTPROPS EQUAL-LESSP PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))))
(PUTPROPS ALMOST-EQUAL1-IN-RANGE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (EQUAL (ELT1 A2 J)
W))
(EQUAL W (IF (EQUAL J I)
E
(ELT1 A1 J)))
(NOT (ZEROP U))
(NOT (LESSP J U))
(NOT (LESSP V J)))
(NOT (ALMOST-EQUAL1 A1 A2 U V I E)))))
(PUTPROPS ALMOST-EQUAL1-IN-RANGE-OPENED-UP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (EQUAL (ELT1 A2 J)
W))
(EQUAL W (IF (EQUAL J I)
E
(ELT1 A1 J)))
(NOT (ZEROP U))
(LEQ U J)
(LEQ J V)
(NOT (ZEROP V))
(NOT (LESSP V U))
(NOT (EQUAL V I))
(EQUAL (ELT1 A2 V)
(ELT1 A1 V)))
(NOT (ALMOST-EQUAL1 A1 A2 U (SUB1 V)
I E)))
((USE (ALMOST-EQUAL1-IN-RANGE))
(DISABLE ALMOST-EQUAL1-IN-RANGE))))
(PUTPROPS ALMOST-EQUAL1-CONTRACTS PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (ALMOST-EQUAL1 A1 A2 U V I E)
(NOT (ZEROP U))
(NOT (LESSP X U))
(NOT (LESSP V Y)))
(ALMOST-EQUAL1 A1 A2 X Y I E))
NIL))
(DEFINEQ
(PROVEALL7
(LAMBDA NIL (* kbr: "19-Oct-85 16:31")
(PROVEALL (QUOTE ((NOTE-LIB FORTRAN)
(PROVE-LEMMA& ZPLUS-COMM1)
(PROVE-LEMMA& ZPLUS-COMM2)
(PROVE-LEMMA& ZPLUS-ASSOC)
(DISABLE ZPLUS)
(ADD-SHELL VEHICLE-STATE NIL VEHICLE-STATEP ((W (NONE-OF)
ZERO)
(Y (NONE-OF)
ZERO)
(V (NONE-OF)
ZERO)))
(DEFN& HD)
(DEFN& TL)
(DEFN& EMPTY)
(PROVE-LEMMA& TL-REWRITE)
(DISABLE TL)
(PROVE-LEMMA& DOWN-ON-TL)
(DEFN& RANDOM-DELTA-WS)
(DEFN& CONTROLLER)
(DISABLE CONTROLLER)
(DEFN& SGN)
(DISABLE SGN)
(DEFN& NEXT-STATE)
(DEFN& FINAL-STATE-OF-VEHICLE)
(DEFN& GOOD-STATEP)
(PROVE-LEMMA& NEXT-GOOD-STATE)
(DEFN& ZERO-DELTA-WS)
(DEFN& APPEND)
(PROVE-LEMMA& LENGTH-0)
(PROVE-LEMMA& DECOMPOSE-LIST-OF-LENGTH-4)
(PROVE-LEMMA& DRIFT-TO-0-IN-4)
(PROVE-LEMMA& CANCEL-WIND-IN-4)
(PROVE-LEMMA& ONCE-0-ALWAYS-0)
(PROVE-LEMMA& FINAL-STATE-OF-VEHICLE-APPEND)
(PROVE-LEMMA& ZERO-DELTA-WS-APPEND)
(DISABLE APPEND)
(DISABLE NEXT-STATE)
(PROVE-LEMMA& GOOD-STATEP-BOUNDED-ABOVE)
(PROVE-LEMMA& GOOD-STATEP-BOUNDED-BELOW)
(DISABLE GOOD-STATEP)
(PROVE-LEMMA& ZLESSP-IS-LESSP)
(DISABLE ZLESSP)
(DEFN& FSV)
(PROVE-LEMMA& ALL-GOOD-STATES)
(PROVE-LEMMA& VEHICLE-STAYS-WITHIN-3-OF-COURSE)
(DISABLE FINAL-STATE-OF-VEHICLE)
(PROVE-LEMMA& ZERO-DELTA-WS-CDDDDR)
(PROVE-LEMMA& GOOD-STATES-FIND-AND-STAY-AT-0)
(PROVE-LEMMA& VEHICLE-GETS-ON-COURSE-IN-STEADY-WIND)))
NIL CONTROLLER)))
)
(PUTPROPS HD DEFN ((X)
(CAR X)))
(PUTPROPS TL DEFN ((X)
(CDR X)))
(PUTPROPS EMPTY DEFN ((X)
(NOT (LISTP X))))
(PUTPROPS RANDOM-DELTA-WS DEFN ((LST)
(IF (EMPTY LST)
T
(AND (OR (EQUAL (HD LST)
-1)
(EQUAL (HD LST)
0)
(EQUAL (HD LST)
1))
(RANDOM-DELTA-WS (TL LST))))))
(PUTPROPS CONTROLLER DEFN ((SGN-Y SGN-OLD-Y)
(ZPLUS (ZTIMES -3 SGN-Y)
(ZTIMES 2 SGN-OLD-Y))))
(PUTPROPS SGN DEFN ((X)
(IF (NEGATIVEP X)
(IF (EQUAL (NEGATIVE-GUTS X)
0)
0 -1)
(IF (ZEROP X)
0 1))))
(PUTPROPS NEXT-STATE DEFN ((DELTA-W STATE)
(VEHICLE-STATE (ZPLUS (W STATE)
DELTA-W)
(ZPLUS (Y STATE)
(ZPLUS (V STATE)
(ZPLUS (W STATE)
DELTA-W)))
(ZPLUS (V STATE)
(CONTROLLER
(SGN (ZPLUS (Y STATE)
(ZPLUS (V STATE)
(ZPLUS (W STATE)
DELTA-W))))
(SGN (Y STATE)))))))
(PUTPROPS FINAL-STATE-OF-VEHICLE DEFN ((DELTA-WS STATE)
(IF (EMPTY DELTA-WS)
STATE
(FINAL-STATE-OF-VEHICLE (TL DELTA-WS)
(NEXT-STATE (HD DELTA-WS)
STATE)))))
(PUTPROPS GOOD-STATEP DEFN ((STATE)
(IF (EQUAL (Y STATE)
0)
(OR (EQUAL (ZPLUS (V STATE)
(W STATE))
-1)
(EQUAL (ZPLUS (V STATE)
(W STATE))
0)
(EQUAL (ZPLUS (V STATE)
(W STATE))
1))
(IF (EQUAL (Y STATE)
1)
(OR (EQUAL (ZPLUS (V STATE)
(W STATE))
-2)
(EQUAL (ZPLUS (V STATE)
(W STATE))
-3))
(IF (EQUAL (Y STATE)
2)
(OR (EQUAL (ZPLUS (V STATE)
(W STATE))
-1)
(EQUAL (ZPLUS (V STATE)
(W STATE))
-2))
(IF (EQUAL (Y STATE)
3)
(EQUAL (ZPLUS (V STATE)
(W STATE))
-1)
(IF (EQUAL (Y STATE)
-3)
(EQUAL (ZPLUS (V STATE)
(W STATE))
1)
(IF (EQUAL (Y STATE)
-2)
(OR (EQUAL (ZPLUS (V STATE)
(W STATE))
1)
(EQUAL (ZPLUS (V STATE)
(W STATE))
2))
(IF (EQUAL (Y STATE)
-1)
(OR (EQUAL (ZPLUS (V STATE)
(W STATE))
2)
(EQUAL (ZPLUS (V STATE)
(W STATE))
3))
F)))))))))
(PUTPROPS ZERO-DELTA-WS DEFN ((LST)
(IF (EMPTY LST)
T
(AND (EQUAL (HD LST)
0)
(ZERO-DELTA-WS (TL LST))))))
(PUTPROPS APPEND DEFN ((X Y)
(IF (LISTP X)
(CONS (CAR X)
(APPEND (CDR X)
Y))
Y)))
(PUTPROPS FSV DEFN ((D S)
(IF (EMPTY D)
S
(FSV (TL D)
(NEXT-STATE (HD D)
S)))))
(PUTPROPS ZPLUS-COMM1 PROVE-LEMMA ((REWRITE)
(EQUAL (ZPLUS X Y)
(ZPLUS Y X))))
(PUTPROPS ZPLUS-COMM2 PROVE-LEMMA ((REWRITE)
(EQUAL (ZPLUS X (ZPLUS Y Z))
(ZPLUS Y (ZPLUS X Z)))))
(PUTPROPS ZPLUS-ASSOC PROVE-LEMMA ((REWRITE)
(EQUAL (ZPLUS (ZPLUS X Y)
Z)
(ZPLUS X (ZPLUS Y Z)))))
(PUTPROPS TL-REWRITE PROVE-LEMMA ((REWRITE)
(EQUAL (TL X)
(CDR X))))
(PUTPROPS DOWN-ON-TL PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (EMPTY X))
(LESSP (COUNT (TL X))
(COUNT X)))))
(PUTPROPS NEXT-GOOD-STATE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (GOOD-STATEP STATE)
(OR (EQUAL R -1)
(EQUAL R 0)
(EQUAL R 1)))
(GOOD-STATEP (NEXT-STATE R STATE)))))
(PUTPROPS LENGTH-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (LENGTH X)
0)
(NLISTP X))))
(PUTPROPS DECOMPOSE-LIST-OF-LENGTH-4 PROVE-LEMMA ((REWRITE)
(IMPLIES (ZERO-DELTA-WS LST)
(EQUAL (LESSP (LENGTH LST)
4)
(NOT (EQUAL LST (APPEND (QUOTE (0 0 0 0))
(CDDDDR LST))))))))
(PUTPROPS DRIFT-TO-0-IN-4 PROVE-LEMMA ((REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(EQUAL (Y (FINAL-STATE-OF-VEHICLE
(QUOTE (0 0 0 0))
STATE))
0))))
(PUTPROPS CANCEL-WIND-IN-4 PROVE-LEMMA ((REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE (QUOTE (0 0 0 0))
STATE))
(W (FINAL-STATE-OF-VEHICLE (QUOTE (0 0 0 0))
STATE)))
0))))
(PUTPROPS ONCE-0-ALWAYS-0 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (ZERO-DELTA-WS LST)
(EQUAL (Y STATE)
0)
(EQUAL (ZPLUS (W STATE)
(V STATE))
0))
(AND (EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE
LST STATE))
(W (FINAL-STATE-OF-VEHICLE
LST STATE)))
0)))))
(PUTPROPS FINAL-STATE-OF-VEHICLE-APPEND PROVE-LEMMA ((REWRITE)
(EQUAL (FINAL-STATE-OF-VEHICLE (APPEND A B)
STATE)
(FINAL-STATE-OF-VEHICLE B
(
FINAL-STATE-OF-VEHICLE A STATE)))))
(PUTPROPS ZERO-DELTA-WS-APPEND PROVE-LEMMA ((REWRITE)
(EQUAL (ZERO-DELTA-WS (APPEND (QUOTE (0 0 0 0))
V))
(ZERO-DELTA-WS V))))
(PUTPROPS GOOD-STATEP-BOUNDED-ABOVE PROVE-LEMMA ((REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(NOT (ZLESSP 3 (Y STATE))))))
(PUTPROPS GOOD-STATEP-BOUNDED-BELOW PROVE-LEMMA ((REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(NOT (ZLESSP (Y STATE)
-3)))))
(PUTPROPS ZLESSP-IS-LESSP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NUMBERP X)
(NUMBERP Y))
(EQUAL (ZLESSP X Y)
(LESSP X Y)))))
(PUTPROPS ALL-GOOD-STATES PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (RANDOM-DELTA-WS LST)
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE)))
((INDUCT (FSV LST STATE)))))
(PUTPROPS VEHICLE-STAYS-WITHIN-3-OF-COURSE PROVE-LEMMA (NIL
(IMPLIES (AND (RANDOM-DELTA-WS LST)
(EQUAL STATE (FINAL-STATE-OF-VEHICLE LST (VEHICLE-STATE 0 0 0))))
(AND (ZLESSEQP -3 (Y STATE))
(ZLESSEQP (Y STATE)
3)))))
(PUTPROPS ZERO-DELTA-WS-CDDDDR PROVE-LEMMA ((REWRITE)
(IMPLIES (ZERO-DELTA-WS X)
(ZERO-DELTA-WS (CDDDDR X)))))
(PUTPROPS GOOD-STATES-FIND-AND-STAY-AT-0 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (GOOD-STATEP STATE)
(ZERO-DELTA-WS LST2)
(NOT (LESSP (LENGTH LST2)
4)))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE
LST2 STATE))
0))))
(PUTPROPS VEHICLE-GETS-ON-COURSE-IN-STEADY-WIND PROVE-LEMMA (NIL
(IMPLIES (AND (RANDOM-DELTA-WS LST1)
(ZERO-DELTA-WS LST2)
(ZGREATEREQP (LENGTH LST2)
4)
(EQUAL STATE (FINAL-STATE-OF-VEHICLE (APPEND LST1 LST2)
(VEHICLE-STATE 0 0 0))))
(EQUAL (Y STATE)
0))
NIL))
(DEFINEQ
(PROVEALL8
(LAMBDA NIL (* kbr: "19-Oct-85 16:31")
(PROVEALL (QUOTE ((NOTE-LIB BOOTSTRAP) (* The floor of the square root.
This definition is taken from Goodstein.
*)
(DEFN& RT)
(PROVE-LEMMA& TIMES-ADD1)
(PROVE-LEMMA& PLUS-ADD1)
(PROVE-LEMMA& SQUARE-0)
(PROVE-LEMMA& SQUARE-MONOTONIC)
(PROVE-LEMMA& SPEC-FOR-RT)
(PROVE-LEMMA& RT-IS-UNIQUE)
(PROVE-LEMMA& NCONS-LEMMA)
(DEFN& NCAR)
(DEFN& NCDR)
(DEFN& NCONS)
(PROVE-LEMMA& NCAR-NCONS)
(PROVE-LEMMA& NCDR-NCONS)
(DEFN& NCADR)
(DEFN& NCADDR)
(PROVE-LEMMA& RT-LESSP)
(* I'm sure the system could prove this without the hint, but it would use induction and this is the obvious way to
do it. *)
(PROVE-LEMMA& RT-LESSEQP)
(PROVE-LEMMA& DIFFERENCE-0)
(PROVE-LEMMA& LESSP-DIFFERENCE-1)
(PROVE-LEMMA& NCAR-LESSEQP)
(PROVE-LEMMA& CROCK)
(PROVE-LEMMA& NCDR-LESSEQP)
(PROVE-LEMMA& NCDR-LESSP)
(DISABLE NCAR)
(DISABLE NCDR)
(DEFN& PR-APPLY)
(DEFN& NON-PR-FN)
(DEFN& COUNTER-EXAMPLE-FOR)
(PROVE-LEMMA& NON-PR-FUNCTIONS-EXIST)
(PROVE-LEMMA& COUNTER-EXAMPLE-FOR-NUMERIC)
(DISABLE PR-APPLY (* Not known to be necessary.
*))
(DEFN& MAX)
(DEFN& MAX2)
(DEFN& MAX1)
(PROVE-LEMMA& MAX2-GTE)
(DEFN& EXCEED)
(DEFN& EXCEED-AT)
(PROVE-LEMMA& MAX1-GTE1)
(PROVE-LEMMA& MAX1-GTE2)
(PROVE-LEMMA& EXCEED-IS-BIGGER)))
NIL PR)))
)
(PUTPROPS RT DEFN ((X)
(IF (ZEROP X)
0
(IF (EQUAL (TIMES (ADD1 (RT (SUB1 X)))
(ADD1 (RT (SUB1 X))))
X)
(ADD1 (RT (SUB1 X)))
(RT (SUB1 X))))))
(PUTPROPS NCAR DEFN ((X)
(DIFFERENCE X (TIMES (RT X)
(RT X)))))
(PUTPROPS NCDR DEFN ((X)
(DIFFERENCE (RT X)
(NCAR X))))
(PUTPROPS NCONS DEFN ((I J)
(PLUS I (TIMES (PLUS I J)
(PLUS I J)))))
(PUTPROPS NCADR DEFN ((X)
(NCAR (NCDR X))))
(PUTPROPS NCADDR DEFN ((X)
(NCAR (NCDR (NCDR X)))))
(PUTPROPS PR-APPLY DEFN ((FN ARG)
(IF
(NOT (NUMBERP FN))
0
(IF (EQUAL (NCAR FN)
0)
0
(IF (EQUAL (NCAR FN)
1)
ARG
(IF (EQUAL (NCAR FN)
2)
(ADD1 ARG)
(IF (EQUAL (NCAR FN)
3)
(RT ARG)
(IF (EQUAL (NCAR FN)
4)
(IF (ZEROP ARG)
0
(PR-APPLY (NCDR FN)
(PR-APPLY FN (SUB1 ARG))))
(IF (EQUAL (NCAR FN)
5)
(PLUS (PR-APPLY (NCADR FN)
ARG)
(PR-APPLY (NCADDR FN)
ARG))
(IF (EQUAL (NCAR FN)
6)
(DIFFERENCE (PR-APPLY (NCADR FN)
ARG)
(PR-APPLY (NCADDR FN)
ARG))
(IF (EQUAL (NCAR FN)
7)
(TIMES (PR-APPLY (NCADR FN)
ARG)
(PR-APPLY (NCADDR FN)
ARG))
(IF (EQUAL (NCAR FN)
8)
(PR-APPLY (NCADR FN)
(PR-APPLY (NCADDR FN)
ARG))
0))))))))))
((LEX2 (LIST (COUNT FN)
(COUNT ARG))))))
(PUTPROPS NON-PR-FN DEFN ((X)
(ADD1 (PR-APPLY X X))))
(PUTPROPS COUNTER-EXAMPLE-FOR DEFN ((X)
(FIX X)))
(PUTPROPS MAX DEFN ((I J)
(IF (LESSP I J)
J I)))
(PUTPROPS MAX2 DEFN ((FN I)
(IF (ZEROP I)
(PR-APPLY FN I)
(MAX (PR-APPLY FN I)
(MAX2 FN (SUB1 I))))))
(PUTPROPS MAX1 DEFN ((FN I)
(IF (ZEROP FN)
(MAX2 FN I)
(MAX (MAX2 FN I)
(MAX1 (SUB1 FN)
I)))))
(PUTPROPS EXCEED DEFN ((J)
(ADD1 (MAX1 J J))))
(PUTPROPS EXCEED-AT DEFN ((I)
I))
(PUTPROPS TIMES-ADD1 PROVE-LEMMA ((REWRITE)
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))))
(PUTPROPS PLUS-ADD1 PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))))
(PUTPROPS SQUARE-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (TIMES X X)
0)
(ZEROP X))))
(PUTPROPS SQUARE-MONOTONIC PROVE-LEMMA (NIL (IMPLIES (NOT (LESSP B A))
(NOT (LESSP (TIMES B B)
(TIMES A A))))))
(PUTPROPS SPEC-FOR-RT PROVE-LEMMA (NIL (AND (NOT (LESSP Y (TIMES (RT Y)
(RT Y))))
(LESSP Y (ADD1 (PLUS (RT Y)
(PLUS (RT Y)
(TIMES (RT Y)
(RT Y)))))))))
(PUTPROPS RT-IS-UNIQUE PROVE-LEMMA (NIL (IMPLIES (AND (NUMBERP A)
(LEQ (TIMES A A)
Y)
(LESSP Y (TIMES (ADD1 A)
(ADD1 A))))
(EQUAL A (RT Y)))
((USE (SPEC-FOR-RT)
(SQUARE-MONOTONIC (A (ADD1 A))
(B (RT Y)))
(SQUARE-MONOTONIC (A (ADD1 (RT Y)))
(B A))))))
(PUTPROPS NCONS-LEMMA PROVE-LEMMA ((REWRITE)
(EQUAL (RT (PLUS U (TIMES (PLUS U V)
(PLUS U V))))
(PLUS U V))
((USE (RT-IS-UNIQUE (Y (PLUS U (TIMES (PLUS U V)
(PLUS U V))))
(A (PLUS U V)))))))
(PUTPROPS NCAR-NCONS PROVE-LEMMA (NIL (IMPLIES (NUMBERP I)
(EQUAL (NCAR (NCONS I J))
I))))
(PUTPROPS NCDR-NCONS PROVE-LEMMA (NIL (IMPLIES (NUMBERP J)
(EQUAL (NCDR (NCONS I J))
J))))
(PUTPROPS RT-LESSP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP X))
(NOT (EQUAL X 1)))
(LESSP (RT X)
X))))
(PUTPROPS RT-LESSEQP PROVE-LEMMA ((REWRITE)
(NOT (LESSP X (RT X)))
((USE (RT-LESSP)))))
(PUTPROPS DIFFERENCE-0 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (LESSP Y X))
(EQUAL (DIFFERENCE X Y)
0))))
(PUTPROPS LESSP-DIFFERENCE-1 PROVE-LEMMA ((REWRITE)
(EQUAL (LESSP (DIFFERENCE A B)
C)
(IF (LESSP A B)
(LESSP 0 C)
(LESSP A (PLUS B C))))))
(PUTPROPS NCAR-LESSEQP PROVE-LEMMA ((REWRITE)
(NOT (LESSP X (NCAR X)))))
(PUTPROPS CROCK PROVE-LEMMA ((REWRITE)
(EQUAL (LESSP X (DIFFERENCE (RT X)
D))
F)
NIL
(*
" This disgusting fact is needed because linear seems to have trouble with"
*)
(*
" nests of DIFFERENCEs. Try disabling this and proving NCDR-LESSEQP below and"
*)
(*
" observe that when D is a DIFFERENCE expression we don't prove it."
*)))
(PUTPROPS NCDR-LESSEQP PROVE-LEMMA ((REWRITE)
(NOT (LESSP X (NCDR X)))))
(PUTPROPS NCDR-LESSP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NUMBERP FN)
(NOT (EQUAL (NCAR FN)
0))
(NOT (EQUAL (NCAR FN)
1)))
(LESSP (NCDR FN)
FN))))
(PUTPROPS NON-PR-FUNCTIONS-EXIST PROVE-LEMMA (NIL (NOT (EQUAL (NON-PR-FN (COUNTER-EXAMPLE-FOR
FN))
(PR-APPLY FN (COUNTER-EXAMPLE-FOR
FN))))))
(PUTPROPS COUNTER-EXAMPLE-FOR-NUMERIC PROVE-LEMMA ((REWRITE)
(NUMBERP (COUNTER-EXAMPLE-FOR X))))
(PUTPROPS MAX2-GTE PROVE-LEMMA ((REWRITE)
(NOT (LESSP (MAX2 I J)
(PR-APPLY I J)))))
(PUTPROPS MAX1-GTE1 PROVE-LEMMA ((REWRITE)
(IMPLIES (NUMBERP FN)
(NOT (LESSP (MAX1 (PLUS J FN)
I)
(PR-APPLY FN I))))))
(PUTPROPS MAX1-GTE2 PROVE-LEMMA ((REWRITE)
(IMPLIES (NUMBERP FN)
(NOT (LESSP (MAX1 (PLUS J FN)
(PLUS J FN))
(PR-APPLY FN (PLUS J FN)))))))
(PUTPROPS EXCEED-IS-BIGGER PROVE-LEMMA (NIL (IMPLIES (NUMBERP FN)
(LESSP (PR-APPLY FN (PLUS J (EXCEED-AT FN)))
(EXCEED (PLUS J (EXCEED-AT FN)))))))
(DEFINEQ
(PROVEALL9
(LAMBDA NIL (* kbr: "19-Oct-85 16:31")
(PROVEALL (QUOTE ((NOTE-LIB BOOTSTRAP)
(ADD-SHELL BTM NIL BTMP)
(DEFN& GET)
(DEFN& PAIRLIST)
(DEFN& SUBRP)
(DEFN& APPLY-SUBR)
(DEFN& EV)
(DEFN& EVAL)
(DEFN& EVLIST)
(* We now define the functions x, va, fa, and k. To do so we first define SUBLIS, which applies a substitution to
an s-expression. Then we use the names CIRC and LOOP in the definitions of x and fa and use SUBLIS to
" replace those names with " new " names. It is not important whether we have" defined this notion of
substitution correctly, since all that is required is that we exhibit some x, va, fa, and k with the desired
properties. *)
(DEFN& APPEND)
(DEFN& ASSOC)
(DEFN& SUBLIS)
(DEFN& X)
(DEFN& FA)
(DEFN& VA)
(DEFN& K)
(* " We wish to prove that having " new " program names in the function
" environment does not effect the computation of the body of HALTS. To state
" this we must first define formally what we mean by " new ". Then we will" prove the general result we need and
then we will instantiate it for the " particular " new " program names we choose." *)
(DEFN& OCCUR)
(DEFN& OCCUR-IN-DEFNS)
(PROVE-LEMMA& OCCUR-OCCUR-IN-DEFNS)
(PROVE-LEMMA& LEMMA1)
(PROVE-LEMMA& COUNT-OCCUR)
(PROVE-LEMMA& COUNT-GET)
(PROVE-LEMMA& COUNT-OCCUR-IN-DEFNS)
(PROVE-LEMMA& COROLLARY1)
(DISABLE LEMMA1 (* We now turn off the key lemma and just rely on the
result just proved. *)
(* Failure to turn off the key lemma causes the system
to spend hundred of *)
(* thousands of conses investigating OCCURrences and
comparing COUNTs on *)
(* almost every EVAL expression involved in the proof.
*)
)
(PROVE-LEMMA& LEMMA2)
(PROVE-LEMMA& COROLLARY2)
(PROVE-LEMMA& LEMMA3)
(PROVE-LEMMA& EXPAND-CIRC)
(PROVE-LEMMA& UNSOLVABILITY-OF-THE-HALTING-PROBLEM)))
NIL UNSOLV)))
)
(PUTPROPS GET DEFN ((ADDR MEM)
(IF (ZEROP ADDR)
(CAR MEM)
(GET (SUB1 ADDR)
(CDR MEM)))))
(PUTPROPS PAIRLIST DEFN ((X Y)
(IF (NLISTP X)
NIL
(CONS (CONS (CAR X)
(CAR Y))
(PAIRLIST (CDR X)
(CDR Y))))))
(PUTPROPS SUBRP DEFN ((FN)
(MEMBER FN
(QUOTE (ZERO TRUE FALSE ADD1 SUB1 NUMBERP CONS CAR CDR LISTP PACK UNPACK LITATOM
EQUAL LIST)))))
(PUTPROPS APPLY-SUBR DEFN ((FN LST)
(IF
(EQUAL FN (QUOTE ZERO))
(ZERO)
(IF
(EQUAL FN (QUOTE TRUE))
(TRUE)
(IF
(EQUAL FN (QUOTE FALSE))
(FALSE)
(IF
(EQUAL FN (QUOTE ADD1))
(ADD1 (CAR LST))
(IF
(EQUAL FN (QUOTE SUB1))
(SUB1 (CAR LST))
(IF
(EQUAL FN (QUOTE NUMBERP))
(NUMBERP (CAR LST))
(IF
(EQUAL FN (QUOTE CONS))
(CONS (CAR LST)
(CADR LST))
(IF (EQUAL FN (QUOTE LIST))
LST
(IF (EQUAL FN (QUOTE CAR))
(CAR (CAR LST))
(IF (EQUAL FN (QUOTE CDR))
(CDR (CAR LST))
(IF (EQUAL FN (QUOTE LISTP))
(LISTP (CAR LST))
(IF (EQUAL FN (QUOTE PACK))
(PACK (CAR LST))
(IF (EQUAL FN (QUOTE UNPACK))
(UNPACK (CAR LST))
(IF (EQUAL FN (QUOTE LITATOM))
(LITATOM (CAR LST))
(IF (EQUAL FN (QUOTE EQUAL))
(EQUAL (CAR LST)
(CADR LST))
0)))))))))))))))))
(PUTPROPS EV DEFN ((FLG X VA FA N)
(IF
(EQUAL FLG (QUOTE AL))
(IF (NLISTP X)
(IF (NUMBERP X)
X
(IF (EQUAL X (QUOTE T))
T
(IF (EQUAL X (QUOTE F))
F
(IF (EQUAL X NIL)
NIL
(GET X VA)))))
(IF (EQUAL (CAR X)
(QUOTE QUOTE))
(CADR X)
(IF (EQUAL (CAR X)
(QUOTE IF))
(IF (BTMP (EV (QUOTE AL)
(CADR X)
VA FA N))
(BTM)
(IF (EV (QUOTE AL)
(CADR X)
VA FA N)
(EV (QUOTE AL)
(CADDR X)
VA FA N)
(EV (QUOTE AL)
(CADDDR X)
VA FA N)))
(IF (BTMP (EV (QUOTE LIST)
(CDR X)
VA FA N))
(BTM)
(IF (SUBRP (CAR X))
(APPLY-SUBR (CAR X)
(EV (QUOTE LIST)
(CDR X)
VA FA N))
(IF (BTMP (GET (CAR X)
FA))
(BTM)
(IF (ZEROP N)
(BTM)
(EV (QUOTE AL)
(CADR (GET (CAR X)
FA))
(PAIRLIST (CAR (GET (CAR X)
FA))
(EV (QUOTE LIST)
(CDR X)
VA FA N))
FA
(SUB1 N)))))))))
(IF (LISTP X)
(IF (BTMP (EV (QUOTE AL)
(CAR X)
VA FA N))
(BTM)
(IF (BTMP (EV (QUOTE LIST)
(CDR X)
VA FA N))
(BTM)
(CONS (EV (QUOTE AL)
(CAR X)
VA FA N)
(EV (QUOTE LIST)
(CDR X)
VA FA N))))
NIL))
((LEX2 (LIST N (COUNT X))))))
(PUTPROPS EVAL DEFN ((FORM ENVRN)
(IF (NUMBERP FORM)
FORM
(IF (LISTP (CDDR FORM))
(CALL (CAR FORM)
(EVAL (CADR FORM)
ENVRN)
(EVAL (CADDR FORM)
ENVRN))
(GETVALUE FORM ENVRN)))))
(PUTPROPS EVLIST DEFN ((X VA FA N)
(EV (QUOTE LIST)
X VA FA N)))
(PUTPROPS APPEND DEFN ((X Y)
(IF (LISTP X)
(CONS (CAR X)
(APPEND (CDR X)
Y))
Y)))
(PUTPROPS ASSOC DEFN ((X Y)
(IF (LISTP Y)
(IF (EQUAL X (CAAR Y))
(CAR Y)
(ASSOC X (CDR Y)))
NIL)))
(PUTPROPS SUBLIS DEFN ((ALIST X)
(IF (NLISTP X)
(IF (ASSOC X ALIST)
(CDR (ASSOC X ALIST))
X)
(CONS (SUBLIS ALIST (CAR X))
(SUBLIS ALIST (CDR X))))))
(PUTPROPS X DEFN ((FA)
(SUBLIS (LIST (CONS (QUOTE CIRC)
(CONS FA 0)))
(QUOTE (CIRC A)))))
(PUTPROPS FA DEFN ((FA)
(APPEND (SUBLIS (LIST (CONS (QUOTE CIRC)
(CONS FA 0))
(CONS (QUOTE LOOP)
(CONS FA 1)))
(QUOTE ((CIRC (A)
(IF (HALTS (QUOTE (CIRC A))
(LIST (CONS (QUOTE A)
A))
A)
(LOOP)
T))
(LOOP NIL (LOOP)))))
FA)))
(PUTPROPS VA DEFN ((FA)
(LIST (CONS (QUOTE A)
(FA FA)))))
(PUTPROPS K DEFN ((N)
(ADD1 N)))
(PUTPROPS OCCUR DEFN ((X Y)
(IF (EQUAL X Y)
T
(IF (LISTP Y)
(IF (OCCUR X (CAR Y))
T
(OCCUR X (CDR Y)))
F))))
(PUTPROPS OCCUR-IN-DEFNS DEFN ((X LST)
(IF (NLISTP LST)
F
(OR (OCCUR X (CADDR (CAR LST)))
(OCCUR-IN-DEFNS X (CDR LST))))
NIL
(*
" This function returns T or F according to whether X occurs in the body of"
*)
(*
" some defn in LST. At first we avoided using this function and just asked"
*)
(*
" instead whether X occurs in LST. However, when so put the following lemma"
*)
(* " is not valid." *)))
(PUTPROPS OCCUR-OCCUR-IN-DEFNS PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (OCCUR-IN-DEFNS FN FA))
(NOT (BTMP (GET X FA))))
(NOT (OCCUR FN (CADR (GET X FA)))))))
(PUTPROPS LEMMA1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (OCCUR FN X))
(NOT (OCCUR-IN-DEFNS FN FA)))
(EQUAL (EV FLG X VA (CONS (CONS FN DEF)
FA)
N)
(EV FLG X VA FA N)))
NIL
(*
" If a FN is not used in X or any defn in FA then it can be ignored."
*)))
(PUTPROPS COUNT-OCCUR PROVE-LEMMA ((REWRITE)
(IMPLIES (LESSP (COUNT Y)
(COUNT X))
(NOT (OCCUR X Y)))
NIL
(*
" This lemma will let us show that the name (CONS FA i) does not occur in FA."
*)))
(PUTPROPS COUNT-GET PROVE-LEMMA ((REWRITE)
(LESSP (COUNT (CADR (GET FN FA)))
(ADD1 (COUNT FA)))
NIL
(*
" This lemma will let us show that the name (CONS FA i) does not occur in any"
*)
(* " defn obtained from FA." *)))
(PUTPROPS COUNT-OCCUR-IN-DEFNS PROVE-LEMMA ((REWRITE)
(IMPLIES (LESSP (COUNT FA)
(COUNT X))
(NOT (OCCUR-IN-DEFNS X FA)))
NIL
(*
" This lemma lets us establish that (CONS FA i) doesn't occur in the defns of"
*)
(* " FA." *)))
(PUTPROPS COROLLARY1 PROVE-LEMMA ((REWRITE)
(EQUAL (EV (QUOTE AL)
(CADR (GET (QUOTE HALTS)
FA))
VA
(CONS (CONS (CONS FA 0)
DEF0)
(CONS (LIST (CONS FA 1)
NIL
(LIST (CONS FA 1)))
FA))
N)
(EV (QUOTE AL)
(CADR (GET (QUOTE HALTS)
FA))
VA FA N))
NIL
(*
" This is the result we needed: evaluating the body of HALTS in an"
*)
(*
" environment containing the two new programs CIRC and LOOP produces the same"
*)
(* " result as without those two programs.
" *)))
(PUTPROPS LEMMA2 PROVE-LEMMA (NIL (IMPLIES (AND (NOT (BTMP (EV FLG X VA FA N)))
(NOT (BTMP (EV FLG X VA FA K))))
(EQUAL (EV FLG X VA FA N)
(EV FLG X VA FA K)))
NIL
(*
" If EV at N and K are both not BTM then they are equal. We will need only"
*)
(*
" COROLLARY2 below, but we must prove the more general version by induction."
*)))
(PUTPROPS COROLLARY2 PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL (EV FLG X VA FA N)
T)
(EV FLG X VA FA K))
((USE (LEMMA2)))
(*
" If EV at N is T then EV at K is not F. We have to tell the system to use"
*)
(* " LEMMA2 to prove this." *)))
(PUTPROPS LEMMA3 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (LISTP X)
(LISTP (CAR X))
(NLISTP (CDR X))
(LISTP (GET (CAR X)
FA))
(EQUAL (CAR (GET (CAR X)
FA))
NIL)
(EQUAL (CADR (GET (CAR X)
FA))
X))
(BTMP (EV (QUOTE AL)
X VA FA N)))
(*
" If a program is defined so as to call itself immediately then it never"
*)
(* " terminates." *)))
(PUTPROPS EXPAND-CIRC PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (BTMP VAL))
(NOT (BTMP (GET (CONS FN 0)
FA))))
(EQUAL (EV (QUOTE AL)
(CONS (CONS FN 0)
(QUOTE (A)))
(LIST (CONS (QUOTE A)
VAL))
FA J)
(IF (ZEROP J)
(BTM)
(EV (QUOTE AL)
(CADR (GET (CONS FN 0)
FA))
(PAIRLIST (CAR (GET (CONS FN 0)
FA))
(EV (QUOTE LIST)
(QUOTE (A))
(LIST (CONS (QUOTE A)
VAL))
FA J))
FA
(SUB1 J)))))
NIL
(* " This lemma forces the system to expand any call of EVAL on CIRC. Were CIRC" *)
(* " defined recursively on the function alist this lemma would cause infinite" *)
(* " rewriting. Without this lemma the system does not expand the call of EVAL" *)
(* " on CIRC because it introduces " worse " calls of EVAL, namely on the args of" *)
(* " the call and body of CIRC. However, once it has stepped from the call of" *)
(* " CIRC to its body it then the calls." *)))
(PUTPROPS UNSOLVABILITY-OF-THE-HALTING-PROBLEM PROVE-LEMMA (NIL
(IMPLIES (EQUAL H (EVAL (LIST (QUOTE HALTS)
(LIST (QUOTE QUOTE)
(X FA))
(LIST (QUOTE QUOTE)
(VA FA))
(LIST (QUOTE QUOTE)
(FA FA)))
NIL FA N))
(AND (IMPLIES (EQUAL H F)
(NOT (BTMP (EVAL (X FA)
(VA FA)
(FA FA)
(K N)))))
(IMPLIES (EQUAL H T)
(BTMP (EVAL (X FA)
(VA FA)
(FA FA)
K)))))
NIL))
(DEFINEQ
(PROVEALL10
(LAMBDA NIL (* kbr: "19-Oct-85 16:31")
(PROVEALL (QUOTE ((NOTE-LIB UNSOLV)
(DEFN& SYMBOL)
(DEFN& HALF-TAPE)
(DEFN& TAPE)
(DEFN& OPERATION)
(DEFN& STATE)
(DEFN& TURING-4TUPLE)
(DEFN& TURING-MACHINE)
(DEFN& INSTR)
(DEFN& NEW-TAPE)
(DEFN& TMI)
(DEFN& INSTR-DEFN)
(DEFN& NEW-TAPE-DEFN)
(DEFN& TMI-DEFN)
(DEFN& KWOTE)
(DEFN& TMI-FA)
(DEFN& TMI-X)
(DEFN& TMI-K)
(DEFN& TMI-N)
(PROVE-LEMMA& LENGTH-0)
(PROVE-LEMMA& PLUS-EQUAL-0)
(PROVE-LEMMA& PLUS-DIFFERENCE)
(TOGGLE DIFFERENCE-OFF DIFFERENCE T)
(PROVE-LEMMA& EVAL-FN-0)
(PROVE-LEMMA& EVAL-FN-1)
(PROVE-LEMMA& EVAL-SUBRP)
(PROVE-LEMMA& EVAL-IF)
(PROVE-LEMMA& EVAL-QUOTE)
(PROVE-LEMMA& EVAL-NLISTP)
(PROVE-LEMMA& EVLIST-NIL)
(PROVE-LEMMA& EVLIST-CONS)
(TOGGLE SUBRP-OFF SUBRP T)
(TOGGLE EV-OFF EV T)
(DEFN& CNB)
(PROVE-LEMMA& CNB-NBTM)
(PROVE-LEMMA& CNB-CONS)
(PROVE-LEMMA& CNB-LITATOM)
(PROVE-LEMMA& CNB-NUMBERP)
(TOGGLE CNB-OFF CNB T)
(PROVE-LEMMA& GET-TMI-FA)
(TOGGLE TMI-FA-OFF TMI-FA T)
(DEFN& INSTRN)
(DEFN& EVAL-INSTR-INDUCTION-SCHEME)
(PROVE-LEMMA& EVAL-INSTR)
(PROVE-LEMMA& EVAL-NEW-TAPE)
(PROVE-LEMMA& CNB-INSTRN)
(PROVE-LEMMA& CNB-NEW-TAPE)
(TOGGLE NEW-TAPE-OFF NEW-TAPE T)
(DEFN& TMIN)
(DEFN& EVAL-TMI-INDUCTION-SCHEME)
(PROVE-LEMMA& EVAL-TMI)
(PROVE-LEMMA& EVAL-TMI-X)
(TOGGLE TMI-X-OFF TMI-X T)
(PROVE-LEMMA& INSTRN-INSTR)
(PROVE-LEMMA& NBTMP-INSTR)
(PROVE-LEMMA& INSTRN-NON-F)
(PROVE-LEMMA& TMIN-BTM)
(PROVE-LEMMA& TMIN-TMI)
(PROVE-LEMMA& SYMBOL-CNB)
(TOGGLE SYMBOL-OFF SYMBOL T)
(PROVE-LEMMA& HALF-TAPE-CNB)
(PROVE-LEMMA& TAPE-CNB)
(TOGGLE TAPE-OFF TAPE T)
(PROVE-LEMMA& OPERATION-CNB)
(TOGGLE OPERATION-OFF OPERATION T)
(PROVE-LEMMA& TURING-MACHINE-CNB)
(TOGGLE TURING-MACHINE-OFF TURING-MACHINE T)
(PROVE-LEMMA& TURING-COMPLETENESS-OF-LISP)))
NIL TMI)))
)
(PUTPROPS SYMBOL DEFN ((X)
(MEMBER X (QUOTE (0 1)))))
(PUTPROPS HALF-TAPE DEFN ((X)
(IF (NLISTP X)
(EQUAL X 0)
(AND (SYMBOL (CAR X))
(HALF-TAPE (CDR X))))))
(PUTPROPS TAPE DEFN ((X)
(AND (LISTP X)
(HALF-TAPE (CAR X))
(HALF-TAPE (CDR X)))))
(PUTPROPS OPERATION DEFN ((X)
(MEMBER X (QUOTE (L R 0 1)))))
(PUTPROPS STATE DEFN ((X)
(LITATOM X)))
(PUTPROPS TURING-4TUPLE DEFN ((X)
(AND (LISTP X)
(STATE (CAR X))
(SYMBOL (CADR X))
(OPERATION (CADDR X))
(STATE (CADDDR X))
(EQUAL (CDDDDR X)
NIL))))
(PUTPROPS TURING-MACHINE DEFN ((X)
(IF (NLISTP X)
(EQUAL X NIL)
(AND (TURING-4TUPLE (CAR X))
(TURING-MACHINE (CDR X))))))
(PUTPROPS INSTR DEFN ((ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F)))
(PUTPROPS NEW-TAPE DEFN ((OP TAPE)
(IF (EQUAL OP (QUOTE L))
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE))
(CDR TAPE)))
(IF (EQUAL OP (QUOTE R))
(CONS (CONS (CAR (CDR TAPE))
(CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP (CDR (CDR TAPE))))))))
(PUTPROPS TMI DEFN ((ST TAPE TM N)
(IF (ZEROP N)
(BTM)
(IF (INSTR ST (CAR (CDR TAPE))
TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE))
TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE))
TM))
TAPE)
TM
(SUB1 N))
TAPE))))
(PUTPROPS INSTR-DEFN DEFN (NIL (QUOTE ((ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F)))))
(PUTPROPS NEW-TAPE-DEFN DEFN (NIL (QUOTE ((OP TAPE)
(IF (EQUAL OP (QUOTE L))
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE))
(CDR TAPE)))
(IF (EQUAL OP (QUOTE R))
(CONS (CONS (CAR (CDR TAPE))
(CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP (CDR (CDR TAPE))))))))))
(PUTPROPS TMI-DEFN DEFN (NIL (QUOTE ((ST TAPE TM)
(IF (INSTR ST (CAR (CDR TAPE))
TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE))
TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE))
TM))
TAPE)
TM)
TAPE)))))
(PUTPROPS KWOTE DEFN ((X)
(LIST (QUOTE QUOTE)
X)))
(PUTPROPS TMI-FA DEFN ((TM)
(LIST (LIST (QUOTE TM)
NIL
(KWOTE TM))
(CONS (QUOTE INSTR)
(INSTR-DEFN))
(CONS (QUOTE NEW-TAPE)
(NEW-TAPE-DEFN))
(CONS (QUOTE TMI)
(TMI-DEFN)))))
(PUTPROPS TMI-X DEFN ((ST TAPE)
(LIST (QUOTE TMI)
(KWOTE ST)
(KWOTE TAPE)
(QUOTE (TM)))))
(PUTPROPS TMI-K DEFN ((ST TAPE TM N)
(DIFFERENCE N (ADD1 (LENGTH TM)))))
(PUTPROPS TMI-N DEFN ((ST TAPE TM K)
(PLUS K (ADD1 (LENGTH TM)))))
(PUTPROPS CNB DEFN ((X)
(IF (LISTP X)
(AND (CNB (CAR X))
(CNB (CDR X)))
(NOT (BTMP X)))))
(PUTPROPS INSTRN DEFN ((ST SYM TM N)
(IF (ZEROP N)
(BTM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTRN ST SYM (CDR TM)
(SUB1 N)))
(INSTRN ST SYM (CDR TM)
(SUB1 N)))
F))))
(PUTPROPS EVAL-INSTR-INDUCTION-SCHEME DEFN ((ST SYM TM-- VA TM N)
(IF (ZEROP N)
T
(EVAL-INSTR-INDUCTION-SCHEME
(QUOTE ST)
(QUOTE SYM)
(QUOTE (CDR TM))
(LIST (CONS (QUOTE ST)
(EVAL ST VA (TMI-FA TM)
N))
(CONS (QUOTE SYM)
(EVAL SYM VA (TMI-FA TM)
N))
(CONS (QUOTE TM)
(EVAL TM-- VA (TMI-FA TM)
N)))
TM
(SUB1 N)))))
(PUTPROPS TMIN DEFN ((ST TAPE TM N)
(IF (ZEROP N)
(BTM)
(IF (BTMP (INSTRN ST (CAR (CDR TAPE))
TM
(SUB1 N)))
(BTM)
(IF (INSTRN ST (CAR (CDR TAPE))
TM
(SUB1 N))
(TMIN (CAR (CDR (INSTRN ST (CAR (CDR TAPE))
TM
(SUB1 N))))
(NEW-TAPE (CAR (INSTRN ST (CAR (CDR TAPE))
TM
(SUB1 N)))
TAPE)
TM
(SUB1 N))
TAPE)))))
(PUTPROPS EVAL-TMI-INDUCTION-SCHEME DEFN ((ST TAPE TM-- VA TM N)
(IF (ZEROP N)
T
(EVAL-TMI-INDUCTION-SCHEME (QUOTE (CAR (CDR (INSTR ST (CAR (CDR TAPE))
TM))))
(QUOTE (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE))
TM))
TAPE))
(QUOTE TM)
(LIST (CONS (QUOTE ST)
(EV (QUOTE AL)
ST VA (TMI-FA TM)
N))
(CONS (QUOTE TAPE)
(EV (QUOTE AL)
TAPE VA (TMI-FA TM)
N))
(CONS (QUOTE TM)
(EV (QUOTE AL)
TM-- VA (TMI-FA TM)
N)))
TM
(SUB1 N)))))
(PUTPROPS LENGTH-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (LENGTH X)
0)
(NLISTP X))))
(PUTPROPS PLUS-EQUAL-0 PROVE-LEMMA ((REWRITE)
(EQUAL (EQUAL (PLUS A B)
0)
(AND (ZEROP A)
(ZEROP B)))))
(PUTPROPS PLUS-DIFFERENCE PROVE-LEMMA ((REWRITE)
(EQUAL (PLUS (DIFFERENCE I J)
J)
(IF (LEQ I J)
(FIX J)
I))))
(PUTPROPS EVAL-FN-0 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (ZEROP N)
(NOT (EQUAL FN (QUOTE QUOTE)))
(NOT (EQUAL FN (QUOTE IF)))
(NOT (SUBRP FN))
(EQUAL VARGS (EV (QUOTE LIST)
ARGS VA FA N)))
(EQUAL (EV (QUOTE AL)
(CONS FN ARGS)
VA FA N)
(BTM)))))
(PUTPROPS EVAL-FN-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL FN (QUOTE QUOTE)))
(NOT (EQUAL FN (QUOTE IF)))
(NOT (SUBRP FN))
(EQUAL VARGS (EV (QUOTE LIST)
ARGS VA FA N)))
(EQUAL (EV (QUOTE AL)
(CONS FN ARGS)
VA FA N)
(IF (BTMP VARGS)
(BTM)
(IF (BTMP (GET FN FA))
(BTM)
(EV (QUOTE AL)
(CADR (GET FN FA))
(PAIRLIST (CAR (GET FN FA))
VARGS)
FA
(SUB1 N))))))))
(PUTPROPS EVAL-SUBRP PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (SUBRP FN)
(EQUAL VARGS (EV (QUOTE LIST)
ARGS VA FA N)))
(EQUAL (EV (QUOTE AL)
(CONS FN ARGS)
VA FA N)
(IF (BTMP VARGS)
(BTM)
(APPLY-SUBR FN VARGS))))))
(PUTPROPS EVAL-IF PROVE-LEMMA ((REWRITE)
(IMPLIES (EQUAL VX1 (EV (QUOTE AL)
X1 VA FA N))
(EQUAL (EV (QUOTE AL)
(LIST (QUOTE IF)
X1 X2 X3)
VA FA N)
(IF (BTMP VX1)
(BTM)
(IF VX1 (EV (QUOTE AL)
X2 VA FA N)
(EV (QUOTE AL)
X3 VA FA N)))))))
(PUTPROPS EVAL-QUOTE PROVE-LEMMA ((REWRITE)
(EQUAL (EV (QUOTE AL)
(LIST (QUOTE QUOTE)
X)
VA FA N)
X)))
(PUTPROPS EVAL-NLISTP PROVE-LEMMA ((REWRITE)
(AND (EQUAL (EV (QUOTE AL)
0 VA FA N)
0)
(EQUAL (EV (QUOTE AL)
(ADD1 N)
VA FA N)
(ADD1 N))
(EQUAL (EV (QUOTE AL)
(PACK X)
VA FA N)
(IF (EQUAL (PACK X)
(QUOTE T))
T
(IF (EQUAL (PACK X)
(QUOTE F))
F
(IF (EQUAL (PACK X)
(QUOTE NIL))
NIL
(GET (PACK X)
VA))))))))
(PUTPROPS EVLIST-NIL PROVE-LEMMA ((REWRITE)
(EQUAL (EV (QUOTE LIST)
NIL VA FA N)
NIL)))
(PUTPROPS EVLIST-CONS PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (EQUAL VX (EV (QUOTE AL)
X VA FA N))
(EQUAL VL (EV (QUOTE LIST)
L VA FA N)))
(EQUAL (EV (QUOTE LIST)
(CONS X L)
VA FA N)
(IF (BTMP VX)
(BTM)
(IF (BTMP VL)
(BTM)
(CONS VX VL)))))))
(PUTPROPS CNB-NBTM PROVE-LEMMA ((REWRITE)
(IMPLIES (CNB X)
(NOT (BTMP X)))))
(PUTPROPS CNB-CONS PROVE-LEMMA ((REWRITE)
(AND (EQUAL (CNB (CONS A B))
(AND (CNB A)
(CNB B)))
(IMPLIES (CNB X)
(CNB (CAR X)))
(IMPLIES (CNB X)
(CNB (CDR X))))))
(PUTPROPS CNB-LITATOM PROVE-LEMMA ((REWRITE)
(IMPLIES (LITATOM X)
(CNB X))))
(PUTPROPS CNB-NUMBERP PROVE-LEMMA ((REWRITE)
(IMPLIES (NUMBERP X)
(CNB X))))
(PUTPROPS GET-TMI-FA PROVE-LEMMA ((REWRITE)
(AND (EQUAL (GET (QUOTE TM)
(TMI-FA TM))
(LIST NIL (KWOTE TM)))
(EQUAL (GET (QUOTE INSTR)
(TMI-FA TM))
(INSTR-DEFN))
(EQUAL (GET (QUOTE NEW-TAPE)
(TMI-FA TM))
(NEW-TAPE-DEFN))
(EQUAL (GET (QUOTE TMI)
(TMI-FA TM))
(TMI-DEFN)))))
(PUTPROPS EVAL-INSTR PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (CNB (EV (QUOTE AL)
ST VA (TMI-FA TM)
N))
(CNB (EV (QUOTE AL)
SYM VA (TMI-FA TM)
N))
(CNB (EV (QUOTE AL)
TM-- VA (TMI-FA TM)
N)))
(EQUAL (EV (QUOTE AL)
(LIST (QUOTE INSTR)
ST SYM TM--)
VA
(TMI-FA TM)
N)
(INSTRN (EV (QUOTE AL)
ST VA (TMI-FA TM)
N)
(EV (QUOTE AL)
SYM VA (TMI-FA TM)
N)
(EV (QUOTE AL)
TM-- VA (TMI-FA TM)
N)
N)))
((INDUCT (EVAL-INSTR-INDUCTION-SCHEME ST SYM TM-- VA TM N)))))
(PUTPROPS EVAL-NEW-TAPE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (CNB (EV (QUOTE AL)
OP VA (TMI-FA TM)
N))
(CNB (EV (QUOTE AL)
TAPE VA (TMI-FA TM)
N)))
(EQUAL (EV (QUOTE AL)
(LIST (QUOTE NEW-TAPE)
OP TAPE)
VA
(TMI-FA TM)
N)
(IF (ZEROP N)
(BTM)
(NEW-TAPE (EV (QUOTE AL)
OP VA (TMI-FA TM)
N)
(EV (QUOTE AL)
TAPE VA (TMI-FA TM)
N)))))))
(PUTPROPS CNB-INSTRN PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N)))))
(PUTPROPS CNB-NEW-TAPE PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (CNB OP)
(CNB TAPE))
(CNB (NEW-TAPE OP TAPE)))))
(PUTPROPS EVAL-TMI PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (CNB (EV (QUOTE AL)
ST VA (TMI-FA TM)
N))
(CNB (EV (QUOTE AL)
TAPE VA (TMI-FA TM)
N))
(CNB (EV (QUOTE AL)
TM-- VA (TMI-FA TM)
N)))
(EQUAL (EV (QUOTE AL)
(LIST (QUOTE TMI)
ST TAPE TM--)
VA
(TMI-FA TM)
N)
(TMIN (EV (QUOTE AL)
ST VA (TMI-FA TM)
N)
(EV (QUOTE AL)
TAPE VA (TMI-FA TM)
N)
(EV (QUOTE AL)
TM-- VA (TMI-FA TM)
N)
N)))
((INDUCT (EVAL-TMI-INDUCTION-SCHEME ST TAPE TM-- VA TM N)))))
(PUTPROPS EVAL-TMI-X PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (CNB ST)
(CNB TAPE)
(CNB TM))
(EQUAL (EV (QUOTE AL)
(TMI-X ST TAPE)
NIL
(TMI-FA TM)
N)
(IF (ZEROP N)
(BTM)
(TMIN ST TAPE TM N))))))
(PUTPROPS INSTRN-INSTR PROVE-LEMMA ((REWRITE)
(IMPLIES (LESSP (LENGTH TM)
N)
(EQUAL (INSTRN ST SYM TM N)
(INSTR ST SYM TM)))))
(PUTPROPS NBTMP-INSTR PROVE-LEMMA ((REWRITE)
(IMPLIES (TURING-MACHINE TM)
(NOT (BTMP (INSTR ST SYM TM))))))
(PUTPROPS INSTRN-NON-F PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (TURING-MACHINE TM)
(LEQ N (LENGTH TM)))
(INSTRN ST SYM TM N))))
(PUTPROPS TMIN-BTM PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (TURING-MACHINE TM)
(LEQ N (LENGTH TM)))
(EQUAL (TMIN ST TAPE TM N)
(BTM)))))
(PUTPROPS TMIN-TMI PROVE-LEMMA ((REWRITE)
(IMPLIES (TURING-MACHINE TM)
(EQUAL (TMI ST TAPE TM K)
(TMIN ST TAPE TM (PLUS K (ADD1 (LENGTH TM))))))))
(PUTPROPS SYMBOL-CNB PROVE-LEMMA ((REWRITE)
(IMPLIES (SYMBOL SYM)
(CNB SYM))))
(PUTPROPS HALF-TAPE-CNB PROVE-LEMMA ((REWRITE)
(IMPLIES (HALF-TAPE X)
(CNB X))))
(PUTPROPS TAPE-CNB PROVE-LEMMA ((REWRITE)
(IMPLIES (TAPE X)
(CNB X))))
(PUTPROPS OPERATION-CNB PROVE-LEMMA ((REWRITE)
(IMPLIES (OPERATION OP)
(CNB OP))))
(PUTPROPS TURING-MACHINE-CNB PROVE-LEMMA ((REWRITE)
(IMPLIES (TURING-MACHINE TM)
(CNB TM))))
(PUTPROPS TURING-COMPLETENESS-OF-LISP PROVE-LEMMA (NIL
(IMPLIES (AND (STATE ST)
(TAPE TAPE)
(TURING-MACHINE TM))
(AND (IMPLIES (NOT (BTMP (EVAL (TMI-X ST TAPE)
NIL
(TMI-FA TM)
N)))
(NOT (BTMP (TMI ST TAPE TM (TMI-K ST TAPE TM N)))))
(IMPLIES (NOT (BTMP (TMI ST TAPE TM K)))
(EQUAL (TMI ST TAPE TM K)
(EVAL (TMI-X ST TAPE)
NIL
(TMI-FA TM)
(TMI-N ST TAPE TM K))))))
NIL))
(DEFINEQ
(PROVEALL11
(LAMBDA NIL (* kbr: "19-Oct-85 16:31")
(PROVEALL (QUOTE ((NOTE-LIB BOOTSTRAP)
(ADD-SHELL ZN NIL ZNP ((POS (ONE-OF NUMBERP)
ZERO)
(NEG (ONE-OF NUMBERP)
ZERO)))
(DEFN& ZLESSP)
(DEFN& ZLESSEQP)
(DEFN& ZMAX)
(DEFN& ZMIN)
(DEFN& ZSUB1)
(DEFN& PZDIFFERENCE)
(DEFN& M1)
(DEFN& M2)
(DEFN& M3)
(DEFN& TAK0)
(DEFN& M)
(PROVE-LEMMA& TAK0-SATISFIES-TAK-EQUATION)
(PROVE-LEMMA& M1-LESSEQP-0)
(PROVE-LEMMA& M1-LESSEQP-1)
(PROVE-LEMMA& M1-LESSEQP-2)
(PROVE-LEMMA& M1-LESSEQP-3)
(PROVE-LEMMA& M2-LESSEQP-0)
(PROVE-LEMMA& M2-LESSEQP-1)
(PROVE-LEMMA& M2-LESSEQP-2)
(PROVE-LEMMA& M2-LESSEQP-3)
(PROVE-LEMMA& M3-LESSP-0)
(PROVE-LEMMA& M3-LESSP-1)
(PROVE-LEMMA& M3-LESSP-2)
(PROVE-LEMMA& M3-LESSP-3)
(DISABLE ZLESSP)
(DISABLE M1)
(DISABLE M2)
(DISABLE M3)
(DISABLE TAK0)
(DISABLE ZSUB1)
(PROVE-LEMMA& M-GOES-DOWN-1)
(PROVE-LEMMA& M-GOES-DOWN-2)
(PROVE-LEMMA& M-GOES-DOWN-3)
(PROVE-LEMMA& M-GOES-DOWN-0)))
NIL ZTAK)))
)
(PUTPROPS ZLESSP DEFN ((X Y)
(LESSP (PLUS (POS X)
(NEG Y))
(PLUS (NEG X)
(POS Y)))))
(PUTPROPS ZLESSEQP DEFN ((X Y)
(NOT (ZLESSP Y X))))
(PUTPROPS ZMAX DEFN ((X Y)
(IF (ZLESSP X Y)
Y X)))
(PUTPROPS ZMIN DEFN ((X Y)
(IF (ZLESSP X Y)
X Y)))
(PUTPROPS ZSUB1 DEFN ((X)
(ZN (POS X)
(ADD1 (NEG X)))))
(PUTPROPS PZDIFFERENCE DEFN ((X Y)
(DIFFERENCE (PLUS (POS X)
(NEG Y))
(PLUS (NEG X)
(POS Y)))))
(PUTPROPS M1 DEFN ((X Y Z)
(IF (ZLESSEQP X Y)
0 1)))
(PUTPROPS M2 DEFN ((X Y Z)
(PZDIFFERENCE (ZMAX X (ZMAX Y Z))
(ZMIN X (ZMIN Y Z)))))
(PUTPROPS M3 DEFN ((X Y Z)
(PZDIFFERENCE X (ZMIN X (ZMIN Y Z)))))
(PUTPROPS TAK0 DEFN ((X Y Z)
(IF (ZLESSEQP X Y)
Y
(IF (ZLESSEQP Y Z)
Z X))))
(PUTPROPS M DEFN ((X Y Z)
(CONS (M1 X Y Z)
(CONS (M2 X Y Z)
(CONS (M3 X Y Z)
NIL)))))
(PUTPROPS TAK0-SATISFIES-TAK-EQUATION PROVE-LEMMA (NIL (EQUAL (TAK0 X Y Z)
(IF (ZLESSEQP X Y)
Y
(TAK0 (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y))))))
(PUTPROPS M1-LESSEQP-0 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M1 X Y Z)
(M1 (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y)))))))
(PUTPROPS M1-LESSEQP-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M1 X Y Z)
(M1 (ZSUB1 X)
Y Z))))))
(PUTPROPS M1-LESSEQP-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M1 X Y Z)
(M1 (ZSUB1 Y)
Z X))))))
(PUTPROPS M1-LESSEQP-3 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M1 X Y Z)
(M1 (ZSUB1 Z)
X Y))))))
(PUTPROPS M2-LESSEQP-0 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M2 X Y Z)
(M2 (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y)))))))
(PUTPROPS M2-LESSEQP-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M2 X Y Z)
(M2 (ZSUB1 X)
Y Z))))))
(PUTPROPS M2-LESSEQP-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (ZSUB1 Y)
Z X)
(M1 X Y Z)))
(NOT (LESSP (M2 X Y Z)
(M2 (ZSUB1 Y)
Z X))))))
(PUTPROPS M2-LESSEQP-3 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (ZSUB1 Z)
X Y)
(M1 X Y Z)))
(NOT (LESSP (M2 X Y Z)
(M2 (ZSUB1 Z)
X Y))))))
(PUTPROPS M3-LESSP-0 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y))
(M1 X Y Z)))
(LESSP (M3 (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y))
(M3 X Y Z)))))
(PUTPROPS M3-LESSP-1 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (ZSUB1 X)
Y Z)
(M1 X Y Z)))
(LESSP (M3 (ZSUB1 X)
Y Z)
(M3 X Y Z)))))
(PUTPROPS M3-LESSP-2 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (ZSUB1 Y)
Z X)
(M1 X Y Z)))
(LESSP (M3 (ZSUB1 Y)
Z X)
(M3 X Y Z)))))
(PUTPROPS M3-LESSP-3 PROVE-LEMMA ((REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (ZSUB1 Z)
X Y)
(M1 X Y Z)))
(LESSP (M2 (ZSUB1 Z)
X Y)
(M2 X Y Z)))))
(PUTPROPS M-GOES-DOWN-1 PROVE-LEMMA (NIL (IMPLIES (NOT (ZLESSEQP X Y))
(LEX3 (M (ZSUB1 X)
Y Z)
(M X Y Z)))))
(PUTPROPS M-GOES-DOWN-2 PROVE-LEMMA (NIL (IMPLIES (NOT (ZLESSEQP X Y))
(LEX3 (M (ZSUB1 Y)
Z X)
(M X Y Z)))))
(PUTPROPS M-GOES-DOWN-3 PROVE-LEMMA (NIL (IMPLIES (NOT (ZLESSEQP X Y))
(LEX3 (M (ZSUB1 Z)
X Y)
(M X Y Z)))))
(PUTPROPS M-GOES-DOWN-0 PROVE-LEMMA (NIL (IMPLIES (NOT (ZLESSEQP X Y))
(LEX3 (M (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y))
(M X Y Z)))
NIL))
(PUTPROPS BOYERMOOREDATA COPYRIGHT ("Xerox Corporation" 1985))
(DECLARE: DONTCOPY
(FILEMAP (NIL (14507 14707 (PROVEALL1 14517 . 14705)) (14708 30715 (PROVEALL2 14718 . 30713)) (102342
104745 (PROVEALL3 102352 . 104743)) (117675 119710 (PROVEALL4 117685 . 119708)) (131637 137671 (
PROVEALL5 131647 . 137669)) (181124 185963 (PROVEALL6 181134 . 185961)) (192829 194716 (PROVEALL7
192839 . 194714)) (201671 203506 (PROVEALL8 201681 . 203504)) (209608 212137 (PROVEALL9 209618 .
212135)) (221968 224451 (PROVEALL10 221978 . 224449)) (237971 239340 (PROVEALL11 237981 . 239338)))))
STOP