One-bit comparator: A greater than B

Q: Why are the three outputs mutually exclusive?

Because they partition the four input rows: equal takes rows 0 and 3, b_greater row 1, a_greater row 2. The engine does not state this as a separate check here; it is read directly off the three columns of the table, which cover every row once.

A one-bit magnitude comparator with three outputs: A AND NOT B for A greater, XNOR(A, B) for equal, NOT A AND B for B greater. The four-row table shows exactly one output true on every row.

Comparing two one-bit numbers has three possible answers, and each gets its own formula. a_greater is true only when A is 1 and B is 0; equal is true when the bits match, which is XNOR; b_greater is the mirror of the first. The model carries all three so the truth table shows them side by side, and reading across any row exactly one column is true: row 0 and row 3 are equal, row 1 is b_greater, row 2 is a_greater. The page's primary output is a_greater, Σm(2).

For a_greater the tautology check is violated with the counterexample A = FALSE, B = FALSE, and satisfiability holds with the witness A = TRUE, B = FALSE, the one true row. The simplifier found no law that shortens the two-operator expression A AND NOT B; both normal-form converters return it unchanged, as a two-clause CNF and a one-term DNF, with no law steps. The Karnaugh map draws one group on cell 2 and reports one prime implicant. The NOR-only form is 2 gates, NOR(NOR(A, A), B); the NAND-only form needs 5.

One-bit comparators are chained to compare wider numbers: the high bit decides unless it is equal, in which case the next bit decides, and the two-bit equality page shows the equal path for two bits. In software the three outputs are the three results of a compare function, and the row-by-row exclusivity is the property to test: a sort comparator that can return two answers for the same pair, or none, corrupts the sort. The table is a complete specification of the function for one bit.

a_greater := A AND NOT B · outputequal := XNOR(A, B) · outputb_greater := NOT A AND B · output

Exact checks

Always true (tautology)? No Counterexample: A = F, B = F · Exhaustively checked and solver cross-checked · 1 rows

Always false (contradiction)? No Counterexample: A = T, B = F · Exhaustively checked and solver cross-checked · 3 rows

Can be true? Yes Example assignment: A = T, B = F · Exhaustively checked and solver cross-checked · 3 rows

Truth table (4 rows)

One-bit comparator: A greater than B
#	A	B	a_greater	equal	b_greater
0	FALSE	FALSE	FALSE	TRUE	FALSE
1	FALSE	TRUE	FALSE	FALSE	TRUE
2	TRUE	FALSE	TRUE	FALSE	FALSE
3	TRUE	TRUE	FALSE	TRUE	FALSE

Plain-language reading

Beginnera_greater is true exactly when A is true and B is false.
In every other case, a_greater is false.
About the operators:
- AND is true only when all of its parts are true.
- NOT reverses a value: true becomes false and false becomes true.

Intermediatea_greater is true exactly when A is true and B is false.
In every other case, a_greater is false.

Advanceda_greater is true exactly when A is true and B is false [conjunction ∧].
In every other case, a_greater is false.
Formal notation: A ∧ ¬B

Logic diagram

Simplification, step by step

The engine found no law that shortens this expression; it is already as short as its rewriting laws can make it.

A AND NOT B

Karnaugh map

A \ B

0m0

0m1

1m2

0m3

cells m2A AND NOT B

A AND NOT B · Derived A AND NOT B. Exactly equivalent on every assignment.

Minterms and maxterms

a_greater(A, B) = Σm(2)a_greater(A, B) = ΠM(0, 1, 3)

Variable order: A, B · 4 rows

Normal forms

Conjunctive normal form (CNF)

A AND NOT B

2 clauses, 2 literals · complete

Disjunctive normal form (DNF)

A AND NOT B

1 terms, 2 literals · complete

NAND-only and NOR-only

NAND-only form

NAND(NAND(A, NAND(B, B)), NAND(A, NAND(B, B)))

5 gates · verified equivalent on every row

NOR-only form

NOR(NOR(A, A), B)

2 gates · verified equivalent on every row

The same rule as code

Python

