theorem Hex.GraphIso.Nauty.recover_lab {κ : Type} {n : Nat} (inf level : Nat) (st : SearchState n κ) : (recover inf level st).lab = st.lab

recover never changes the current labelling.

theorem Hex.GraphIso.Nauty.recover_ptn {κ : Type} {n : Nat} (inf level : Nat) (st : SearchState n κ) (q : Nat) : (recover inf level st).ptn[q]! = if q < n ∧ st.ptn[q]! > level then inf else st.ptn[q]!

recover reopens exactly the entries above its receiving level.

theorem Hex.GraphIso.Nauty.recover_ptn_size {κ : Type} {n : Nat} (inf level : Nat) (st : SearchState n κ) : (recover inf level st).ptn.size = st.ptn.size

Reopening a partition preserves its array size.

theorem Hex.GraphIso.Nauty.recover_out {n k : Nat} {G : Colored n k} {level : Nat} {st : Search n} (hlev : level + 1 < n + 2) (hreach : CellsReach G st.lab) : SearchOut G level level st (recover (n + 2) level st)

One recover step satisfies the exit contract at its own level.

theorem Hex.GraphIso.Nauty.root_searchOk {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : SearchOk G 1 (initialPartition G).snd.length (initial n (initialPartition G).fst (initialPartition G).snd)

The production initial state satisfies the partition invariant.