Interface TExpressionMutations<TArg, TPremise, TExpr, TVar>

Adds an expression to this premise's tree.

If the expression has parentId: null it becomes the root; only one root is permitted per premise. All Structural rules (implies/iff root-only, child limits, position uniqueness, derivation root operator) are enforced at mutation time.

P-1 (non-not operator under operator) is not enforced at mutation time — the AN-1 post-hook in assistive behavior inserts the formula buffer; in permissive behavior the un-buffered state stays and surfaces via engine.validate('presentable').

Adds an expression immediately before or after an existing sibling, with position computed automatically.

Composite-mutation behavior (S-9): sibling positions are always shifted as part of the bundled op when the computed midpoint position would collide with an existing sibling. Only the minimal set of nodes is repositioned. Repositioned siblings appear in changes.expressions.modified.

Adds an expression as the last child of the given parent, with position computed automatically. If parentId is null, the expression becomes the root.

Composite-mutation behavior (S-9): sibling positions are always shifted as part of the bundled op when the computed position would collide with an existing sibling. Repositioned siblings appear in changes.expressions.modified.

Changes the operator type of an existing operator expression.

Handles three structural cases automatically:

• Simple change: Updates the operator type in place, keeping its id, children and their positions. Applies when the operator has fewer than 3 children and no merge applies, or when it has more, newOperator is and, or or xor, and neither child id is given — those take any number of operands, so the whole node swaps. In assistive mode the post-mutation normalization may then absorb the node into a same-operator parent, as after any change.
• Merge: The operator has fewer than 2 children and its parent (or its grandparent, through a formula buffer) is the same type as newOperator. Dissolves the current operator and reparents its children under that operator.
• Split: The operator has >2 children and both child ids are given. Extracts sourceChildId and targetChildId into a new sub-operator of type newOperator, inserting a formula buffer between the parent and the new sub-operator (the buffer is part of the bundled composite mutation so the resulting tree satisfies P-1 regardless of the engine's behavior setting). implies and iff cannot be split out this way, since they must be roots.

Splices a new expression between existing nodes in the tree. The new expression inherits the tree slot of the anchor node (leftNodeId ?? rightNodeId).

P-1 (non-not operator under operator) is not enforced at mutation time — the AN-1 post-hook in assistive behavior inserts the formula buffer; in permissive behavior the un-buffered state stays and surfaces via engine.validate('presentable').

Removes an expression and optionally its entire descendant subtree.

This method does not collapse the surviving parent — AN-3 (post-mutation hook in assistive mode) handles 0/1-child operator/formula collapse on the surviving parent.

Toggles negation on an expression. If the expression's parent is a NOT operator, removes the NOT (promoting the expression). Otherwise, wraps the expression with a new NOT operator.

P-1 (non-not operator under operator) and P-2 (NOT(NOT(x)) double-negation) are not enforced at mutation time. The post-mutation AN hook handles them in assistive behavior: AN-1 inserts the formula buffer between NOT and a non-not operator child; AN-2 collapses NOT(NOT(x)) → x. In permissive behavior both states stay and surface via engine.validate('presentable').

Updates mutable fields of an existing expression. Only position, variableId, and operator may be updated.

Wraps an existing expression with a new operator and a new sibling in a single atomic operation.

The operator takes the existing node's slot in the tree. Both the existing node and the new sibling become children of the operator. Exactly one of leftNodeId / rightNodeId must be provided — it identifies the existing node and which child slot it occupies.

P-1 (non-not operator under operator) is not enforced at mutation time — the AN-1 post-hook in assistive behavior inserts the formula buffer; in permissive behavior the un-buffered state stays and surfaces via engine.validate('presentable').