# -*- coding: utf-8 -*-
# Generated by Tangibool (tangibool.python/1). Do not edit by hand; regenerate from the source revision.
# Model: not stated
# Source revision: reference
# Interpretation status: not stated
"""Tangibool evaluator (decision model).

Generated deterministically from the validated Boolean model; it evaluates exactly that
model. It does not establish that the model is a complete, legal, or safe statement of a
real-world rule, and evaluating examples does not verify the rule.

Source revision: reference
Interpretation status: not stated
Exporter: 1.0.0 (format tangibool.python/1; engine 1.0.0; semantics tangibool-semantics/1)
Logic digest: ce3061f3118e63deb627c83dce3015981ebcf5e0eb9d3f9781afed948ea18bdd
Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78

Inputs (dict keys, declared order) and generated parameter names:
    'A' -> input_A
    'B' -> input_B

Outputs (declared order) and their functions:
    'a_greater' -> output_a_greater(inputs)
    'equal' -> output_equal(inputs)
    'b_greater' -> output_b_greater(inputs)

Assumptions (the declared scope, checked by in_scope(inputs)):
    none; every complete assignment is in scope.

Input contract:
    Every required input must be exactly True or False (type(value) is bool). Missing
    inputs, None, strings, integers (including 0 and 1), and keys that are not declared
    inputs raise InputError before anything is evaluated, including inputs that a
    short-circuiting operator would never read. Results are always bool.

Scope:
    Decision functions raise OutOfScopeError when the inputs violate an assumption; an
    out-of-scope assignment is never turned into a False result. Pass check_scope=False
    to evaluate without the scope check, and use in_scope(inputs) to test it separately.

Usage:

    import tangibool_model as model

    model.evaluate({'A': False, 'B': False})
    # -> {'a_greater': False, 'equal': True, 'b_greater': False}
    model.output_a_greater({'A': False, 'B': False})
    # -> False
    model.evaluate({'A': 1, 'B': False})
    # raises InputError: 1 is an int, not a bool
"""

import collections.abc as _abc
from typing import Dict, Mapping, Tuple

__all__ = [
    "MODEL_INFO",
    "IDENTIFIER_MAP",
    "INPUT_NAMES",
    "OUTPUT_NAMES",
    "ASSUMPTIONS",
    "InputError",
    "OutOfScopeError",
    "minterm_index",
    "in_scope",
    "evaluate",
    "output_a_greater",
    "output_equal",
    "output_b_greater",
]

MODEL_INFO = {
    "format": "tangibool.python/1",
    "mode": "decision",
    "model": None,
    "revision": "reference",
    "interpretation": None,
    "exporter": "1.0.0",
    "engine_version": "1.0.0",
    "semantics_version": "tangibool-semantics/1",
    "logic_digest": "ce3061f3118e63deb627c83dce3015981ebcf5e0eb9d3f9781afed948ea18bdd",
    "assumptions_digest": "d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78",
    "primary_output": "a_greater",
    "unused_inputs": (),
    "subcircuits": (),
}

# Stable ID -> generated identifier (reversible mapping; names are exact, escaped strings).
IDENTIFIER_MAP = {
    "v_e700039344a6": {"kind": "input", "name": "A", "identifier": "input_A"},
    "v_13f8cb6d7acd": {"kind": "input", "name": "B", "identifier": "input_B"},
    "f_d2e00b96bf68": {"kind": "output", "name": "a_greater", "identifier": "output_a_greater"},
    "f_ff29627d161f": {"kind": "output", "name": "equal", "identifier": "output_equal"},
    "f_97d43ff3af41": {"kind": "output", "name": "b_greater", "identifier": "output_b_greater"},
}

INPUT_NAMES = ("A", "B")
OUTPUT_NAMES = ("a_greater", "equal", "b_greater")
ASSUMPTIONS = ()

_DECLARED_INPUTS = frozenset(INPUT_NAMES)
_SCOPE_INPUTS = ()
_ASSUMPTION_FORMULAS = {entry["name"]: entry["formula"] for entry in ASSUMPTIONS}


class InputError(ValueError):
    """Raised when inputs are missing, undeclared, or not exactly True/False.

    Every required input must satisfy type(value) is bool. Missing inputs, None, strings,
    integers (including 0 and 1), and keys that are not declared inputs are rejected before
    anything is evaluated. A missing input is never treated as False. The individual problems
    are listed in the problems attribute.
    """

    def __init__(self, problems):
        self.problems = tuple(problems)
        super().__init__("Invalid inputs: " + "; ".join(self.problems))


class OutOfScopeError(ValueError):
    """Raised when the inputs violate the model's assumptions (its declared scope).

    Outside its assumptions the rule has no decision: this error is never a False result.
    The names of the violated assumptions are in the violated attribute.
    """

    def __init__(self, violated):
        self.violated = tuple(violated)
        details = ", ".join(name + " (" + _ASSUMPTION_FORMULAS.get(name, "?") + ")" for name in self.violated)
        super().__init__(
            "Out of scope: the inputs violate "
            + ("assumption " if len(self.violated) == 1 else "assumptions ")
            + details
            + ". The rule has no decision outside its assumptions; this is not a False result."
        )


