Formulae that the proof assumes to be present on this branch (i.e., premisses of rules applied in the proof).
The constraint resulting from this proof
Set of constants occurring in this certificate.
Constants bound by the root operator of the certificate.
Formulae that are introduced into the antecedent by this rule application (one set for each subproof).