import type { TCorePropositionalExpression } from "../schemata/index.js";
/**
 * Returns `true` iff the subtree rooted at `expressionId` contains a
 * variadic connective (`and`, `or` or `xor`). Traversal stops at nested
 * formulas (each formula starts a new P-3 scope).
 *
 * The starting node itself counts: if the caller asks "does formula
 * F's bounded subtree contain a variadic connective?", they pass F's
 * **child** (not F itself) — because traversal stops at the first
 * nested formula encountered, and starting at F would immediately
 * stop. (Equivalently: callers may iterate F's children and call this
 * helper on each child, or pass F's only child for the typical
 * `formula(x)` case.)
 *
 * Note: `implies` and `iff` are intentionally excluded. S-5 restricts both
 * to premise roots, so they cannot appear as formula descendants in a
 * Structural-valid tree. `xor` is not root-restricted and is included:
 * omitting it would make AN-3 strip the very buffer AN-1 inserts around a
 * nested `xor`, and `applyANToFixedPoint` would oscillate to its cap.
 *
 * @param expressionId Subtree root id.
 * @param lookup `(id) => children` — must return live children at
 *               call time. Typical bindings: a closure over a
 *               pre-built `TChildMap` for validator use, or
 *               `pe.getChildExpressions.bind(pe)` for AN-pass use.
 * @param getExpression `(id) => TCorePropositionalExpression | undefined`
 *               — resolve the starting node by id; the lookup function
 *               returns descendants by id but doesn't include the
 *               start node itself.
 */
export declare function hasBinaryOperatorInBoundedSubtree(expressionId: string, lookup: (id: string) => readonly TCorePropositionalExpression[], getExpression: (id: string) => TCorePropositionalExpression | undefined): boolean;
//# sourceMappingURL=bounded-subtree.d.ts.map