Term

def args : List[Term]

Returns the list of arguments if this term is a function and java.lang.UnsupportedOperationException otherwise.

def isVar : Boolean

Returns true if this term is a variable and false otherwise.

def root : Either[V, F]

Returns scala.Left(variable_name) if the root symbol of this term is a variable and scala.Right(function_name) otherwise.

def != (arg0: AnyRef): Boolean

def != (arg0: Any): Boolean

def ## (): Int

def == (arg0: AnyRef): Boolean

def == (arg0: Any): Boolean

def apply (s: Subst): Term

Returns this term after the substitution s was applied.

def apply (p: Pos): Term

Returns the subterm of this term at position p.

def asInstanceOf [T0] : T0

def byRule (rs: TRS): Option[R]

Returns the first rule from the term rewrite system rs which may be used to rewrite this term and scala.None if there is no such rule in rs.

def clone (): AnyRef

def contains (that: Term): Boolean

Returns true if some subterm of this term subsumes that term.

def contract (irs: List[()]): (Int, Term)

def contract (rs: TRS): Term

Returns the contraction of this term and some rule in the term rewrite system rs if it exists and this term otherwise.

def contract (r: R): Term

Returns the term you get when applying the matching substitution from this term and the left-hand side of the rule r to the right-hand side of r.

def depth : Int

Returns the depth of the syntax tree of this term.

def eq (arg0: AnyRef): Boolean

def equals (arg0: Any): Boolean

def finalize (): Unit

def freshVars (): Subst

Returns a substitution from all variables in this term to fresh variables.

def funs : Set[F]

Returns a set of all function symbol names contained in this term.

def getClass (): java.lang.Class[_]

def hashCode (): Int

def irewritableAt (irs: List[()]): Option[Pos]

def irewritableWithSubst (ir: ()): Option[Subst]

def irewriteStep (irs: List[()]): Option[(Int, Term)]

def isGround : Boolean

Returns true if this term contains no variables and false otherwise.

def isInstanceOf [T0] : Boolean

def isNF (rs: TRS): Boolean

Returns true if this term is in normal form with respect to the term rewrite system rs and 'false' otherwise.

def isReducible (rs: TRS): Boolean

def matcheLs (ts: List[Term]): Boolean

Returns true if this term matches at least one of the terms in ts.

def matches (that: Term): Boolean

Returns true if this term matches that term and false otherwise.

def mmatch (that: Term): Subst

Returns a matching substitution of this and that term if they can be matched.

def ne (arg0: AnyRef): Boolean

def notify (): Unit

def notifyAll (): Unit

def poss : Set[Pos]

Returns the set of all positions, including the root position epsilon in this term.

def possf : Set[Pos]

Returns the set of all function positions in this term.

def possv : Set[Pos]

Returns the set of all variable positions in this term.

def reduce (rs: TRS): Option[Term]

A synonym for rewriteStep.

def reducibleByRule (rs: TRS): Option[R]

def rewrite (rs: TRS): Term

Returns the resulting term if this term may be rewritten with respect to the term rewrite system rs and this term otherwise.

def rewriteStep (rs: TRS): Option[Term]

Returns the term you get when rewriting this term one time with respect to the term rewrite system rs and scala.None if no rewrite step is possible.

def rewriteToNF (itrs: ITRS): List[(Term, Int, Term)]

def size : Int

Returns the number of variables and function symbols contained in this term.

def strlen : Int

Returns the length of the nice string version of this term (including whitespaces).

def subsums (that: Term): Boolean

Returns true if that term mathes this term.

def subterm (that: Term): Boolean

Returns true if this term is a proper subterm of that term and false otherwise.

def subtermeq (that: Term): Boolean

Returns true if this term is a proper subterm of or equal to that term and false otherwise.

def subterms : Set[Term]

Returns the set of all subterms (including this term itself).

def synchronized [T0] (arg0: ⇒ T0): T0

def toHtmlString : String

Returns a html string of this term where variables are enclosed in <font>-tags with blue color.

def toNiceString : String

Returns a nicer string representation of this term where variables are colored blue.

def toString (): String

Returns the string representation of this term.

def unifiable (that: Term): Boolean

Returns true if this and that term are unifiable and false otherwise.

def unify (that: Term): Subst

Returns a unifying substitution of this and that term if they are unifiable.

def update (p: Pos, s: Term): Term

Returns this term where only the subterm at position p was replaced with term s.

def variantOf (that: Term): Boolean

Returns true if this term is a variant of that term and false otherwise.

def vars : Set[V]

Returns a set of all variable names contained in this term.

def wait (): Unit

def wait (arg0: Long, arg1: Int): Unit

def wait (arg0: Long): Unit