def OneHot0(*xs, simplify=True, conj=True):
    """
    Return an expression that means
    "at most one input function is true".

    If *simplify* is ``True``, return a simplified expression.

    If *conj* is ``True``, return a CNF.
    Otherwise, return a DNF.
    """
    xs = [Expression.box(x).node for x in xs]
    terms = list()
    if conj:
        for x0, x1 in itertools.combinations(xs, 2):
            terms.append(exprnode.or_(exprnode.not_(x0),
                                      exprnode.not_(x1)))
        y = exprnode.and_(*terms)
    else:
        for _xs in itertools.combinations(xs, len(xs) - 1):
            terms.append(exprnode.and_(*[exprnode.not_(x) for x in _xs]))
        y = exprnode.or_(*terms)
    if simplify:
        y = y.simplify()
    return _expr(y)
Return an expression that means
    "at most one input function is true".

    If *simplify* is ``True``, return a simplified expression.

    If *conj* is ``True``, return a CNF.
    Otherwise, return a DNF.