Function assumeConjunctionInner

src/compute-engine/assume.ts:195–208

(proposition: Expression)

  if (op === 'NotElement') return assumeNotElement(proposition);
  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';

  // Outright malformed input (not a predicate operator at all) reports
  // `'not-a-predicate'` too — errors are VALUES (error-propagation design
  // §8a): the throw escaped to the host on the direct route (`Assume(Ln("a"))`
  // via `ce.box`), while the same program run through Epsil became an
  // `["Error", …]` value, so the two routes disagreed on whether an
  // unassumable proposition is catastrophic. Every sub-dispatcher below
  // already reports malformed input this way (`!isFunction(proposition)`,