A B C D E F G H I J K L M N O P R S T U V W

A

add_escapes(String) - Method in class ParseException

Used to convert raw characters to their escaped version when these raw version cannot be used as part of an ASCII string literal.

addLayoutComponent(Component) - Method in class FillBoxLayout

Adds the specified component to the layout.

addRuleFrom(SpecialClause) - Method in class RuleTable

Makes a rule with the specified special clause if possible and add it to this table.

addToDefiniton(RewriteRule) - Method in class RuleTable

Puts a new rewrite rule at the definitions.

allLowerThan(Node) - Method in class NodeList

Test if all elements of this list are lower than a specified node.

applySubst(Substitution) - Method in class Conjecture

Applies a substitution map to this conjecture

applySubst(Substitution) - Method in class Node

Applies a substitution to this term.

applySubst(Substitution) - Method in class EqualList

Applies a substitution map to this list.

applySubst(Substitution) - Method in class Equality

Applies a substitution to this equality node.

applySubst(Substitution) - Method in class FunctionCallNode

Applies a substitution to this term.

applySubst(Substitution) - Method in class VariableNode

Applies a substitution to this node.

argument(int) - Method in class FunctionCallNode

Returns the argument of the call at the specified position.

arguments() - Method in class FunctionCallNode

Returns the arguments of the call.

axiomNumber() - Method in class SpecialClause

Returns the number of the axiom.

B

body() - Method in class Clause

Returns the body of an clause.

bot(Path) - Method in class Node

Computes bottom part of the term.

bot(Path) - Method in class FunctionCallNode

Computes bottom part of the term.

botPath() - Method in class Node

Compute MAXIMUN BOTTOM PATH.

botPath() - Method in class FunctionCallNode

Compute MAXIMUN BOTTOM PATH.

C

canUse(SpecialClause) - Method in class Conjecture

Tests if a specified rule could be used to simplify this conjecture.

caseSimplify(Conjecture) - Method in class RewriteSystem

Applies a case rewrite step on a specified conjecture.

caseSimplify(ConjectureList) - Method in class RewriteSystem

Applies a case rewrite step on each conjecture of a specified list.

changed - Variable in class FileFrame

Indicates if file have changed.

changedUpdate(DocumentEvent) - Method in class EnableListener

Disables all buttons.

Clause - class Clause.

This class implements a clause.

Clause(EqualList, EqualList) - Constructor for class Clause

Constructor of a clause.

ClauseList - class ClauseList.

This class represents a list of clauses

ClauseList() - Constructor for class ClauseList

clone() - Method in class RewriteSystem

Creates and returns a copy of this object.

compile() - Method in class RewriteSystem

Compiles this rewrite system.

compile(File) - Method in class Compiler

Compile a specified file.

compiler - Variable in class FileFrame

Compiler of the file.

Compiler - class Compiler.

This class implements a compiler.

Compiler() - Constructor for class Compiler

conditions() - Method in class Clause

Returns the conditions of an clause.

conj - Variable in class Clause

Both side of the clause.

Conjecture - class Conjecture.

This class implements a conjecture.

Conjecture(Equality) - Constructor for class Conjecture

Constructor of a conjecture.

Conjecture(EqualList, EqualList) - Constructor for class Conjecture

Constructor of a conjecture.

ConjectureList - class ConjectureList.

This class represents a list of special clauses

ConjectureList() - Constructor for class ConjectureList

constant() - Method in class Type

Returns the constant of the type.

contains(Node) - Method in class NodeList

Tests if this list contains a specified node.

currentToken - Variable in class ParseException

This is the last token that has been consumed successfully.

D

DEC(RuleTable, Node) - Static method in class Equality

Makes the decoupage of a term according to all prefix of top and bottom path.

declareFunction(String, boolean, boolean, Type, SortList) - Method in class IdentTable

Declares a new function in this table Throw an error if the function is allready declared.

declareType(String) - Method in class IdentTable

