import type { TViolation } from "../types.js";
import type { TValidatorContext } from "./context.js";
/**
 * D-1 — Derivation premise canonical shape. Every `type='derivation'`
 * premise's tree matches one of two canonical forms:
 *
 * - **Naked-Q**: a single `variable` expression at the root, bound to
 *   `derivedClaimId`.
 * - **Populated**: root `IMPLIES` with consequent at position 1 (variable
 *   bound to `derivedClaimId`); antecedent at position 0, after peeling
 *   formula buffers, is either a single claim-bound variable
 *   (citation/axiomatic) — see D-2 — or an `OR` whose children (each
 *   peeled of formulas) are all claim-bound variables of the same
 *   grounding type. IFF at root fails D-1 (Structurally allowed per
 *   S-14; D-1 narrows derivation premise root to IMPLIES).
 *
 * Wrong-root-operator cases (and/or/not/formula at root) are already
 * caught by Structural S-14; D-1 silently skips them.
 */
export declare function validateD1(ctx: TValidatorContext): readonly TViolation[];
/**
 * D-2 — Single-citation derivation form. If a derivation premise has a
 * populated form whose antecedent (peeled of formula buffers) is an `OR`
 * with exactly one child (also peeled of formulas), that's wrong — the
 * canonical single-grounding form is `IMPLIES(claim-var, Q)` without the
 * `OR` wrapper.
 *
 * Note: a 1-child `OR` also fails E-1 (variadic ≥ 2) and P-4
 * (single-child binary). D-2 is the Derivable-tier UI hint specifically
 * naming the "drop the OR wrapper" remediation.
 */
export declare function validateD2(ctx: TValidatorContext): readonly TViolation[];
/**
 * D-3 — No mixing axioms and citations in one derivation. For each
 * derivation premise's populated form, collect all claim-bound variables
 * in the antecedent subtree. If they bind to claims of more than one
 * grounding type (citation vs axiomatic), emit D-3.
 *
 * Formula nodes are traversed transparently by
 * `collectVariableExpressionsInSubtree`'s plain DFS descent — no
 * explicit `peelFormulas` call needed for D-3, since the DFS visits
 * formula descendants like any other node and the variable collector
 * picks up the claim-bound variables regardless of nesting depth.
 */
export declare function validateD3(ctx: TValidatorContext): readonly TViolation[];
/**
 * D-4 — Axiomatic claim placement. Variables bound to `type='axiomatic'`
 * claims appear only in the antecedent of a derivation premise, never in
 * freeform premises and never in a derivation premise's consequent slot.
 */
export declare function validateD4(ctx: TValidatorContext): readonly TViolation[];
/**
 * D-5 — Citation claim placement. Mirror of D-4 for citation claims.
 */
export declare function validateD5(ctx: TValidatorContext): readonly TViolation[];
/**
 * D-6 — Derivation premise role. Every `type='derivation'` premise has
 * `role='supporting'` — concretely, `roleState.conclusionPremiseId !==
 * premise.id`.
 */
export declare function validateD6(ctx: TValidatorContext): readonly TViolation[];
export declare function validateDerivable(ctx: TValidatorContext): readonly TViolation[];
//# sourceMappingURL=derivable.d.ts.map