structure Hex.GraphIso.Nauty.Generic.FrameEq {n : Nat} {σ : Type} (view : σ → Search n) (st out : σ) : Prop

The four arrays read by the partition-effect contract are unchanged.

• lab : (view out).lab = (view st).lab
• ptn : (view out).ptn = (view st).ptn
• first : (view out).firstlab = (view st).firstlab
• canon : (view out).canonlab = (view st).canonlab

theorem Hex.GraphIso.Nauty.Generic.FrameEq.out {n k : Nat} {σ : Type} {view : σ → Search n} {G : Colored n k} {B level : Nat} {base st out : σ} (h : FrameEq view st out) (hbefore : SearchOut G B level (view base) (view st)) : SearchOut G B level (view base) (view out)

Bookkeeping changes preserve an already established call effect.

structure Hex.GraphIso.Nauty.Generic.Local {n k : Nat} {σ : Type} (G : Colored n k) (view : σ → Search n) (level numcells : Nat) (st out : σ) : Prop

A local operation preserves the live partition and moves labels only within its current cells, including any newly installed leaf references.

• ok : SearchOk G level numcells (view out)
• effect : SearchOut G level level (view st) (view out)

theorem Hex.GraphIso.Nauty.Generic.Local.trans {n k : Nat} {σ : Type} {G : Colored n k} {view : σ → Search n} {level numcells : Nat} {st middle out : σ} (h₁ : Local G view level numcells st middle) (h₂ : Local G view level numcells middle out) : Local G view level numcells st out

Compose two local operations.

def Hex.GraphIso.Nauty.Generic.Target {n : Nat} {σ : Type} (view : σ → Search n) (level tc : Nat) (cell : VSet n) (st : σ) : Prop

A surviving target set consists of vertices in one nontrivial cell. The empty set needs no target-cell witness.

Equations

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

theorem Hex.GraphIso.Nauty.Generic.Target.subset {n : Nat} {σ : Type} {view : σ → Search n} {level tc : Nat} {cell smaller : VSet n} {st : σ} (h : Target view level tc cell st) (hsub : ∀ (v : Nat), smaller.mem v = true → cell.mem v = true) : Target view level tc smaller st

Removing target vertices preserves the target-cell witness.

theorem Hex.GraphIso.Nauty.Generic.Target.of_out {n k : Nat} {σ : Type} {view : σ → Search n} {G : Colored n k} {level tc : Nat} {cell : VSet n} {st out : σ} (h : Target view level tc cell st) (hout : SearchOut G level level (view st) (view out)) : Target view level tc cell out

A sweep's frame effect transports membership of every remaining target vertex into the returned labelling.

structure Hex.GraphIso.Nauty.Generic.ReachPolicy {n k : Nat} {σ γ : Type} [Policy σ n] (G : Colored n k) (ctx : γ) (inf tcLevel : Nat) (view : σ → Search n) : Prop

Partition rules for the local policy operations. The child and refinement rules compose their own changes with the finer recursive effect; recovery restores the parent's level convention.

• visit (level numcells : Nat) (st : σ) : 1 ≤ level → SearchOk G level numcells (view st) → let r := Policy.visit ctx level numcells st; SearchOk G level r.fst (view r.snd.snd) ∧ ∀ (out : σ), SearchOut G level level (view r.snd.snd) (view out) → SearchOut G (level - 1) level (view st) (view out)
• record (level code numcells : Nat) (st : σ) : SearchOk G level numcells (view st) → Local G view level numcells st (Policy.recordFirst level code st)
• compare (level code numcells : Nat) (st : σ) : SearchOk G level numcells (view st) → Local G view level numcells st (Policy.compareCodes level code st)
• target (first : Bool) (level numcells : Nat) (st : σ) : 1 ≤ level → SearchOk G level numcells (view st) → let r := Policy.chooseTarget first ctx tcLevel level numcells st; Local G view level numcells st r.snd.snd.snd ∧ Target view level r.fst.toNat r.snd.fst r.snd.snd.snd
• firstterminal (level numcells : Nat) (st : σ) : SearchOk G level numcells (view st) → Local G view level numcells st (Policy.firstterminal level st)
• classify (level numcells : Nat) (st : σ) : SearchOk G level numcells (view st) → Local G view level numcells st (Policy.classify ctx level numcells st).snd
• leaf (leaf : Leaf) (level numcells : Nat) (st : σ) : SearchOk G level numcells (view st) → Local G view level numcells st (Policy.leafExit leaf level st).snd
• cheap (first : Bool) (level numcells : Nat) (st : σ) : SearchOk G level numcells (view st) → Local G view level numcells st (Policy.cheapCheck first level st)
• child (first : Bool) (level numcells tc tv : Nat) (cell : VSet n) (st : σ) : 1 ≤ level → SearchOk G level numcells (view st) → Target view level tc cell st → cell.mem tv = true → let child := Policy.child first level tc tv st; SearchOk G (level + 1) (numcells + 1) (view child) ∧ ∀ (out : σ), SearchOut G level (level + 1) (view child) (view out) → SearchOut G level level (view st) (view out)
• afterChild (level tv : Nat) (st : σ) : FrameEq view st (Policy.afterChildFirst level tv st)
• leave (tv : Nat) (st : σ) : FrameEq view st (Policy.leaveChild tv st)
• short (cell : VSet n) (st : σ) (v : Nat) : (Policy.shortprune cell st).mem v = true → cell.mem v = true
• long (cell : VSet n) (st : σ) (v : Nat) : (Policy.longprune cell st).mem v = true → cell.mem v = true
• recover (level numcells : Nat) (st out : σ) : 1 ≤ level → SearchOk G level numcells (view st) → SearchOut G level level (view st) (view out) → Local G view level numcells st (Policy.recover inf level out)
• afterSweep (first : Bool) (level size index : Nat) (st : σ) : FrameEq view st (Policy.afterSweep first level size index st)

