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

A short return carries a property established by its emitting leaf.

Equations

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

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

Only leaf emission and cleanup along an unconsumed return must preserve the property. A receiving loop may consume it and resume.

• leaf (ctx : γ) (level numcells : Nat) (st : σ) : let c := Policy.classify ctx level numcells st; ∀ (target : Nat), (Policy.leafExit c.fst level c.snd).fst = Exit.unwind target true → P target (Policy.leafExit c.fst level c.snd).snd
• afterFirst (level tv target : Nat) (st : σ) : P target st → P target (Policy.afterChildFirst level tv st)
• leave (tv target : Nat) (st : σ) : P target st → P target (Policy.leaveChild tv st)

theorem Hex.GraphIso.Nauty.Generic.short_resume {n : Nat} {σ γ : Type} [Policy σ n] {P : Nat → σ → Prop} {fuel cfuel : Nat} {next : SweepFn σ n} (hnext : (shortContract P).sweepValid fuel cfuel next) (inf : Nat) (first : Bool) (level numcells tc tv1 tv : Nat) (cell : VSet n) (index : Nat) (st : σ) (target : Nat) : (resume inf next first level numcells tc tv1 tv cell index st).fst = Exit.unwind target true → P target (resume inf next first level numcells tc tv1 tv cell index st).snd.snd

Resuming a sweep obtains any new short return from its continuation.

theorem Hex.GraphIso.Nauty.Generic.short_advance {n : Nat} {σ γ : Type} [Policy σ n] {P : Nat → σ → Prop} {fuel cfuel : Nat} {next : SweepFn σ n} (hnext : (shortContract P).sweepValid fuel cfuel next) (inf : Nat) (first : Bool) (level numcells tc tv1 tv : Nat) (cell : VSet n) (index : Nat) (st : σ) (exit : Exit) (hout : ∀ (target : Nat), exit = Exit.unwind target true → P target st) (target : Nat) : (advance inf next first level numcells tc tv1 tv cell index st exit).fst = Exit.unwind target true → P target (advance inf next first level numcells tc tv1 tv cell index st exit).snd.snd

An intermediate loop transports an unconsumed short return.

theorem Hex.GraphIso.Nauty.Generic.short_node {n : Nat} {σ γ : Type} [Policy σ n] {P : Nat → σ → Prop} (h : ShortPolicy P) {fuel : Nat} {next : SweepFn σ n} (hnext : (shortContract P).sweepValid fuel (n + 1) next) (ctx : γ) (tcLevel : Nat) (first : Bool) (level numcells : Nat) (st : σ) (target : Nat) : (nodeStep ctx tcLevel next first level numcells st).fst = Exit.unwind target true → P target (nodeStep ctx tcLevel next first level numcells st).snd

A node can emit a short return only at a leaf or through its sweep.

theorem Hex.GraphIso.Nauty.Generic.short_sweep {n : Nat} {σ γ : Type} [Policy σ n] {P : Nat → σ → Prop} (h : ShortPolicy P) {fuel cfuel : Nat} {descend : NodeFn σ} {next : SweepFn σ n} (hdescend : (shortContract P).nodeValid fuel descend) (hnext : (shortContract P).sweepValid fuel cfuel next) (inf : Nat) (first : Bool) (level numcells tc tv1 tv : Nat) (cell : VSet n) (index : Nat) (st : σ) (target : Nat) : (sweepStep inf descend next first level numcells tc tv1 tv cell index st).fst = Exit.unwind target true → P target (sweepStep inf descend next first level numcells tc tv1 tv cell index st).snd.snd

Cleanup preserves the emitting leaf's property before the loop either transports the return or resumes its continuation.

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

The leaf rules instantiate the common recursion's contract.

theorem Hex.GraphIso.Nauty.Generic.node_short {n : Nat} {σ γ : Type} [Policy σ n] {P : Nat → σ → Prop} (h : ShortPolicy P) (first : Bool) (ctx : γ) (inf tcLevel fuel level numcells : Nat) (st : σ) (target : Nat) : (node first ctx inf tcLevel fuel level numcells st).fst = Exit.unwind target true → P target (node first ctx inf tcLevel fuel level numcells st).snd

Every short return carries a property of its emitting leaf.

theorem Hex.GraphIso.Nauty.Generic.sweep_short {n : Nat} {σ γ : Type} [Policy σ n] {P : Nat → σ → Prop} (h : ShortPolicy P) (first : Bool) (ctx : γ) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (index : Nat) (st : σ) (target : Nat) : (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).fst = Exit.unwind target true → P target (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

An unconsumed short return retains its emitting leaf's property through any number of intermediate sweeps.