Declares a new type in this table.

disj - Variable in class Clause

Both side of the clause.

DOWN - Static variable in class FillBoxLayout

Place components from south to north.

E

Empty - Static variable in class Path

Empty path

emptyBody() - Method in class Clause

Indicates if this clause posses an empty body.

EnableListener - class EnableListener.

This class implements a document listener whose toggle enabled / disabled a list of button.

EnableListener(AbstractButton) - Constructor for class EnableListener

Constructs a new EnableListener with a first button.

enables(boolean) - Method in class EnableListener

Enables or disables all buttons.

eol - Variable in class ParseException

The end of line string for this machine.

equal(Type) - Method in class Type

Indicates whether some other type is corresponding to this one.

Equality - class Equality.

This class implements an equality between two nodes.

Equality(Node, Node) - Constructor for class Equality

Constructor of the equality node.

EqualList - class EqualList.

This class represents a list of equalities in a clause.

EqualList() - Constructor for class EqualList

equals(NodeList) - Method in class NodeList

Tests if some other node list is "equal to" this one.

equals(Object) - Method in class Clause

Tests if some other object is "equal to" this one.

equals(Object) - Method in class Equality

Tests if some other object is "equal to" this one.

equals(Object) - Method in class FunctionCallNode

Tests if some other object is "equal to" this one.

equals(Object) - Method in class VariableNode

Tests if some other object is "equal to" this node.

ErrType - Static variable in class Type

Error Type.

expectedTokenSequences - Variable in class ParseException

Each entry in this array is an array of integers.

F

file - Variable in class FileFrame

Associated File.

FileFrame - class FileFrame.

This class implements a frame which edits a file.

FileFrame(File) - Constructor for class FileFrame

Constructor of the editting frame.

FillBoxLayout - class FillBoxLayout.

This layout allows multiple components to be layed out either vertically or horizontally with the same size.

FillBoxLayout(int, int) - Constructor for class FillBoxLayout

Creates a FillBoxLayout.

find(Node) - Method in class Node

Find the path to a substerm in a term.

find(Node) - Method in class FunctionCallNode

Find the path to a substerm in a term.

forceHypothesis(ConjectureList) - Method in class RewriteSystem

Applies once hypothesis even if it's not a Rewrite Rule for each conjecture of a specified list.

fromFile(File) - Static method in class Nice

Puts a file in a String.

Function - class Function.

This class represents a function indentifier

Function(String, boolean, boolean, Type, SortList) - Constructor for class Function

Constructor of the function.

FunctionCallNode - class FunctionCallNode.

This class implements a function call node.

FunctionCallNode(Function, NodeList) - Constructor for class FunctionCallNode

Constructor of the function call node.

FunctionDefinition - class FunctionDefinition.

This class represents a definition of a function as a list of rewrite axiom.

FunctionDefinition() - Constructor for class FunctionDefinition

G

generalize(Conjecture) - Method in class RewriteSystem

Applies a generalize step on a specified conjecture.

generalize(ConjectureList) - Method in class RewriteSystem

Applies the generalize rule on a specified list of conjecture.

generates(Conjecture) - Method in class RewriteSystem

Applies the generate rule on a specified conjecture.

generates(ConjectureList) - Method in class RewriteSystem

Applies the generate rule on a specified list of conjecture.

genSplitStep(ConjectureList) - Method in class RewriteSystem

Makes one cycle of spliting method.

genStep(ConjectureList) - Method in class RewriteSystem

Make one cycle.

genTrack - Variable in class RewriteSystem

getAllDefinitions() - Method in class RuleTable

Returns a list of all definitions in this table.

getAsPart(Node) - Method in class Node

Tests if this term as an other as part.

getAsPart(Node) - Method in class FunctionCallNode

Tests if this function call node as an other as part.

getAxiom(int) - Method in class FunctionDefinition

Returns the definition at the specified position in this list.

getAxioms() - Method in class RewriteSystem

