fmrisc.ProofNavigator.Commands
Class Induction
java.lang.Object
fmrisc.ProofNavigator.Commands.CommandBase
fmrisc.ProofNavigator.Commands.ProofCommandBase
fmrisc.ProofNavigator.Commands.Induction
- All Implemented Interfaces:
- Command, ProofCommand
public final class Induction
- extends ProofCommandBase
Command "induction": induction on a univerally quantified NAT/INT variable.
Field Summary |
static java.lang.String |
Name
|
Constructor Summary |
Induction(Identifier var,
java.lang.String label)
Create an "induction" command. |
Method Summary |
static Command |
newCommand(org.w3c.dom.Node node)
Convert DOM node to command. |
void |
printCore(java.io.PrintWriter out)
Prints text representation on out (without new line termination). |
Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Methods inherited from interface fmrisc.ProofNavigator.Commands.Command |
toNode |
Name
public static final java.lang.String Name
- See Also:
- Constant Field Values
Induction
public Induction(Identifier var,
java.lang.String label)
- Create an "induction" command.
- Parameters:
var
- the variable on which to run the induction or null
(if null, induction runs on the first INTEGER variable).label
- the label of the goal to be proved by induction.
(if null, induction runs on the single goal)
newCommand
public static Command newCommand(org.w3c.dom.Node node)
- Convert DOM node to command.
- Parameters:
node
- the DOM representation of the command.
- Returns:
- the command (null, if an error occured).
printCore
public void printCore(java.io.PrintWriter out)
- Prints text representation on out (without new line termination).
- Specified by:
printCore
in class CommandBase
- Parameters:
out
- the stream on which the text is written