Finding available circuit wires

synthesis_available proves membership and inclusion of wire families by following unions, indexed bundles, and local availability hypotheses. It also finds the wires retained by a Synthesis.Builder. Semantic rewrites and bounds on indices remain ordinary local lemmas. The tactic never adds a gate or invokes a synthesis theorem.

Main definitions

• synthesis_available: close an available-wire obligation by structural proof search.
• synthesis_step b using rule: append a certified construction to b, finding its input wires.

def synthesisAvailable : Lean.ParserDescr

Find already available wires, without synthesizing new functions.

def synthesisStep : Lean.ParserDescr

Append a synthesis rule to the named builder, solving its available-wire premises.