QuantifiedTree

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

final def asInstanceOf[T0]: T0

def bindingContext: BindingContext

def clone(): AnyRef

lazy val closingConstantFreedom: ConstantFreedom

The constants that can be considered free (resp., that have to be considered non-free) in this proof tree.

lazy val closingConstraint: Conjunction

The fully simplified closing constraint

def constantFreedom: ConstantFreedom

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

lazy val fixedConstantFreedom: Boolean

true if the sets of free constants have reached a fixed point

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

def newConstantFreedomForSubtree(cf: ConstantFreedom): ConstantFreedom

Given a new constant freedom for this proof tree, derive the corresponding freedom for the direct subtree.

final def notify(): Unit

final def notifyAll(): Unit

def order: TermOrder

val quan: Quantifier

val quantifiedConstants: Seq[ConstantTerm]

lazy val stepMeaningful: Boolean

true if there are chances that the closingConstraint of this tree changes by applying rules to any goal

lazy val stepPossible: Boolean

true if it is possible to apply rules to any goal in this tree

val subtree: ProofTree

val subtreeOrder: TermOrder

lazy val subtrees: Seq[ProofTree]

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

def toString(): String

def update(newSubtree: ProofTree, newConstantFreedom: ConstantFreedom): ProofTree

Replace the subtree and the constant freedom status with new values.

val vocabulary: Vocabulary

the vocabulary available at a certain node in the proof

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit