Formulae that the proof assumes to be present on this branch (i.e., premisses of rules applied in the proof).
Formulae that the proof assumes to be present on this branch (i.e., premisses of rules applied in the proof). We assume that all formulae live in the antecedent.
The constraint resulting from this proof
The constraint resulting from this proof
Set of constants occurring in this certificate.
Set of constants occurring in this certificate. By default this will contain the set of all constants in sub-certificates, as well as constants in assumed formulas.
Constants bound by the root operator of the 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).
Formulae that are introduced into the antecedent by this rule application (one set for each subproof). This will implicitly simplify formulae (all simplifications that are built into the datastructures are carried out).
Certificate corresponding to a (possibly repeated) application of the strengthen rule: the inequality
weakInEq(0) >= 0
is strengthened to the equationsweakInEq(0) === 0
,weakInEq(0) === 1
, etc. and the inequalityweakInEq(0) >= eqCases
.