def Hex.GraphIso.Nauty.Sparse.Limited.Ready {n : Nat} (s : State n) : Prop

Equations

• Hex.GraphIso.Nauty.Sparse.Limited.Ready s = (s.exhausted = false)

def Hex.GraphIso.Nauty.Sparse.Limited.nodeValue {n : Nat} (r : Generic.Exit × State n) : Generic.Exit × Sparse.State n

Erase only limit bookkeeping from a node return.

Equations

• Hex.GraphIso.Nauty.Sparse.Limited.nodeValue r = (r.fst, r.snd.value)

def Hex.GraphIso.Nauty.Sparse.Limited.sweepValue {n : Nat} (r : Generic.Exit × Nat × State n) : Generic.Exit × Nat × Sparse.State n

Erase only limit bookkeeping from a sibling-sweep return.

Equations

• Hex.GraphIso.Nauty.Sparse.Limited.sweepValue r = (r.fst, r.snd.fst, r.snd.snd.value)

def Hex.GraphIso.Nauty.Sparse.Limited.NodeEq {n : Nat} (f : Generic.NodeFn (State n)) (plain : Generic.NodeFn (Sparse.State n)) : Prop

On a non-exhausted return, both engines agree exactly; the input was also non-exhausted. This backward condition excludes recovery from failure.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Limited.SweepEq {n : Nat} (f : Generic.SweepFn (State n) n) (plain : Generic.SweepFn (Sparse.State n) n) : Prop

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Limited.map_ready {n : Nat} (f : Sparse.State n → Sparse.State n) (s : State n) : Ready (map f s) ↔ Ready s

theorem Hex.GraphIso.Nauty.Sparse.Limited.map_value {n : Nat} (f : Sparse.State n → Sparse.State n) {s : State n} (hs : Ready s) : (map f s).value = f s.value

theorem Hex.GraphIso.Nauty.Sparse.Limited.visit_ready {n : Nat} {g : Graph n} {level nc : Nat} {s : State n} (h : Ready (visit g level nc s).snd.snd) : Ready s ∧ 0 < s.remaining

theorem Hex.GraphIso.Nauty.Sparse.Limited.visit_value {n : Nat} (g : Graph n) (level nc : Nat) {s : State n} (hs : Ready s) (hq : 0 < s.remaining) : have r := visit g level nc s; (r.fst, r.snd.fst, r.snd.snd.value) = Sparse.visit g level nc s.value

An admitted visit projects to the literal native refinement call.

theorem Hex.GraphIso.Nauty.Sparse.Limited.recover_ready {n : Nat} (inf level : Nat) (s : State n) : Ready (Generic.Policy.recover inf level s) ↔ Ready s

theorem Hex.GraphIso.Nauty.Sparse.Limited.recover_value {n : Nat} (inf level : Nat) {s : State n} (hs : Ready s) : (Generic.Policy.recover inf level s).value = Generic.Policy.recover inf level s.value

theorem Hex.GraphIso.Nauty.Sparse.Limited.orbit_value {n : Nat} (tv : Nat) {s : State n} (hs : Ready s) : Generic.Policy.orbit s tv = Generic.Policy.orbit s.value tv

theorem Hex.GraphIso.Nauty.Sparse.Limited.longprune_value {n : Nat} (cell : VSet n) {s : State n} (hs : Ready s) : Generic.Policy.longprune cell s = Generic.Policy.longprune cell s.value

theorem Hex.GraphIso.Nauty.Sparse.Limited.shortprune_value {n : Nat} (cell : VSet n) {s : State n} (hs : Ready s) : Generic.Policy.shortprune cell s = Generic.Policy.shortprune cell s.value

theorem Hex.GraphIso.Nauty.Sparse.Limited.resume_eq {n : Nat} {next : Generic.SweepFn (State n) n} {plain : Generic.SweepFn (Sparse.State n) n} (hn : SweepEq next plain) (inf : Nat) (first : Bool) (level nc tc tv1 tv index : Nat) (cell : VSet n) (s : State n) (h : Ready (Generic.resume inf next first level nc tc tv1 tv cell index s).snd.snd) : Ready s ∧ sweepValue (Generic.resume inf next first level nc tc tv1 tv cell index s) = Generic.resume inf plain first level nc tc tv1 tv cell index s.value

Recovery, the long filter and the orbit-index update project to the native continuation whenever the resumed sweep returns successfully.

theorem Hex.GraphIso.Nauty.Sparse.Limited.advance_eq {n : Nat} {next : Generic.SweepFn (State n) n} {plain : Generic.SweepFn (Sparse.State n) n} (hn : SweepEq next plain) (inf : Nat) (first : Bool) (level nc tc tv1 tv index : Nat) (cell : VSet n) (s : State n) (exit : Generic.Exit) (h : Ready (Generic.advance inf next first level nc tc tv1 tv cell index s exit).snd.snd) : Ready s ∧ sweepValue (Generic.advance inf next first level nc tc tv1 tv cell index s exit) = Generic.advance inf plain first level nc tc tv1 tv cell index s.value exit

Nonlocal returns and the short filter retain exact native control flow.

theorem Hex.GraphIso.Nauty.Sparse.Limited.child_ready {n : Nat} (first : Bool) (level tc tv : Nat) (s : State n) : Ready (Generic.Policy.child first level tc tv s) ↔ Ready s

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

theorem Hex.GraphIso.Nauty.Sparse.Limited.leave_ready {n : Nat} (tv : Nat) (s : State n) : Ready (Generic.Policy.leaveChild tv s) ↔ Ready s

theorem Hex.GraphIso.Nauty.Sparse.Limited.leave_value {n : Nat} (tv : Nat) {s : State n} (hs : Ready s) : (Generic.Policy.leaveChild tv s).value = Generic.Policy.leaveChild tv s.value

theorem Hex.GraphIso.Nauty.Sparse.Limited.afterFirst_ready {n : Nat} (level tv : Nat) (s : State n) : Ready (Generic.Policy.afterChildFirst level tv s) ↔ Ready s

theorem Hex.GraphIso.Nauty.Sparse.Limited.afterFirst_value {n : Nat} (level tv : Nat) {s : State n} (hs : Ready s) : (Generic.Policy.afterChildFirst level tv s).value = Generic.Policy.afterChildFirst level tv s.value