def
Hex.GraphIso.Nauty.Sparse.RouteRecorded
{n : Nat}
(G : SparseGraph n)
(tcLevel level tc : Nat)
(st : State n)
:
While first-code agreement is live, a target used by the production sweep is either the native unhinted target or the saved first target.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.chooseTarget_hint_eq
{n : Nat}
{g : Graph n}
{tcLevel level numcells : Nat}
{st : State n}
(hl : 0 < level)
(hnc : numcells < n)
(he : st.eqlevFirst = level)
(hneg : st.compCanon < 0)
(hkeep : (chooseTarget false g tcLevel level numcells st).snd.snd.snd.eqlevFirst = level)
:
The hinted branch explicitly drops agreement when its returned target differs from the saved slot. Retained agreement therefore identifies the slot.
theorem
Hex.GraphIso.Nauty.Sparse.route_recorded
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel level numcells : Nat}
{st : State n}
(hn : 0 < n)
(hl : 0 < level)
(h : Ready G level numcells st)
(hb : st.eqlevFirst ≤ level)
(hnc : numcells < n)
:
have r := chooseTarget false (Graph.ofGraph G.graph) tcLevel level numcells st;
RouteRecorded G.graph tcLevel level r.fst.toNat r.snd.snd.snd
The literal cached selector supplies the guided target condition. All cache and partition premises concern the actual prepared state.
theorem
Hex.GraphIso.Nauty.Sparse.RouteRecorded.congr
{n : Nat}
{G : SparseGraph n}
{tcLevel level tc : Nat}
{st out : State n}
(h : RouteRecorded G tcLevel level tc st)
(he : out.eqlevFirst = st.eqlevFirst)
(hl : out.lab = st.lab)
(hp : out.ptn = st.ptn)
(ht : out.firsttc = st.firsttc)
:
RouteRecorded G tcLevel level tc out
theorem
Hex.GraphIso.Nauty.Sparse.RouteRecorded.cheap
{n : Nat}
{G : SparseGraph n}
{tcLevel level tc : Nat}
{st : State n}
(h : RouteRecorded G tcLevel level tc st)
(first : Bool)
:
RouteRecorded G tcLevel level tc (cheapCheck first level st)
theorem
Hex.GraphIso.Nauty.Sparse.Ready.target_recover
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel level numcells : Nat}
{st out : State n}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(hx : FrameOut G level level st out)
:
have r := Generic.Policy.recover (n + 2) level out;
targetcell (Graph.ofGraph G.graph) r.lab r.ptn level tcLevel (-1) = targetcell (Graph.ofGraph G.graph) st.lab st.ptn level tcLevel (-1)
Returning from a child and restoring its parent's partition preserves the native unhinted target even when labels inside cells have changed order.