Returns the list of axioms of the system.

getClause(int) - Method in class SCList

Returns the clause at the specified position in this list.

getConjecture(int) - Method in class ConjectureList

Returns the clause at the specified position in this list.

getCP() - Method in class Function

Get contextual position of the function.

getDefinition(Function) - Method in class RuleTable

Gets the definition of a specified function in this table.

getDP() - Method in class Function

Get downward position of the function.

getEquality(int) - Method in class EqualList

Returns the node at the specified position in this list.

getFunction(String) - Method in class IdentTable

Gets a function in this table.

getFunctions(Type) - Method in class RewriteSystem

Gets all functions with a specified type of this system.

getHypotheses() - Method in class RewriteSystem

Return the list of axioms of the system.

getImage(Object) - Method in class Substitution

Returns the node to which the specified node is mapped.

getIP() - Method in class Function

Get one induction position of this function.

getLemmas() - Method in class RewriteSystem

Returns the list of lemmas of the system.

getMessage() - Method in class ParseException

This method has the standard behavior when this object has been created using the standard constructors.

getMessage() - Method in class SemanticException

Returns the error message string of this throwable object.

getName() - Method in class Ident

Accessor of the name of the identifier.

getNode(int) - Method in class NodeList

Returns the node at the specified position in this list.

getNumber(Type) - Method in class Node

Returns number of sub term with a specified type of this node.

getNumber(Type) - Method in class FunctionCallNode

Returns number of sub term with a specified type of this node.

getNumber(Type) - Method in class VariableNode

Returns number of sub term with a specified type of this node.

getOrderNum() - Method in class Function

Accessor of the order number of the function.

getParamsType() - Method in class Function

Returns list of types of parameters.

getPositions() - Method in class RewriteSystem

Returns a string representation of all induction positions of functions defined in this system.

getPositions() - Method in class RuleTable

Returns a string representation of all induction positions of functions defined in this table.

getRA() - Method in class Function

Get reflexive argument position of the function.

getsIn(EqualList) - Method in class Conjecture

Tests if the conjecture gets a specified list of equalities in its conditions.

getSort(int) - Method in class SortList

Returns the sort at the specified position in this list.

getSorts() - Method in class RewriteSystem

Gets all sorts of this system.

getSP() - Method in class Function

Get transversal position of the function.

getSpecialPosition() - Method in class RewriteSystem

Returns a string representation of all special positions of functions defined in this table.

getSubterm(Path) - Method in class Node

Gives subterm at specified path.

getSubterm(Path) - Method in class FunctionCallNode

Get subterm at specified path.

getTestSets() - Method in class RewriteSystem

Returns a string representation of all test sets of this system.

getTP() - Method in class Function

Get topward position of the function.

getTwo(Type) - Method in class FunctionCallNode

Tests if this term got two sub term of a specified type.

getType() - Method in class Node

Returns the type of the term.

getType() - Method in class Function

Returns the return type of the function.

getType() - Method in class Variable

Returns the type of the variable.

getType() - Method in class FunctionCallNode

Returns the type of the term.

getType() - Method in class VariableNode

Returns the type of the node.

getType(String) - Method in class IdentTable

Get a type in this table.

getVariables(Set) - Method in class Node

Extends the set of variables apparing in this term.

getVariables(Set) - Method in class FunctionCallNode

Extends the set of variables with the ones of this term.

getVariables(Set) - Method in class VariableNode

Extends the set of variables with this one.

greaterThan(Node) - Method in class Node

Tests if this term is greater (in order) than an other.

greaterThan(Node) - Method in class FunctionCallNode

Tests if this function call node is greater (in order) than an other term.

greaterThan(Node) - Method in class VariableNode

Tests if this variable node is greater (in order) than a function call node.

H

hashCode() - Method in class VariableNode

Returns a hash code for this variable node.

Hypothese - interface Hypothese.

This interface represent an hypothese.

