import type { TCoreDerivationPremise, TCorePropositionalExpression, TCorePropositionalVariable } from "../schemata/propositional.js";
import type { TInvariantValidationResult } from "../types/validation.js";
/**
 * 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.
 */
export declare function validateDerivationStructure(premise: TCoreDerivationPremise, expressions: TCorePropositionalExpression[], variables: TCorePropositionalVariable[]): TInvariantValidationResult;
//# sourceMappingURL=derivation-validation.d.ts.map