Interface TPremiseCrud<TArg, TPremise, TExpr, TVar>

Creates a new premise with an auto-generated UUID and registers it with this engine.

Two call styles are supported:

• Typed-bag (preferred, since 0.11.0):

  engine.createPremise({
      type: "freeform",        // or "derivation"
      derivedClaimId: claimId, // required when type === "derivation"
      extras: { label: "P1" },
      symbol: "P1",
  })
  Copy

• Legacy positional (kept for compatibility):

  engine.createPremise(extras, symbol)  // creates a freeform premise
  Copy

When type === "derivation", the engine looks up derivedClaimId in the claim library, materializes a claim-bound variable for it (via ensureClaimBoundVariable) if one does not already exist, and initializes the premise's expression tree to the naked-Q form — a single variable expression at the root referencing the consequent.

Creates a premise with a caller-supplied ID and registers it with this engine. Mirrors createPremise exactly, but accepts an explicit id as the first argument instead of generating one.

Two call styles are supported:

• Typed-bag (preferred, since 0.11.0):

  engine.createPremiseWithId(id, {
      type: "freeform",        // or "derivation"
      derivedClaimId: claimId, // required when type === "derivation"
      extras: { label: "P1" },
      symbol: "P1",
  })
  Copy

• Legacy positional (kept for compatibility):

  engine.createPremiseWithId(id, extras, symbol)  // creates a freeform premise
  Copy

When type === "derivation", the same derivation initialization as createPremise runs: variable materialization and naked-Q tree setup.

Returns the PremiseEngine containing the given expression, or undefined.

Returns the premise with the given ID, or undefined if not found.

Returns true if a premise with the given ID exists.

Returns all premise IDs in lexicographic order.

Returns all premises in lexicographic ID order.

Removes a premise and reassigns any role assignments that reference it.

Invariant guard (1.0.2): when the removed premise was the conclusion AND other premises remain after the delete, the conclusion role is atomically reassigned to the lowest-id remaining premise (sorted lexicographically) rather than left undefined, preserving the engine-level invariant that a non-empty argument always has a conclusion designated (E-7). When the removed premise was the conclusion AND no premises remain, the role is cleared as before (vacuous invariant on the empty argument). Consumers that want a different reassignment policy (e.g., server-side createdOn ordering or a UI-defined sibling position) should issue their own setConclusionPremise(...) call immediately after this method returns — the post-mutation E-7 will continue to pass because a conclusion stays designated throughout.