HYPOTHESE_NUM - Static variable in class Clause

Clause number for an hypothese.

hypothese() - Method in class Conjecture

Returns hypothese of the conjecture.

hypotheseOf() - Method in interface Hypothese

Returns father hypothese of this one.

I

Ident - class Ident.

This class provides a skeletal implementation of an indentifier.

Ident(String) - Constructor for class Ident

Constructor of the identifier.

identifier() - Method in class FunctionCallNode

Returns the identifier of the function.

identifier() - Method in class VariableNode

Returns the identifier of the variable.

IdentTable - class IdentTable.

This class implement the table of ident of the parser.

IdentTable() - Constructor for class IdentTable

incrNumGene() - Method in class Type

Increments and returns number of generated variables from this type.

inductionPosition(int) - Method in class Function

Indicates if a specified position is an induction position.

inductionPositions() - Method in class Function

Returns a List representation of induction position of this function.

inductionVariables() - Method in class Conjecture

Returns the list of induction variable of this conjecture.

inductionVariables(Map) - Method in class Equality

Extends the map of induction variable with the ones of this equality.

inductionVariables(Map, int) - Method in class Node

Extends the map of induction variable with the ones of this term.

inductionVariables(Map, int) - Method in class FunctionCallNode

Extends the map of induction variable with the ones of this term.

inductionVariables(Map, int) - Method in class VariableNode

Extends the map of induction variable with the one of this term.

init() - Method in class RewriteSystem

Inits rewrite system.

initMenu() - Method in class FileFrame

Inits menu of this frame.

insertUpdate(DocumentEvent) - Method in class EnableListener

Disables all buttons.

isBoolean() - Method in class Type

Indicates if this type has boolean property.

isConstant() - Method in class Node

Indicates if this term is a constant.

isConstant() - Method in class Function

Indicates if this function symbol is a constant.

isConstant() - Method in class FunctionCallNode

Indicates if this term is a constant.

isConstructor() - Method in class Function

Indicates if this function symbol is a constructor.

isConstructorRooted() - Method in class Node

Tests if this term is rooted by a constructor symbol.

isConstructorRooted() - Method in class FunctionCallNode

Tests if this term is rooted by a constructor symbol.

isGround() - Method in class Node

Indicates if this term is ground.

isInfix() - Method in class Function

Indicates if this function is infix.

isMonomorphic() - Method in class RewriteSystem

Says if this system is monomorphic.

isNFEqual(RuleTable) - Method in class Conjecture

Tests if this conjecture is an equality that normal form

isNFEqual(RuleTable) - Method in class Equality

Tests if this normal form of both sides are equals.

isTotology() - Method in class Conjecture

Tests if this conjecture is a totology.

isTotology(Conjecture) - Method in class RewriteSystem

Tests if a specified conjecture is a totology.

J

jc - Variable in class FileFrame

One for all file chooser.

K

keep(String) - Method in class IdentTable

Gets a Ident in this table.

L

lastUsed() - Method in class RuleTable

Returns last rule used.

LEFT - Static variable in class FillBoxLayout

Place components from west to east.

leftSide() - Method in class Equality

Returns the left hand side of the equality.

leftSide() - Method in class RewriteRule

Returns the left side of body of this rule.

LEMMA_NUM - Static variable in class Clause

Clause number for a lemma.

length() - Method in class Path

Returns the length of the path.

lexiGreaterThan(NodeList) - Method in class NodeList

Tests if this list is greater in lexicographic order than some other.

lowerThan(Function) - Method in class Function

Tests if this function is before (in order) than an other.

lowerThan(Node) - Method in class EqualList

Tests if each both sides of equalities in this list are lower than a specified term.

lowerThan(Node) - Method in class Equality

Tests if both sides of this equality are lower than a specified term.

M

main(String[]) - Static method in class Nice

Main method of the program.

makeFilter(Node, Node) - Static method in class Substitution

Returns a filter between two nodes, if possible.

