def
Hex.GraphIso.Nauty.Sparse.RouteHistory
{n : Nat}
(G : SparseGraph n)
(tcLevel level agreed numcells : Nat)
(st : State n)
:
The saved selected reference and the current guided native history at the actual first ancestor. This invariant applies outside cheap subtrees.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.RouteHistory.bound
{n : Nat}
{G : SparseGraph n}
{tcLevel level agreed numcells : Nat}
{st : State n}
(h : RouteHistory G tcLevel level agreed numcells st)
:
theorem
Hex.GraphIso.Nauty.Sparse.RouteHistory.transport
{n : Nat}
{G : SparseGraph n}
{tcLevel level agreed numcells : Nat}
{st out : State n}
{level' agreed' numcells' : Nat}
(h : RouteHistory G tcLevel level agreed numcells st)
(hr : SearchState.reference out = SearchState.reference st)
(hg : out.gcaFirst = st.gcaFirst)
(ha :
∀ (root : RefineSt n),
RouteAligned G tcLevel st.gcaFirst root level agreed numcells st →
RouteAligned G tcLevel st.gcaFirst root level' agreed' numcells' out)
:
RouteHistory G tcLevel level' agreed' numcells' out
theorem
Hex.GraphIso.Nauty.Sparse.RouteHistory.compare
{n : Nat}
{G : SparseGraph n}
{tcLevel level numcells : Nat}
{st : State n}
(h : RouteHistory G tcLevel level (level - 1) numcells st)
(hl : 0 < level)
(code : Nat)
:
RouteHistory G tcLevel level level numcells (compareCodes level code st)
theorem
Hex.GraphIso.Nauty.Sparse.RouteHistory.target
{n : Nat}
{G : SparseGraph n}
{tcLevel level numcells : Nat}
{st : State n}
(h : RouteHistory G tcLevel level level numcells st)
:
RouteHistory G tcLevel level level numcells (chooseTarget false (Graph.ofGraph G) tcLevel level numcells st).snd.snd.snd
theorem
Hex.GraphIso.Nauty.Sparse.RouteHistory.classify
{n : Nat}
{G : SparseGraph n}
{tcLevel level numcells : Nat}
{st : State n}
(h : RouteHistory G tcLevel level level numcells st)
:
RouteHistory G tcLevel level level numcells (Sparse.classify (Graph.ofGraph G) level numcells st).snd
theorem
Hex.GraphIso.Nauty.Sparse.RouteHistory.leaf
{n : Nat}
{G : SparseGraph n}
{tcLevel level numcells : Nat}
{st : State n}
(h : RouteHistory G tcLevel level level numcells st)
(leaf : Leaf)
:
RouteHistory G tcLevel level level numcells (leafExit leaf level st).snd
theorem
Hex.GraphIso.Nauty.Sparse.RouteHistory.cheap
{n : Nat}
{G : SparseGraph n}
{tcLevel level numcells : Nat}
{st : State n}
(h : RouteHistory G tcLevel level level numcells st)
(first : Bool)
:
RouteHistory G tcLevel level level numcells (cheapCheck first level st)
theorem
Hex.GraphIso.Nauty.Sparse.RouteHistory.child
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel level numcells tc tv : Nat}
{st : State n}
{cell : VSet n}
(h : RouteHistory G.graph tcLevel level level numcells st)
(first : Bool)
(hok : Ready G level numcells st)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(hrecord : RouteRecorded G.graph tcLevel level tc st)
:
have next := Generic.Policy.child first level tc tv st;
have r := visit (Graph.ofGraph G.graph) (level + 1) (numcells + 1) next;
RouteHistory G.graph tcLevel (level + 1) level r.fst r.snd.snd
Guided target choices extend both reference histories through the actual individualized child and its cached refinement.
theorem
Hex.GraphIso.Nauty.Sparse.RouteHistory.child_return
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc tv : Nat}
{st : State n}
{cell : VSet n}
(h : RouteHistory G.graph tcLevel level level numcells st)
(first : Bool)
(hl : 1 ≤ level)
(hok : Ready G level numcells st)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
:
have out :=
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd;
have result := Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv out);
RouteHistory G.graph tcLevel level level numcells result ∧ (RouteRecorded G.graph tcLevel level tc st → RouteRecorded G.graph tcLevel level tc result)
An actual off-path child retains the guided history and target choice at its recovered parent. The proof uses full-call frame and divergence results, including for a truncated child call.