(setq *pvs-rulebase-signatures* (quote (
(ABS-SIMP (LIST-STATE-PREDICATES &OPTIONAL (FNUMS *)
 (EXCLUSIVE? NIL) (PROOF-COUNTER 10)))
(ABSTRACT
 (LIST-STATE-PREDICATES &OPTIONAL (CASES-REWRITE? T) EXCLUSIVE?
  (PROOF-COUNTER 10)))
(ABSTRACT$
 (LIST-STATE-PREDICATES &OPTIONAL (CASES-REWRITE? T) EXCLUSIVE?
  (PROOF-COUNTER 10)))
(ABSTRACT-AND-MC
 (LIST-STATE-PREDICATES &OPTIONAL (CASES-REWRITE? T) EXCLUSIVE?
  (PROOF-COUNTER 10)))
(ABSTRACT-AND-MC$
 (LIST-STATE-PREDICATES &OPTIONAL (CASES-REWRITE? T) EXCLUSIVE?
  (PROOF-COUNTER 10)))
(AP-ASSERT NIL)
(AP-ASSERT$ NIL)
(APPLY (STRATEGY &OPTIONAL COMMENT SAVE? TIME?))
(APPLY-ETA (TERM &OPTIONAL TYPE))
(APPLY-ETA$ (TERM &OPTIONAL TYPE))
(APPLY-EXTENSIONALITY (&OPTIONAL (FNUM +) KEEP? HIDE?))
(APPLY-EXTENSIONALITY$ (&OPTIONAL (FNUM +) KEEP? HIDE?))
(ASSERT (&OPTIONAL (FNUMS *) REWRITE-FLAG FLUSH? LINEAR? CASES-REWRITE?
         (TYPE-CONSTRAINTS? T) IGNORE-PROVER-OUTPUT?))
(ASSERT$
 (&OPTIONAL (FNUMS *) REWRITE-FLAG FLUSH? LINEAR? CASES-REWRITE?
  (TYPE-CONSTRAINTS? T) IGNORE-PROVER-OUTPUT?))
(ASSUMING-TCC NIL)
(ASSUMING-TCC$ NIL)
(AUTO-REWRITE (&REST NAMES))
(AUTO-REWRITE! (&REST NAMES))
(AUTO-REWRITE!! (&REST NAMES))
(AUTO-REWRITE!!$ (&REST NAMES))
(AUTO-REWRITE!$ (&REST NAMES))
(AUTO-REWRITE-DEFS (&OPTIONAL EXPLICIT? ALWAYS? EXCLUDE-THEORIES))
(AUTO-REWRITE-DEFS$ (&OPTIONAL EXPLICIT? ALWAYS? EXCLUDE-THEORIES))
(AUTO-REWRITE-EXPLICIT (&OPTIONAL ALWAYS?))
(AUTO-REWRITE-EXPLICIT$ (&OPTIONAL ALWAYS?))
(AUTO-REWRITE-THEORIES (&REST THEORIES))
(AUTO-REWRITE-THEORIES$ (&REST THEORIES))
(AUTO-REWRITE-THEORY (NAME &OPTIONAL EXCLUDE DEFS ALWAYS? TCCS?))
(AUTO-REWRITE-THEORY$ (NAME &OPTIONAL EXCLUDE DEFS ALWAYS? TCCS?))
(AUTO-REWRITE-THEORY-ALWAYS (THLIST))
(AUTO-REWRITE-THEORY-ALWAYS$ (THLIST))
(AUTO-REWRITE-THEORY-WITH-IMPORTINGS
 (NAME &OPTIONAL EXCLUDE-THEORIES IMPORTCHAIN? EXCLUDE DEFS ALWAYS? TCCS?))
(AUTO-REWRITE-THEORY-WITH-IMPORTINGS$
 (NAME &OPTIONAL EXCLUDE-THEORIES IMPORTCHAIN? EXCLUDE DEFS ALWAYS? TCCS?))
(BASH (&OPTIONAL (IF-MATCH T) (UPDATES? T) POLARITY? (INSTANTIATOR INST?)))
(BASH$ (&OPTIONAL (IF-MATCH T) (UPDATES? T) POLARITY? (INSTANTIATOR INST?)))
(BDDSIMP (&OPTIONAL (FNUMS *) (DYNAMIC-ORDERING? NIL) (IRREDUNDANT? T)))
(BETA (&OPTIONAL (FNUMS *) REWRITE-FLAG))
(BOTH-SIDES (OP TERM &OPTIONAL (FNUM 1)))
(BOTH-SIDES$ (OP TERM &OPTIONAL (FNUM 1)))
(BRANCH (STEP STEPLIST))
(CASE (&REST FORMULAS))
(CASE* (&REST FORMULAS))
(CASE*$ (&REST FORMULAS))
(CASE-REPLACE (FORMULA))
(CASE-REPLACE$ (FORMULA))
(CASES-TCC NIL)
(CASES-TCC$ NIL)
(CHAIN-ANTECEDENT (FNUM))
(CHAIN-ANTECEDENT$ (FNUM))
(CHAIN-ANTECEDENT* (FNUMS))
(CHAIN-ANTECEDENT*$ (FNUMS))
(CHECKPOINT NIL)
(COMMENT (STRING))
(COND-COVERAGE-TCC NIL)
(COND-COVERAGE-TCC$ NIL)
(COND-DISJOINT-TCC NIL)
(COND-DISJOINT-TCC$ NIL)
(COPY (FNUM))
(COPY$ (FNUM))
(DECOMPOSE-EQUALITY (&OPTIONAL (FNUM *) (HIDE? T)))
(DECOMPOSE-EQUALITY$ (&OPTIONAL (FNUM *) (HIDE? T)))
(DELETE (&REST FNUMS))
(DETUPLE-BOUNDVARS (&OPTIONAL (FNUMS *) SINGLES?))
(DETUPLE-BOUNDVARS$ (&OPTIONAL (FNUMS *) SINGLES?))
(DETUPLE-BOUNDVARS-IN-FORMULAS (FORMULAS SINGLES?))
(DETUPLE-BOUNDVARS-IN-FORMULAS$ (FORMULAS SINGLES?))
(DO-REWRITE
 (&OPTIONAL (FNUMS *) REWRITE-FLAG FLUSH? LINEAR? CASES-REWRITE?
  (TYPE-CONSTRAINTS? T)))
(DO-REWRITE$
 (&OPTIONAL (FNUMS *) REWRITE-FLAG FLUSH? LINEAR? CASES-REWRITE?
  (TYPE-CONSTRAINTS? T)))
(ELSE (STEP1 STEP2))
(ETA (TYPE))
(ETA$ (TYPE))
(EVAL (EXPR &OPTIONAL DESTRUCTIVE?))
(EVAL$ (EXPR &OPTIONAL DESTRUCTIVE?))
(EXISTENCE-TCC NIL)
(EXISTENCE-TCC$ NIL)
(EXPAND (FUNCTION-NAME &OPTIONAL (FNUM *) OCCURRENCE IF-SIMPLIFIES ASSERT?))
(EXPAND* (&REST NAMES))
(EXPAND*$ (&REST NAMES))
(EXPAND1* (NAMES))
(EXPAND1*$ (NAMES))
(EXTENSIONALITY (TYPE))
(FAIL NIL)
(FLATTEN (&REST FNUMS))
(FLATTEN$ (&REST FNUMS))
(FLATTEN-DISJUNCT (&OPTIONAL FNUMS DEPTH))
(FORWARD-CHAIN (LEMMA-OR-FNUM))
(FORWARD-CHAIN$ (LEMMA-OR-FNUM))
(GENERALIZE (TERM VAR &OPTIONAL TYPE (FNUMS *) (SUBTERMS-ONLY? T)))
(GENERALIZE$ (TERM VAR &OPTIONAL TYPE (FNUMS *) (SUBTERMS-ONLY? T)))
(GENERALIZE-SKOLEM-CONSTANTS (&OPTIONAL (FNUMS *)))
(GENERALIZE-SKOLEM-CONSTANTS$ (&OPTIONAL (FNUMS *)))
(GRIND
 (&OPTIONAL (DEFS !) THEORIES REWRITES EXCLUDE (IF-MATCH T) (UPDATES? T)
  POLARITY? (INSTANTIATOR INST?)))
(GRIND$
 (&OPTIONAL (DEFS !) THEORIES REWRITES EXCLUDE (IF-MATCH T) (UPDATES? T)
  POLARITY? (INSTANTIATOR INST?)))
(GROUND NIL)
(GROUND$ NIL)
(GROUND-FORWARD-CHAIN (&REST NAMES))
(GROUND-FORWARD-CHAIN-THEORY (NAME &OPTIONAL EXCLUDE TCCS?))
(GROUND-FORWARD-CHAIN-THEORY$ (NAME &OPTIONAL EXCLUDE TCCS?))
(GROUND-REWRITE (&OPTIONAL (FNUMS *) (REPLACE? T)))
(HELP (&OPTIONAL (NAME *)))
(HIDE (&REST FNUMS))
(HIDE-ALL-BUT (&OPTIONAL KEEP-FNUMS (FNUMS *)))
(HIDE-ALL-BUT$ (&OPTIONAL KEEP-FNUMS (FNUMS *)))
(IFF (&REST FNUMS))
(INDUCT (VAR &OPTIONAL (FNUM 1) NAME))
(INDUCT$ (VAR &OPTIONAL (FNUM 1) NAME))
(INDUCT-AND-REWRITE (VAR &OPTIONAL (FNUM 1) &REST REWRITES))
(INDUCT-AND-REWRITE! (VAR &OPTIONAL (FNUM 1) &REST REWRITES))
(INDUCT-AND-REWRITE!$ (VAR &OPTIONAL (FNUM 1) &REST REWRITES))
(INDUCT-AND-REWRITE$ (VAR &OPTIONAL (FNUM 1) &REST REWRITES))
(INDUCT-AND-SIMPLIFY
 (VAR &OPTIONAL (FNUM 1) NAME (DEFS T) (IF-MATCH BEST) THEORIES REWRITES
  EXCLUDE (INSTANTIATOR INST?)))
(INDUCT-AND-SIMPLIFY$
 (VAR &OPTIONAL (FNUM 1) NAME (DEFS T) (IF-MATCH BEST) THEORIES REWRITES
  EXCLUDE (INSTANTIATOR INST?)))
(INST (FNUM &REST TERMS))
(INST!
 (&OPTIONAL (FNUMS *) SUBST (WHERE *) COPY? (IF-MATCH BEST) COMPLETE?
  (RELATIVIZE? T)))
(INST!$
 (&OPTIONAL (FNUMS *) SUBST (WHERE *) COPY? (IF-MATCH BEST) COMPLETE?
  (RELATIVIZE? T)))
(INST$ (FNUM &REST TERMS))
(INST-CP (FNUM &REST TERMS))
(INST-CP$ (FNUM &REST TERMS))
(INST? (&OPTIONAL (FNUMS *) SUBST (WHERE *) COPY? IF-MATCH POLARITY? (TCC? T)))
(INST?$
 (&OPTIONAL (FNUMS *) SUBST (WHERE *) COPY? IF-MATCH POLARITY? (TCC? T)))
(INSTALL-GROUND-REWRITES NIL)
(INSTALL-REWRITES (&OPTIONAL DEFS THEORIES REWRITES EXCLUDE-THEORIES EXCLUDE))
(INSTALL-REWRITES$ (&OPTIONAL DEFS THEORIES REWRITES EXCLUDE-THEORIES EXCLUDE))
(INSTANTIATE (FNUM TERMS &OPTIONAL COPY?))
(INSTANTIATE-ONE (FNUM TERMS &OPTIONAL COPY?))
(INSTANTIATE-ONE$ (FNUM TERMS &OPTIONAL COPY?))
(JUST-INSTALL-PROOF (PROOF))
(LABEL (LABEL FNUMS &OPTIONAL PUSH?))
(LABEL-FNUMS (LABELS FNUMS &OPTIONAL PUSH?))
(LABEL-FNUMS$ (LABELS FNUMS &OPTIONAL PUSH?))
(LEMMA (NAME &OPTIONAL SUBST))
(LET (BINDINGS BODY))
(LIFT-IF (&OPTIONAL FNUMS (UPDATES? T)))
(LISP (LEXP))
(MEASURE-INDUCT (MEASURE VARS &OPTIONAL (FNUM 1) ORDER))
(MEASURE-INDUCT$ (MEASURE VARS &OPTIONAL (FNUM 1) ORDER))
(MEASURE-INDUCT+ (MEASURE VARS &OPTIONAL (FNUM 1) ORDER))
(MEASURE-INDUCT+$ (MEASURE VARS &OPTIONAL (FNUM 1) ORDER))
(MEASURE-INDUCT-AND-SIMPLIFY
 (MEASURE VARS &OPTIONAL (FNUM 1) ORDER EXPAND (DEFS T) (IF-MATCH BEST)
          THEORIES REWRITES EXCLUDE (INSTANTIATOR INST?)))
(MEASURE-INDUCT-AND-SIMPLIFY$
 (MEASURE VARS &OPTIONAL (FNUM 1) ORDER EXPAND (DEFS T) (IF-MATCH BEST)
          THEORIES REWRITES EXCLUDE (INSTANTIATOR INST?)))
(MERGE-FNUMS (FNUMS))
(MERGE-FNUMS$ (FNUMS))
(MODEL-CHECK
 (&OPTIONAL (DYNAMIC-ORDERING? T) (CASES-REWRITE? T) DEFS THEORIES REWRITES
  EXCLUDE IRREDUNDANT?))
(MODEL-CHECK$
 (&OPTIONAL (DYNAMIC-ORDERING? T) (CASES-REWRITE? T) DEFS THEORIES REWRITES
  EXCLUDE IRREDUNDANT?))
(MONOTONICITY-TCC NIL)
(MONOTONICITY-TCC$ NIL)
(MUSIMP (&OPTIONAL (FNUMS *) DYNAMIC-ORDERING? IRREDUNDANT? VERBOSE?))
(NAME (NAME EXPR))
(NAME-INDUCT-AND-REWRITE (VAR &OPTIONAL (FNUM 1) NAME &REST REWRITES))
(NAME-INDUCT-AND-REWRITE$ (VAR &OPTIONAL (FNUM 1) NAME &REST REWRITES))
(NAME-REPLACE (NAME EXPR &OPTIONAL (HIDE? T)))
(NAME-REPLACE$ (NAME EXPR &OPTIONAL (HIDE? T)))
(NAME-REPLACE* (NAME-AND-EXPRS &OPTIONAL (HIDE? T)))
(NAME-REPLACE*$ (NAME-AND-EXPRS &OPTIONAL (HIDE? T)))
(POSTPONE (&OPTIONAL (PRINT? T)))
(PROP NIL)
(PROP$ NIL)
(PROPAX NIL)
(QE (&OPTIONAL (FNUMS '*) VERBOSE?))
(QUANT? (&OPTIONAL (FNUMS *) SUBST (WHERE *) COPY? IF-MATCH))
(QUANT?$ (&OPTIONAL (FNUMS *) SUBST (WHERE *) COPY? IF-MATCH))
(QUERY* NIL)
(QUIT NIL)
(RECORD
 (&OPTIONAL (FNUMS *) REWRITE-FLAG FLUSH? LINEAR? (TYPE-CONSTRAINTS? T)
  IGNORE-PROVER-OUTPUT?))
(RECORD$
 (&OPTIONAL (FNUMS *) REWRITE-FLAG FLUSH? LINEAR? (TYPE-CONSTRAINTS? T)
  IGNORE-PROVER-OUTPUT?))
(REDUCE (&OPTIONAL (IF-MATCH T) (UPDATES? T) POLARITY? (INSTANTIATOR INST?)))
(REDUCE$ (&OPTIONAL (IF-MATCH T) (UPDATES? T) POLARITY? (INSTANTIATOR INST?)))
(REPEAT (STEP))
(REPEAT* (STEP))
(REPLACE (FNUM &OPTIONAL (FNUMS *) DIR HIDE? ACTUALS?))
(REPLACE* (&REST FNUMS))
(REPLACE*$ (&REST FNUMS))
(REPLACE-ETA (TERM &OPTIONAL TYPE KEEP?))
(REPLACE-ETA$ (TERM &OPTIONAL TYPE KEEP?))
(REPLACE-EXTENSIONALITY (F G &OPTIONAL EXPECTED KEEP?))
(REPLACE-EXTENSIONALITY$ (F G &OPTIONAL EXPECTED KEEP?))
(RERUN (&OPTIONAL PROOF RECHECK? BREAK?))
(REVEAL (&REST FNUMS))
(REWRITE
 (LEMMA-OR-FNUM &OPTIONAL (FNUMS *) SUBST (TARGET-FNUMS *) (DIR LR)
  (ORDER IN)))
(REWRITE$
 (LEMMA-OR-FNUM &OPTIONAL (FNUMS *) SUBST (TARGET-FNUMS *) (DIR LR)
  (ORDER IN)))
(REWRITE-DIRECTLY-WITH-FNUM (FNUM &OPTIONAL (FNUMS *) (DIR LR)))
(REWRITE-DIRECTLY-WITH-FNUM$ (FNUM &OPTIONAL (FNUMS *) (DIR LR)))
(REWRITE-LEMMA (LEMMA SUBST &OPTIONAL (FNUMS *) (DIR LR)))
(REWRITE-LEMMA$ (LEMMA SUBST &OPTIONAL (FNUMS *) (DIR LR)))
(REWRITE-MSG-OFF NIL)
(REWRITE-MSG-ON NIL)
(REWRITE-WITH-FNUM (FNUM &OPTIONAL SUBST (FNUMS *) (DIR LR)))
(REWRITE-WITH-FNUM$ (FNUM &OPTIONAL SUBST (FNUMS *) (DIR LR)))
(RULE-INDUCT (REL &OPTIONAL (FNUM +) NAME))
(RULE-INDUCT$ (REL &OPTIONAL (FNUM +) NAME))
(RULE-INDUCT-STEP (REL &OPTIONAL (FNUM -) NAME))
(RULE-INDUCT-STEP$ (REL &OPTIONAL (FNUM -) NAME))
(SAME-NAME (NAME1 NAME2 &OPTIONAL TYPE))
(SAME-NAME-TCC NIL)
(SAME-NAME-TCC$ NIL)
(SET-PRINT-DEPTH (&OPTIONAL DEPTH))
(SET-PRINT-LENGTH (&OPTIONAL LENGTH))
(SET-PRINT-LINES (&OPTIONAL LINES))
(SIMPLE-INDUCT (VAR FMLA &OPTIONAL NAME))
(SIMPLE-INDUCT$ (VAR FMLA &OPTIONAL NAME))
(SIMPLE-MEASURE-INDUCT (MEASURE VARS &OPTIONAL (FNUM 1) ORDER))
(SIMPLE-MEASURE-INDUCT$ (MEASURE VARS &OPTIONAL (FNUM 1) ORDER))
(SIMPLIFY
   (&OPTIONAL (FNUMS *) RECORD? REWRITE? REWRITE-FLAG FLUSH? LINEAR?
    CASES-REWRITE? (TYPE-CONSTRAINTS? T) IGNORE-PROVER-OUTPUT?))
(SIMPLIFY-WITH-REWRITES
 (&OPTIONAL (FNUMS *) DEFS THEORIES REWRITES EXCLUDE-THEORIES EXCLUDE))
(SIMPLIFY-WITH-REWRITES$
 (&OPTIONAL (FNUMS *) DEFS THEORIES REWRITES EXCLUDE-THEORIES EXCLUDE))
(SKIP NIL)
(SKIP-MSG (MSG &OPTIONAL FORCE-PRINTING?))
(SKOLEM (FNUM CONSTANTS))
(SKOLEM! (&OPTIONAL (FNUM *) KEEP-UNDERSCORE?))
(SKOLEM!$ (&OPTIONAL (FNUM *) KEEP-UNDERSCORE?))
(SKOLEM-TYPEPRED (&OPTIONAL (FNUM *)))
(SKOLEM-TYPEPRED$ (&OPTIONAL (FNUM *)))
(SKOSIMP (&OPTIONAL (FNUM *) PREDS?))
(SKOSIMP$ (&OPTIONAL (FNUM *) PREDS?))
(SKOSIMP* (&OPTIONAL PREDS?))
(SKOSIMP*$ (&OPTIONAL PREDS?))
(SMASH (&OPTIONAL (UPDATES? T)))
(SMASH$ (&OPTIONAL (UPDATES? T)))
(SPLIT (&OPTIONAL (FNUM *) DEPTH))
(SPREAD (STEP STEPLIST))
(SPREAD! (STEP STEPLIST))
(SPREAD@ (STEP STEPLIST))
(STOP-REWRITE (&REST NAMES))
(STOP-REWRITE-THEORY (&REST THEORIES))
(STOP-REWRITE-THEORY$ (&REST THEORIES))
(SUBTYPE-TCC NIL)
(SUBTYPE-TCC$ NIL)
(TCC (&OPTIONAL (DEFS !)))
(TCC$ (&OPTIONAL (DEFS !)))
(TCC-BDD (&OPTIONAL (DEFS !)))
(TCC-BDD$ (&OPTIONAL (DEFS !)))
(TERMINATION-TCC NIL)
(TERMINATION-TCC$ NIL)
(THEN (&REST STEPS))
(THEN* (&REST STEPS))
(THEN@ (&REST STEPS))
(TIME (STRAT))
(TRACE (&REST NAMES))
(TRACE$ (&REST NAMES))
(TRACK-REWRITE (&REST NAMES))
(TRY (STRATEGY THEN ELSE))
(TRY-BRANCH (STEP STEPLIST ELSE-STEP))
(TYPEPRED (&REST EXPRS))
(TYPEPRED! (EXPRS &OPTIONAL ALL?))
(UNDO (&OPTIONAL (TO 1)))
(UNLABEL (&OPTIONAL FNUMS))
(UNTRACE (&REST NAMES))
(UNTRACE$ (&REST NAMES))
(UNTRACK-REWRITE (&REST NAMES))
(USE (LEMMA &OPTIONAL SUBST (IF-MATCH BEST) (INSTANTIATOR INST?)))
(USE$ (LEMMA &OPTIONAL SUBST (IF-MATCH BEST) (INSTANTIATOR INST?)))
(USE* (&REST NAMES))
(USE*$ (&REST NAMES))
(WELL-FOUNDED-TCC NIL)
(WELL-FOUNDED-TCC$ NIL)
(WITH-LABELS (RULE LABELS &OPTIONAL PUSH?))
(WITH-LABELS$ (RULE LABELS &OPTIONAL PUSH?))
(WS1S
 (&OPTIONAL (FNUMS *) (EXAMPLES? T) (AUTOMATON? NIL) (TRACES? NIL)
  (VERBOSE? T) (DEFS !) THEORIES REWRITES EXCLUDE))
(WS1S$
 (&OPTIONAL (FNUMS *) (EXAMPLES? T) (AUTOMATON? NIL) (TRACES? NIL)
  (VERBOSE? T) (DEFS !) THEORIES REWRITES EXCLUDE))
(WS1S-SIMP
 (&OPTIONAL (FNUMS *) (EXAMPLES T) (AUTOMATON NIL) (TRACES NIL) (VERBOSE T)))

)))