makeFilter(Node, Substitution) - Method in class Node

Constructs a filter between this term and an other.

makeFilter(Node, Substitution) - Method in class FunctionCallNode

Constructs a filter between this function call node and an other one.

makeFilter(Node, Substitution) - Method in class VariableNode

Constructs a filter between this variable node and an other node.

makeHypotheseFrom(Conjecture) - Method in class RuleTable

Makes an hypothese with the specified conjecture and add it to this table if the clause is oriented, add to hypothesis table if semi-oriented or just make an hypothese.

MAX_PRIORITY - Static variable in class Node

The highest priority for an induction variable.

MIN_PRIORITY - Static variable in class Node

The lowest priority for an induction variable.

N

nbt(Path) - Method in class Node

Computes nbt part of the term.

nbt(Path) - Method in class FunctionCallNode

Computes nbt part of the term.

next - Variable in class Path

Rest of the path.

nf(RuleTable, Node) - Static method in class Equality

Returns the normal form of a specified term.

Nice - class Nice.

This class implements the main method of the program.

Nice() - Constructor for class Nice

Node - class Node.

This class provides a skeletal implementation of a term.

Node() - Constructor for class Node

NodeList - class NodeList.

This class represents a list of node.

NodeList() - Constructor for class NodeList

normalForm(Conjecture) - Method in class RewriteSystem

Returns the normal form of a specified conjecture.

ntp(Path) - Method in class Node

Computes npt part of the term.

ntp(Path) - Method in class FunctionCallNode

Computes npt part of the term.

num - Variable in class SpecialClause

Clause number in specification.

num - Variable in class Path

Number of the argument.

num(int) - Static method in class Clause

Returns a representation of a clause number.

numAsPart(Node) - Method in class Node

Counts how many times this term as an other as part.

numAsPart(Node) - Method in class FunctionCallNode

Counts how many times this term as an other as part.

O

oneSplitStep(ConjectureList) - Method in class RewriteSystem

Makes one step of spliting method.

oneStep(ConjectureList) - Method in class RewriteSystem

Rewrite list of conjecture.

openFile(File) - Static method in class Nice

Creates a buffered input strem from a file name.

oppositeOf(Node) - Method in class Type

Gives opposite of a specified boolean constant.

oriented() - Method in class Clause

Returns an orientation of this clause if possible.

P

parse(File) - Static method in class Nice

ParseException - exception ParseException.

This exception is thrown when parse errors are encountered.

ParseException() - Constructor for class ParseException

The following constructors are for use by you for whatever purpose you can think of.

ParseException(String) - Constructor for class ParseException

ParseException(Token, int[][], String[]) - Constructor for class ParseException

This constructor is used by the method "generateParseException" in the generated parser.

parsePositions(boolean) - Method in class RuleTable

Parse positions in function definitions.

Path - class Path.

This class implements a path in a term.

Path(int, Path) - Constructor for class Path

Constructor of the path.

pattern(ConjectureList) - Method in class RewriteSystem

Apply pattern splitting on a specified list of conjecture.

patterns(RuleTable) - Method in class Equality

Use patterns to split the equality.

prefix(int) - Static method in class Clause

Returns a representation of a clause number between brackets.

prefix(int) - Method in class Path

Returns the prefix of the path of a specified length.

print() - Method in class ConjectureList

Prints a representation of this list of conjecture.

putTitle() - Method in class FileFrame

Updates title of frame according with associated file.

R

remove(SCList) - Method in class RuleTable

Removes all rewrite rules of a specified list from this table.

removesEquals(ConjectureList) - Method in class RewriteSystem

Removes equalities that normal form of both sides are equals.

removesTotology(ConjectureList) - Method in class RewriteSystem

Removes totologies in a specified list of conjectures.

removeUpdate(DocumentEvent) - Method in class EnableListener

Disables all buttons.

remplaceSubterm(Path, Node) - Method in class Node

