ProofTreeOneChild

abstract val closingConstantFreedom: ConstantFreedom

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

abstract val closingConstraint: Conjunction

The fully simplified closing constraint

abstract val fixedConstantFreedom: Boolean

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

abstract def newConstantFreedomForSubtree(cf: ConstantFreedom): ConstantFreedom

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

abstract val stepMeaningful: Boolean

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

abstract val subtree: ProofTree

abstract val subtreeOrder: TermOrder

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

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

abstract val vocabulary: Vocabulary

the vocabulary available at a certain node in the proof

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

final def asInstanceOf[T0]: T0

def bindingContext: BindingContext

def clone(): AnyRef

def constantFreedom: ConstantFreedom

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

def order: TermOrder

lazy val stepPossible: Boolean

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

lazy val subtrees: Seq[ProofTree]

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

def toString(): String

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit