import type { TViolation } from "../types.js";
import type { TValidatorContext } from "./context.js";
/**
 * E-1 — Variadic operator arity floor. `and`, `or` and `xor` each have at
 * least two children. (Unary `not`/`formula` are constrained Structurally
 * per S-12/S-13; binary `implies`/`iff` per S-8.)
 */
export declare function validateE1(ctx: TValidatorContext): readonly TViolation[];
/**
 * E-3 — Variable binding resolves. Every variable's claim or premise
 * reference points at an existing target. External premise bindings
 * (`boundArgumentId !== argument.id`) resolve in a different argument
 * and are out of scope here — those targets aren't in this context.
 */
export declare function validateE3(ctx: TValidatorContext): readonly TViolation[];
/**
 * E-4 — Axiomatic-binding constraint. Axiomatic-bound variables must not
 * be assigned in the caller's evaluation input. This is a **runtime
 * guard** on caller-supplied input, not an AST invariant — the check
 * runs inside `ArgumentEngine.evaluate` / `.checkValidity` and rejects
 * pre-flight with the engine-error code `AXIOM_VARIABLE_ASSIGNMENT_FORBIDDEN`.
 * The AST-level validator cannot detect E-4 from the argument tree alone
 * and intentionally returns an empty array.
 */
export declare function validateE4(_ctx: TValidatorContext): readonly TViolation[];
/**
 * E-5 — Derivation premise consequent present. Every `type='derivation'`
 * premise's expression tree includes a variable bound to its
 * `derivedClaimId`. Naked-Q satisfies this (the lone variable at the
 * root *is* the consequent).
 */
export declare function validateE5(ctx: TValidatorContext): readonly TViolation[];
/**
 * E-6 — Claim-derivation pairing. For every `type='normal'` claim
 * referenced in the argument, at most one `type='derivation'` premise
 * exists with `derivedClaimId` matching that claim. Zero is valid (the
 * post-publish-pruning state); two or more is the violation.
 */
export declare function validateE6(ctx: TValidatorContext): readonly TViolation[];
/**
 * E-7 — Argument has conclusion premise. An argument that has at least
 * one premise has exactly one premise designated as the conclusion via
 * `roleState.conclusionPremiseId`. A brand-new argument with zero
 * premises is exempt.
 *
 * As of 1.0.2 the engine itself guards the "non-empty argument always
 * has a conclusion" invariant at the mutation surface: the public
 * paths that previously let callers clear or remove the conclusion
 * out from under a non-empty argument (`clearConclusionPremise`,
 * `removePremise` on the current conclusion when others remain) now
 * no-op or auto-promote rather than break the invariant. E-7 stays
 * as the validate-time safety net for snapshot loads and direct
 * data-shape construction — paths the engine cannot guard at
 * mutation time.
 */
export declare function validateE7(ctx: TValidatorContext): readonly TViolation[];
export declare function validateEvaluable(ctx: TValidatorContext): readonly TViolation[];
//# sourceMappingURL=evaluable.d.ts.map