Remplace subterm at specified path by an other.

remplaceSubterm(Path, Node) - Method in class FunctionCallNode

Remplaces subterm at specified path by an other.

RewriteRule - class RewriteRule.

This class implements an oriented rule.

RewriteSystem - class RewriteSystem.

This class implements a rewrite system.

RewriteSystem(String, SCList, IdentTable) - Constructor for class RewriteSystem

Constructor of the rewrite system.

RIGHT - Static variable in class FillBoxLayout

Place components from east to west.

rightSide() - Method in class Equality

Returns the right hand side of the equality.

rightSide() - Method in class RewriteRule

Returns the right side of body of this rule.

RuleTable - class RuleTable.

This class implement the table of oriented rules of a system.

RuleTable() - Constructor for class RuleTable

Constructor of the table of rule.

RuleTable(Hypothese) - Constructor for class RuleTable

Constructor from only one Hypothese.

S

SCList - class SCList.

This class represents a list of special clauses

SCList() - Constructor for class SCList

SemanticException - exception SemanticException.

Thrown when an syntaxic error is detected in a system.

SemanticException(String) - Constructor for class SemanticException

Constructs a SemanticException with the specified detail message.

SemanticException(String, Node) - Constructor for class SemanticException

Constructs a SemanticException with the specified detail message and the node with problem.

SemanticException(Type, Type, Node) - Constructor for class SemanticException

Constructs a SemanticException with types in conflict.

semiOriented() - Method in class Clause

Returns a semi-orientation of this close.

setConjecture(File) - Static method in class Nice

setCP(int) - Method in class Function

Set a specified position as an contextual position for the function.

setDP(int) - Method in class Function

Set a specified position as an downward position for the function.

setInductionPosition(int) - Method in class Function

Set a specified position as an induction position of the function.

setLastUsed(RewriteRule) - Method in class RuleTable

Sets last rule used.

setLemmas(SCList) - Method in class RewriteSystem

Sets Lemmas of rewrite system.

setOrderNum(int) - Method in class Function

Sets the order number of the function.

setRA(int) - Method in class Function

Set a specified position as an reflexive argument position for a constructor.

setSP(int) - Method in class Function

Set a specified position as an transversal position for the function.

setTestSet(NodeList) - Method in class Type

Sets the test set of the type to a specified list of term.

setTestSet(Type, NodeList) - Method in class RewriteSystem

Sets a test set of a speficied type.

setTP(int) - Method in class Function

Set a specified position as an topward position for the function.

setTypes() - Method in class ConjectureList

Sets types in each Conjecture.

setTypes() - Method in class RewriteSystem

Sets types in whole rewrite system.

sidesEqual() - Method in class Equality

Indicates whether this equality is a syntaxic equality.

simplify(Conjecture) - Method in class RewriteSystem

Applies a rewrite step on a specified conjecture.

simplify(ConjectureList) - Method in class RewriteSystem

Applies a rewrite step on each conjecture of a specified list.

simplify(RuleTable) - Method in class Conjecture

Applies a rewrite step on this conjecture.

simplify(RuleTable, Conjecture) - Method in class VariableNode

Applies a rewrite step on this node in a specified conjecture.

SortList - class SortList.

This class represents a list of types of function parameters.

SortList() - Constructor for class SortList

SpecialClause - class SpecialClause.

This class implements an special clause (axioms, hypotheses or lemma).

SpecialClause(EqualList, EqualList, int) - Constructor for class SpecialClause

Constructor of a special clause.

specialConstructor - Variable in class ParseException

This variable determines which constructor was used to create this object and thereby affects the semantics of the "getMessage" method (see below).

split(ConjectureList) - Method in class RewriteSystem

Split a specified list of conjecture.

split(RuleTable) - Method in class Equality

Split the equality.

splitingMotor(ConjectureList) - Method in class RewriteSystem

Direct spliting motor.

splitTrack - Variable in class RewriteSystem

