def Hex.GraphIso.Nauty.Sparse.Limited.tail {n : Nat} {σ γ : Type} [Generic.Policy σ n] (next : Generic.SweepFn σ n) (first : Bool) (level nc tc size : Nat) (cell : VSet n) (s : σ) : Generic.Exit × σ

The literal common tail of Generic.nodeStep, for either state type.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Limited.nodeStep_eq {n : Nat} {σ γ : Type} [Generic.Policy σ n] (g : γ) (tcLevel : Nat) (next : Generic.SweepFn σ n) (first : Bool) (level nc : Nat) (s : σ) : Generic.nodeStep g tcLevel next first level nc s = have r := Generic.Policy.visit g level nc s; have recorded := if first = true then Generic.Policy.recordFirst level r.snd.fst r.snd.snd else Generic.Policy.compareCodes level r.snd.fst r.snd.snd; have t := Generic.Policy.chooseTarget first g tcLevel level r.fst recorded; if first = true then if (r.fst == n) = true then (Generic.Exit.unwind (level - 1) false, Generic.Policy.firstterminal level t.snd.snd.snd) else tail next first level r.fst t.fst.toNat t.snd.snd.fst t.snd.fst t.snd.snd.snd else have c := Generic.Policy.classify g level r.fst t.snd.snd.snd; have e := Generic.Policy.leafExit c.fst level c.snd; match e.fst with | Generic.Exit.done => tail next first level r.fst t.fst.toNat t.snd.snd.fst t.snd.fst e.snd | x => e

This decomposition is definitionally the executed node step.

theorem Hex.GraphIso.Nauty.Sparse.Limited.cheap_ready {n : Nat} (first : Bool) (level : Nat) (s : State n) : Ready (Generic.Policy.cheapCheck first level s) ↔ Ready s

theorem Hex.GraphIso.Nauty.Sparse.Limited.cheap_value {n : Nat} (first : Bool) (level : Nat) {s : State n} (hs : Ready s) : (Generic.Policy.cheapCheck first level s).value = Generic.Policy.cheapCheck first level s.value

theorem Hex.GraphIso.Nauty.Sparse.Limited.afterSweep_ready {n : Nat} (first : Bool) (level size index : Nat) (s : State n) : Ready (Generic.Policy.afterSweep first level size index s) ↔ Ready s

theorem Hex.GraphIso.Nauty.Sparse.Limited.afterSweep_value {n : Nat} (first : Bool) (level size index : Nat) {s : State n} (hs : Ready s) : (Generic.Policy.afterSweep first level size index s).value = Generic.Policy.afterSweep first level size index s.value

theorem Hex.GraphIso.Nauty.Sparse.Limited.tail_eq {n : Nat} {next : Generic.SweepFn (State n) n} {plain : Generic.SweepFn (Sparse.State n) n} (hn : SweepEq next plain) (first : Bool) (level nc tc size : Nat) (cell : VSet n) (s : State n) (h : Ready (tail next first level nc tc size cell s).snd) : Ready s ∧ nodeValue (tail next first level nc tc size cell s) = tail plain first level nc tc size cell s.value

theorem Hex.GraphIso.Nauty.Sparse.Limited.nodeStep_exhausted {n : Nat} (g : Graph n) (tcLevel : Nat) (next : Generic.SweepFn (State n) n) (first : Bool) (level nc : Nat) (s : State n) (hg : (s.exhausted || s.remaining == 0) = true) : (Generic.nodeStep g tcLevel next first level nc s).snd.exhausted = true

Rejecting a visit produces an exhausted node immediately; it cannot call the supplied sibling continuation or execute native callbacks.

theorem Hex.GraphIso.Nauty.Sparse.Limited.nodeStep_value {n : Nat} {next : Generic.SweepFn (State n) n} {plain : Generic.SweepFn (Sparse.State n) n} (hn : SweepEq next plain) (g : Graph n) (tcLevel : Nat) (first : Bool) (level nc : Nat) (s : State n) (h : Ready (Generic.nodeStep g tcLevel next first level nc s).snd) : Ready s ∧ nodeValue (Generic.nodeStep g tcLevel next first level nc s) = Generic.nodeStep g tcLevel plain first level nc s.value

An accepted bounded node takes exactly the native visit, classification and child-sweep path. Rejected visits cannot produce an accepted return.