Validate that a derivation premise's expression tree conforms to the
structural rules in the v0.11.0 spec:
Root must be either a single variable expression for a variable bound
to the derived claim (naked form), or an implies/iff operator with
arity 2.
When the root is implies/iff:
position 0 (antecedent slot) is any valid expression tree.
position 1 (consequent slot) is exactly a variable expression for
a variable bound to the derived claim. No operator subtree, no
variable bound elsewhere, no formula wrapper.
A claim may bind more than one variable, and each of them stands for that
claim — so any of them satisfies the consequent slot.
Returns a TInvariantValidationResult with one violation per detected
rule break, all using DERIVATION_STRUCTURE_INVALID (the message
differentiates them).
This is a pure function — it takes a premise, its expressions, and the
argument's variables. It has no engine dependencies and no side effects.
Validate that a derivation premise's expression tree conforms to the structural rules in the v0.11.0 spec:
implies/iffoperator with arity 2.implies/iff:A claim may bind more than one variable, and each of them stands for that claim — so any of them satisfies the consequent slot.
Returns a
TInvariantValidationResultwith one violation per detected rule break, all usingDERIVATION_STRUCTURE_INVALID(the message differentiates them).This is a pure function — it takes a premise, its expressions, and the argument's variables. It has no engine dependencies and no side effects.