stepTrack - Variable in class RewriteSystem

Substitution - class Substitution.

This class represents a substitution map between nodes.

Substitution() - Constructor for class Substitution

Constructs a new, empty substitution map.

Substitution(Node, Node) - Constructor for class Substitution

Constructs a new substitution map with only one mapping and very little capacity.

SubstitutionStop - exception SubstitutionStop.

Thrown when an substitution map is impossible to make.

SubstitutionStop() - Constructor for class SubstitutionStop

T

test(File) - Method in class Compiler

Compile and test a specified file.

testSet() - Method in class Type

Returns test set of the type.

TextDialog - class TextDialog.

This class implements a dilog which contains just a text.

textualMotor(ConjectureList) - Method in class RewriteSystem

Direct textual motor.

toFile() - Method in class FileFrame

Returns string representation of the fields.

toggles() - Method in class Equality

If left (or right) sides is a boolean constant toggles it.

toggles(ConjectureList) - Method in class RewriteSystem

Toggles boolean equalities from conditions to body on each conjecture of a specified list.

tokenImage - Variable in class ParseException

This is a reference to the "tokenImage" array of the generated parser within which the parse error occurred.

top(Path) - Method in class Node

Computes top part of the term.

top(Path) - Method in class FunctionCallNode

Computes top part of the term.

topPath() - Method in class Node

Compute MAXIMUN TOP PATH.

topPath() - Method in class FunctionCallNode

Compute MAXIMUN TOP PATH.

toString() - Method in class Ident

Returns a string representation of this identifier.

toString() - Method in class Clause

Returns a string representation of this clause.

toString() - Method in class ConjectureList

Returns a string representation of this conjecture list.

toString() - Method in class Path

Returns string representation of the path.

toString() - Method in class EqualList

Returns a string representation of this list.

toString() - Method in class Equality

Returns a string representation of this equality node.

toString() - Method in class RewriteSystem

Returns a string representation of the rewrite system rules.

toString() - Method in class Type

Returns a string representation of this identifier.

toString() - Method in class Function

Returns a string representation of this function.

toString() - Method in class SCList

Returns a string representation of this special clause list with semi-colon separator.

toString() - Method in class Variable

Returns a string representation of this variable.

toString() - Method in class FunctionCallNode

Returns a string representation of this function call node.

toString() - Method in class VariableNode

Returns a string representation of this variable node.

toStringIndent() - Method in class ConjectureList

Returns a string representation of this conjecture list.

toStringInfix() - Method in class Node

Returns a string representation of this term when it is an argument of an infix call.

toStringInfix() - Method in class FunctionCallNode

Returns a string representation of this function call node when it is an argument of an infix call.

toStringN() - Method in class SpecialClause

Returns a string representation of this clause.

toStringN() - Method in class Conjecture

Returns a string representation of this clause with axiom number.

toStringN() - Method in class ConjectureList

Returns a string representation of this conjecture list.

toStringN() - Method in class RewriteRule

Returns a string representation of this rule.

track - Variable in class RewriteSystem

trueRule() - Method in class RewriteRule

Says if it is a true rewrite rule (not hypothesis).

Type - class Type.

This class represents a type indentifier

Type(String) - Constructor for class Type

Constructor of the type.

U

UnivType - Static variable in class Type

Universal Type.

UP - Static variable in class FillBoxLayout

Place components from north to south.

update() - Method in class FileFrame

Updates fields according current file.

V

Variable - class Variable.

This class represents a variable indentifier.

Variable(String, Type) - Constructor for class Variable

Constructor of the variable.

Variable(Type) - Constructor for class Variable

Construct a new variable from a specified type.

VariableNode - class VariableNode.

This class implements a variable node.

VariableNode(Variable) - Constructor for class VariableNode

Constructor of the variable node.

W

withNewVariables() - Method in class Node

Remplaces varia1bles in term by new variables.

A B C D E F G H I J K L M N O P R S T U V W