def normalize(operation, expr):
    """
    Transform a expression into its normal form in the given operation.

    Returns a tuple of arguments that will satisfy the condition
    operation(*args) == expr (here mathematical equality is meant) and
    the operation doesn't occur in any arg. Also NOT is only appearing
    in literals.
    """
    dualoperation = operation.getdual()
    # Move NOT inwards.
    expr = expr.literalize()
    # Simplify as much as possible, otherwise rdistributive may take
    # forever.
    expr = expr.eval()
    # Totally flatten everything.
    def rdistributive(expr):
        if expr.isliteral:
            return expr
        args = tuple(rdistributive(arg).eval() for arg in expr.args)
        if len(args) == 1:
            return args[0]
        expr = expr.__class__(*args)
        if isinstance(expr, dualoperation):
            expr = expr.distributive()
        return expr
    expr = rdistributive(expr)
    # Canonicalize
    expr = expr.eval()
    if isinstance(expr, operation):
        args = expr.args
    else:
        args = (expr,)
    return args