structure Hex.GraphIso.Nauty.Sparse.CellActive {n : Nat} (level first last : Nat) (before after : VSet n) (ptn : Array Nat) : Prop

Refining a cell activates all its fragments when it was active, and leaves at most one inactive fragment otherwise.

• all : before.mem first = true → ∀ (u : Nat), first ≤ u → u < last → u = first ∨ ptn[u - 1]! ≤ level → after.mem u = true
• one : ∃ (w : Nat), ∀ (u : Nat), first ≤ u → u < last → u = first ∨ ptn[u - 1]! ≤ level → u ≠ w → after.mem u = true

theorem Hex.GraphIso.Nauty.Sparse.CellActive.refl {n : Nat} {active : VSet n} {ptn : Array Nat} {level first last : Nat} (hc : IsCell ptn level first (last - first)) : CellActive level first last active active ptn

theorem Hex.GraphIso.Nauty.Sparse.CellActive.binary_starts {ptn : Array Nat} {level first last cut u : Nat} (hc : IsCell ptn level first (last - first)) (hf : first < cut) (hl : cut < last) (hu : first ≤ u) (hu' : u < last) (hs : u = first ∨ (ptn.setIfInBounds (cut - 1) level)[u - 1]! ≤ level) : u = first ∨ u = cut

theorem Hex.GraphIso.Nauty.Sparse.CellActive.binary_left {n : Nat} {active : VSet n} {ptn : Array Nat} {level first last cut : Nat} (hc : IsCell ptn level first (last - first)) (hf : first < cut) (hl : cut < last) (hb : last ≤ n) (ha : active.mem first = false) : CellActive level first last active (active.insert first) (ptn.setIfInBounds (cut - 1) level)

theorem Hex.GraphIso.Nauty.Sparse.CellActive.binary_right {n : Nat} {active : VSet n} {ptn : Array Nat} {level first last cut : Nat} (hc : IsCell ptn level first (last - first)) (hf : first < cut) (hl : cut < last) (hb : last ≤ n) : CellActive level first last active (active.insert cut) (ptn.setIfInBounds (cut - 1) level)

def Hex.GraphIso.Nauty.Sparse.Activation (n level : Nat) (before ptn : Array Nat) (active out : VSet n) : Prop

The fragment-activation rule for every original cell of a pass.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Activation.refl {n : Nat} (ptn : Array Nat) (active : VSet n) (level : Nat) : Activation n level ptn ptn active active

theorem Hex.GraphIso.Nauty.Sparse.Activation.step {n level first last : Nat} {before ptn out : Array Nat} {active current after : VSet n} (h : Activation n level before ptn active current) (hc : IsCell before level first (last - first)) (hl : CellActive level first last current after out) (ha : ∀ (u : Nat), u < first ∨ last ≤ u → after.mem u = current.mem u) (hp : ∀ (q : Nat), q < first ∨ last - 1 ≤ q → out[q]! = ptn[q]!) : Activation n level before out active after

A pass may process its original cells in any order: a local activation proof composes with all guarantees already established on disjoint cells.

theorem Hex.GraphIso.Nauty.Sparse.Activation.cut_left {n level first cut last : Nat} {before ptn : Array Nat} {active current : VSet n} (h : Activation n level before ptn active current) (hc : IsCell before level first (last - first)) (ht : IsCell ptn level first (last - first)) (hf : first < cut) (hl : cut < last) (hb : last ≤ n) (ha : current.mem first = false) : Activation n level before (ptn.setIfInBounds (cut - 1) level) active (current.insert first)

Activate the first fragment when the original cell is inactive.

theorem Hex.GraphIso.Nauty.Sparse.Activation.cut_right {n level first cut last : Nat} {before ptn : Array Nat} {active current : VSet n} (h : Activation n level before ptn active current) (hc : IsCell before level first (last - first)) (ht : IsCell ptn level first (last - first)) (hf : first < cut) (hl : cut < last) (hb : last ≤ n) : Activation n level before (ptn.setIfInBounds (cut - 1) level) active (current.insert cut)

Activate the second fragment; an already active first fragment stays active.