Function visit

src/compute-engine/symbolic/logic-utils.ts:674–690

(e: Expression)

      }
      // For n-ary Xor negation, first convert Xor to binary, then negate
      return toNNF(ce._fn('Not', [toNNF(inner, ce)]), ce);
    }

    // Negation of Nand: ¬NAND(A, B) ≡ A ∧ B
    if (innerOp === 'Nand') {
      return toNNF(ce._fn('And', fnOps(inner)!), ce);
    }

    // Negation of Nor: ¬NOR(A, B) ≡ A ∨ B
    if (innerOp === 'Nor') {
      return toNNF(ce._fn('Or', fnOps(inner)!), ce);
    }

    // Literal: ¬x stays as is
    return expr;
  }

  // Handle Implies: A → B ≡ ¬A ∨ B
  if (op === 'Implies') {
    const a = fnOp1(expr)!;