# Proofs

proof_type: f_proof
decl_type: formula
library: while
theory: congruence
signature: nil
run_date: Unknown date
run_time: ----
status: proved-complete
description: nil
script:
  (""
   (lemma "structural_induction")
   (inst - "lambda (S:Stm): P(continuation.SS(S), direct.SS(S))")
   (skosimp)
   (split)
   (("1" (inst - "S!1"))
    ("2"
     (hide 2)
     (expand "SS")
     (expand "P")
     (skosimp*)
     (apply-extensionality 1 :hide? t)
     (expand "o")
     (propax))
    ("3"
     (hide 2)
     (expand "SS")
     (expand "P")
     (expand "I")
     (expand "o ")
     (skosimp)
     (apply-extensionality 1 :hide? t))
    ("4"
     (hide 2)
     (skosimp*)
     (expand "P")
     (skosimp*)
     (expand "SS" 1)
     (expand "o" 1 1)
     (inst -2 "c!1")
     (replace -2 1)
     (hide -2)
     (inst - "c!1 o direct.SS(S2!1)")
     (replace -1 1)
     (hide -1)
     (apply-extensionality 1 :hide? t)
     (expand "o" 1 2)
     (expand "o" 1 2)
     (expand "o" 1 2)
     (case-replace "direct.SS(S1!1)(x!1)=bottom")
     (("1" (assert)) ("2" (assert) (expand "o") (propax))))
    ("5"
     (hide 2)
     (skosimp)
     (expand "P")
     (skosimp)
     (expand "SS" 1)
     (expand "conditional")
     (apply-extensionality 1 :hide? t)
     (expand "o")
     (case-replace "B(b!1)(x!1)")
     (("1" (inst -2 "c!1") (replace -2 1) (assert))
      ("2" (assert) (inst -2 "c!1") (replace -2 2) (assert))))
    ("6"
     (hide 2)
     (skosimp)
     (expand "SS" 1)
     (lemma "admissible_P")
     (lemma "dual_fixpoint_induction"
      ("p"
       "P"
       "phi"
       "LAMBDA (g:(scott_continuous?[Cont,Cont,(sq_le),(sq_le)])): LAMBDA c: conditional(B(b!1), continuation.SS(S1!1)(g(c)), c)"
       "psi"
       "LAMBDA c: conditional(B(b!1), c o direct.SS(S1!1), LAMBDA s: up(s))"))
     (("1"
       (split -1)
       (("1" (propax))
        ("2"
         (hide 2)
         (expand "admissible_pred?")
         (skosimp)
         (expand "P")
         (skosimp)
         (inst -3 "x!1(c!1)")
         (replace -3)
         (inst -1 "c!1")
         (hide -2 -3)
         (lemma "composition_conditional" ("b" "b!1" "c" "c!1"))
         (inst - "y!1 o direct.SS(S1!1)" "_")
         (inst - "LAMBDA s: up(s)")
         (replace -1 1 rl)
         (hide -1)
         (apply-extensionality 1 :hide? t)
         (expand "conditional")
         (case-replace "B(b!1)(x!2)")
         (("1" (replace -2) (hide -1 -2) (grind))
          ("2" (assert) (expand "o") (propax))))))
      ("2"
       (hide 2)
       (expand "increasing?")
       (skosimp)
       (expand "conditional")
       (expand "sq_le")
       (skosimp)
       (expand "o")
       (case-replace "B(b!1)(s1!1)")
       (("1"
         (case-replace "direct.SS(S1!1)(s1!1)=bottom")
         (("1" (assert))
          ("2"
           (assert)
           (inst - "down(direct.SS(S1!1)(s1!1))" "s2!1")
           (assert))))
        ("2" (assert))))
      ("3"
       (hide 2)
       (expand "increasing?")
       (skosimp)
       (typepred "continuation.SS(S1!1)")
       (expand "scott_continuous?")
       (expand "increasing?")
       (flatten)
       (hide -2)
       (expand "continuous_pointwise")
       (expand "pointwise")
       (skosimp)
       (inst -2 "x!2")
       (inst - "x!1(x!2)" "y!1(x!2)")
       (assert)
       (hide-all-but (-1 1))
       (expand "sq_le")
       (skosimp)
       (inst - "s1!1" "s2!1")
       (expand "conditional")
       (case-replace "B(b!1)(s1!1)")
       (("1" (assert)) ("2" (assert))))
      ("4"
       (hide 2)
       (skosimp)
       (typepred "g!1")
       (typepred "continuation.SS(S1!1)")
       (lemma "composition_continuous"
        ("f" "continuation.SS(S1!1)" "g" "g!1"))
       (lemma "identity_continuous")
       (lemma "conditional_continuous"
        ("b" "b!1" "f" "continuation.SS(S1!1) o g!1" "g" "I[Cont]"))
       (expand "o" -1)
       (expand "I" -1)
       (propax))
      ("5" (propax))))))


proof_type: t_proof
decl_type: tcc
library: while
theory: congruence
signature: nil
run_date: Unknown date
run_time: ----
status: proved-complete
description: nil
script:
  (""
   (expand "scott_continuous?")
   (case-replace "increasing?(LAMBDA c: LAMBDA s: bottom[State])")
   (("1"
     (expand "lub_preserving?")
     (skosimp*)
     (expand "image")
     (case-replace
      "{y: Cont | EXISTS (x: (D!1)): y = (LAMBDA s: bottom[State])} = singleton[Cont](LAMBDA s: bottom[State])")
     (("1" (hide -1) (rewrite "lub_singleton"))
      ("2"
       (hide 2)
       (apply-extensionality 1 :hide? t)
       (expand "singleton")
       (case-replace "x!1 = (LAMBDA s: bottom[State])")
       (("1"
         (typepred "D!1")
         (expand "nonempty?")
         (expand "empty?")
         (skosimp)
         (expand "member")
         (inst + "x!2"))
        ("2" (replace 1 2) (assert))))))
    ("2"
     (hide 2)
     (expand "increasing?")
     (skosimp)
     (expand "sq_le")
     (propax))))


proof_type: t_proof
decl_type: tcc
library: while
theory: congruence
signature: nil
run_date: Unknown date
run_time: ----
status: proved-complete
description: nil
script:
  (""
   (expand "directed_complete_partial_order?")
   (expand "partial_order?")
   (expand "preorder?")
   (expand "directed_complete?")
   (split)
   (("1" (grind)) ("2" (grind)) ("3" (grind))
    ("4"
     (skosimp)
     (typepred "D!1")
     (expand "least_bounded_above?")
     (case "D!1(FALSE)")
     (("1"
       (inst + "FALSE")
       (expand "least_upper_bound?")
       (expand "upper_bound?")
       (skosimp*)
       (assert)
       (inst - "FALSE"))
      ("2"
       (inst + "TRUE")
       (expand "least_upper_bound?")
       (expand "upper_bound?")
       (skosimp)
       (typepred "r!1")
       (expand "nonempty?")
       (expand "empty?")
       (skosimp)
       (expand "member")
       (grind))))))


# Steps

step_type: primitive_rule
library: prelude
docstring:
  (fail): 
      Signals a failure.  This is primarily used within strategies.
  For example, a top-level strategy of the form (then (strat1)(fail))
  applies strat1 and quits the proof unless strat1 completes the proof.
  See the prover manual for more details.


step_type: primitive_rule
library: prelude
docstring:
  (skolem fnum constants &optional (skolem-typepreds? dont-simplify?)): 
      Replaces the universally quantified variables in FNUM with new
  skolem constants in CONSTANTS.  If SKOLEM-TYPEPREDS? is T, then typepreds
  will be generated for the introduced constants.  If DONT-SIMPLIFY? is T,
  then the simplifications that occur automatically during substitution are
  suppressed.  
  Example: (skolem 1 ("A" "B"))
  See also SKOLEM!, SKOSIMP, SKOSIMP*.


step_type: primitive_rule
library: prelude
docstring:
  (bddsimp &optional
   ((fnums *) (dynamic-ordering? nil) (irredundant? t))): 
      Propositional simplification using Binary Decision Diagrams (BDDs).
    Dynamic ordering means the BDD package can reorder literals
    to reduce BDD size.
    See also PROP.


step_type: primitive_rule
library: prelude
docstring:
  (rahd-simp &optional
   ((fnums *) (simplify-division? t) verbosity search-model
    print-model)): 
      Real Algebra in High Dimensions


step_type: primitive_rule
library: prelude
docstring:
  (copy fnum): 
      Introduces a copy of formula number FNUM as the first antecedent
  or succedent formula in the sequent.


step_type: primitive_rule
library: prelude
docstring:
  (hide &rest fnums): 
      (hide <fnums>): Hides the formulas in FNUMS.
    See REVEAL and DELETE, and also the Emacs command M-x show-hidden-formulas.


step_type: primitive_rule
library: prelude
docstring:
  (musimp &optional ((fnums *) dynamic-ordering? irredundant? verbose?)): 
      MU Calculus Simplification.  Dynamic-ordering? set to T means the BDD
  package can reorder literals to reduce BDD size.  Irredundant? T computes
  the disjunctive normal form of the result (which can take quite a bit of
  time).  Verbose? set to T provides more information.


