Package  Description 

fmrisc.ProofNavigator.Commands 
Modifier and Type  Class and Description 

class 
Assume
Commnand "assume": split proof state by an assumption and its proof.

class 
Auto
Command "auto": try to close state by automatic instantiation
of quantified formulas.

class 
AutoStar
command "autostar": apply auto to current node and its successor siblings.

class 
Case
The "case" command: split state into multiple cases.

class 
CounterExample
Command "counterexample": show potential counterexample for current
state (may be timeconsuming)

class 
Decompose
command "decompose": decompose proof state by repeated skolemization
and flattening.

class 
Expand
Command "expand": expand a definition.

class 
Flatten
Command "flatten": decompose compound formulas without splitting the state.

class 
Flip
Command "flip": flip a formula from goal position to assumption position
or vice versa.

class 
Goal
Command "goal": let a formula become the single goal.

class 
Goto
The "goto" command: goto an open proof state.

class 
Induction
Command "induction": induction on a univerally quantified NAT/INT variable.

class 
Instantiate
The "instantiate" command: instantiate a quantified formula.

class 
Lemma
The "lemma" command: import other formulas.

class 
Next
The "next" command: goto next open proof state.

class 
Open
The "open" command: display the list of open states.

class 
Option
The "option" command: set a system option.

class 
Prev
The "prev" command: goto previous open proof state.

class 
ProofCommandBase
Base class of proof commands.

class 
Proved
Pseudocommand "proved": indicate the termination of a proof branch.

class 
Redo
The "redo" command: goto an open proof state and redo its proof.

class 
Scatter
command "scatter": scatter proof state by repeated decomposition
and goalsplitting.

class 
Simplify
Command "simplify": simplify a proof state.

class 
Skolemize
Command "skolemize": skolemize universal formulas in goal position and
existential formulas in assumption position.

class 
Split
Command "split": split a proof state.

class 
TypeAxiom
The "typeaxiom" command: instantiate a quantified type axiom.

class 
Undo
The "undo" command: goto a closed proof state and undo its proof.
