theorem Hex.GraphIso.Nauty.Sparse.Replay.sibling_of_check {check : Nat → CertNode → Option Bool} {witness : Nat → Nat → Array Nat → Bool} {seen : Array Bool} {o : Nat} {c : CertNode} {a : Bool} (hne : ∀ (earlier : Nat) (raw : Array Nat), c ≠ CertNode.autom earlier raw) (hs : seen.size = o) (h : check o c = some a) : sibling check witness seen c = some a

An accepted ordinary node enters the sibling scan with the same flag.

def Hex.GraphIso.Nauty.Sparse.Replay.emit (choose : Nat → Option (Nat × Array Nat)) (witness : Nat → Nat → Array Nat → Bool) (fallback : Nat → CertNode) (o : Nat) : CertNode

Emit a checked earlier-sibling reference when available. The fallback is a function so compiled execution never expands a pruned subtree eagerly.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.Replay.emit_replays {choose : Nat → Option (Nat × Array Nat)} {witness : Nat → Nat → Array Nat → Bool} {fallback : Nat → CertNode} {check : Nat → CertNode → Option Bool} {seen : Array Bool} {o : Nat} (hs : seen.size = o) (h : ∃ (a : Bool), sibling check witness seen (fallback o) = some a) : ∃ (a : Bool), sibling check witness seen (emit choose witness fallback o) = some a

Emission cannot invalidate a successful fallback: a reference is emitted only after exactly the same check that the sibling scan will replay.