step_type: primitive_rule
library: prelude
docstring:
  (abs-simp cstate astate amap &optional
   ((strategy '(assert)) feasible verbose?)): 
      Builds an abstraction of the current sequent where AMAP is an
  abstraction map between concrete state type CSTATE and abstract state type
  ASTATE, FEASIBLE is a predicate characterizing the set of abstract states
  that correspond to some concrete state, and STRATEGY is the proof strategy
  to be used for discharging the abstraction proof obligations.


step_type: primitive_rule
library: prelude
docstring:
  (help &optional ((name *))): 
      Describes rules and strategies, but behaves like SKIP otherwise.
   (HELP <rule-or-strategy-name>) returns the help information for the
       given rule or strategy;
   (HELP rules) returns help for all the primitive commands;
   (HELP defined-rules) returns help for all the defined rules;
   (HELP strategies) returns help for all the strategies;
   (HELP) returns all of the above and should be avoided in
      favor of the Emacs command M-x help-pvs-prover.


step_type: primitive_rule
library: prelude
docstring:
  (open-frag-ex-inf-cad &optional ((fnums *))): 
      fragmented cylindrical algebraic decomposition with EX-INF-MANY relaxation for open predicates via QEPCAD-B


step_type: primitive_rule
library: prelude
docstring:
  (residue-class-ring-ineqs &optional ((fnums *))): 
      reduction of terms in inequalities to canonical rep's in residue class ring induced by equational constraints


step_type: primitive_rule
library: prelude
docstring:
  (expand function-name &optional
          ((fnum *) occurrence if-simplifies assert? actuals?)): 
      Expands (and simplifies) the definition of FUNCTION-NAME at a given
  OCCURRENCE.  If no OCCURRENCE is given, then all instances of the
  definition are expanded.  The OCCURRENCE is given as a number n
  referring to the nth occurrence of the function symbol counting
  from the left, or as a list of such numbers.  If the IF-SIMPLIFIES
  flag is T, then any definition expansion occurs only if the RHS
  instance simplifies (using the decision procedures).  Note that the
  EXPAND step also applies simplification with decision procedures
  (i.e. SIMPLIFY with default options) to any sequent formulas where
  an expansion has occurred.  ASSERT? can be either NONE (meaning no
  simplification), NIL (meaning simplify using SIMPLIFY), or T (meaning
  simplify using ASSERT).  If ACTUALS? is T, expansion is also done in
  actual parameters, mappings, and types.


step_type: primitive_rule
library: prelude
docstring:
  (yices2 &optional ((fnums *) nonlinear?)): 
      Invokes Yices as an endgame SMT solver to prove that the conjunction
  of the negations of the selected formulas is unsatisfiable. 


step_type: primitive_rule
library: prelude
docstring:
  (unlabel &optional (fnums label hidden?)): 
      Removes specified label (or all labels if none specified)
     from the formulas FNUMS (or when FNUMS is not specified, all formulas).
     FNUMS are considerd to be hidden formulas when hidden? is set to t.


step_type: primitive_rule
library: prelude
docstring:
  (stop-rewrite &rest names): 
      Turns off automatic rewriting.  Disables all rewrites if no
  arguments are given.  Disabled rewrites have to be enabled by
  AUTO-REWRITE, AUTO-REWRITE!, or AUTO-REWRITE-THEORY. E.g.,
   (stop-rewrite "assoc" "delete"). 


step_type: primitive_rule
library: prelude
docstring:
  (propax): 
      Checks if sequent has form ...,A |- ...A or ...|- a = a, ..., in
  which case it considers the subgoal proved and moves to the next pending
  (unproved) subgoal, if any.  If there are no more pending subgoals, the
  proof is complete.  Note that this rule is processed automatically after
  every proof step, and is rarely invoked by the user.


step_type: primitive_rule
library: prelude
docstring:
  (flatten-disjunct &optional (fnums depth)): 
      Disjunctively simplifies chosen formulas.  It simplifies 
  top-level antecedent conjunctions, equivalences, and negations, and
  succedent disjunctions, implications, and negations from the sequent.
  The DEPTH argument can either be a non-negative integer indicating
  the nesting of top-level disjunctions to be elimnated, or NIL
  which eliminates all top-level disjuncts in the indicated FNUMS.


step_type: primitive_rule
library: prelude
docstring:
  (random-test &optional
   ((fnum *) (count 10) (size 100) (dtsize 10) all? verbose? instance
    (subtype-gen-bound 1000))): 
      Runs a random test on the given FNUMs, by creating random values for the
  skolem constants and running the ground evaluator on those values.  This is
  useful for checking if the given sequent is worth proving - if it comes back
  with a counter example, then it may not be worth trying to prove.  Of
  course, it may just be that a lemma is needed, or relevant formulas were
  hidden, and that it isn't really a counter example.  COUNT tests are run,
  and SIZE controls how the random data is generated by providing a bound, if
  necessary (e.g., an integer will be generated between -SIZE and SIZE).
  Normally the test stops when a counter example is found; if ALL? is t then
  it stops only after COUNT tests.  VERBOSE?, if t, causes each test to be
  printed before evaluation.  INSTANCE allows formals and uninterpreted types
  and constants to be given as a theory instance with actuals and mappings.
  The current theory may also be instantiated this way.


step_type: primitive_rule
library: prelude
docstring:
  (open-ex-inf-cad &optional ((fnums *))): 
      cylindrical algebraic decomposition with EX-INF-MANY relaxation for open predicates via QEPCAD-B


step_type: primitive_rule
library: prelude
docstring:
  (trust! orcl stamp): 
      Trusts oracle ORCL with STAMP. This strategy *must* only be used in proof rules.


step_type: primitive_rule
library: prelude
docstring:
  (name name expr): 
      Introduces an EXPR = NAME premise.  Useful for generalizing the goal, and
  replacing exprs with bound variables, so that the ground prover can be
  applied to them.  In addition to the new antecedent, a definition is generated
  for the NAME, which may subsequently be expanded or rewritten.
  See also NAME-REPLACE


step_type: primitive_rule
library: prelude
docstring:
  (lemma name &optional (subst)): 
      Adds lemma named NAME as the first antecedent formula
   after applying the substitutions in SUBST to it.  Example:
    (LEMMA "assoc" ("x" 1 "y" 2 "z" 3)).


step_type: primitive_rule
library: prelude
docstring:
  (replace fnum &optional ((fnums *) dir hide? actuals? dont-delete?)): 
      Rewrites the given formulas in FNUMS with the formula FNUM.  If FNUM is
  an antecedent equality, then it rewrites left-to-right if DIR is LR (the
  default), and right-to-left if DIR is RL.  If FNUM is not an antecedent
  equality, then any occurrence of the formula FNUM in FNUMS is replaced by
  TRUE if FNUM is an antecedent, FALSE for a succedent.  If HIDE? is T, then
  FNUM is hidden afterward.  When ACTUALS?  is T, the replacement is done
  within actuals of names in addition to the expression level replacements,
  including in types.  When the DONT-DELETE? flag is T, top-level sequent
  formulas are not deleted through being replaced by TRUE/FALSE.


step_type: primitive_rule
library: prelude
docstring:
  (ws1s-simp &optional
   ((fnums *) (examples? t) (automaton? nil) (traces? nil)
    (verbose? t))): 
      WS1S Decision Procedure.


step_type: primitive_rule
library: prelude
docstring:
  (yices &optional ((fnums *))): 
      Invokes Yices as an endgame SMT solver to prove that the conjunction
  of the negations of the selected formulas is unsatisfiable. 


step_type: primitive_rule
library: prelude
docstring:
  (simp-real-null &optional ((fnums *))): 
      extraction of simple real nullstellensatz refutation certificates from equational constraints


step_type: primitive_rule
library: prelude
docstring:
  (typepred! exprs &optional (all? implicit?)): 
      Extract subtype constraints for EXPRS and add as antecedents.
  ALL? flag when T also brings in nat (>= 0), integer_pred,
  rational_pred, real_pred type constraints.  IMPLICIT? when T means
  bring in subtype constraints that are implicit.  An imlpicit
  constraint is one that is implied by the terms of the sequent, e.g.,
  if the sequent contains the formula "1/(x*y) < 0", then
   (typepred! "x*y" :implicit? t) adds "x * y /= 0" as an antecedent.
  The reason TYPEPRED is not used for this is that keywords may not be used
  with &rest arguments.  Note that subtype constraints are also automatically
  recorded by the decision procedures.


step_type: primitive_rule
library: prelude
docstring:
  (delete &rest fnums): 
      Deletes a list of formulas that may have become irrelevant.
  The HIDE rule is a more conservative alternative, since hidden formulas
  may be revealed.
  See also HIDE, REVEAL


step_type: primitive_rule
library: prelude
docstring:
  (beta &optional ((fnums *) rewrite-flag (let-reduce? t))): 
      Beta-reduces chosen formulas. If REWRITE-FLAG is LR(RL), then
  left(right)-hand-side is left undisturbed for rewriting using
  REWRITE and REWRITE-LEMMA.  If LET-REDUCE? is t, then LET expressions
  are reduced.  Example reduction steps are:
   (LAMBDA x, y: x + y)(2, 3) to 2 + 3
   (LET x := 1, y := 2 in x + y) to 1 + 2
   b((# a:=1, b:= 2 #)) to 2
   PROJ_2(2, 3) to 3
   cons?(nil) to FALSE
   car(cons(2, nil)) to 2.


step_type: primitive_rule
library: prelude
docstring:
  (typepred &rest exprs): 
      Extract subtype constraints for EXPRS and add as antecedents.
   Note that subtype constraints are also automatically recorded by
  the decision procedures. E.g.,
   (typepred "abs(c)"): Adds abs(c) > 0 to the antecedent.


step_type: primitive_rule
library: prelude
docstring:
  (auto-rewrite &rest names): 
      Installs automatic rewrite rules given in the NAMES list.  The rewrites
  are applied by the ASSERT and DO-REWRITE commands.  Each entry in the list
  NAMES is either an antecedent formula number or names a definition,
  assumption or formula.  The complete syntax is
    rewrite-name-or-fnum ::= fnum | rewrite-name

    fnum ::= ['-'] number ['!' ['!']]

    rewrite-name ::= name ['!' ['!']] [':' {type-expr|formula-name}]

  With no exclamation points, the rewrite is lazy, with one it is eager, and
  with two it is a macro.  Rewrites only take effect if relevant conditions
  and TCCs simplify to T.  For lazy rewrites, if there is an IF or CASES at
  the outermost part of the righthand-side, then it is treated as a
  condition.  When a function definition is curried, lazy and eager rewrites
  only match when the most applied form of the function is used, whereas
  macros always match any occurrence of the function.  For example, in
  (AUTO-REWRITE A B! 1! C -3!! D!!), A and C are lazy rewrites, B and
  formula number 1 are eager rewrites, and formula number -3 and D are macro
  rewrites.

  Eager and macro rewrites may also be indicated by the level of
  parenthesization - the above example is equivalent to
  (AUTO-REWRITE A (B 1) C ((-3 D))).  This older form is deprecated, but
  still supported for backward compatibility.
    E.g.,
    (auto-rewrite "assoc" "delete!" "union!" -3 -4! -5!)
    (auto-rewrite :names ("assoc" "delete!" "union!")). 


step_type: primitive_rule
library: prelude
docstring:
  (label label fnums &optional (push?)): 
      Labels a collection of formulas given by FNUMS by the
  string  LABEL.  If PUSH? is T, then the new label is added to any existing
  ones.  Otherwise, the new label replaces all existing ones.


step_type: primitive_rule
library: prelude
docstring:
  (undo &optional ((to 1))): 
      Undoes proof back n steps or to label or command name.
  The last undo may be undone if no commands have been
  used since the undo by (undo undo)


step_type: primitive_rule
library: prelude
docstring:
  (simplify &optional
            ((fnums *) record? rewrite? rewrite-flag flush? linear?
             cases-rewrite? (type-constraints? t) ignore-prover-output?
             let-reduce? quant-simp? implicit-typepreds?
             ignore-typepreds?)): 
      Uses the decision procedures to to simplify the formulas in
  FNUM and record them for further simplification.  The proof steps
  ASSERT, RECORD, SIMPLIFY, DO-REWRITE are instances of this primitive
  rule and should always be preferred.  The arguments have the following
  effect:
   RECORD?: If T, the formula is simplified and recorded as true or false
            by the decision procedures to be used for further
            simplification.  The formula is only recorded if it does not
            contain top-level Boolean connectives or conditionals.
   REWRITE?: If T, the installed rewrite rules are applied but no
            simplification is done except on the right-hand side.
            Full-blown simplify is used to simplify the right-hand side
            instance of the rewrite, the TCCs, and the conditions of
            conditional rewrite rules.
   If  REWRITE? is NIL the formula is simplified so that
      1. arithmetic expressions are put into a sum-of-products form.
      2. lambda, tuple, record, datatype, and update redexes are reduced.
      3. decision procedures are used to determine whether boolean
         expressions are TRUE/FALSE in the context in which they appear.
      3. Boolean/conditional expressions are simplified to eliminate
         TRUE/FALSE.
   REWRITE-FLAG: If RL(LR) then only lhs(rhs) is simplified.
   FLUSH?: If T, then the current asserted facts are deleted for
           efficiency.
   LINEAR?: Ignored.
   CASES-REWRITE: If T, then the selections and else parts of a
           CASES expression are simplified, otherwise, they are only
           simplified when simplification selects a case.
   TYPE-CONSTRAINTS?: IF T (the default) asserts subtype constraints of each
           sub-expression to the ground prover data-structures.
   IGNORE-PROVER-OUTPUT?: The ground prover returns a disjunction of literals
           equivalent to the asserted formula.  At the end of a SIMPLIFY with
           RECORD? set to T, PVS tries to show that the conjunction of these
           disjunctions is unsatisfiable using the ground prover.  This step
           can sometimes be expensive and fruitless, and setting
           IGNORE-PROVER-OUTPUT? to T, cases this step to be skipped.
   LET-REDUCE?: LET expressions are normally beta-reduced, unless LET-REDUCE?
            is NIL.
   QUANT-SIMP?: Carries out quantifier simplifications like reducing
           (EXISTS x: x = t AND P(x)) to P(t).
   IMPLICIT-TYPEPREDS?: If T asserts implicit subtype constraints of each
           sub-expression to the ground prover.  See TYPEPRED! for details.
   IGNORE-TYPEPREDS?: If T typepreds are not processed to see if the proof is
           finished.  In some cases (especially for large arithmetic formulas)
           processing the typepreds can take a very long time, and they only
           occasionally finish a proof.  Note that this affects the completeness
           of simplify, not soundness.  Default is to process typepreds.


step_type: primitive_rule
library: prelude
docstring:
  (instantiate fnum terms &optional (copy?)): 
      Instantiates the top quantifier in the formula FNUM with the TERMS.
  FNUM can also be *, +, or -, in which case the first suitably quantified
  formula is chosen for instantiation.  Each term in TERMS is typechecked
  against the type of the variable it instantiates.  A copy of the
  quantified formula is hidden by default and can be reintroduced by REVEAL.
  If COPY? is T, then the copy is not hidden.  TERMS is a list of
  expressions or underscores, corresponding to the bound variables of the
  specified formula.  Underscores indicate that the corresponding variables
  are to be left uninstantiated.
   Example: (instantiate 2 ("x" _ "2"))
     Instantiates the first and third bound variables in formula number 2.
   See also INST, INST?


step_type: primitive_rule
library: prelude
docstring:
  (case &rest formulas): 
      Splits according to the truth or falsity of the formulas in FORMULAS.
   (CASE a b c) on a sequent A |- B generates subgoals:
   a, b, c, A  |- B;
     a, b, A |- c, B;
     a, A |- b, B;
     A |- a, B.
   See also CASE-REPLACE, CASE*


step_type: primitive_rule
library: prelude
docstring:
  (apply strategy &optional (comment save? time? timeout)): 
      Applies STRATEGY as if it were a rule, and prints COMMENT string.
  If SAVE? is T, then the APPLY step is saved even if the strategy
  does nothing, e.g., (SKIP), which is useful for setting values of
  globals, e.g., (APPLY (LISP (setq *xx* ...)) "recording value of *xx*" T).
  If TIME? is t, prints the time used to apply the strategy.  TIMEOUT is
  the number of seconds for the strategy to complete, if it does not complete
  by then, it is treated as a (SKIP).  If it does complete, it is saved with
  the TIMEOUT removed.
  This is the basic way of converting a glass-box strategy into an
  atomic step so that internal execution of the strategy is hidden
  and only the resulting subgoals are returned.  E.g.,
   (apply (then (skosimp*)(flatten)(inst?))
        "Skolemizing, flattening, and instantiating").


step_type: primitive_rule
library: prelude
docstring:
  (extensionality type): 
      Adds extensionality axiom for given TYPE as a sequent formula.
   Example axioms for given type include:
    [nat->nat]: (FORALL (f, g: [nat->nat]): (FORALL (i:nat): f(i) = g(i))
                   IMPLIES f = g);
    [nat, nat]: (FORALL (r, s: [nat, nat]):
                  PROJ_1(r) = PROJ_1(s) AND PROJ_2(r) = PROJ_2(s)
                  IMPLIES r = s);
    [# a: nat, b: nat #]: (FORALL (r, s: [# a: nat, b: nat #]):
                             a(r) = a(s) AND b(r) = b(s) IMPLIES r = s)
    (cons?): (FORALL (l, m: (cons?)): car(l) = car(m) AND cdr(l) = cdr(m)
                                      IMPLIES l = m).
   See also ETA,  APPLY-EXTENSIONALITY and REPLACE-EXTENSIONALITY.


step_type: primitive_rule
library: prelude
docstring:
  (just-install-proof proof): 
      Installs an edited PROOF without actually checking it,
  declares the subgoal as finished, but then marks the proof as
  unfinished.


step_type: primitive_rule
library: prelude
docstring:
  (same-name name1 name2 &optional (type)): 
      Assume given constants are identical if their actuals are equal.
  This is used to indicate that names are equal even if their actuals are
  not syntactically equal.  TYPE can be given to disambiguate NAME1 and
  NAME2.
  Example: (same-name "bvec0[i + j]" "bvec0[j + i]").


step_type: primitive_rule
library: prelude
docstring:
  (postpone &optional ((print? t))): 
      Places current goal on parent's list of pending (unproved)
  subgoals, moving to the next one.  Repeated POSTPONEs cycle through the
  pending subgoals.  When PRINT? is nil, commentary is suppressed.


step_type: primitive_rule
library: prelude
docstring:
  (rcr-ineqs &optional ((fnums *))): 
      reduction of terms in inequalities to canonical rep's in residue class ring induced by equational constraints


step_type: primitive_rule
library: prelude
docstring:
  (univ-sturm-ineqs &optional ((fnums *))): 
      sturm sequence sign-change analysis for univariate open-interval systems


step_type: primitive_rule
library: prelude
docstring:
  (split &optional ((fnum *) depth)): 
      Conjunctively splits formula FNUM.  If FNUM is -, + or *, then
  the first conjunctive sequent formula is chosen from the antecedent,
  succedent, or the entire sequent.  Splitting eliminates any
  top-level conjunction, i.e., positive AND, IFF, or IF-THEN-ELSE, and
  negative OR, IMPLIES, or IF-THEN-ELSE.


step_type: primitive_rule
library: prelude
docstring:
  (reveal &rest fnums): 
      Moves the hidden formulas (hidden by HIDE or quantifier
  instantiation) in FNUMS back to the sequent.  Use the Emacs command
  M-x show-hidden-formulas to see the hidden formulas.


step_type: primitive_rule
library: prelude
docstring:
  (lift-if &optional (fnums (updates? t))): 
      Lifts IF occurrences to the top of chosen formulas.
  CASES, COND, and WITH applications, are treated as IF occurrences.
  The UPDATE? flag controls whether update-applications are converted
  into IF-THEN-ELSE form and lifted.  IF-lifting is the transformation
  that takes f(IF A THEN b ELSE c ENDIF) to
  (IF A THEN f(b) ELSE f(c) ENDIF).  LIFT-IF only lifts the
  leftmost-innermost contiguous block of conditionals  so it might
  have to be applied repeatedly to lift all the conditionals. E.g.,
   (lift-if) : applies IF-lifting to every sequent formula.
   (lift-if - :updates? nil) : lifts only antecedent IF that are not
    applications of updates.


step_type: primitive_rule
library: prelude
docstring:
  (iff &rest fnums): 
      Converts top level Boolean equality into an IFF.
  Otherwise, propositional simplification (other than by BDDSIMP)
  is not applied to such equalities.


step_type: primitive_rule
library: prelude
docstring:
  (int-dom-zpb &optional ((fnums *))): 
      integral domain zero product branching for explicit zero indeterminate products


step_type: primitive_rule
library: prelude
docstring:
  (rcr-svars &optional ((fnums *))): 
      scalar-valued indeterminate fertilization via bounded indeterminate power sequence reduction over residue class ring induced by equational constraints


step_type: defined_rule
library: prelude
docstring:
  (inst*/$ fnum &rest terms-lists) :
      Instantiates a given formula, creating as many copies of the formula FNUM as
     needed to use the TERMS-LISTS.  The original formula is hidden afterward, copy
     it before this command if desired.  If there is an error in any of the instances,
     the entire command fails.
     Examples:
      (inst* -1 (1 2) (3 4) (5 6) (7 8) (9 10))
        Assuming FNUM -1 is a universal formula that expects two numbers, this would
        create five instances of that formula.
      (inst* -1 (1 2) (3 4) (5) (7 8) (9 10))
        Gives the error "No quantified formula matching given number of terms."
        and the sequent is unchanged.
      


step_type: defined_rule
library: prelude
docstring:
  (skosimp*/$ &optional preds? dont-simplify?) :
      Repeatedly Skolemizes (with typepreds on skolem constants when PREDS?
  is T) and disjunctively simplifies.


step_type: defined_rule
library: prelude
docstring:
  (cancel-terms/$ &optional (fnums *) (end l) (sign nil) (try-just nil)) :
      [Manip] Cancel left-most or right-most terms, which need not be identical,
  from both sides of relational formulas involving arithmetic expressions.
  Introduces a case split to prove the terms are equal.  END may be used to
  select L or R end of a chain of associative terms for cancellation.  The
  `-' operator is considered equivalent to `+' for this purpose.  On the
  other hand, only the outer-most application in a chain of `/'-separated
  terms is recognized.  SIGN may be used to indicate polarity as in cancel.


step_type: defined_rule
library: prelude
docstring:
  (auto-rewrite-theories/$ &rest theories) :
      Iterated version of auto-rewrite-theory.  Each entry in
  THEORIES must either be a theory name or a list in the form of
  the arguments to AUTO-REWRITE-THEORY. 
  E.g.: (auto-rewrite-theories "real_props" ("sets" :defs explicit)).


step_type: defined_rule
library: prelude
docstring:
  (case-if*/$ cases-list) :
      Iterative version that applies case-if successively to each element of the
  conditions given in cases-list.


step_type: defined_rule
library: prelude
docstring:
  (sub-formulas/$ fnum1 fnum2 &optional (hide? t) label
   (tcc-step (extra-tcc-step))) :
      [Field] Subtracts relational formulas FNUM1 and FNUM2. If HIDE? is t,
  the original formulas are hidden.  The new formula is labeled as LABEL,
  if specified. TCCs generated during the execution of the command are discharged
  with the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (reduce-with-ext/$ &optional (if-match t) (updates? t) polarity?
   (instantiator inst?) (let-reduce? t) quant-simp? no-replace?
   implicit-typepreds? cases-rewrite? ignore-typepreds?) :
      Core of GRIND-WITH-EXT (ASSERT, BDDSIMP, INST?, SKOLEM-TYPEPRED, FLATTEN,
  LIFT-IF, i.e., BASH then REPLACE*), like REDUCE, but includes
  APPLY-EXTENSIONALITY.  See reduce for an explanation of the arguments.


step_type: defined_rule
library: prelude
docstring:
  (let-name-replace/$ &optional (fnum *) hide? (where top)) :
      Replaces the LET variables by names in LET expressions in FNUM that do
  not occur in a binding.  It attempts to use the names given by the LET, then
  appends "_1", etc. until a new name is generated.  If HIDE? is t, the
  names are hidden.  WHERE may be one of:
    top - for only a top-level LET expession,
    first - for the first LET expression not inside a binding
    all - for all LET expressions not inside a binding.
  See name-replace.


step_type: defined_rule
library: prelude
docstring:
  (skoletin*/$ &optional (fnum *) postfix hide?
   (tcc-step (extra-tcc-step)) n old?) :
      [Extrategies] Iterates N times skoletin (or until it does nothing if N is nil) in FNUM.

  CAVEAT: The order in which formulas are introduced by skoletin in version 6.0 is different
  from previous versions. The option OLD? reproduces the old order.


step_type: defined_rule
library: prelude
docstring:
  (swap/$ lhs operator rhs &optional (infix? t)) :
      [Manip] Try commutatively swapping two terms and replacing.  Set INFIX?
  to nil for prefix applications.  Commutativity proof for operator will
  be tried automatically.


step_type: defined_rule
library: prelude
docstring:
  (match/$ &rest spec-items) :
      [Manip] Try matching syntax patterns against formulas in the sequent.
  Each pattern can be of the form <patt> or ([fnums] <patt> [occur]), where
  <patt> can be either a symbol or a string "patt".  Successful matches
  can bind subexpressions to pattern variables (identifiers having a leading
  '%').  Use these variables to instantiate template expressions and affect
  the sequent.  Actions are specified using a symbol, where the choices
  include 'rep' (replace first matched instance with template), 'case' (use
  case splitting on expressions), a binary relation symbol (split on case
  <instance> <op> <template>), 'step' (invoke template as a proof step or
  strategy), and a symbol <rule> (invoke <rule> on templates).  Proof steps
  for all cases can be provided. See the Manip user's guide for a full
  description of all features.


step_type: defined_rule
library: prelude
docstring:
  (name-label/$ name expr &optional label (fnums *) (dir lr) hide?
   (tcc-step (extra-tcc-step)) tcc-label) :
      [Extrategies] Adds formula EXPR=NAME, where NAME is a new name, as
  a hypothesis and replaces EXPR by NAME in FNUMS. The added formula is
  labeled LABEL:, by default LABEL is set to NAME. DIR indicates the
  direction of the name definition, e.g., EXPR=NAME, if DIR is lr, or
  NAME=EXPR, if DIR is rl. The added formula is hidden when HIDE? is
  t. If TCC-STEP is not null and EXPR yields TCCs, these TCCs are added
  as hypotheses to the main branch. If a TCC-LABEL is provided, these
  hypotheses are labeled TCC-LABEL. Otherwise, these hypotheses are
  labeled LABEL-TCC: and hidden from the sequent.  In branches other
  than the main branch, the strategy tries to discharge these TCCs with
  the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (auto-rewrite-explicit/$ &optional always?) :
      Installs all the explicit (non-recursive) definitions in the original
  statement.  If always? is T, then it uses auto-rewrite! else auto-rewrite.


step_type: defined_rule
library: prelude
docstring:
  (field/$ &optional (fnum (+ -)) theories cancel?
   (tcc-step (extra-tcc-step))) :
      [Field] Removes divisions and apply simplification heuristics to the relational
  formula on real numbers FNUM. It autorewrites with THEORIES when possible. If CANCEL?
  is t, then it tries to cancel common terms once the expression is free of divisions.
  TCCs generated during the execution of the command are discharged with the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (claim/$ cond &optional (try-just nil) &rest expr-specs) :
      [Manip] Generalized case step that uses a parameterized condition
  applied to multiple terms (two-way split only).  COND can be regarded
  as a template expression with %1, %2, ..., serving as implicit template
  variables to represent terms to be substituted in the parameterized
  condition expression.  The justification step can be tried by setting
  TRY-JUST to a proof step.  Example: (claim "%1 < %2" t "x" "y+z")
  case splits on `x < y+z' and tries to prove the relation using grind.


step_type: defined_rule
library: prelude
docstring:
  (rahd/$ &optional (fnums *) (simplify-division? t) verbosity
   search-model print-model) :
      Real Algebra in High Dimensions


step_type: defined_rule
library: prelude
docstring:
  (grind-with-ext/$ &optional (defs !) theories rewrites exclude
   (if-match t) (updates? t) polarity? (instantiator inst?)
   (let-reduce? t) cases-rewrite? quant-simp? no-replace?
   implicit-typepreds? ignore-typepreds?) :
      Like GRIND, but calls REDUCE-EXT, which also uses APPLY-EXTENSIONALITY.  See GRIND for an explanation of the arguments.


step_type: defined_rule
library: prelude
docstring:
  (case-if/$ cases) :
      Creates a case split according to a given structure so that
     (cases '(A (B (C nil nil) (D nil nil)) (E nil nil))) yields
     sequents with A, B, C |-...,
                A, -B, D |- ...,
                -A, E  |- ...


step_type: defined_rule
library: prelude
docstring:
  (grind-with-lemmas/$ &optional (lazy-match? t) (lazy-inst? nil)
   (if-match t) (polarity? t) (defs !) rewrites theories exclude
   (updates? t) (let-reduce? t) &rest lemmas) :
      Does a combination of (lemma) and (grind); if lazy-match? is t,
       postpones instantiations to follow a first round of simplification.


step_type: defined_rule
library: prelude
docstring:
  (flip-ineq/$ fnums &optional (hide? t)) :
      [Manip] Negate the inequality formulas and move the resulting formulas
  by exchanging between antecedents and consequents.  Conjunctions and
  disjunctions of inequalities are also accepted, causing each conjunct
  or disjunct in the form of an inequality to be negated and moved.
  If HIDE? is set to NIL, the original formulas are left intact.


step_type: defined_rule
library: prelude
docstring:
  (abstract/$ cstate astate amap &optional theories rewrites exclude
   (strategy '(assert)) feasible verbose?) :
      Constructs an abstraction of the given sequent by mapping the
  concrete state CSTATE to the abstract state ASTATE based on the abstraction
  map AMAP.  CSTATE and ASTATE must be record types.  The field types
  of ASTATE must be either booleans or scalars (for the time being).
  THEORIES, REWRITES, and EXCLUDE are as in install-rewrites.
  STRATEGY (defaults to ASSERT) is the proof strategy used to discharge abstraction proof obligations.  FEASIBLE is a predicate over ASTATE that identifies
  the concretely feasible abstract states.  VERBOSE? when T prints out the
  abstraction proof obligations. 


step_type: defined_rule
library: prelude
docstring:
  (grind-reals/$ &optional defs theories rewrites exclude (if-match t)
   (updates? t) polarity? (instantiator inst?) (let-reduce? t)
   dontdistrib protect) :
      [Field] Apply grind with "real_props". This strategy supports the same
  options as grind. Additionally, grind-reals blocks distribution laws in main level
  expressions in the list of formulas DONTDISTRIB and protects formulas in PROTECT.


step_type: defined_rule
library: prelude
docstring:
  (op-ident/$ fnum &optional (side l) (operation *1)) :
      [Manip] Apply the operator identity given by OPERATION to rewrite
  the expression found on SIDE (L or R) of relational formula FNUM.
  Performs the following operations using these designated symbols:
     z+      +z      -z      1*      *1      /1
     0 + x   x + 0   x - 0   1 * x   x * 1   x / 1


step_type: defined_rule
library: prelude
docstring:
  (grind/$ &optional (defs !) theories rewrites exclude (if-match t)
   (updates? t) polarity? (instantiator inst?) (let-reduce? t)
   cases-rewrite? quant-simp? no-replace? implicit-typepreds?
   ignore-typepreds?) :
      A super-duper strategy.  Does auto-rewrite-defs/theories,
  auto-rewrite then applies skolem!, inst?, lift-if, bddsimp, and
  assert, until nothing works. Here
   DEFS is either
     NIL:  defns in the statement are not installed as auto-rewrites
     T: All defns are installed as conditional rewrites
     !: All defns are installed, but with explicit (non-recursive) defns as
        unconditional rewrites
     explicit: Only explicit defns installed as conditional rewrites
     explicit!: Only explicit defns installed as unconditional rewrites.
   THEORIES is a list of theories to be rewritten in the format expected 
            by AUTO-REWRITE-THEORY,
   REWRITES is a list of rewrite rules in AUTO-REWRITE format,
   EXCLUDE is a list of rewrite rules to be disabled (by STOP-REWRITE),
   IF-MATCH is either NIL (no instantiation), T (yes instantiation),
       ALL (all instances) or BEST (best instance) depending on which version
       of INST? is required.
   If the UPDATES? option is NIL, update applications are not if-lifted.
   POLARITY? if T, a positively occurring template is only matched against
       negatively occuring subexpressions, and less-than term occurrences
       are matched against greater-than occurrences.
  The INSTANTIATOR argument can be used to specify use of an alternative
  instantiation mechanism.  This defaults to the (INST?) strategy.


step_type: defined_rule
library: prelude
docstring:
  (forward-chain*/$ &rest lemmas-or-fnums) :
      Given a list of forward chain lemmas or formula numbers, apply forward-chaining
  repeatedly until no more changes occur.  The rules are applied in the order
  given, but if any succeeds, it starts over from the beginning.


step_type: defined_rule
library: prelude
docstring:
  (distrib/$ fnums &optional (side *) (term-nums *)) :
      [Manip] Distribute multiplication operators over factors having the form
  of additive subexpressions.  Apply this action to the top-level additive
  terms given by TERM-NUMS for the expression found on SIDE (L or R) of each
  relational formula in FNUMS.


step_type: defined_rule
library: prelude
docstring:
  (redlet/$ &optional (fnum (+ -)) name (nth 1)
   (tcc-step (extra-tcc-step))) :
      [Extrategies] Reduces the NTH occurrence of NAME (left-right, depth-first) in a let-in expression
  in FNUM. If NAME is nil, the NTH name is reduced instead. TCCs generated during the execution of the
  command are discharged with the proof command TCC-STEP.

  NOTE: This command works better when all let-in variables are explicitly typed as in LET x:posreal = 2
  IN 1/x.


step_type: defined_rule
library: prelude
docstring:
  (measure-induct-and-simplify/$ measure vars &optional (fnum 1) order
   expand (defs t) (if-match best) theories rewrites exclude
   (instantiator inst?) skolem-typepreds?) :
      Invokes MEASURE-INDUCT+ on MEASURE, VARS, FNUM, and ORDER, and then
  repeatedly expands definition(s) taken from EXPAND in the succedent,
  skolemizes, simplifies using rewrite rules taken from THEORIES and
  REWRITES, instantiates, and lifts IFs.

   ORDER is a well-founded relation;
         if not specified defaults to < on nats or ordinals
   EXPAND is either a single definition name, or a list of names
   DEFS is either
     NIL:  defns in the statement are not installed as auto-rewrites
     T: All defns are installed as conditional rewrites
     !: All defns are installed, but with explicit (non-recursive) defns as
        unconditional rewrites
     explicit: Only explicit defns installed as conditional rewrites
     explicit!: Only explicit defns installed as unconditional rewrites.
   IF-MATCH is either all, best, or T, as in INST?,
               or NIL meaning don't use INST?.
   THEORIES is a list of theories to be rewritten in format expected by
            AUTO-REWRITE-THEORY,
   REWRITES is a list of rewrite rules in AUTO-REWRITE format.
   EXCLUDE is a list of rewrite rules on which rewriting must be stopped.
   INSTANTIATOR argument can be used to specify use of an alternative
         instantiation mechanism.  This defaults to the (INST?) strategy.
   SKOLEM-TYPEPREDS? when T indicates that typepreds should be generated for
         the introduced skolem constants.

  Example:
      (measure-induct-and-simplify "size(x)" ("x") :expand "unfold" :if-match all).


step_type: defined_rule
library: prelude
docstring:
  (show-subst/$ command &rest expr-specs) :
      [Manip] Tests command formation with substitutions extracted from
  extended expression specifications.  Emits messages to show what
  substitutions occur, but doesn't invoke any commands.  Use the idiom
      (show-subst ($*) <ext expr 1> ... <ext expr n>)
  to see the evaluation of extended expressions against the current sequent.


step_type: defined_rule
library: prelude
docstring:
  (case*/$ &rest formulas) :
      Complete version of CASE command where all the formulas are case split
  along every branch.


step_type: defined_rule
library: prelude
docstring:
  (both-sides/$ op term &optional (fnum 1)) :
      Applies OP to TERM uniformly over a conjunction of inequalities.
  Example: (both-sides "*" "2") multiplies both sides of the target
           inequalities by 2


step_type: defined_rule
library: prelude
docstring:
  (skeep*/$ &optional (fnum '*) preds? postfix n) :
      [Extrategies] Iterates N times skeep (or until it does nothing if N is nil) in a universally 
  quantified formula in FNUM. If POSTFIX is provided, it is appended to the names of the bounded 
  variables. Names that clash with other names in the current sequent are replaced by fresh 
  names. Type predicates are introduced as hypothesis when PREDS? is t.


step_type: defined_rule
library: prelude
docstring:
  (show-parens/$ &optional (fnums *)) :
      [Manip] Show how infix operators and operands are associated by displaying
  formulas with full parenthesization.  This strategy overlaps the built-in
  feature of PVS (since 3.0), M-x pvs-set-proof-parens (also available from
  the PVS menu).


step_type: defined_rule
library: prelude
docstring:
  (induct-and-rewrite/$ var &optional (fnum 1) &rest rewrites) :
      Performs induction according to the type of VAR using FNUM
  to formulate induction predicate, and then simplifies using the given 
  REWRITES.
   (induct-and-rewrite "x" 1 "append" "reverse"): Inducts on x in formula 1,
     then simplifies the base and induction using the definitions append and
     reverse. 


step_type: defined_rule
library: prelude
docstring:
  (metit/$ &optional (fnums 1) (timeout 60) options arch about?) :
      Calls MetiTarski on first order formulas FNUMS. TIMEOUT is a processor time limit 
  (in seconds). Additional options to MetiTarski can be provided through OPTIONS. 
  Executables of MetiTarski and z3 are pre-intstalled in the NASA PVS Library.* 
  By default, the strategy tries to use the versions of MetiTarski and z3 installed 
  in the system. If the executables are not in the path, the pre-installed versions
  are tried. The option ARCH forces the strategy to use the pre-installed version for 
  a given architecture. If ABOUT? is set to t, the strategy prints information about
  MetiTarski and z3 and then exits.

  MetiTarski requires an external algebraic decision method (EADM). The default EADM
  is z3. However, other EADM are also supported, e.g., QEP and Mathematica. See 
  MetiTarski's documentation for information about using a different EADM.

  If current theory imports MetiTarski@Disable, metit does nothing.

  * The files METIT-LICENSE.txt and Z3-LICENSE.txt in nasalib/MetiTarski/dist
    contains MetiTarski's and z3's license of use, respectively.


step_type: defined_rule
library: prelude
docstring:
  (group/$ term1 operator term2 term3 &optional (side l) (infix? t)) :
      [Manip] Try associatively regrouping three terms toward SIDE (L or R)
  and replacing.  Set INFIX? to nil for prefix applications.  Associativity
  proof for operator will be tried automatically.


step_type: defined_rule
library: prelude
docstring:
  (generalize/$ term var &optional type (fnums *) (subterms-only? t)) :
      Generalizes TERM in FNUMS by VAR of type TYPE.  By default, only the
  subterm occurrences of TERM will be generalized and not those occurrences
  in types or actuals.  If the command is invoked with the SUBTERMS-ONLY? flag
  set to the NIL, then every occurrence of TERM will be generalized.  This
  might go too far so if a more delicate generalization of selected occurrences
  is needed, the best option is to use CASE.


step_type: defined_rule
library: prelude
docstring:
  (group!/$ expr-loc &optional (side l)) :
      [Manip] Try associatively regrouping the three subexpressions of the
  function applications found at EXPR-LOC toward SIDE (L or R).  Associativity
  proof for operator will be tried automatically.


step_type: defined_rule
library: prelude
docstring:
  (mult-eq/$ rel-fnum eq-fnum &optional (sign +)) :
      [Manip] Given two formulas, one a relation `a R b', and the other an
  antecedent equality `x = y', introduce a new formula relating the products,
  a * x R b * y.  If R is an inequality, the SIGN argument can be set to
  one of the symbols in {+, -, 0+, 0-} to indicate the polarity of x and y.
  A SIGN of `*' is not supported (yet).  The relational formula may appear
  on either side of the sequent, but the equality must be an antecedent.


step_type: defined_rule
library: prelude
docstring:
  (record/$ &optional (fnums *) rewrite-flag flush? linear?
   (type-constraints? t) ignore-prover-output?) :
      Uses decision procedures to simplify and record the formulas
  in FNUMS for further simplification.   Variant of SIMPLIFY with RECORD?
  flag set to T and REWRITE? flags set to NIL. If REWRITE-FLAG is
  RL(LR) then only lhs(rhs) is simplified.  If FLUSH? is T then the
  current asserted facts are deleted for efficiency.  LINEAR? is ignored.
  Example:
   (record - :flush? T): flushes database and records antecedent formulas.


step_type: defined_rule
library: prelude
docstring:
  (tccs-step step &optional label hide?):
      [Extrategies] If STEP generates subgoals, e.g., TCCs, these subgoals are added as hypotheses to the
  first subgoal. Added hypotheses are labeled LABEL(s), if LABEL is not nil. They are hidden when
  HIDE? is t.


step_type: defined_rule
library: prelude
docstring:
  (apply-eta/$ term &optional type) :
      Instantiates eta axiom scheme for type TYPE or type of TERM with TERM
  See also ETA


step_type: defined_rule
library: prelude
docstring:
  (cancel-by/$ fnum expr &optional (tcc-step (extra-tcc-step))
   (auto-step (assert))) :
      [Field] Cancels the common expression EXPR in the relational formula FNUM.
  TCCs generated during the execution of the command are discharged with the 
  proof command TCC-STEP. At the end, the strategy tries to discharge the 
  current branch using the proof command AUTO-STEP.


step_type: defined_rule
library: prelude
docstring:
  (real-props/$ &optional (fnums *) theories simple? (let-reduce? t)
   (distrib? t)) :
      [Field] Autorewrites with "real_props" and THEORIES in FNUMS. If SIMPLE? is t,
  only basic rewrite rules are applied. If LET-REDUCE? is nil, let-in expressions will
  not be reduced. If DISTRIB? is nil, distribution laws will not be applied.


step_type: defined_rule
library: prelude
docstring:
  (auto-rewrite-defs/$ &optional explicit? always? exclude-theories) :
      Installs all the definitions used directly or indirectly in the
  original statement as auto-rewrite rules.  If the explicit? flag is T, the
  recursive definitions are not installed and only the explicit ones are.
  If always? is !!, it uses auto-rewrite!!, and if it 
  is T, then it uses auto-rewrite! on explicit definitions,
  else auto-rewrite.


step_type: defined_rule
library: prelude
docstring:
  (isolate-replace/$ fnum side term-num &optional (targets *)) :
      [Manip] Isolate the term TERM-NUM on SIDE (L or R) of relational formula FNUM,
  then replace and hide it.  Use TARGETS to restrict scope of replacement.


step_type: defined_rule
library: prelude
docstring:
  (auto-rewrite!!/$ &rest names) :
      Similar to auto-rewrite! except that explicit (non-recursive)
  definitions are always expanded even when all the arguments
  do not occur in the expression.   Examples:
   (auto-rewrite!! "compose"):  Installs the rewrite so that compose(f, g)
    is expanded.  


step_type: defined_rule
library: prelude
docstring:
  (skodef/$ &optional (fnum (+ -)) name var postfix hide?
   (tcc-step (extra-tcc-step))) :
      [Extrategies] Given a antecedent formula FNUM of the form
     FORALL(..,NAME:<type>,..) : NAME=<expr> AND ... IMPLIES ...
  or a consequent formula FNUM of the form
     EXISTS (..,NAME:<type>,..) : NAME=<expr> AND ...,
  this strategy introduces a name definition <var>=expr as hypothesis and
  instantiates NAME in FNUM with <var>. By default, <var> is NAME, with
  a POSTFIX if provided. An explicit name can be provided using the option VAR.
  Names that clash with other names in the current sequent are replaced by
  fresh names. 

  Name definitions are hidden when HIDE? is t; they can be recalled at any
  time with the command (reveal "<name>:"), where <name> is the name
  introduced by the strategy. TCCs generated during the execution of the command
  are discharged with the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (for-each/$ command &rest expr-specs) :
      [Manip] Repeatedly invoke a rule or strategy by instantiating COMMAND
  with substitutions extracted from the extended expression specifications
  EXPR-SPECS.  For each expression specified, instantiate and invoke
  COMMAND with a different binding for parameters %1, $1, etc.


step_type: defined_rule
library: prelude
docstring:
  (generalize-skolem-constants/$ &optional (fnums *)) :
      Merges the formulas and universally generalizes the skolem constants
  in the given fnums.


step_type: defined_rule
library: prelude
docstring:
  (replace-eta/$ term &optional type keep?) :
      Instantiates eta axiom scheme for type TYPE or type of TERM with TERM
  See also ETA, APPLY-ETA.


step_type: defined_rule
library: prelude
docstring:
  (all-typepreds/$ &optional (fnums *)) :
      Provides useful typepreds for all subexpressions of specified FNUMS,
  meaning those that are not already dealt with by the ground prover.  Thus a
  typepred is deemed useful if it has an expandable definition or is
  propositional, since these will have been treated as uninterpreted in the
  ground prover until they are exposed.


step_type: defined_rule
library: prelude
docstring:
  (assert/$ &optional (fnums *) rewrite-flag flush? linear?
   cases-rewrite? (type-constraints? t) ignore-prover-output?
   (let-reduce? t) quant-simp? implicit-typepreds? ignore-typepreds?) :
      Simplifies/rewrites/records formulas in FNUMS using decision
  procedures.  Variant of SIMPLIFY with RECORD? and REWRITE? flags set
  to T. If REWRITE-FLAG is RL(LR) then only lhs(rhs) of equality
  is simplified. If FLUSH? is T then the current asserted facts are
  deleted for efficiency.  LINEAR? is currently ignored.
    If CASES-REWRITE? is T, then
  the selections and else parts of a CASES expression are simplified,
  otherwise, they are only simplified when simplification selects
  a case.  See also SIMPLIFY, RECORD, DO-REWRITE.
  Examples:
   (assert):  Simplifies, rewrites, and records all formulas.
   (assert -1 :rewrite-flag RL): Apply assert to formula -1 leaving
      RHS untouched if the formula is an equality.
   (assert :flush? T): Apply assert after flushing existing decision procedure
    database.


step_type: defined_rule
library: prelude
docstring:
  (tccs-formula* &optional (fnums *) label hide?):
      [Extrategies] Adds TCCs of formulas FNUMS as hypotheses to the current sequent. Added hypotheses
  are labeled LABEL(s), if LABEL is not nil. They are hidden when HIDE? is t.


step_type: defined_rule
library: prelude
docstring:
  (mult-cases/$ fnum &optional (abs? nil) (mult-op *1)) :
      [Manip] Generate case analyses for relational formulas containing
  products.  If FNUM has the form `x * y R 0' (or 0 R x * y), rewrite FNUM
  to two cases relating x and y to 0, as appropriate.  Some flattening and
  simplification will be attempted after rewriting.

  IF FNUM is a consequent inequality of the form a * b R c * d, generate
  sufficient conditions to establish the inequality by considering relations
  between a and c, and between b and d.  Likewise, for an antecedent inequality
  of this form, generate necessary conditions for FNUM.  There is likely to
  be some branching of the sequent.  The lemmas used contain instances of the
  abs function, which are normally expanded.  To suppress this expansion,
  set ABS? to T.

  IF FNUM is an inequality of the form 'a * b R c' or 'a R c * d', first
  transform FNUM into the form a * b R c * d by multiplying c or a by 1.
  MULT-OP may be set to *1 (1*) to multiply on the right (left).  Then
  proceed as in the previous case.


step_type: defined_rule
library: prelude
docstring:
  (name-replace/$ name expr &optional (hide? t)) :
      Uses NAME, REPLACE, and HIDE to abbreviate an expression with a
  newly chosen name


step_type: defined_rule
library: prelude
docstring:
  (auto-rewrite-theory/$ name &optional exclude defs always? tccs?) :
      Installs an entire theory (or only (explicit (non-recursive))
  definitions if DEFS is T(EXPLICIT)) as auto-rewrites.  In the case of a parametric
  theory, unless the DEFS flag is T or EXPLICIT, the actual parameters must be given.
  If ALWAYS? is T the rewrites are installed also so that any rewrite other than a
  recursive definition always takes effect (see auto-rewrite!).  (If ALWAYS? is set
  to !!, then the non-recursive definitions are always rewritten even when only a
  few of the curried arguments have been provided.)  Declarations named in EXCLUDE
  are not introduced and any current rewrite rules in the EXCLUDE list are disabled.
  By default, TCCs in the theory are excluded but they can be included when the TCC?
  flag is T.
    Examples:
      (auto-rewrite-theory "sets" :exclude ("union" "subset?")
  			          :defs explicit)
      (auto-rewrite-theory "lists[nat]" :always? T)
      (auto-rewrite-theory "connectives" :always? !!).


step_type: defined_rule
library: prelude
docstring:
  (rewrite/$ lemma-or-fnum &optional (fnums *) subst (target-fnums *)
   (dir lr) (order in) dont-delete?) :
      Rewrites using LEMMA-OR-FNUM (lemma name or fnum) of the form
  H IMPLIES L = R by finding match L' for L and replacing L' by R' with
  subgoal proof obligations for H'.  A lemma H IMPLIES L is treated as
  H IMPLIES L = TRUE, and also H can be empty.
  FNUMS constrains where to search for a match,
  SUBST takes a partial substitution and tries to find a match extending this,
  TARGET-FNUMS constrains where the rewriting occurs,
  DIR is left-to-right(LR) or right-to-left(RL),
  ORDER is inside-out(IN) or outside-in (OUT),
  DONT-DELETE? prevents antecedent/succedent formulas from being rewritten to
        true/false.


step_type: defined_rule
library: prelude
docstring:
  (auto-rewrite-theory-with-importings/$ name &optional exclude-theories
   importchain? exclude defs always? tccs?) :
      Installs rewrites in theory NAME and along with any theories
  imported by NAME.  The full import chain of theories can be
  installed by supplying the IMPORTCHAIN? flag as T.  Theories named
  in EXCLUDE-THEORIES are ignored.  The other arguments are similar
  to those of auto-rewrite-theory and apply uniformly to each of
  the theories to be installed.


step_type: defined_rule
library: prelude
docstring:
  (eval-expr/$ expr &optional safe? (auto? t) quiet?) :
      [PVSio] Adds the hypothesis expr=eval(EXPR) to the current goal, 
  where eval(EXPR) is the ground evaluation of EXPR. If SAFE? is t and EXPR
  generates TCCs, the expression is not evaluated. Otherwise, TCCs
  are added as subgoals and the expression is evaluated. If AUTO? is t,
  TCCs are ground evaluated. The strategy is sound in the sense that
  user-defined semantic attachments are not evaluated. However, if SAFE? is nil,
  the strategy may not terminate properly in the presence of unproven TCCs. When
  QUIET? is t, the strategy fails silently.


step_type: defined_rule
library: prelude
docstring:
  (name-induct-and-rewrite/$ var &optional (fnum 1) name &rest rewrites) :
      Performs induction according to the type of VAR or the induction scheme
  named NAME, using FNUM to formulate induction predicate, and then
  simplifies using given REWRITES. 


step_type: defined_rule
library: prelude
docstring:
  (y2simp/$ &optional (fnums *) nonlinear?) :
      Repeatedly skolemizes and flattens, and then applies the Yices2 SMT solver


step_type: defined_rule
library: prelude
docstring:
  (ws1s/$ &optional (fnums *) (examples? t) (automaton? nil)
   (traces? nil) (verbose? t) (defs !) theories rewrites exclude) :
      Decision procedure for Weak Second-order monadic logic of 1 Successor (WS1S)
     based on the Mona package developed at BRICS (http://www.brics.dk/~mona).
     Expands definitions in the formulas specified by FNUMS, applies Boolean
     abstraction for formulas outside the scope of WS1S, and constructs an
     automata that recognizes the language of interpretations of these formulas.

     The argument FNUMS restricts the focus of the strategy to the thereby specified sequent
     formulas. If EXAMPLES? is true, a witness and a counterexample are being displayed if
     these formulas turn out to be satisfiable but not valid. Setting the flag AUTOMATON?
     causes the strategy to display the constructed automaton, TRACES? displays a
     trace version of the witness. For a description of the remaining flags
     DEFS, THEORIES, REWRITES, and EXCLUDE see e.g. (help install-rewrites).

     The supported fragment includes boolean expressions, arithmetic on the
     natural numbers restricted to addition/subraction with/from a constant, and
     operations on finite sets over the naturals like union, intersection, set
     difference, addition and removal of a natural.  Predicates include arithmetic
     comparisons like <, <=, >, >=, equality, disequality, the subset relation,
     and membership in the form P(i). There is quantification over the booleans,
     the natural numbers, finite sets of naturals, and predicate subtypes of the
     aforementioned types built from formulas in the set just being described.
     Furthermore, this strategy tries to apply boolean abstraction for non-WS1S formulas,
     and natural numbers, and finite sets of natural numbers may also be described
     using the 'the' operator; e.g. ripple-carry addition may be defined as:
       +(P, Q: finite_set[nat]): finite_set[nat] = 
         the({R: finite_set[nat] | 
           EXISTS (C: finite_set[nat]): NOT(C(0)) AND
             FORALL (t: nat):
               (C(t + 1) = ((P(t) AND Q(t)) OR (P(t) AND C(t)) OR (Q(t) AND C(t)))) AND
                   (R(t) = P(t) = Q(t) = C(t))});


step_type: defined_rule
library: prelude
docstring:
  (track-rewrite/$ &rest names) :
      Tracks the named rewrite rules during rewriting when the rule fails to
  apply.  Behaves like a (SKIP), otherwise.


step_type: defined_rule
library: prelude
docstring:
  (for/$ n &rest steps) :
      [Extrategies] Iterates N times STEP1 ... STEPn, or until it does nothing if N is nil,
  along all the branches.


step_type: defined_rule
library: prelude
docstring:
  (replace-extensionality/$ f g &optional expected keep?) :
      Uses the extensionality axiom on the type of F (or with
  EXPECTED as the type when given) to replace F by G.  Retains the
  extensionality axiom scheme if KEEP? is T, and discards it otherwise.
  See also EXTENSIONALITY, APPLY-EXTENSIONALITY.


step_type: defined_rule
library: prelude
docstring:
  (model-check/$ &optional (dynamic-ordering? t) cases-rewrite? defs
   theories rewrites exclude irredundant?) :
      Rewrites temporal operators into mu/nu expressions, and
  simplifies using mu-calculus checker.  If DYNAMIC-ORDERING? is T,
  the BDD package uses dynamic ordering to minimize the BDD size.
  If CASES-REWRITE is NIL, this turns off rewriting within the
  selections of unsimplified CASES expressions.  The optional arguments
  DEFS, THEORIES, REWRITES, and EXCLUDE are as in INSTALL-REWRITES.


step_type: defined_rule
library: prelude
docstring:
  (induct-and-simplify/$ var &optional (fnum 1) name (defs t)
   (if-match best) theories rewrites exclude (instantiator inst?)) :
      Inducts on VAR in formula number FNUM using the induction
  scheme named NAME, then simplifies using rewrite rules taken
  from THEORIES and REWRITES.
   DEFS is either
     NIL:  defns in the statement are not installed as auto-rewrites
     T: All defns are installed as conditional rewrites
     !: All defns are installed, but with explicit (non-recursive) defns as
        unconditional rewrites
     explicit: Only explicit defns installed as conditional rewrites
     explicit!: Only explicit defns installed as unconditional rewrites.
   IF-MATCH is either all, best, or T, as in INST?,
               or NIL meaning don't use INST?.
   THEORIES is a list of theories to be rewritten in format expected by
            AUTO-REWRITE-THEORY,
   REWRITES is a list of rewrite rules in AUTO-REWRITE format.
   EXCLUDE is a list of rewrite rules on which rewriting must be stopped.
  The INSTANTIATOR argument can be used to specify use of an alternative
  instantiation mechanism.  This defaults to the (INST?) strategy.

    (induct-and-simplify "i" :defs ! :theories "real_props"
                 :rewrites "assoc" :exclude ("div_times" "add_div")):
      If i has type nat, then the natural number induction
      scheme is instantiated with a predicate constructed from sequent
      formula 1, and the resulting cases are simplified using
      definitions in the given sequent (unconditionally expanding
      explicit definitions), the rewrites in the  prelude theory 
      real_props but excluding div_times and add_div,
      and the rewrite rule assoc.


step_type: defined_rule
library: prelude
docstring:
  (split-ineq/$ fnum &optional replace?) :
      [Manip] Given that FNUM is a nonstrict antecedent inequality (<= or >=),
  split it into two cases, e.g., an equal-to and a less-than case.  Also
  works if FNUM is a strict consequent inequality.  Simplification using
  (ASSERT) is applied after splitting.  The equality may be optionally
  used for replacement by supplying  the direction LR or RL for the
  REPLACE? argument.


step_type: defined_rule
library: prelude
docstring:
  (splash/$ &optional (fnum *) reverse? order
   (tcc-step (extra-tcc-step))) :
      [Extrategies] Asymmetrically splits a (-)-disjunctive or (+)-conjunctive formula in FNUM.
  The direction of the split is reversed when REVERSE? is t (this may generate unprovable TCCs
  since Boolean operators in PVS are non-strict.) Particular components of the formula can be
  specified in ORDER, which is a list of integers (i1 .. in). An integer ik represents the ik-th
  component of the formula, left to right if ik is positive, right to left if ik is negative.
  TCCs generated during the execution of the command are discharged with the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (insteep*/$ &optional (fnum '*) postfix n) :
      [Extrategies] Iterates N times insteep (or until it does nothing if N is nil) in an
  existentially quantified formula in FNUM.  If POSTFIX is provided, it is appended to the 
  names of the bounded variables.


step_type: defined_rule
library: prelude
docstring:
  (presburger/$ &optional (fnums *)) :
      Decision procedure for Presburger arithmetic by
     reduction to WS1S.


step_type: defined_rule
library: prelude
docstring:
  (measure-induct+/$ measure vars &optional (fnum 1) order
   skolem-typepreds?) :
      Uses MEASURE-INDUCT but recasts induction hypothesis in a more usable form,
  i.e. (FORALL x, w: m(x) < m(y) IMPLIES p(x, w)) rather than
       (FORALL x: m(x) < m(y) IMPLIES (FORALL w: p(x, w))).
  This form should always be preferred over MEASURE-INDUCT.

  Suitably instantiates and uses the measure induction scheme in the
  PVS prelude.  Selects an instance of measure induction with measure
  MEASURE containing only free variables from VARS using formula FNUM to
  formulate an induction predicate.   Uses ORDER as the well-founded
  relation; if not specified defaults to < on nats or ordinals.
  Adds typepreds of the introduced skolem constants if SKOLEM-TYPEPREDS? is T.
  Simplifies out the result to yield the induction goal.

  Example:  (measure-induct+ "length(x) + length(y)" ("x" "y")).


step_type: defined_rule
library: prelude
docstring:
  (rewrite-with-fnum/$ fnum &optional subst (fnums *) (dir lr)
   dont-delete?) :
      Rewrites using the formula named in FNUM given input substitution
  SUBST, target FNUMS where rewrites are to occur, and the rewrite direction
  DIR (LR for left-to-right, and RL, otherwise).


step_type: defined_rule
library: prelude
docstring:
  (invoke/$ command &rest expr-specs) :
      [Manip] Invoke a rule or strategy by instantiating COMMAND with
  substitutions extracted from the extended expression specifications
  EXPR-SPECS.  Example: suppose formula 1 is f(x+y) = f(a*(z+1)).  Then
     (invoke (case "%1 = %2") (? 1 "f(%1) = f(%2)"))
  would match and create the bindings %1=`x+y' and %2=`a*(z+1)', which
  results in the prover command (case "x+y = a*(z+1)") being invoked.


step_type: defined_rule
library: prelude
docstring:
  (delabel/$ label &optional hide? (hidden? t)) :
      [Extrategies] Removes LABEL(s). If HIDE? is t, hides the delabeled formulas.
  If HIDDEN? is t, LABEL(s) are also removed from hidden formulas.


step_type: defined_rule
library: prelude
docstring:
  (rewrite-lemma/$ lemma subst &optional (fnums *) (dir lr)
   dont-delete?) :
      Rewrites using the given lemma/defintion as a (conditional) rewrite
   rule, relative to the given substitution (which must provide substitutions
   for all of the substitutable variables).  See REWRITE.


step_type: defined_rule
library: prelude
docstring:
  (skeep/$ &optional (fnum (+ -)) preds? postfix but) :
      [Extrategies] Skolemizes a universally quantified formula in FNUM, using the names
  of the bounded variables as the names of the skolem constants. If POSTFIX is provided, it 
  is appended to the variable names. Names that clash with other names in the current
  sequent are replaced by fresh names. Type predicates are introduced as hypothesis when 
  PREDS? is t.

  BUT is a list of variable references of the form <VAR> or (<VAR> <NAME>), where <VAR> is either 
  a quantified variable name or a relative position of a variable in the quantifier (positive means 
  left to right, negative means right to left). If <NAME> is not provided, the variable referred to 
  by <VAR> will be excluded from the skolemization. If <NAME> is provided, it is used as the name of 
  the skolem constant for the variable <VAR>.  For example, (skeep :but "x") skolemizes all variables 
  but excludes "x", (skeep :but ("x" ("y" "YY"))) skolemizes all variables but "x" and 
  uses "YY" as the name of the skolem constant for "y".


step_type: defined_rule
library: prelude
docstring:
  (apply-lemma/$ lemma &rest expr-specs) :
      [Manip] Try applying a lemma (via USE) with explicit instantiations using
  an implicit variable list.  In PVS, lemma variables appear in alphabetical
  order when introduced by the LEMMA rule.  That order needs to be observed
  when entering EXPR-SPECS.


step_type: defined_rule
library: prelude
docstring:
  (instantiate-one/$ fnum terms &optional copy?) :
      Same as INSTANTIATE but treated as a SKIP if the instantiation would
  introduce a duplicate formula.


step_type: defined_rule
library: prelude
docstring:
  (rewrite-expr/$ lemmas expr-loc) :
      [Manip] Rewrite LEMMAS in the expressions located by EXPR-LOC.  Only these
  expressions will be involved in the rewriting.


step_type: defined_rule
library: prelude
docstring:
  (with-tccs/$ step &optional steps (fnums *)
   (tcc-step (extra-tcc-steps))) :
      [Extrategies] Applies STEP after introducing TCCs for the formulas in FNUMS. If STEP generates
  subgoals, these subgoals are consecutively discharged using STEPS, which is a list of steps.
  TCCs generated during the execution of the command are discharged with the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (abstract-and-mc/$ cstate astate amap &optional theories rewrites
   exclude (strategy '(assert)) feasible verbose?) :
      Invokes abstraction followed by symbolic mu-calculus model checking.


step_type: defined_rule
library: prelude
docstring:
  (skip-steps/$ &rest steps) :
      [Extrategies] Skips steps. This strategy is using for debugging purposes.


step_type: defined_rule
library: prelude
docstring:
  (auto-rewrite-expr/$ lemmas expr-loc) :
      [Manip] Rewrite LEMMAS in the expressions located by EXPR-LOC.  Only these
  expressions will be involved in the rewriting.


step_type: defined_rule
library: prelude
docstring:
  (cross-mult/$ &optional (fnums *)) :
      [Manip] Apply cross multiplication to relational expressions.  Multiply
  both sides of a formula by the respective divisors of each side and
  then simplify.  Checks for negative real divisors and invokes suitable
  lemmas as needed.  Applies cross multiplication recursively until all
  outermost division operators are gone.


step_type: defined_rule
library: prelude
docstring:
  (auto-rewrite!/$ &rest names) :
       Similar to auto-rewrite except that the rewrites of lemmas and
  explicit (non-recursive) definitions always occur independent of the
  righthand-side.  Examples:
   (auto-rewrite! "assoc" -3 "distrib" "square"):  Installs rewrites.
   (auto-rewrite! :names ("assoc" -3 "distrib" "square")): Same.


step_type: defined_rule
library: prelude
docstring:
  (wrap-manip/$ fnum manip &optional (tcc-step (extra-tcc-step))
   (labels? t)) :
      [Field] Applies Manip's command MANIP,  dicharges TCCs using TCC-STEP, and
  preserves labels of FNUM when labels? is t.


step_type: defined_rule
library: prelude
docstring:
  (sq-simp/$ &optional (fnum *) (auto-step (assert))) :
      [Field] Simplifies FNUM with lemmas from sq and sqrt. At the end, the strategy tries to 
  discharge the current branch using the proof command AUTO-STEP.


step_type: defined_rule
library: prelude
docstring:
  (insteep/$ &optional (fnum (+ -)) postfix but) :
      [Extrategies] Instantiates an existentially quantified formula in FNUM, using the names
  of the bounded variables. If POSTFIX is provided, it is appended to the variable names. 

  BUT is a list of variable references of the form <VAR> or (<VAR> <EXPR>), where <VAR> is either 
  a quantified variable name or a relative position of a variable in the quantifier (positive means 
  left to right, negative means right to left). If <EXPR> is not provided, the variable referred to 
  by <VAR> will be excluded from the instantiation. If <EXPR> is provided, <VAR> is instantiated with
  <EXPR>. For example, (insteep :but "x") instantiates all variables using the names of the quantified
  formula but excludes "x", (insteep :but ("x" ("y" "100"))) instantiates all variables but 
  "x" and instantiates "y" with "100".


step_type: defined_rule
library: prelude
docstring:
  (elim-unary/$ fnum &optional (side *)) :
      [Manip] Eliminate unary minus functions where possible in additive
  expressions.  Convert expressions of the form x +/- -y to the form
  x -/+ y.  Also convert -x + y to y - x.


step_type: defined_rule
library: prelude
docstring:
  (permute-mult/$ fnums &optional (side r) (term-nums 2) (end l)) :
      [Manip] Reorder multiplicative terms from the factors given by TERM-NUMS 
  for the expression found on SIDE (L or R) of relational formulas FNUMS.
  Those factors cited in TERM-NUMS will be moved to the END in the order
  listed.  The remaining factors will be placed at the other END in their
  original order.


step_type: defined_rule
library: prelude
docstring:
  (stop-rewrite-theory/$ &rest theories) :
      Turns off rewriting for entire theories given their names.
  If THEORIES contains a generic theory, this turns off the
  generic definitional rewrite rules installed by AUTO-REWRITE,
  AUTO-REWRITE-THEORY, or AUTO-REWRITE-THEORIES. E.g.,
   (stop-rewrite-theory "real_proofs" "sets[nat]" "sequences").


step_type: defined_rule
library: prelude
docstring:
  (factor/$ fnums &optional (side *) (term-nums *) id?) :
      [Manip] Extract common multiplicative factors from the additive terms
  given by TERM-NUMS for the expression found on SIDE (L or R) of each
  relational formula in FNUMS, then rearrange.  ID? = T indicates the factor
  made of summed terms should be embedded in a call to the identity function
  to prevent later distribution.


step_type: defined_rule
library: prelude
docstring:
  (div-by/$ fnums term &optional (sign +)) :
      [Manip] Divide both sides of relational formulas by the factor TERM.
  If TERM is known to be positive or negative, use + or - as the SIGN
  argument.  Otherwise, use *, which introduces a conditional expression
  to handle the two cases.


step_type: defined_rule
library: prelude
docstring:
  (protect/$ fnums step &optional label hide?) :
      [Extrategies] Protects formulas FNUMS so that they are not afected by STEP. The protected formulas
   are labeled LABEL(s), if LABEL is not nil.


step_type: defined_rule
library: prelude
docstring:
  (discriminate/$ step &optional label strict?) :
      [Extrategies] Labels formulas generated by STEP as LABEL(s). When STRICT? is set to t,
  all formulas that are considered new by PVS are also labeled.


step_type: defined_rule
library: prelude
docstring:
  (unwind-protect/$ main-step cleanup-step) :
      [Manip] Invoke MAIN-STEP followed by CLEANUP-STEP, which is performed
  even if MAIN-STEP leads to a proof of the current goal.


step_type: defined_rule
library: prelude
docstring:
  (skodef*/$ &optional (fnum *) hide? postfix (tcc-step (extra-tcc-step))
   n) :
      [Extrategies] Iterates N times skodef (or until it does nothing if N is nil) in FNUM.
  TCCs generated during the execution of the command are discharged with the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (ground/$ &optional (let-reduce? t) quant-simp? implicit-typepreds?
   cases-rewrite? ignore-typepreds?) :
      Does propositional simplification followed by the use of decision procedures.


step_type: defined_rule
library: prelude
docstring:
  (inst/$ fnum &rest terms) :
      Instantiates the top quantifier in formula FNUM. See INST-CP for copying
  quantified formula.


step_type: defined_rule
library: prelude
docstring:
  (cut/$ cases &optional (tcc-step (extra-tcc-step))) :
      [Extrategies] The proof command (cut (<e1> ... <en>)) behaves as (case <e1> ... <en>).
  TCCs generated during the execution of the command are discharged with the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (smash/$ &optional (updates? t) (let-reduce? t) quant-simp?
   implicit-typepreds? cases-rewrite? ignore-typepreds?) :
      Repeatedly tries BDDSIMP, ASSERT, and LIFT-IF.  If the UPDATES?
  option is NIL, update applications are not if-lifted.


step_type: defined_rule
library: prelude
docstring:
  (suffices/$ fnum expr &optional after-var after-qn
   (tcc-step (extra-tcc-step))) :
      [Extrategies] Introduces a sufficient hypothesis EXPR to a universally quantified formula
  in FNUM. If FNUM is in the consequent, it is expected to have the form FORALL(<vars>):<expr>;
  if FNUM is in the antecedent it is expected to have the form EXISTS(<vars>):<expr>. In the
  first case, the resulting formula has the form FORALL(<vars>):EXPR IMPLIES <expr>. In the
  second case, the resulting formula has the form EXISTS(<vars>): EXPR AND <expr>. The hypothesis
  EXPR is added after the quantified variable AFTER-VAR, if provided, and/or after the AFTER-QN-th
  quantifier, if provided.


step_type: defined_rule
library: prelude
docstring:
  (name-replace*/$ names-and-exprs &optional (fnums *) (dir lr) hide?
   (tcc-step (extra-tcc-step)) tcc-label) :
      [Extrategies] Same as name-label* without labeling the formulas.


step_type: defined_rule
library: prelude
docstring:
  (neg-formula/$ &optional (fnum (+ -)) (hide? t) label
   (tcc-step (extra-tcc-step)) (auto-step (assert))) :
      [Field] Negates both sides of the relational formula FNUM. If HIDE? is t,
  the original formula is hidden.  The new formula is labeled as the original
  one, unless an explicit LABEL is provided. TCCs generated during the execution
  of the command are discharged with the proof command TCC-STEP. At the end, the
  strategy tries to discharge the current branch using the proof command AUTO-STEP.


step_type: defined_rule
library: prelude
docstring:
  (bash/$ &optional (if-match t) (updates? t) polarity?
   (instantiator inst?) (let-reduce? t) quant-simp? implicit-typepreds?
   cases-rewrite? ignore-typepreds?) :
      Core of REDUCE.  Does ASSERT, BDDSIMP, INST?, SKOLEM-TYPEPRED, 
  FLATTEN, and LIFT-IF once and in that order.  The IF-MATCH option
  can be NIL, T, ALL, or BEST for no, some, all, or the best instantiation.
  If the UPDATES? option is NIL, update applications are not if-lifted.
  When the POLARITY? flag is T, INST? matches templates against
  complementary subexpressions.
  The INSTANTIATOR argument can be used to specify use of an alternative
  instantiation mechanism.  This defaults to the (INST?) strategy.


step_type: defined_rule
library: prelude
docstring:
  (name-label*/$ names-and-exprs &optional label (fnums *) (dir lr) hide?
   (tcc-step (extra-tcc-step)) tcc-label) :
      [Extrategies] Iterates name-label on NAMES-AND-EXPRS, which is assumed to be a list of the form
  (NAME1 EXPR1 NAME2 EXPR2 ... NAMEn EXPRn). Options are provided as in name-label.

  ADVANCED USE: The options LABEL, TCC-STEP, and TCC-LABEL can be lists of the form (:pairing e1 ... en).
  In this case, each ei is paired to the i-th element in NAMES-AND-EXPRS.


step_type: defined_rule
library: prelude
docstring:
  (copy*/$ fnums &optional label hide? labels?) :
      [Extrategies] Copies formulas in FNUMS. The copied formulas are labeled LABEL(s), if
  LABEL is not nil. When HIDE? is t, the copied formulas are hidden. If LABELS? is t,
  labels are also copied.


step_type: defined_rule
library: prelude
docstring:
  (swap-group/$ term1 operator term2 term3 &optional (side l)
   (infix? t)) :
      [Manip] Try associatively regrouping and swapping three terms according
  to the scheme indicated by SIDE: 
    L: x op (y op z) ==> y op (x op z)  R: (x op y) op z ==> (x op z) op y
  so as to lift and move center term to the left or right.  Set INFIX? to
  nil for prefix applications.  Justification proof for operator will be
  tried automatically.


step_type: defined_rule
library: prelude
docstring:
  (name-mult!/$ name expr-loc &optional (term-nums *)) :
      [Manip] Select a list of factors (indicated by TERM-NUMS) from the
  expression found at EXPR-LOC.  Assign a NAME to the product of the selected
  factors and replace the product by NAME.  Can only handle first expression
  that results from EXPR-LOC.


step_type: defined_rule
library: prelude
docstring:
  (name-extract/$ name &rest expr-specs) :
      [Manip] Extract expressions using the extended expression specifications
  supplied in EXPR-SPECS.  Assign NAME (or NAME_1, NAME_2,...) to the
  expressions and replace them throughout the sequent, leaving the
  antecedent equalities visible.


step_type: defined_rule
library: prelude
docstring:
  (use-with/$ lemma &rest fnums) :
      [Manip] USE a lemma with formula preferences for instantiation.  A
  temporary copy of the terms in FNUMS is constructed and placed at the
  front of the sequent (formula -1).  Then a USE command for LEMMA is
  invoked so that the search for instantiable terms begins with the
  temporary formula.  The effect is to match terms from the user's preferred
  formulas (in the order given) before looking elsewhere in the sequent.


step_type: defined_rule
library: prelude
docstring:
  (rewrites/$ lemmas-or-fnums &optional (fnums *) (target-fnums *)
   (dir lr) (order in) dont-delete?) :
      [Extrategies] Rewrites with a list of lemmas or fnums. LEMMAS-OR-FNUMS has the form
  (LEMMAS-OR-FNUMS1 ... LEMMAS-OR-FNUMS). Options are as in rewrite.


step_type: defined_rule
library: prelude
docstring:
  (simple-induct/$ var fmla &optional name) :
      Selects an induction scheme according to the type of VAR in FMLA and uses FMLA
   to formulate  an induction predicate.  The name of the induction
  formula can be explicitly supplied using the optional NAME argument.
  See also INDUCT.


step_type: defined_rule
library: prelude
docstring:
  (simple-measure-induct/$ measure vars &optional (fnum 1) order) :
      Selects and insert as an antecedent, an instance of measure
  induction with measure MEASURE containing only free variables from
  VARS using formula FNUM to formulate an induction predicate.
  Uses ORDER as the well-founded relation; if not specified defaults
  to < on nats or ordinals.

  Example: (simple-measure-induct "i+j" ("i" "j")).
  See also SIMPLE-MEASURE-INDUCT.


step_type: defined_rule
library: prelude
docstring:
  (tccs-expression expr &optional label hide?
   (tcc-step (extra-tcc-step))):
      [Extrategies] Adds TCCs of expression EXPR as hypotheses to the current sequent. Added hypotheses
  are labeled LABEL(s), if LABEL is not nil. They are hidden when HIDE? is t. TCCs generated during
  the execution of the command are discharged with the proof command TCC-STEP. If TCC-STEP is nil,
  the strategy does nothing.


step_type: defined_rule
library: prelude
docstring:
  (move-terms/$ fnum side &optional (term-nums *)) :
      [Manip] Move additive terms numbered TERM-NUMS in relational formula FNUM
  from SIDE (L or R) to the other side, adding or substracting as needed.


step_type: defined_rule
library: prelude
docstring:
  (factor!/$ expr-loc &optional (term-nums *) (id? nil)) :
      [Manip] Extract common multiplicative factors from the additive terms
  given by TERM-NUMS for the expressions found at EXPR-LOC, then rearrange.
  ID? = T indicates the factor made of summed terms should be embedded in
  a call to the identity function to prevent later distribution.


step_type: defined_rule
library: prelude
docstring:
  (cancel-formula/$ &optional (fnum (+ -)) (tcc-step (extra-tcc-step))) :
      [Field] Factorizes common terms in FNUM and then cancels them.
  TCCs generated during the execution of the command are discharged 
  with the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (inst?/$ &optional (fnums *) subst (where *) copy? if-match polarity?
   (tcc? t)) :
      Tries to automatically instantiate a quantifier:
  FNUMS indicates which quantified formula:  *,-, +, or (n1, n2,..)
  SUBST is a partial substitution for the bound variable names.
  WHERE indicates which fnums to search for a match.
  COPY? if T, the quantified formula is copied.
  IF-MATCH if all, all possible instantiations of a chosen template 
                   subexpression containing all the instantiable variables
                   of the chosen quantified formula are found, and if
                   this fails, then it tries INST? with IF-MATCH set to NIL,
           if best, the instantiation from the all case that generates
                    the fewest TCCs is chosen,
           if T, the instantiation only occurs if the match succeeds,
                 otherwise the given partial substitution is used.
           if first*, all possible instantiations of the
                      first successful template are chosen.
  POLARITY? if T, a positively occurring template is only matched against
                  negatively occuring subexpressions, and less-than
                  term occurrences are matched against greater-than
                  occurrences.
  TCC? if NIL only selects instantiations that do not generate any TCCs.
       The default value is T.  There is no check to see if the TCCs are
       true in the given context.


step_type: defined_rule
library: prelude
docstring:
  (skolem!/$ &optional (fnum *) keep-underscore? dont-simplify?) :
      Skolemizes by automatically generating skolem constants.
  When KEEP-UNDERSCORE? is T, a bound variable x_1 is replaced by skolem constant
  x_1!n rather than x!n, for some number n.


step_type: defined_rule
library: prelude
docstring:
  (redlet*/$ &optional (fnum *) (tcc-step (extra-tcc-step)) (n 1)) :
      [Extrategies] Iterates N times redlet (or until it does nothing if N is nil). TCCs generated during
  the execution of the command are discharged with the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (isolate-mult/$ fnum &optional (side l) (term-num 1) (sign +)) :
      [Manip] Select factor TERM-NUM from one SIDE of formula FNUM and divide
  both sides as needed to leave the selected term isolated.  SIGN indicates
  the sign of the product of the unselected factors.  A case split to generate
  the appropriate condition on the divisor is automatically introduced.


step_type: defined_rule
library: prelude
docstring:
  (unlabel*/$ &optional (fnums *) label hidden?) :
      [Extrategies] Removes specified LABEL(s) (or all labels if LABEL is nil) from FNUMS.
  FNUMS are considered to be hidden formulas when hidden? is set to t.


step_type: defined_rule
library: prelude
docstring:
  (detuple-boundvars/$ &optional (fnums *) singles?) :
      Replaces formulas given by FNUMS by equivalent formulas where any
  bound variable of tuple type is replaced by a list of variables.
  When SINGLES? is T, detupling is restricted to those bound variables
  of tuple/record type that are the sole bound variables of a binding operator,
  i.e. those x of the form (FORALL x: ...), (EXISTS x: ...),
  or (LAMBDA x: ...).


step_type: defined_rule
library: prelude
docstring:
  (tccs-formula/$ &optional (fnum 1) label hide?) :
      [Extrategies] Adds TCCs of formula FNUM as hypotheses to the current sequent. Added hypotheses
  are labeled LABEL(s), if LABEL is not nil. They are hidden when HIDE? is t.


step_type: defined_rule
library: prelude
docstring:
  (try-rewrites/$ fnums &rest lemmas) :
      [Manip] Try rewriting LEMMAS in sequence within FNUMS until first one succeeds.


step_type: defined_rule
library: prelude
docstring:
  (rule-induct/$ rel &optional (fnum *) name) :
      Applies rule (co)induction over an inductive relation REL in order to
  prove a sequent of the form
        ...|- (FORALL ...: REL(...) IMPLIES ... or
       ..., REL(x1,...,xn) ... |-- ...
     or, for coinductive REL,
        ...|- (FORALL ...: REL(...) IMPLIES ... or
       ..., REL(x1,...,xn) ... |-- ... 
  RULE-INDUCT first applies repeated skolemization  and flattening to the
  specified FNUM (or the first skolemizable formula) before invoking
  RULE-INDUCT-STEP.   The strategy uses the default weak (co)induction scheme
  but can be told to use strong (co)induction by giving REL_induction
  or REL_coinduction as the NAME argument.


step_type: defined_rule
library: prelude
docstring:
  (rewrite*/$ lemmas-or-fnums &optional (fnums *) (target-fnums *)
   (dir lr) (order in) dont-delete?) :
      [Extrategies] Recursively rewrites LEMMAS-OR-FNUMS on the first branch. Options are as in rewrites.


step_type: defined_rule
library: prelude
docstring:
  (for@/$ n &rest steps) :
      [Extrategies] Iterates N times STEP1 ... STEPn, or until it does nothing if N is nil,
  along the first branch.


step_type: defined_rule
library: prelude
docstring:
  (with-labels/$ rule labels &optional push?) :
      If RULE generates subgoal sequents S1...Sn where each Si has
  new formulas, i.e., those numbered with {}, numbered fi1..fim, then
  if LABELS is a list of list of labels ((l11 ... l1k)...(ln1...lnm)),
  then each formula fij is labelled with label lij.  As usual, any of
  the lists can be replaced a single label, and if there are not enough
  labels in a list, then the last label is applied to the remaining
  fnums.


step_type: defined_rule
library: prelude
docstring:
  (move-to-front/$ &rest fnums) :
      [Manip] Rearranges the order of antecedent and consequent formulas.
  Takes the FNUMS given and moves the corresponding formulas to the front
  of the antecedent and consequent lists as appropriate.


step_type: defined_rule
library: prelude
docstring:
  (use/$ lemma &optional subst (if-match best) (instantiator inst?)
   polarity? let-reduce?) :
      Introduces lemma LEMMA, then does BETA and INST? (repeatedly) on
   the lemma.  The INSTANTIATOR argument may be used to specify an alternative
   to INST?.


step_type: defined_rule
library: prelude
docstring:
  (swap!/$ expr-loc) :
      [Manip] Try commutatively swapping the two arguments of the function
  application found at EXPR-LOC.  Commutativity proof for operator will
  be tried automatically.


step_type: defined_rule
library: prelude
docstring:
  (recip-mult!/$ expr-loc) :
      [Manip] Convert the top-level division operation for the expressions found
  at EXPR-LOC to a multiplication by the reciprocal of the divisor.


step_type: defined_rule
library: prelude
docstring:
  (install-rewrites/$ &optional defs theories rewrites exclude-theories
   exclude) :
      Sets up auto-rewrites from definitions of operators in the statement,
  THEORIES and REWRITES, and stops rewriting on EXCLUDE-THEORIES
  and EXCLUDE.   DEFS is either
     NIL:  defns in the statement are not installed as auto-rewrites
     T: All defns are installed as conditional rewrites
     !: All defns are installed, but with explicit (non-recursive) defns as
        unconditional rewrites
     !!: All defns are installed, but with explicit defns as
         unconditional rewrites even when partially applied
     explicit: Only explicit defns installed as conditional rewrites
     explicit!: Only explicit defns installed as unconditional rewrites
     explicit!!: Only explicit defns installed as !! rewrites.
  THEORIES is a list of theories to be rewritten in the format expected by
            AUTO-REWRITE-THEORY.
  REWRITES is a list of rewrite rules definitions/lemmas/assumptions
  in the format expected by the AUTO-REWRITE rule.
  EXCLUDE-THEORIES is a list of theories.
  EXCLUDE is a list of rewrite rules. 


step_type: defined_rule
library: prelude
docstring:
  (induct-and-rewrite!/$ var &optional (fnum 1) &rest rewrites) :
      Performs induction according to the type of VAR using FNUM
  to formulate induction predicate, and then simplifies using the given 
  REWRITES while expanding all definitions.
   (induct-and-rewrite! "x"): Inducts on x then simplifies the base and
     induction using the definitions of functions appearing in the sequent.


step_type: defined_rule
library: prelude
docstring:
  (skosimp/$ &optional (fnum *) preds? dont-simplify?) :
      Skolemize (with typepreds on skolem constants when PREDS? is T)
  then disjunctively simplify.  


step_type: defined_rule
library: prelude
docstring:
  (case-replace/$ formula &optional hide?) :
      Case splits on a given FORMULA lhs=rhs and replaces lhs by rhs.
  See also CASE, CASE*.  Hides FORMULA when HIDE? is T.


step_type: defined_rule
library: prelude
docstring:
  (equate/$ lhs rhs &optional (try-just nil) (fnums *)) :
      [Manip] Try equating two expressions and replacing the LHS by the
  RHS in FNUMS.  Proof of the justification step can be tried or deferred.
  Use TRY-JUST to supply the rule for the justification proof or T for
  the default rule (GRIND).


step_type: defined_rule
library: prelude
docstring:
  (hide-all-but/$ &optional keep-fnums (fnums *)) :
      Hides all sequent formulas from FNUMS except those listed in
  KEEP-FNUMS.  Useful when all but a few formulas need to be hidden.


step_type: defined_rule
library: prelude
docstring:
  (forward-chain-theory/$ theory-name) :
      Forward-chains on all applicable formulas of the given theory-name


step_type: defined_rule
library: prelude
docstring:
  (replaces/$ &optional (fnums -) (in *) but from to (hide? t) (dir lr)) :
      [Extrategies] Iterates the proof command replace to rewrite with the formulas in FNUMS,
  respecting the order, the formulas in IN but not in BUT. The keys DIR and HIDE? are like
  in REPLACE. Notice that in contrast to REPLACE, the default value of HIDE? is T. Instead
  of using FNUMS, rewriting formulas can be addressed via FROM and TO.


step_type: defined_rule
library: prelude
docstring:
  (rule-induct-step/$ rel &optional (fnum *) name) :
      Applies rule (co)induction over a (co)inductive relation REL in order to
  prove a sequent of the form
       ..., REL(x1,...,xn) ... |-- ... for an inductive REL, or
       ... |-- ..., REL(x1,...,xn) ... for a coinductive REL.
  RULE-INDUCT-STEP searches for an antecedent (for inductive REL) or
  consequent (for coinductive REL) formula of this form but this can also be
  given explicitly as FNUM.  The (co)induction predicate is formulated using
  all the sequent formulas containing x1,...,xn.   The strategy uses the
  weak (co)induction scheme by default but can be told to use an alternative 
  scheme by giving a different NAME argument, e.g., REL_induction or
  REL_coinduction.


step_type: defined_rule
library: prelude
docstring:
  (yices2-with-rewrites/$ &optional (fnums *) defs theories rewrites
   exclude-theories exclude) :
      Installs rewrites from statement (DEFS is either NIL, T, !, explicit,
  or explicit!), from THEORIES, and REWRITES, then applies (assert fnums) followed
  by (yices fnums), then turns off all the installed rewrites.  Examples:
   (yices-with-rewrites  + ! ("real_props" ("sets[nat]"))
                           ("assoc"))
   (yices-with-rewrites * nil :rewrites ("assoc" "distrib")).


step_type: defined_rule
library: prelude
docstring:
  (op-ident!/$ expr-loc &optional (operation *1)) :
      [Manip] Apply the operator identity given by OPERATION to rewrite
  the expression found at EXPR-LOC.  Currently performs the following
  operations using these designated symbols:
     z+      +z      -z      1*      *1      /1
     0 + x   x + 0   x - 0   1 * x   x * 1   x / 1


step_type: defined_rule
library: prelude
docstring:
  (ygrind/$ &optional (defs !) theories rewrites exclude (if-match t)
   (updates? t) polarity? (instantiator inst?) (let-reduce? t)
   cases-rewrite? quant-simp? no-replace? implicit-typepreds?) :
      Core of GRIND: Installs rewrites, repeatedly applies BASH, and then
     invokes YICES.  See BASH for more explanation.


step_type: defined_rule
library: prelude
docstring:
  (apply-extensionality/$ &optional (fnum +) keep? hide?) :
      Tries to prove an equality indicated by FNUM via extensionality.  Note that
  if FNUM is not given, then the first consequent that is an equation is used.
  If KEEP? is T, the equality is retained as an antecedent.
  If HIDE? is T, the equality formula to which extensionality is applied,
  is hidden.
  See also EXTENSIONALITY.


step_type: defined_rule
library: prelude
docstring:
  (untrack-rewrite/$ &rest names) :
      (See TRACK-REWRITE) Turns off tracking for all rewrite rules when NAMES is
  empty, and for the named rewrite rules, otherwise.  Behaves like (SKIP) otherwise.


step_type: defined_rule
library: prelude
docstring:
  (mult-ineq/$ fnum1 fnum2 &optional (signs (+ +))) :
      [Manip] Given two antecedent inequalities, a R1 b and x R2 y, form an
  inequality on their products, a * x R3 b * y.  If R2 is not in the same
  direction as R1, the strategy uses y rev(R2) x instead.  R3 is strict if
  either R1 or R2 is.  SIGNS indicates the polarity of the pairs (a,b) and
  (x,y).  Only inequalities on terms of matching signs can be usefully
  multiplied.  Example: SIGNS = (+ -) indicates a,b are positive terms
  while x,y are negative.  If either formula appears as a consequent,
  its relation is negated before carrying out the multiplication.


step_type: defined_rule
library: prelude
docstring:
  (skolem-typepred/$ &optional (fnum *) dont-simplify?) :
      Skolemizes and then introduces type-constraints of the Skolem
  constants.
  See also SKOLEM!, TYPEPRED.


step_type: defined_rule
library: prelude
docstring:
  (elim-unary!/$ expr-loc) :
      [Manip] Eliminate unary minus functions where possible in additive
  expressions.  Convert expressions of the form x +/- -y to the form
  x -/+ y.  Also convert -x + y to y - x.


step_type: defined_rule
library: prelude
docstring:
  (swap-rel/$ &rest fnums) :
      [Manip] Swap the two sides of relational formulas and reverse the direction
  of the relational operators.


step_type: defined_rule
library: prelude
docstring:
  (induct/$ var &optional (fnum 1) name) :
      Selects an induction scheme according to the type of VAR in FNUM and uses
  formula FNUM to formulate an induction predicate, then simplifies yielding base
  and induction cases.  The induction scheme can be explicitly supplied
  as the optional NAME argument.
   (induct "i"): If i has type nat and occurs outermost universally quantified
     in formula FNUM, the nat_induction scheme is instantiated with a predicate
     constructed from formula FNUM, and beta-reduced and simplified to yield base
     and induction subcases.  If i has type that is a datatype, then the
     induction scheme for that datatype is used by default.
   (induct "x" :fnum 2 :name "below_induction[N]"): The below_induction
     scheme is instantiated with an induction predicate constructed from fnum 2.


step_type: defined_rule
library: prelude
docstring:
  (name-mult/$ name fnum side &optional (term-nums *)) :
      [Manip] Select a list of factors (indicated by TERM-NUMS) from the
  expression found on SIDE (L or R) of relational formula FNUM.  Assign a
  NAME to the product of the selected factors and replace the product by NAME.


step_type: defined_rule
library: prelude
docstring:
  (forward-chain@/$ &rest lemmas-or-fnums) :
      Given a list of forward chain lemmas or formula numbers, this tries each in
  turn until one succeeds.


step_type: defined_rule
library: prelude
docstring:
  (both-sides-f/$ fnum f &optional (hide? t) label
   (tcc-step (extra-tcc-step)) (auto-step (assert))) :
      [Field] Applies function F to both sides of the relational expression in FNUM. If
  HIDE? is t, the original formula is hidden. The new formulas are labeled as the original
  one, unless an explicit LABEL is provided. TCCs generated during the execution of the
  command are discharged with the proof command TCC-STEP. At the end, the strategy tries to 
  discharge the current branch using the proof command AUTO-STEP.


step_type: defined_rule
library: prelude
docstring:
  (cross-add/$ &optional (fnums *)) :
      [Manip] Apply cross addition to relational formulas.  Add to both sides
  of a formula the respective subtrahend of each side and then simplify.
  Applies cross addition recursively until all outermost subtraction
  operators are gone.


step_type: defined_rule
library: prelude
docstring:
  (mult-extract!/$ name expr-loc &optional (term-nums *)) :
      [Manip] Extract additive terms TERM-NUMS from the expression found at
  EXPR-LOC.  Each term is treated as a product of factors, some of which
  contain divisions.  Each selected product term is assigned a name derived
  from NAME and extracted using name-replace to form a new antecedent equality.
  Then all the divisors are cross multiplied and any common factors are
  identified and canceled.  Can only handle first expression from EXPR-LOC.


step_type: defined_rule
library: prelude
docstring:
  (permute-terms/$ fnum side &optional (term-nums 1) (end r)) :
      [Manip] Reorder additive terms found on SIDE (L or R) of relational
  formula FNUM.  Those terms cited in TERM-NUMS will be moved to the END in
  the order listed.  The remaining factors will be placed at the other END
  in their original order.


step_type: defined_rule
library: prelude
docstring:
  (deftactic/$ name arg_or_step &optional step) :
      [Extrategies] Defines a tactic named NAME. A tactic is a strategy that is local to the current branch
  of the proof. NAME needs to be a valid identifier in PVS. A tactic definition can be either
  (deftactic NAME STEP) or (deftactic NAME (ARGUMENTS) STEP). For example,

  (deftactic myfirsttactic (then (flatten) (assert) (grind)))

  defines a tactic (myfirsttactic) that sequentially applies (flatten),
  (assert), and (grind). Tactics can be parametric, for example

  (deftactic mysecondtactic (fnums) (then (flatten) (assert fnums) (grind)))

  defines a tactic (mysecondtactic <fnum>), where <fnum> is a parameter provided by the user,
  that sequentially applies (flatten), (assert <fnum>), and (grind). Parameters can be
  optional and have a default value, for example,

  (deftactic mythirdtactic (&optional (fnums *)) (then (flatten) (assert fnums) (grind)))

  defines a tactic that behaves as (myfirsttactic) when used without parameters, e.g.,
  (mythirdtactic), and as (mysecondtactic <fnum>) when used with a parameter, e.g.,
  (mythirdtactic <fnum>).


step_type: defined_rule
library: prelude
docstring:
  (eval/$ expr &optional safe? quiet?) :
      [PVSio] Prints the evaluation of expression EXPR. If SAFE? is t and EXPR 
  generates TCCs, the expression is not evaluated. This strategy evaluates
  semantic attachments. Therefore, it may not terminate properly. When QUIET? 
  is t, the strategy fails silently.


step_type: defined_rule
library: prelude
docstring:
  (branch-back/$ step steplist) :
      [Manip] Perform a branching STEP that has subproofs with automatic
  backtracking for branches that fail to completely prove their goals.
  Similar to the built-in strategy BRANCH except that the elements of
  STEPLIST are attempted in all-or-nothing fashion.  If the step for a
  branch fails to prove its goal completely, the proof state (for that
  branch only) is rolled back to the point before the step was invoked.


step_type: defined_rule
library: prelude
docstring:
  (add-formulas/$ fnum1 &optional fnum2 (hide? t) label
   (tcc-step (extra-tcc-step)) (auto-step (assert))) :
      [Field] Adds relational formulas FNUM1 and FNUM2. If FNUM2 is nil, adds FNUM to itself.
  If HIDE? is t, the original formulas are hidden.  The new formula is labeled as LABEL,
  if specified. TCCs generated during the execution of the command are discharged with
  the proof command TCC-STEP. At the end, the strategy tries to discharge the current 
  branch using the proof command AUTO-STEP.


step_type: defined_rule
library: prelude
docstring:
  (mult-extract/$ name fnum &optional (side *) (term-nums *)) :
      [Manip] Extract additive terms TERM-NUMS from the expression found on 
  SIDE of relational formula FNUM.  Each term is treated as a product of
  factors, some of which contain divisions.  Each selected product term is
  assigned a name derived from NAME and is extracted using name-replace to
  form a new antecedent equality.  Then all the divisors are cross multiplied
  and any common factors are identified and canceled.


step_type: defined_rule
library: prelude
docstring:
  (distrib!/$ expr-loc) :
      [Manip] Distribute multiplication operators over factors having the
  form of additive subexpressions.  Apply this action to the multiplicative
  expression found at EXPR-LOC.


step_type: defined_rule
library: prelude
docstring:
  (reduce/$ &optional (if-match t) (updates? t) polarity?
   (instantiator inst?) (let-reduce? t) quant-simp? no-replace?
   implicit-typepreds? cases-rewrite? ignore-typepreds?) :
      Core of GRIND (ASSERT, BDDSIMP, INST?, SKOLEM-TYPEPRED, FLATTEN,
  LIFT-IF, i.e., BASH then REPLACE*) without reestablishing all the rewrites.
  See BASH for more explanation.


step_type: defined_rule
library: prelude
docstring:
  (cancel-add!/$ expr-loc) :
      [Manip] Cancel additive terms from selected expressions.  The matching terms
  can appear in any relative position within their containing expressions.


step_type: defined_rule
library: prelude
docstring:
  (mult-by/$ fnums term &optional (sign +)) :
      [Manip] Multiply both sides of relational formulas by the factor TERM.
  If TERM is known to be positive or negative, use + or - as the SIGN
  argument.  Otherwise, use *, which introduces a conditional expression
  to handle the two cases.


step_type: defined_rule
library: prelude
docstring:
  (default-strategy/$) :
      This invokes user defined default strategies.  It first looks for a strategy
  of the name 'foo-strategy', where 'foo' is the current theory.  If that is not
  defined, it looks for 'context-strategy', and if that is not found, it
  invokes 'grind'.


step_type: defined_rule
library: prelude
docstring:
  (simplify-with-rewrites/$ &optional (fnums *) defs theories rewrites
   exclude-theories exclude) :
      Installs rewrites from statement (DEFS is either NIL, T, !, explicit,
  or explicit!), from THEORIES, and REWRITES, then applies (assert fnums), and
  then turns off all the installed rewrites.  Examples:
   (simplify-with-rewrites  + ! ("real_props" ("sets[nat]"))
                           ("assoc"))
   (simplify-with-rewrites * nil :rewrites ("assoc" "distrib")).


step_type: defined_rule
library: prelude
docstring:
  (relabel/$ label fnums &optional pairing? (push? t)) :
      [Extrategies] Labels FNUMS as LABEL(s), keeping the old ones. If PAIRING? is t and
  LABEL is a list of the form (LAB1 ... LABn), each LABi is paired to the i-th formula in FNUM.
  If PUSH? is t, then the new labels are added to the existing ones. Otherwise, the new labels
  replace all existing ones.

  ADVANCED USE: If LABEL has the form (:pairing LAB1 ... LABn), PAIRING? is set to t.


step_type: defined_rule
library: prelude
docstring:
  (y2grind/$ &optional (defs !) theories rewrites exclude (if-match t)
   (updates? t) polarity? (instantiator inst?) (let-reduce? t)
   cases-rewrite? quant-simp? no-replace? implicit-typepreds?
   nonlinear?) :
      Core of GRIND: Installs rewrites, repeatedly applies BASH, and then
     invokes YICES.  See BASH for more explanation.


step_type: defined_rule
library: prelude
docstring:
  (permute-terms!/$ expr-loc &optional (term-nums 1) (end r)) :
      [Manip] Reorder additive terms found in expression at EXPR-LOC.  Those
  terms cited in TERM-NUMS will be moved to the END in the order listed.  The
  remaining factors will be placed at the other END in their original order.


step_type: defined_rule
library: prelude
docstring:
  (swap-group!/$ expr-loc &optional (side l)) :
      [Manip] Try associatively regrouping the three subexpressions of the
  function applications found at EXPR-LOC according to the scheme indicated
  by SIDE: 
    L: x op (y op z) ==> y op (x op z)  R: (x op y) op z ==> (x op z) op y
  so as to lift and move center term to the left or right.  Justification
  proof for operator will be tried automatically.


step_type: defined_rule
library: prelude
docstring:
  (forward-chain/$ lemma-or-fnum &optional quiet?) :
      Forward chains on given lemma or antecedent formula of the form
     A1 & A2 & A3 IMPLIES B
  by introducing the antecedent instance B' when the corresponding
  instances A1', A2', and A3' can be found as antecedents in the
  current goal.  If the instance B' already exists as an antecedent,
  this rule backtracks to find a fresh instance.  Note that the free variables
  in B must occur among the free variables in the Ai.


step_type: defined_rule
library: prelude
docstring:
  (cancel-add/$ &optional (fnums *)) :
      [Manip] Cancel additive terms from both sides of selected formulas.
  The matching terms can appear in any relative position within their
  containing expressions.  Also works for a term and its negation on the
  same side of a relation.


step_type: defined_rule
library: prelude
docstring:
  (yices-with-rewrites/$ &optional (fnums *) defs theories rewrites
   exclude-theories exclude) :
      Installs rewrites from statement (DEFS is either NIL, T, !, explicit,
  or explicit!), from THEORIES, and REWRITES, then applies (assert fnums) followed
  by (yices fnums), then turns off all the installed rewrites.  Examples:
   (yices-with-rewrites  + ! ("real_props" ("sets[nat]"))
                           ("assoc"))
   (yices-with-rewrites * nil :rewrites ("assoc" "distrib")).


step_type: defined_rule
library: prelude
docstring:
  (transform-both/$ fnum transform &optional (swap nil) (try-just nil)) :
      [Manip] Apply TRANSFORM to both sides of relational formula FNUM, where
  a transform has the form `...%1...', and `%1' represents the left- and
  righthand side expressions in the relation.  The transform can be
  regarded as a template expression with `%1' as an implicit template
  variable.  Example: (transform-both 3 "2 * %1 + 1") multiplies both
  sides of formula 3 by 2 then adds 1.  The flag SWAP is used to indicate
  when the terms should be swapped (e.g., when multiplying by a negative
  number).  Proof of the justification step can be tried by supplying
  a proof step for TRY-JUST.


step_type: defined_rule
library: prelude
docstring:
  (lazy-grind/$ &optional (if-match t) polarity? (defs !) rewrites
   theories exclude (updates? t) (let-reduce? t) quant-simp?
   implicit-typepreds? cases-rewrite? ignore-typepreds?) :
      Equiv. to (grind) with the instantiations postponed until after simplification.


step_type: defined_rule
library: prelude
docstring:
  (recip-mult/$ fnums side) :
      [Manip] Convert the top-level division operation for the expression found
  on SIDE (L or R) of relational formulas FNUMS to a multiplication by the
  reciprocal of the divisor.


step_type: defined_rule
library: prelude
docstring:
  (decompose-equality/$ &optional (fnum *) (hide? t)) :
      Decomposes an equality or disequality to the component equalities.
  This only works for equalities between functions, records, or tuples.  If
  HIDE? is T, the original (dis)equality is hidden.  If it is an equality in
  the consequents or a disequality in the antecedents then this simply
  invokes apply-extensionality.  Otherwise it decomposes the
   (dis)equality into its component equalities.


step_type: defined_rule
library: prelude
docstring:
  (isolate/$ fnum side term-num) :
      Move all additive terms except that numbered TERM-NUM in relational
  formula FNUM from SIDE (L or R) to the other side.


step_type: defined_rule
library: prelude
docstring:
  (has-sign/$ term &optional (sign +) (try-just nil)) :
      [Manip] Try claiming that a TERM has the designated SIGN (relationship
  to 0).  Symbols for SIGN are (+ - 0 0+ 0- +-), which have meanings positive,
  negative, zero, nonnegative, nonpositive, and nonzero.  Proof of the
  justification step can be tried or deferred.  Use TRY-JUST to supply
  a step for the justification proof or T for the default rule (GRIND).


step_type: defined_rule
library: prelude
docstring:
  (inst-cp/$ fnum &rest terms) :
      Instantiates the top quantifier in formula FNUM but retains a copy of the
  quantified formula.
  See INST for a non-copying version.


step_type: defined_rule
library: prelude
docstring:
  (tccs-expr expr &optional label hide? (tcc-step (extra-tcc-step))):
      [Extrategies] Adds TCCs of expression EXPR as hypotheses to the current sequent. Added hypotheses
  are labeled as LABEL(s), if LABEL is not nil. They are hidden when HIDE? is t. TCCs generated during
  the execution of the command are discharged with the proof command TCC-STEP.


step_type: defined_rule
library: prelude
docstring:
  (touch/$ &optional (step (skip))) :
      [Extrategies] Does step and touches the proof context so that try and else consider that step
  does something, even when it doesn't.


step_type: defined_rule
library: prelude
docstring:
  (apply-rewrite/$ lemma &rest expr-specs) :
      [Manip] Try applying a (purely equational) rewrite rule with explicit
  instantiations using an implicit variable list.  In PVS, lemma variables
  appear in alphabetical order when introduced by the LEMMA rule.  That
  order needs to be observed when entering EXPR-SPECS.


step_type: defined_rule
library: prelude
docstring:
  (for-each-rev/$ command &rest expr-specs) :
      [Manip] Repeatedly invoke a rule or strategy by instantiating COMMAND
  with substitutions extracted from the extended expression specifications
  EXPR-SPECS.  For each expression specified, instantiate and invoke
  COMMAND with a different binding for parameters %1, $1, etc.  Performs
  the invocations in reverse order.


step_type: defined_rule
library: prelude
docstring:
  (skoletin/$ &optional (fnum (+ -)) name (nth 1) var postfix hide?
   (tcc-step (extra-tcc-step)) old?) :
      [Extrategies] Names the NTH occurrence (left-right, depth-first) of
  NAME in a let-binding of the form
     LET ...,NAME = <expr>,... IN <e>
  in FNUM and introduces the equality <var>=expr as hypothesis. All occurrences
  of NAME in <e> are replaced by <var>. By default, <var> is NAME, with a POSTFIX
  if provided. An explicit name can be provided using the option VAR. Names that
  clash with other names in the current sequent are replaced by fresh names.

  If NAME is nil, the name of the NTH let-in binding is chosen by the strategy.
  In this case, if the NTH let-in binding is an expression (<x1>,...,<xn>) = <expr>,
  the equalities <var1>=<expr>`1,...,<varn>=<expr>`n are introduced to the sequent.
  By default, <vari> is <xi>. Explicit names can be provided using the
  option VAR as a list (<var1> ... <varm>), where m <= n. In this list,
  if <vari> is _, <xi> is used instead of <vari>.

  Name definitions are hidden when HIDE? is t; they can be recalled at any time with
  the command (reveal "<name>:"), where <name> is one of the names introduced by the
  strategy. TCCs generated during the execution of the command are discharged with the
  proof command TCC-STEP.

  CAVEAT: The order in which formulas are introduced by skoletin in version 6.0 is different
  from previous versions. The option OLD? reproduces the old order. 

  NOTE: This command works better when all let-in variables are explicitly typed as in
  LET x:posreal = 2 IN 1/x.


step_type: defined_rule
library: prelude
docstring:
  (flatten/$ &rest fnums) :
      Disjunctively simplifies chosen formulas.  It simplifies 
  top-level antecedent conjunctions, equivalences, and negations, and
  succedent disjunctions, implications, and negations from the sequent.


step_type: defined_rule
library: prelude
docstring:
  (do-rewrite/$ &optional (fnums *) rewrite-flag flush? linear?
   cases-rewrite? (type-constraints? t)) :
      Uses decision procedures to rewrite the formulas in FNUMS.
  Variant of SIMPLIFY with RECORD? flag set to NIL and REWRITE? flags set to
  T. If REWRITE-FLAG is RL(LR) then only lhs(rhs) is simplified.  If FLUSH?
  is T then the current asserted facts are deleted for efficiency.  If
  LINEAR? is T, then multiplication and division are uninterpreted.  If
  CASES-REWRITE? is T, then the selections and else parts of a CASES
  expression are simplified, otherwise, they are only simplified when
  simplification selects a case.
  Examples: (do-rewrite): Simplify every sequent formula with rewriting.
  (do-rewrite :rewrite-flag RL :linear? T): Apply rewriting only to left-hand
            sides of any equalities with uninterpreted nonlinear arithmetic.


step_type: defined_rule
library: prelude
docstring:
  (eval-formula/$ &optional (fnum 1) safe? quiet?) :
      [PVSio] Evaluates the formula FNUM in Common Lisp and adds the result to 
  the antecedent of the current goal. If SAFE? is t and FNUM generates TCCs, 
  the expression is not evaluated. The strategy is safe in the sense that 
  user-defined semantic attachments are not evaluated. However, 
  if SAFE? is nil, the strategy may not terminate properly in
  the presence of unproven TCCs.  When QUIET? is t, the strategy fails silently


step_type: defined_rule
library: prelude
docstring:
  (cancel/$ &optional (fnums *) sign) :
      [Manip] Cancel terms from both sides of relational formulas involving
  arithmetic expressions.  If SIGN = NIL, common terms are assumed to be
  (non)positive or (non)negative as needed for the appropriate rewrite
  rules to apply.  Otherwise, an explicit SIGN can be supplied to force
  a case split so the rules will apply.  If SIGN is `+' or `-', terms
  are claimed to be positive or negative.  If SIGN is `0+' or `0-', terms
  are nonnegative or nonpositive.  If SIGN is `*', the terms  are assumed
  to be arbitrary reals and a three-way case split is used.


step_type: defined_rule
library: prelude
docstring:
  (permute-mult!/$ expr-loc &optional (term-nums 2) (end l)) :
      [Manip] Reorder multiplicative terms from the factors given by TERM-NUMS 
  for the expressions found at EXPR-LOC.  Those factors cited in TERM-NUMS
  will be moved to the END in the order listed.  The remaining factors
  will be placed at the other END in their original order.


step_type: strategy
library: prelude
docstring:
  (unless-label/$ label &rest steps) :
      [Extrategies]  Sequentially applies STEPS to all branches as long as no formula is labeled
  as LABEL in the sequent.


step_type: strategy
library: prelude
docstring:
  (trust/$ orcl step &optional steps) :
      This strategy enables the addition of trusted formulas into the current sequent.
  Examples of such additions are type-checking information (TCCs), ground evaluations,
  and external *trusted* oracles. The strategy *must* only be used in proof rules.


step_type: strategy
library: prelude
docstring:
  (try-branch/$ step steplist else-step) :
      Like BRANCH, tries STEP and then pairs the steps in STEPLIST to the
  resulting subgoals.  The last step is used for any excess subgoals.
  If STEP does nothing, then ELSE-STEP is applied.


step_type: strategy
library: prelude
docstring:
  (with-fnums@ bindings &rest steps):
      [Extrategies] Allows variables in body to be bound to formulas in the current sequent.
  STEPS are sequentially applied to the main branch. BINDINGS has either the form (!VAR FNUMS) or
  ((!VAR1 FNUMS1) ... (!VARN FNUMSn)). For example,

  (with-fnums@ (!l -2) (split) (inst? !l))

  splits the current sequent and then instantatiates, on the main branch, the formula that
  used to be -2 in the original sequent.


step_type: strategy
library: prelude
docstring:
  'step:
      This simply evaluates to step.  This is used by the let strategy to
  ensure that the values for variables are not evaluated again after
  substitution.  It is unlikely to be useful otherwise.


step_type: strategy
library: prelude
docstring:
  (try strategy then else):
      Tries strategy STRATEGY on current goal, and if successful, applies
  strategy THEN to the subgoals.  If no change, then the ELSE strategy is
  applied to current goal.
  E.g., (try (skip)(flatten)(skolem!)) is just (skolem!)
        (try (lemma "assoc")(beta)(flatten)) is just lemma followed
             by beta if lemma assoc exists.


step_type: strategy
library: prelude
docstring:
  (mapstep@/$ funstep &optional list list?) :
      [Extrategies] Sequentially applies FUNSTEP to each element of LIST. FUNSTEP is a function
  in Lisp that takes one argument and returns a proof command. After each application of FUNSTEP,
  the resulting proof command is applied to the first branch. When LIST? is nil, the argument of
  FUNSTEP represents the head of the list at each iteration. If LIST? is t, the argument of FUNSTEP
  represents the complete list at each iteration. See (help mapstep) for examples of use.


step_type: strategy
library: prelude
docstring:
  (when/$ flag &rest steps) :
      [Extrategies] Behaves as (if FLAG (then STEP1 ... STEPn) (skip)). Due to the execution model
  of strategies in PVS, FLAG must be a variable.


step_type: strategy
library: prelude
docstring:
  (commentf/$ msg &rest args) :
      [Extrategies] Adds the formatted comment MSG to the sequent using the format
  arguments ARGS. ARGS can only have constant values.


step_type: strategy
library: prelude
docstring:
  (let bindings body):
      Allows variables in body to be bound to the results of Lisp
  computations.  E.g.,
    (let ((x (car *new-fmla-nums*)))
        (then (inst? x)(split x))).


step_type: strategy
library: prelude
docstring:
  (with-fresh-labels@ bindings &rest steps):
      [Extrategies] Creates fresh labels and binds them to formulas specified in BINDINGS. 
  Then, sequentially applies STEPS to the main branch. Created labels are removed before 
  ending. BINDINGS are specified as in WITH-FRESH-LABELS.


step_type: strategy
library: prelude
docstring:
  (then@/$ &rest steps) :
      Applies first step to the current goal and remaining
  steps to the first subgoal, postponing remaining subgoals.


step_type: strategy
library: prelude
docstring:
  (when@/$ flag &rest steps) :
      [Extrategies] Behaves as (if FLAG (then@ STEP1 ... STEPn) (skip)). Due to the execution model
  of strategies in PVS, FLAG must be a simple variable.


step_type: strategy
library: prelude
docstring:
  (name-distrib/$ &optional (fnums *) (prefix "ND") label hide?
   (tcc-step (extra-tcc-step))) :
      [Field] Introduces new names, which are based on PREFIX, to block the automatic
  application of distributive laws in formulas FNUMS. Labels as LABEL(s) the formulas
  where new names are defined. These formulas are hidden if HIDE? is t. TCCs generated
  during the execution of the command are discharged with the proof command TCC-STEP.


step_type: strategy
library: prelude
docstring:
  (spread@/$ step steplist) :
      Like SPREAD, applies STEP and then pairs the steps in STEPLIST with
  the subgoals, but generates warnings if number of subgoals do not match
  the number of subproofs.


step_type: strategy
library: prelude
docstring:
  (checkpoint):
      A synonym for (query*): inserting (checkpoint) an edited proof and
   rerunning it causes the non-checkpointed subproofs to be installed
   (using JUST-INSTALL-PROOF) so that the proof is only run up to the
  checkpoint.  


step_type: strategy
library: prelude
docstring:
  (with-fresh-names@ bindings &rest steps):
      [Extrategies] Creates fresh names and binds them to expressions
  specified in BINDINGS.  Then, sequentially applies STEPS to the main
  branch. BINDINGS are specified as in WITH-FRESH-NAMES.


step_type: strategy
library: prelude
docstring:
  (with-fresh-names bindings &rest steps):
      [Extrategies] Creates fresh names and binds them to expressions
   specified in BINDINGS.  Then, sequentially applies STEPS to all
   branches. All created names are expanded before the strategy
   exits. BINDINGS has either the form (VAR [EXPR]) or ((VAR1 [EXPR1
   [OPT1]]) ...  (VARn [EXPRn [OPTn]])). Optional information OPTi can
   be either :tccs, :tccs? t|nil, or :tcc-step TCC-STEP. The option
   :tccs? nil behaves as if no option is provided.  In the other cases,
   TCCs of EXPRi are added as hypotheses to the sequent by applying
   (tccs-expression EXPRi) before STEPS. These TCCs are discharged by a
   default strategy or by TCC-STEP, if one is provided.  The TCCs
   formulas of EXPRi are automatically labeled using a new label denoted
   by the implicit variable *VARi-tccs*.  For all 1 <= i <= n, an
   implicit variable *VARi* is defined such that it denotes the label of
   the formula introduced by (name VARi EXPRi). The strategy removes all
   added labels and hypotheses before exiting.


  For example,

  (with-fresh-names 
    ((e "x+2") (f "sqrt(x)" :tccs)) 
    (inst 1 e f))

  creates fresh names e and f, and issues the proof commands (name e
  "x+2"), (name f "sqrt(x)"), and (tccs-expression "sqrt(x)").
  Then, the strategy instantiates formula 1 with the expressions denoted
  by e and f. Finally, it expands names e and f and removes all added
  hypotheses and labels.


step_type: strategy
library: prelude
docstring:
  (if condition step1 step2):
      Evaluates the condition (in Lisp) and if it evaluates to nil, step2 is
  applied, otherwise step1 is applied.


step_type: strategy
library: prelude
docstring:
  (unless@/$ flag &rest steps) :
      [Extrategies] Behaves as (if (not FLAG) (then@ STEP1 ... STEPn) (skip)). Due to
  the execution model of strategies in PVS, FLAG must be a simple variable.


step_type: strategy
library: prelude
docstring:
  (inductionfree/$ &optional (recvar "v")) :
      [Extrategies] Extracts induction free principle from definition of recursive function. RECVAR is the
  name of the quantified variable that encodes the recursive call.


step_type: strategy
library: prelude
docstring:
  (when-label/$ label &rest steps) :
      [Extrategies]  Sequentially applies STEPS to all branches as long as at least one formula
  is labeled LABEL in the sequent.


step_type: strategy
library: prelude
docstring:
  (if-label/$ label then-step &optional (else-step (skip))) :
      [Extrategies]  Applies THEN-STEP if at least one formula is labeled LABEL in the current
  sequent; otherwise, applies ELSE-STEP.


step_type: strategy
library: prelude
docstring:
  (branch/$ step steplist) :
      Like SPREAD, applies STEP then pairs steps
  in STEPLIST with the resulting subgoals, using the last step in STEPLIST
  for any excess subgoals.  If STEP does nothing, the first step in STEPLIST
  is applied.


step_type: strategy
library: prelude
docstring:
  (unless/$ flag &rest steps) :
      [Extrategies] Behaves as (if (not FLAG) (then STEP1 ... STEPn) (skip)). Due to the
  execution model of strategies in PVS, FLAG must be a simple variable.


step_type: strategy
library: prelude
docstring:
  (mapstep/$ funstep &optional list list?) :
      [Extrategies] Sequentially applies FUNSTEP to each element of LIST. FUNSTEP is a function
  in Lisp that takes one argument and returns a proof command. After each application of FUNSTEP,
  the resulting proof command is applied to all branches. When LIST? is nil, the argument of
  FUNSTEP represents the head of the list at each iteration. For example,

  (mapstep #'(lambda(x)`(name ,x "1")) ("One" "Uno"))

  behaves as (then (name "One" "1") (name "Uno" "1")).

  If LIST? is t, the argument of FUNSTEP represents the complete list at each iteration.
  For example,

  (mapstep #'(lambda(x)`(name ,(car x) ,(length x))) ("Two" "One") :list? t)

  behaves as (then (name "Two" 2) (name "One" 1)).

  Technicality: Note the use of quotation and anti-quotation in the examples. Variables in FUNSTEP
  other than FUNSTEP's parameter can be unquoted only if they were defined outside FUNSTEP
  as (list 'quote <something>), e.g.,

  (let ((lbs (list 'quote '("a" "b" "c"))))
    (mapstep #'(lambda(x)`(relabel ,lbs ,x)) (-1 1)))


step_type: strategy
library: prelude
docstring:
  (with-fresh-labels bindings &rest steps):
      [Extrategies] Creates fresh labels and binds them to formulas
  specified in BINDINGS.  Then, sequentially applies STEPS to all
  branches. All created labels are removed before the strategy
  exits. BINDINGS has either the form (VAR [FNUMS]) or ((VAR1 [FNUMS1
  [OPT1]]) ...  (VARn [FNUMSn [OPTn]])). Optional information OPTi can
  be either :tccs or :tccs?  t|nil. The option :tccs? nil behaves as if
  no option is provided.  In the other cases, TCCs of FNUMSi are added
  as hypotheses to the sequent by applying (tccs-formula FNUMi) before
  STEPS. The TCCs formulas of FNUMi are automatically labeled using a
  new label denoted by the implicit variable *VARi-tccs*. The strategy
  removes all added hypotheses before exiting.

  For example,

  (with-fresh-labels 
    ((l 1) (m -1 :tccs)) 
    (inst? l :where m))

  creates fresh labels, which are denoted by the variables l and m, and
  issues the proof command (label l 1), (label m -1), and (tccs-formula
  m). Then, the strategy instantiates formula l with matches from
  formula m. Finally, it removes all added hypotheses and labels.


step_type: strategy
library: prelude
docstring:
  (spread!/$ step steplist) :
      Like SPREAD, applies STEP and then pairs the steps in STEPLIST with
  the subgoals, but generates an error and queries the user if the number
  of subgoals do not match the number of subproofs.


step_type: strategy
library: prelude
docstring:
  (printf/$ msg &rest args) :
      [Extrategies] Prints the Lisp formatted string MSG using the format arguments
  ARGS. ARGS must be constant values.


step_type: strategy
library: prelude
docstring:
  (skip-msg/$ msg &optional force-printing?) :
      Prints the given string but behaves like a skip.
  Useful for generating error messages in strategies.


step_type: strategy
library: prelude
docstring:
  (rerun/$ &optional proof recheck? break?) :
      Strategy to rerun existing or supplied proof. The RECHECK? flag when T is
  used to rerun an entire proof using only primitive proof steps.  Normally
  rerun gives warnings when there is a mismatch between the number of sobgoals
  and the number of subproofs.  The BREAK? flag causes an error and queries
  the user instead.


step_type: strategy
library: prelude
docstring:
  (with-fnums bindings &rest steps):
      [Extrategies] Allows variables in body to be bound to formulas in the current sequent.
  STEPS are sequentially applied to all branches. BINDINGS has either the form (!VAR FNUMS) or
  ((!VAR1 FNUMS1) ... (!VARN FNUMSn)). For example,

  (with-fnums (!l -2) (flatten) (inst? !l))

  flattens the current sequent and then instantatiates the formula that used to be -2 in the
  original sequent.


