(setq pvs-rule-and-strategy-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))) 
(after-justification nil) 
(after-justification$ nil) 
(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?)) 
(apply-lemma (lemma-name &rest expressions)) 
(apply-lemma$ (lemma-name &rest expressions)) 
(apply-rewrite (lemma-name &rest expressions)) 
(apply-rewrite$ (lemma-name &rest expressions)) 
(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)) 
(cancel (&optional (fnums *) sign)) 
(cancel$ (&optional (fnums *) sign)) 
(cancel-any (fnum sign)) 
(cancel-any$ (fnum sign)) 
(cancel-basic
 (fnum formula name? cancel-term left-term op rel right-term &optional
  (polarity ""))) 
(cancel-basic$
 (fnum formula name? cancel-term left-term op rel right-term &optional
  (polarity ""))) 
(cancel-cases
 (fnum formula sign name? cancel-term left-term op rel right-term)) 
(cancel-cases$
 (fnum formula sign name? cancel-term left-term op rel right-term)) 
(cancel-lr-one (fnum end sign try-just)) 
(cancel-lr-one$ (fnum end sign try-just)) 
(cancel-one (fnum formula name? cancel-term left-term op rel right-term)) 
(cancel-one$ (fnum formula name? cancel-term left-term op rel right-term)) 
(cancel-terms (&optional (fnums *) (end l) (sign nil) (try-just nil))) 
(cancel-terms$ (&optional (fnums *) (end l) (sign nil) (try-just nil))) 
(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) 
(claim (cond &optional (try-just nil) &rest terms)) 
(claim$ (cond &optional (try-just nil) &rest terms)) 
(comment (string)) 
(cond-coverage-tcc nil) 
(cond-coverage-tcc$ nil) 
(cond-disjoint-tcc nil) 
(cond-disjoint-tcc$ nil) 
(consider (cond &rest terms)) 
(consider$ (cond &rest terms)) 
(copy (fnum)) 
(copy$ (fnum)) 
(cross-add (&optional (fnums *))) 
(cross-add$ (&optional (fnums *))) 
(cross-add-lr (fnum side)) 
(cross-add-lr$ (fnum side)) 
(cross-add-one (fnum &optional (depth-limit 10))) 
(cross-add-one$ (fnum &optional (depth-limit 10))) 
(cross-mult (&optional (fnums *))) 
(cross-mult$ (&optional (fnums *))) 
(cross-mult-lr (fnum side)) 
(cross-mult-lr$ (fnum side)) 
(cross-mult-one (fnum &optional (depth-limit 10))) 
(cross-mult-one$ (fnum &optional (depth-limit 10))) 
(cross-mult-pos-neg-lr (fnum side)) 
(cross-mult-pos-neg-lr$ (fnum side)) 
(cross-mult-typed-lr (fnum side)) 
(cross-mult-typed-lr$ (fnum side)) 
(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?)) 
(div-by (fnums term &optional (sign +))) 
(div-by$ (fnums term &optional (sign +))) 
(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)) 
(else* (&rest steps)) 
(else*$ (&rest steps)) 
(equate (lhs rhs &optional (try-just nil))) 
(equate$ (lhs rhs &optional (try-just nil))) 
(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)) 
(expand-try (fn fnums force)) 
(expand-try$ (fn fnums force)) 
(expand1* (names)) 
(expand1*$ (names)) 
(extensionality (type)) 
(factor (fnum &optional (side *) (term-nums *) id?)) 
(factor$ (fnum &optional (side *) (term-nums *) id?)) 
(factor-terms-one (fnum side term-nums id?)) 
(factor-terms-one$ (fnum side term-nums id?)) 
(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))) 
(group (term1 operator term2 term3 &optional (side l))) 
(group$ (term1 operator term2 term3 &optional (side l))) 
(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?)) 
(invoke* (rule/strat fnums pattern)) 
(invoke*$ (rule/strat fnums pattern)) 
(invoke1 (rule/strat fnums pattern)) 
(invoke1$ (rule/strat fnums pattern)) 
(is-neg (term &optional (try-just nil))) 
(is-neg$ (term &optional (try-just nil))) 
(is-pos (term &optional (try-just nil))) 
(is-pos$ (term &optional (try-just nil))) 
(is-zero (term &optional (try-just nil))) 
(is-zero$ (term &optional (try-just nil))) 
(isolate (fnum side term-num)) 
(isolate$ (fnum side term-num)) 
(isolate-mult (fnum side &optional (term-num 1) (sign +))) 
(isolate-mult$ (fnum side &optional (term-num 1) (sign +))) 
(isolate-mult-rest (fnum side sign)) 
(isolate-mult-rest$ (fnum side sign)) 
(isolate-replace (fnum side term-num &optional (targets *))) 
(isolate-replace$ (fnum side term-num &optional (targets *))) 
(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) 
(move-terms (fnum side &optional (term-nums *))) 
(move-terms$ (fnum side &optional (term-nums *))) 
(move-terms-one (rel fnum side term-nums)) 
(move-terms-one$ (rel fnum side term-nums)) 
(move-to-front (&rest fnums)) 
(move-to-front$ (&rest fnums)) 
(mult-by (fnums term &optional (sign +))) 
(mult-by$ (fnums term &optional (sign +))) 
(mult-by-real (term fnum sign formula relation)) 
(mult-by-real$ (term fnum sign formula relation)) 
(mult-eq (rel-fnum eq-fnum &optional (sign +))) 
(mult-eq$ (rel-fnum eq-fnum &optional (sign +))) 
(mult-eq-one (rel-formula eq-formula eq-fnum sign)) 
(mult-eq-one$ (rel-formula eq-formula eq-fnum sign)) 
(mult-ineq (fnum1 fnum2 &optional (signs (+ +)))) 
(mult-ineq$ (fnum1 fnum2 &optional (signs (+ +)))) 
(mult-ineq-one (formula1 formula2 signs)) 
(mult-ineq-one$ (formula1 formula2 signs)) 
(mult/div-by (op term fnum sign)) 
(mult/div-by$ (op term fnum sign)) 
(mult/div-by-nz (op term fnum sign formula relation)) 
(mult/div-by-nz$ (op term fnum sign formula relation)) 
(musimp (&optional (fnums *) dynamic-ordering? irredundant? verbose?)) 
(name (name expr)) 
(name-extract (name fnum pattern)) 
(name-extract$ (name fnum pattern)) 
(name-induct-and-rewrite (var &optional (fnum 1) name &rest rewrites)) 
(name-induct-and-rewrite$ (var &optional (fnum 1) name &rest rewrites)) 
(name-mult (name fnum side &optional (term-nums *))) 
(name-mult$ (name fnum side &optional (term-nums *))) 
(name-mult-rest (name fnum side term-nums)) 
(name-mult-rest$ (name fnum side term-nums)) 
(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))) 
(permute-mult (fnum &optional (side r) (term-nums 2))) 
(permute-mult$ (fnum &optional (side r) (term-nums 2))) 
(permute-mult-one (fnum side term-nums end)) 
(permute-mult-one$ (fnum side term-nums end)) 
(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) 
(recip-mult (fnum side)) 
(recip-mult$ (fnum side)) 
(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?)) 
(replace-hide (n)) 
(replace-hide$ (n)) 
(replace-hide* (&optional (flist 0))) 
(replace-hide*$ (&optional (flist 0))) 
(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-reals (&optional (fnums *))) 
(rewrite-reals$ (&optional (fnums *))) 
(rewrite-with-fnum (fnum &optional subst (fnums *) (dir lr))) 
(rewrite-with-fnum$ (fnum &optional subst (fnums *) (dir lr))) 
(rotate++ nil) 
(rotate++$ nil) 
(rotate-- nil) 
(rotate--$ nil) 
(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)) 
(show-match (command fnums pattern)) 
(show-match$ (command fnums pattern)) 
(show-parens (&optional (fnums *))) 
(show-parens$ (&optional (fnums *))) 
(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)) 
(split-disjunctions* nil) 
(split-disjunctions*$ nil) 
(split-mult (fnum &optional (move? t))) 
(split-mult$ (fnum &optional (move? t))) 
(split-mult-one (fnum formula left-mult move?)) 
(split-mult-one$ (fnum formula left-mult move?)) 
(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) 
(swap (lhs operator rhs)) 
(swap$ (lhs operator rhs)) 
(swap-group (term1 operator term2 term3 &optional (side l))) 
(swap-group$ (term1 operator term2 term3 &optional (side l))) 
(swap-ineq (fnum)) 
(swap-ineq$ (fnum)) 
(swap-ineq-one (fnum formula operator)) 
(swap-ineq-one$ (fnum formula operator)) 
(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)) 
(transform-both (fnum transform &optional (swap nil) (try-just nil))) 
(transform-both$ (fnum transform &optional (swap nil) (try-just nil))) 
(try (strategy then else)) 
(try-branch (step steplist else-step)) 
(try-justification (try-just)) 
(try-justification$ (try-just)) 
(typepred (&rest exprs)) 
(typepred! (exprs &optional all?)) 
(undo (&optional (to 1))) 
(unfinished-justification (msg)) 
(unfinished-justification$ (msg)) 
(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))) 
)))