Function storeNotElement

src/compute-engine/assume.ts:263–280

* Store a `NotElement(x, setExpr)` exclusion fact in the assumptions DB. * If `x` has a value, the exclusion is decided by evaluation instead.

(
  ce: ComputeEngine,
  x: Expression,
  setExpr: Expression
)

]);

/**
 * Assume a conjunction: each conjunct is assumed independently
 * (design §3.2, "shallow saturation").
 *
 * Result: `'contradiction'` if any conjunct contradicts,
 * `'not-a-predicate'` if any conjunct is unsupported, `'tautology'` if
 * every conjunct was already known, `'ok'` otherwise.
 */
function assumeConjunction(proposition: Expression): AssumeResult {
  console.assert(proposition.operator === 'And');
  if (!isFunction(proposition)) return 'not-a-predicate';

  const ce = proposition.engine;

  // Atomicity (SYM P2-9): a conjunction must apply all-or-nothing when it
  // contradicts. The historical loop applied each conjunct in turn, so a
  // later contradictory conjunct left the earlier ones installed (e.g.
  // `And(p > 0, p < −5)` reported `'contradiction'` yet left `p > 0`).
  //
  // Validate the whole conjunction in an isolated child scope first: the
  // child inherits the caller's assumptions (copied) and symbol bindings (via