Subcircuit expansion (Tangibool rewriting step)

Subcircuit expansion replaces an instance of a reusable subcircuit by its definition body, with the instance's arguments wired to the definition's inputs.

Engine name: Subcircuit expansionFR: Expansion d'un sous-circuitDE: Expansion einer Teilschaltung

A subcircuit instance is replaced by its definition body, with its inputs connected to the instance’s arguments.

In Tangibool a subcircuit is a named, versioned block such as maj(A, B, C) for the majority function. When the engine needs to check, simplify or export a formula that uses an instance, it expands the instance in place: the body (A AND B) OR (A AND C) OR (B AND C) takes the place of the call, and the expansion is recorded as a step with this law's name so the trace stays honest about what was rewritten.

This page exists so that every step name the engine can print has a reference; the expansion is not an identity between two closed formulas and is not indexed as one. The app's subcircuit library and the semantics specification describe pinning, versions and the Name@N notation.

Statement

This rewriting step involves subcircuits and is not stated as an identity between two closed expressions; the lesson and the app show the expansion.

Questions

Does expansion change the function?

No. By construction the expanded formula has exactly the behaviour of the instance; the engine's size limit applies to the expanded form, which is why a deeply nested library can hit the node bound.

Related

Tools

• Boolean algebra calculator and simplifier with steps (every law named and verified)
• Logical equivalence checker: two expressions, exact verdict, counterexample

See also

• Named-output reference expansion (Tangibool rewriting step)
• Majority of three (2-out-of-3 voting): truth table, K-map and NAND form

Laws

• XOR identities: A XOR FALSE = A, A XOR TRUE = NOT A, A XOR A = FALSE
• Associative law: (A AND B) AND C = A AND (B AND C)
• Implication elimination: A → B = NOT A OR B, and the →E rule
• Biconditional elimination: the A ↔ B rewrite and the ↔E rule

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.