def Hex.GraphIso.Nauty.Generic.reachContract {n k : Nat} {σ : Type} (G : Colored n k) (view : σ → Search n) : Contract σ n

Entry and exit assertions for partition reachability. They apply also to truncated searches: exhaustion preserves all frame facts.

Equations

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

theorem Hex.GraphIso.Nauty.Generic.ReachPolicy.finish {n k : Nat} {σ γ : Type} [Policy σ n] {G : Colored n k} {ctx : γ} {inf tcLevel : Nat} {view : σ → Search n} (h : ReachPolicy G ctx inf tcLevel view) {fuel : Nat} {next : SweepFn σ n} (hnext : (reachContract G view).sweepValid fuel (n + 1) next) (first : Bool) (level numcells tc size : Nat) (cell : VSet n) (st : σ) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells (view st)) (htarget : Target view level tc cell st) : have tv := cell.nextElem none; have r := next first level numcells tc (tv.getD 0) tv cell 0 st; SearchOut G level level (view st) (view (match r.fst with | Exit.done => pure (Exit.unwind (level - 1) false, Policy.afterSweep first level size r.snd.fst r.snd.snd) | x => pure (r.fst, r.snd.snd)).run.snd)

Finishing a node's child sweep preserves its frame for every exit.

theorem Hex.GraphIso.Nauty.Generic.ReachPolicy.node_step {n k : Nat} {σ γ : Type} [Policy σ n] {G : Colored n k} {ctx : γ} {inf tcLevel : Nat} {view : σ → Search n} (h : ReachPolicy G ctx inf tcLevel view) {fuel : Nat} {next : SweepFn σ n} (hnext : (reachContract G view).sweepValid fuel (n + 1) next) (first : Bool) (level numcells : Nat) (st : σ) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells (view st)) : SearchOut G (level - 1) level (view st) (view (nodeStep ctx tcLevel next first level numcells st).snd)

Local partition rules compose across refinement and one node's decisions, assuming the child sweep has its frame effect.

theorem Hex.GraphIso.Nauty.Generic.ReachPolicy.advance {n k : Nat} {σ γ : Type} [Policy σ n] {G : Colored n k} {ctx : γ} {inf tcLevel : Nat} {view : σ → Search n} (h : ReachPolicy G ctx inf tcLevel view) {fuel cfuel : Nat} {next : SweepFn σ n} (hnext : (reachContract G view).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (base out : σ) (exit : Exit) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells (view base)) (htarget : Target view level tc cell base) (hout : SearchOut G level level (view base) (view out)) : SearchOut G level level (view base) (view (Generic.advance inf next first level numcells tc tv1 tv cell index out exit).snd.snd)

Consume a child's exit, prune the remaining target, and recover the parent before continuing the sweep.

theorem Hex.GraphIso.Nauty.Generic.ReachPolicy.sweep_step {n k : Nat} {σ γ : Type} [Policy σ n] {G : Colored n k} {ctx : γ} {inf tcLevel : Nat} {view : σ → Search n} (h : ReachPolicy G ctx inf tcLevel view) {fuel cfuel : Nat} {descend : NodeFn σ} {next : SweepFn σ n} (hdescend : (reachContract G view).nodeValid fuel descend) (hnext : (reachContract G view).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st : σ) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells (view st)) (htarget : Target view level tc cell st) (htv : cell.mem tv = true) : SearchOut G level level (view st) (view (sweepStep inf descend next first level numcells tc tv1 tv cell index st).snd.snd)

One sweep iteration preserves its parent frame when both recursive continuations preserve theirs.

theorem Hex.GraphIso.Nauty.Generic.ReachPolicy.sound {n k : Nat} {σ γ : Type} [Policy σ n] {G : Colored n k} {ctx : γ} {inf tcLevel : Nat} {view : σ → Search n} (h : ReachPolicy G ctx inf tcLevel view) : SoundPolicy ctx inf tcLevel (reachContract G view)

The local partition rules instantiate the generic recursion contract.

theorem Hex.GraphIso.Nauty.Generic.node_reach {n k : Nat} {σ γ : Type} [Policy σ n] {G : Colored n k} {ctx : γ} {inf tcLevel : Nat} {view : σ → Search n} (h : ReachPolicy G ctx inf tcLevel view) (first : Bool) (fuel level numcells : Nat) (st : σ) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells (view st)) : SearchOut G (level - 1) level (view st) (view (node first ctx inf tcLevel fuel level numcells st).snd)

Every policy satisfying the local partition rules preserves node reachability.

theorem Hex.GraphIso.Nauty.Generic.sweep_reach {n k : Nat} {σ γ : Type} [Policy σ n] {G : Colored n k} {ctx : γ} {inf tcLevel : Nat} {view : σ → Search n} (h : ReachPolicy G ctx inf tcLevel view) (first : Bool) (fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : σ) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells (view st)) (htarget : Target view level tc cell st) (hcursor : ∀ (v : Nat), cursor = some v → cell.mem v = true) : SearchOut G level level (view st) (view (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd)

Every policy satisfying the local partition rules preserves sweep reachability.