(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)))
)))