The constants that can be considered free (resp., that have to be considered non-free) in this proof tree.
The fully simplified closing constraint
true if the sets of free constants have reached a fixed point
Given a new constant freedom for this proof tree, derive the corresponding freedom for the direct subtree.
true if there are chances that the
closingConstraint of this tree changes by applying rules
to any goal
true if it is possible to apply rules to any goal in this
Replace the subtree and the constant freedom status with new values.
the vocabulary available at a certain node in the proof