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.
As of v1.0 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').
The expression to add, including position and parent assignment.
The added expression (with checksum) and changeset.
Adds an expression immediately before or after an existing sibling, with position computed automatically.
Composite-mutation behavior (spec §8 / 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.
The ID of the existing sibling expression.
Whether to insert "before" or "after"
the sibling.
The expression to add (position is auto-assigned).
The added expression (with checksum) and changeset.
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 (spec §8 / 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.
The parent expression ID, or null for root.
The expression to add (position is auto-assigned).
The added expression (with checksum) and changeset.
Changes the operator type of an existing operator expression.
Handles three structural cases automatically:
newOperator. Dissolves the current operator and
reparents its children under the parent.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).The operator expression to change.
The target operator type.
OptionalsourceChildId: stringFirst child to include in a split (required when >2 children).
OptionaltargetChildId: stringSecond child to include in a split (required when >2 children).
OptionalextraFields: Partial<TExpr>Optional partial expression fields merged into any newly created expressions (formula buffer, new sub-operator). Structural fields (id, type, operator, parentId, position, premiseId, argumentId, argumentVersion) cannot be overridden.
result — For simple change: the updated operator expression. For merge: null (operator was dissolved). For split: the newly created sub-operator expression. changes — Full changeset with correct hierarchical checksums.
Splices a new expression between existing nodes in the tree. The new
expression inherits the tree slot of the anchor node
(leftNodeId ?? rightNodeId).
As of v1.0 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').
The expression to insert, including position and parent assignment.
OptionalleftNodeId: stringThe existing node to become the left child of the new expression.
OptionalrightNodeId: stringThe existing node to become the right child of the new expression.
The inserted expression (with checksum) and changeset.
Removes an expression and optionally its entire descendant subtree.
As of v1.0 the pre-mutation 0/1-child collapse cascade is gone — AN-3 (post-mutation hook in assistive mode) handles 0/1-child operator/formula collapse on the surviving parent.
The ID of the expression to remove.
Whether to remove all descendants as well.
The removed root expression, or undefined if not found.
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.
As of v1.0 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').
The ID of the expression to toggle negation on.
OptionalextraFields: Partial<TExpr>Optional additional fields to merge into newly created expressions (NOT and formula nodes). Structural fields (id, type, operator, parentId, position, premiseId, argumentId, argumentVersion) cannot be overridden.
The new NOT expression when adding negation, or null when
removing it, along with the changeset.
Updates mutable fields of an existing expression. Only position,
variableId, and operator may be updated.
The ID of the expression to update.
The fields to update.
The updated expression and changeset.
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.
As of v1.0 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').
The new operator expression to wrap with.
The new sibling expression to add alongside the existing node.
OptionalleftNodeId: stringThe existing node to place as the left child.
OptionalrightNodeId: stringThe existing node to place as the right child.
The inserted operator (with checksum) and changeset.
Single-premise expression tree mutations.