def _short_repr(value: object) -> str:
    text = repr(value)
    return text if len(text) <= 60 else text[:57] + "..."


def _checked_inputs(inputs: Mapping[str, bool], required: Tuple[str, ...], check_scope: bool) -> Dict[str, bool]:
    """Validate inputs strictly before anything is evaluated and return a plain copy."""
    if type(check_scope) is not bool:
        raise TypeError("check_scope must be True or False")
    if not isinstance(inputs, _abc.Mapping):
        raise InputError(["inputs must be a mapping from input names to True/False, got " + type(inputs).__name__])
    problems = []
    for key in inputs:
        if type(key) is not str or key not in _DECLARED_INPUTS:
            declared = ", ".join(repr(name) for name in INPUT_NAMES) or "none"
            problems.append("undeclared input " + _short_repr(key) + " (declared inputs: " + declared + ")")
    needed = tuple(required) + (_SCOPE_INPUTS if check_scope else ())
    for name in needed:
        if name not in inputs:
            problems.append("missing required input " + repr(name))
    for key, value in inputs.items():
        if type(key) is str and key in _DECLARED_INPUTS and type(value) is not bool:
            problems.append(
                "input " + repr(key) + " must be True or False (type bool), got "
                + type(value).__name__ + " " + _short_repr(value)
            )
    if problems:
        raise InputError(list(dict.fromkeys(problems)))
    return dict(inputs.items())


def _require_bool_args(function: str, pairs: Tuple[Tuple[str, object], ...]) -> None:
    problems = [
        "argument " + repr(name) + " of " + function + " must be True or False (type bool), got "
        + type(value).__name__ + " " + _short_repr(value)
        for name, value in pairs
        if type(value) is not bool
    ]
    if problems:
        raise InputError(problems)


def minterm_index(*values: bool) -> int:
    """Row index of an assignment over a declared variable order.

    The first value is the most significant bit, so all-False is row 0. Used for indexed
    minterm (sum) and maxterm (product) forms.
    """
    index = 0
    for value in values:
        if type(value) is not bool:
            raise InputError(["minterm_index() takes True/False values, got " + type(value).__name__ + " " + _short_repr(value)])
        index = index * 2 + (1 if value else 0)
    return index


def _scope_values(values: Dict[str, bool]) -> Tuple[Tuple[str, bool], ...]:
    """Value of every enabled, confirmed assumption for validated inputs, in declared order."""
    return ()


def _require_in_scope(values: Dict[str, bool]) -> None:
    violated = tuple(name for name, holds in _scope_values(values) if not holds)
    if violated:
        raise OutOfScopeError(violated)


def in_scope(inputs: Mapping[str, bool]) -> bool:
    """True when the inputs satisfy every assumption (the model's declared scope).

    Requires the inputs the assumptions read; raises InputError for invalid inputs.
    """
    values = _checked_inputs(inputs, (), True)
    return all(holds for _, holds in _scope_values(values))


# ---- Formula bodies (inputs are validated by the public functions below) ----


def _compute_output_a_greater(input_A: bool, input_B: bool) -> bool:
    """Decision output 'a_greater': A AND NOT B"""
    return input_A and (not input_B)


def _compute_output_equal(input_A: bool, input_B: bool) -> bool:
    """Decision output 'equal': XNOR(A, B)"""
    return input_A == input_B


def _compute_output_b_greater(input_A: bool, input_B: bool) -> bool:
    """Decision output 'b_greater': NOT A AND B"""
    return (not input_A) and input_B


# ---- Public API ----


