AndTree

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

lazy val height: Int

final def isInstanceOf[T0]: Boolean

val left: ProofTree

final def ne(arg0: AnyRef): Boolean

def newConstantFreedomForSubtrees(cf: ConstantFreedom): (ConstantFreedom, ConstantFreedom)

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

final def notify(): Unit

final def notifyAll(): Unit

def order: TermOrder

val partialCertificate: PartialCertificate

val right: ProofTree

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

lazy val subtrees: Seq[ProofTree]

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

def toString(): String

def update(newLeft: ProofTree, newRight: ProofTree, newPartialCertificate: PartialCertificate): ProofTree

def update(newLeft: ProofTree, newRight: ProofTree, newConstantFreedom: ConstantFreedom): ProofTree

def update(newSubtrees: Seq[ProofTree]): ProofTree

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