Function assumeNotEqual

src/compute-engine/assume.ts:214–219

* Assume a disequality `NotEqual(x, v)` or `NotEqual(Part(x), v)` * (design §4.1; stored in the §3.2 normal form `NotEqual(subject, v)`).

(proposition: Expression)

  if (op === 'Equal') return assumeEquality(proposition);
  if (op === 'NotEqual') return assumeNotEqual(proposition);
  if (op === 'And') return assumeConjunction(proposition);
  if (isInequalityOperator(op)) return assumeInequality(proposition);

  // Well-formed predicate shapes that the assumptions layer cannot
  // represent (disjunctions, quantifiers...): return 'not-a-predicate'
  // instead of throwing, so callers (e.g. the Fungrim loader) can probe
  // guard dischargeability in bulk (design §4.1, §9).
  if (UNSUPPORTED_PREDICATE_OPERATORS.has(op)) return 'not-a-predicate';