def Hex.GraphIso.Nauty.Generic.preserveContract {σ : Type} (n : Nat) (P : σ → Prop) : Contract σ n

A persistent assertion on every node and sweep, including the first descent, exhausted calls, and nonlocal returns.

Equations

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

structure Hex.GraphIso.Nauty.Generic.Preserve {n : Nat} {σ γ : Type} [Policy σ n] (ctx : γ) (inf tcLevel : Nat) (P : σ → Prop) : Prop

Local preservation rules for the actual policy operations. These have no recursive correctness premise; sound composes them by the shared engine.

• visit (level numcells : Nat) (st : σ) : P st → P (Policy.visit ctx level numcells st).snd.snd
• record (level code : Nat) (st : σ) : P st → P (Policy.recordFirst level code st)
• compare (level code : Nat) (st : σ) : P st → P (Policy.compareCodes level code st)
• target (first : Bool) (level numcells : Nat) (st : σ) : P st → P (Policy.chooseTarget first ctx tcLevel level numcells st).snd.snd.snd
• terminal (level : Nat) (st : σ) : P st → P (Policy.firstterminal level st)
• classify (level numcells : Nat) (st : σ) : P st → P (Policy.classify ctx level numcells st).snd
• leaf (leaf : Leaf) (level : Nat) (st : σ) : P st → P (Policy.leafExit leaf level st).snd
• cheap (first : Bool) (level : Nat) (st : σ) : P st → P (Policy.cheapCheck first level st)
• child (first : Bool) (level tc tv : Nat) (st : σ) : P st → P (Policy.child first level tc tv st)
• afterChild (level tv : Nat) (st : σ) : P st → P (Policy.afterChildFirst level tv st)
• leave (tv : Nat) (st : σ) : P st → P (Policy.leaveChild tv st)
• recover (level : Nat) (st : σ) : P st → P (Policy.recover inf level st)
• afterSweep (first : Bool) (level size index : Nat) (st : σ) : P st → P (Policy.afterSweep first level size index st)

theorem Hex.GraphIso.Nauty.Generic.Preserve.node_step {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {P : σ → Prop} (h : Preserve ctx inf tcLevel P) {fuel : Nat} {next : SweepFn σ n} (hn : (preserveContract n P).sweepValid fuel (n + 1) next) (first : Bool) (level numcells : Nat) (st : σ) (hp : P st) : P (nodeStep ctx tcLevel next first level numcells st).snd

theorem Hex.GraphIso.Nauty.Generic.Preserve.sweep_step {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {P : σ → Prop} (h : Preserve ctx inf tcLevel P) {fuel cfuel : Nat} {descend : NodeFn σ} {next : SweepFn σ n} (hd : (preserveContract n P).nodeValid fuel descend) (hn : (preserveContract n P).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st : σ) (hp : P st) : P (sweepStep inf descend next first level numcells tc tv1 tv cell index st).snd.snd

theorem Hex.GraphIso.Nauty.Generic.Preserve.sound {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {P : σ → Prop} (h : Preserve ctx inf tcLevel P) : SoundPolicy ctx inf tcLevel (preserveContract n P)

The shared mutual recursion preserves the assertion on every path.