def Hex.GraphIso.Nauty.Sparse.Limited.agreement {n : Nat} (g : Graph n) (inf tcLevel : Nat) : Generic.Contract (State n) n

Exact projection to the native recursion on every successful return. No validity assumption on the raw search state is needed for this comparison.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Limited.agreementPolicy {n : Nat} (g : Graph n) (inf tcLevel : Nat) : Generic.SoundPolicy g inf tcLevel (agreement g inf tcLevel)

The actual bounded callbacks satisfy all local rules of the shared engine; the recursive premises concern only its supplied smaller calls.

theorem Hex.GraphIso.Nauty.Sparse.Limited.node_eq {n : Nat} (g : Graph n) (inf tcLevel fuel level nc : Nat) (first : Bool) (s : State n) (h : Ready (Generic.node first g inf tcLevel fuel level nc s).snd) : Ready s ∧ nodeValue (Generic.node first g inf tcLevel fuel level nc s) = Generic.node first g inf tcLevel fuel level nc s.value

Every successful bounded node has the native engine's exact exit and complete state, including scratch, generator trace and all diagnostics.

theorem Hex.GraphIso.Nauty.Sparse.Limited.sweep_eq {n : Nat} (g : Graph n) (inf tcLevel fuel cfuel level nc tc tv1 : Nat) (first : Bool) (cursor : Option Nat) (cell : VSet n) (index : Nat) (s : State n) (h : Ready (Generic.sweep first g inf tcLevel fuel cfuel level nc tc tv1 cursor cell index s).snd.snd) : Ready s ∧ sweepValue (Generic.sweep first g inf tcLevel fuel cfuel level nc tc tv1 cursor cell index s) = Generic.sweep first g inf tcLevel fuel cfuel level nc tc tv1 cursor cell index s.value

theorem Hex.GraphIso.Nauty.Sparse.Limited.run?_eq {n limit : Nat} {g : Graph n} {lab : Array Nat} {ends : List Nat} {s : State n} (h : run? limit g lab ends = some s) : s.value = run g lab ends

A successful bounded root returns the direct runner's entire state.

theorem Hex.GraphIso.Nauty.Sparse.Limited.runColored?_eq {n k limit : Nat} {G : Sparse.Colored n k} {s : State n} (h : runColored? limit G = some s) : s.value = runColored G

theorem Hex.GraphIso.Nauty.Sparse.Limited.runPair?_eq {n k limit : Nat} {G H : Sparse.Colored n k} {a b : State n} (h : runPair? limit G H = some (a, b)) : a.value = runColored G ∧ b.value = runColored H