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 the derived
claim's variable (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 the variable expression
for the derived claim's variable. No operator subtree, no other
variable, no formula wrapper.
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: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.