def Hex.GraphIso.Nauty.Sparse.DistanceState.Rel {n : Nat} (σ : Renaming n) (level : Nat) (s t : RefineSt n) (a b : RefineSt n × Nat) : Prop

The two executed distance scans have valid states, the same cursor, and corresponding refinement observations.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.DistanceState.step_rel {n : Nat} (σ : Renaming n) (level first : Nat) (s t a b : RefineSt n) (hs : RefineSt.Valid level s) (ht : RefineSt.Valid level t) (hv : ∀ (v : Nat), v < n → s.hits[v]! ≤ n) (hw : ∀ (v : Nat), v < n → t.hits[v]! ≤ n) (hkeys : ∀ (v : Nat), v < n → t.hits[σ.toFun v]! = s.hits[v]!) (ha : DistanceState level s a first) (hb : DistanceState level t b first) (he : RefineSt.Equiv σ level a b) : Loop.Rel (Rel σ level s t) (if first ≥ n then ForInStep.done (a, first) else have last := a.cellend[first]!; if first < last then ForInStep.yield (splitCounts level first true a, last + 1) else ForInStep.yield (a, last + 1)) (if first ≥ n then ForInStep.done (b, first) else have last := b.cellend[first]!; if first < last then ForInStep.yield (splitCounts level first true b, last + 1) else ForInStep.yield (b, last + 1))

One literal distance-loop callback transports its state and its stop/continue choice, including skipped singleton cells.