def output_a_greater(inputs: Mapping[str, bool], *, check_scope: bool = True) -> bool:
    """Decision output 'a_greater' (stable ID f_d2e00b96bf68).

    'a_greater' := A AND NOT B

    Required inputs: 'A', 'B'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("A", "B"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_a_greater_value = _compute_output_a_greater(values["A"], values["B"])
    return output_a_greater_value


def output_equal(inputs: Mapping[str, bool], *, check_scope: bool = True) -> bool:
    """Decision output 'equal' (stable ID f_ff29627d161f).

    'equal' := XNOR(A, B)

    Required inputs: 'A', 'B'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("A", "B"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_equal_value = _compute_output_equal(values["A"], values["B"])
    return output_equal_value


def output_b_greater(inputs: Mapping[str, bool], *, check_scope: bool = True) -> bool:
    """Decision output 'b_greater' (stable ID f_97d43ff3af41).

    'b_greater' := NOT A AND B

    Required inputs: 'A', 'B'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("A", "B"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_b_greater_value = _compute_output_b_greater(values["A"], values["B"])
    return output_b_greater_value


def evaluate(inputs: Mapping[str, bool], *, check_scope: bool = True) -> Dict[str, bool]:
    """Evaluate every output (declared order); each output is computed once.

    Required inputs: 'A', 'B'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("A", "B"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_a_greater_value = _compute_output_a_greater(values["A"], values["B"])
    output_equal_value = _compute_output_equal(values["A"], values["B"])
    output_b_greater_value = _compute_output_b_greater(values["A"], values["B"])
    return {
        "a_greater": output_a_greater_value,
        "equal": output_equal_value,
        "b_greater": output_b_greater_value,
    }

PostgreSQL

-- Tangibool PostgreSQL export (tangibool.postgresql/1)
-- Target: PostgreSQL 16 or later with typed boolean inputs; tested with PostgreSQL 18.3 (PGlite 0.5.8).
-- Not a claim of compatibility with other SQL dialects.
-- Model: not stated
-- Source revision: reference
-- Interpretation status: not stated
-- Exporter: 1.0.0 (engine 1.0.0; semantics tangibool-semantics/1)
-- Logic digest: ce3061f3118e63deb627c83dce3015981ebcf5e0eb9d3f9781afed948ea18bdd
-- Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78
-- Mode: decision
--
-- Read-only: this file contains only WITH / VALUES / SELECT statements. No DDL, DML,
-- procedures, credentials, network access, or database changes. The expressions are pure
-- Boolean expressions, so their result does not depend on SQL evaluation order.
--
-- NON-NULL INPUT PRECONDITION: NULL is not a truth value of this rule. Every fragment below
-- is defined only when every input column it reads is a non-NULL boolean. The guard template
-- (section 2) marks any NULL input as 'invalid_input' and any row that violates the
-- assumptions as 'out_of_scope', and fills output columns only for 'ok' rows; a NULL in an
-- output column of another row is an envelope marker, not a third truth value. Never wrap
-- the fragments in COALESCE(..., FALSE) or otherwise choose a meaning for unknown inputs.
-- This evaluates the supplied model; it does not show that the model is a complete, legal,
-- or safe statement of a real-world rule.
--
-- Input columns (stable ID: name -> column):
--   v_e700039344a6: A -> "in_A"
--   v_13f8cb6d7acd: B -> "in_B"
-- Output columns:
--   f_d2e00b96bf68: a_greater -> "out_a_greater"
--   f_ff29627d161f: equal -> "out_equal"
--   f_97d43ff3af41: b_greater -> "out_b_greater"
-- Assumptions (scope K; exported separately and never folded into an output):
--   none; every complete input row is in scope.

-- ----------------------------------------------------------------------------------------------
-- 1. Expression fragments (parenthesised; non-NULL boolean inputs required)
-- ----------------------------------------------------------------------------------------------
--
-- [out_a_greater] output a_greater (stable ID f_d2e00b96bf68)
--   a_greater := A AND NOT B
--   PRECONDITION: "in_A", "in_B" are non-NULL booleans.
--   ("in_A" AND (NOT "in_B"))
--
-- [out_equal] output equal (stable ID f_ff29627d161f)
--   equal := XNOR(A, B)
--   PRECONDITION: "in_A", "in_B" are non-NULL booleans.
--   ("in_A" = "in_B")
--
-- [out_b_greater] output b_greater (stable ID f_97d43ff3af41)
--   b_greater := NOT A AND B
--   PRECONDITION: "in_A", "in_B" are non-NULL booleans.
--   ((NOT "in_A") AND "in_B")
--

-- ----------------------------------------------------------------------------------------------
-- 2. Guard template (read-only SELECT over an inputs list)
-- ----------------------------------------------------------------------------------------------
-- Replace the example rows between the markers with your own rows, or replace the inputs
-- CTE with a SELECT that provides the boolean columns listed in the header. status is
-- 'invalid_input' when any input is NULL, 'out_of_scope' when the assumptions are false, and
-- 'ok' otherwise; output columns are filled only for 'ok' rows (NULL elsewhere is an
-- envelope marker). Assumption columns are shown for rows with complete inputs.
WITH inputs ("row_id", "in_A", "in_B") AS (
  -- tangibool:example-rows:begin
  VALUES
    (1, FALSE, FALSE),
    (2, FALSE, TRUE),
    (3, TRUE, FALSE),
    (4, TRUE, TRUE),
    (5, NULL::boolean, FALSE)
  -- tangibool:example-rows:end
),
checked AS (
  SELECT
    inputs.*,
    CASE
      WHEN "in_A" IS NULL OR "in_B" IS NULL THEN 'invalid_input'
      ELSE 'ok'
    END AS "status"
  FROM inputs
)
SELECT
  "row_id",
  "in_A",
  "in_B",
  "status",
  CASE WHEN "status" = 'ok' THEN ("in_A" AND (NOT "in_B")) END AS "out_a_greater",
  CASE WHEN "status" = 'ok' THEN ("in_A" = "in_B") END AS "out_equal",
  CASE WHEN "status" = 'ok' THEN ((NOT "in_A") AND "in_B") END AS "out_b_greater"
FROM checked
ORDER BY "row_id";

SMT-LIB

; Tangibool SMT-LIB export (tangibool.smtlib/1)
; Profile: SMT-LIB 2.6 Boolean subset (QF_UF): Bool constants, define-fun, let, push/pop, assert, check-sat, echo.
; Tested with Z3 5.1.0 (z3-solver 5.2.0, WebAssembly build).
; Model: not stated
; Source revision: reference
; Interpretation status: not stated
; Exporter: 1.0.0 (engine 1.0.0; semantics tangibool-semantics/1)
; Logic digest: ce3061f3118e63deb627c83dce3015981ebcf5e0eb9d3f9781afed948ea18bdd
; Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78
; Mode: decision
;
; Reading results: each query block states what sat and unsat mean for its question. A sat
; answer comes with a witness or counterexample (ask for it with (get-model) after sat only);
; unsat settles that scoped query and is solver-checked, not an independently checked proof
; certificate; unknown settles nothing. Blocks are scoped with push/pop, so assertions never
; accumulate across questions. This checks the supplied model, not whether it is a complete,
; legal, or safe statement of a real-world rule.
;
; Symbols (stable ID: name -> symbol):
;   v_e700039344a6: A -> in_A
;   v_13f8cb6d7acd: B -> in_B
;   f_d2e00b96bf68: a_greater -> out_a_greater
;   f_ff29627d161f: equal -> out_equal
;   f_97d43ff3af41: b_greater -> out_b_greater

(set-option :produce-models true)
(set-info :smt-lib-version 2.6)
(set-logic QF_UF)

; ---- Inputs (declared order)
(declare-const in_A Bool) ; A
(declare-const in_B Bool) ; B

; ---- Outputs (dependencies first)
; output a_greater (stable ID f_d2e00b96bf68): A AND NOT B
(define-fun out_a_greater () Bool (and in_A (not in_B)))
; output equal (stable ID f_ff29627d161f): XNOR(A, B)
(define-fun out_equal () Bool (= in_A in_B))
; output b_greater (stable ID f_97d43ff3af41): NOT A AND B
(define-fun out_b_greater () Bool (and (not in_A) in_B))

; ---- Assumptions (the scope K; never folded into an output)
; K: conjunction of the enabled, confirmed assumptions (true when there are none)
(define-fun K () Bool true)

; ---- Definitions only: nothing is asserted and no check is run.
; Add (assert ...) and (check-sat) inside (push 1) ... (pop 1) to ask a question.

LaTeX

a_greater = A \cdot \overline{B}
equal = \overline{A \oplus B}
b_greater = \overline{A} \cdot B

The common slip

Writing the greater-than output as A AND B or as A OR NOT B and reasoning it through only for the obvious inputs. The table has four rows; A AND NOT B is true on exactly one, A = TRUE, B = FALSE, and any other candidate lights a row where the other outputs already claim the answer.

Questions

Why are the three outputs mutually exclusive?

Because they partition the four input rows: equal takes rows 0 and 3, b_greater row 1, a_greater row 2. The engine does not state this as a separate check here; it is read directly off the three columns of the table, which cover every row once.

Operators and gates

Tools

Worked examples

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.

One-bit comparator: A greater than B

Exact checks

Truth table (4 rows)

Plain-language reading

Logic diagram

Simplification, step by step

Karnaugh map

Minterms and maxterms

Normal forms

Conjunctive normal form (CNF)

Disjunctive normal form (DNF)

NAND-only and NOR-only

NAND-only form

NOR-only form

The same rule as code

The common slip

Questions

Related

Operators and gates

Tools

See also

Worked examples