theorem
Hex.GraphIso.Nauty.Sparse.prepareFirst_noncheap
{n : Nat}
(g : Graph n)
(tcLevel level numcells : Nat)
(st : State n)
:
theorem
Hex.GraphIso.Nauty.Sparse.firstLeaf_noncheap
{n : Nat}
{g : Graph n}
{tcLevel fuel level numcells last bound : Nat}
{st leaf : State n}
(path : Generic.FirstPath g tcLevel fuel level numcells st last leaf)
(hl : bound < level)
(h : bound < st.noncheaplevel)
:
Descending the actual first branch cannot enable a failed guard above it.
theorem
Hex.GraphIso.Nauty.Sparse.firstPath_noncheap
{n : Nat}
{g : Graph n}
{inf tcLevel fuel level numcells last bound : Nat}
{st leaf : State n}
(path : Generic.FirstPath g tcLevel fuel level numcells st last leaf)
(hl : bound < level)
(h : bound < st.noncheaplevel)
:
The complete first-path search retains every failed ancestor guard, including all later siblings and returns past intervening frames.
def
Hex.GraphIso.Nauty.Sparse.FirstShape
{n : Nat}
(G : SparseGraph n)
(level numcells : Nat)
(st : State n)
:
A skipped cheap test on the first branch inherits the earlier passing guard's shape for the literal cached refinement at this entry.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.FirstShape.initial
{n : Nat}
(G : SparseGraph n)
(lab : Array Nat)
(ends : List Nat)
:
FirstShape G 1 ends.length (Sparse.initial (Graph.ofGraph G) lab ends)
theorem
Hex.GraphIso.Nauty.Sparse.FirstShape.prepare
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel level numcells : Nat}
{st : State n}
(h : FirstShape G.graph level numcells st)
(hok : NodeInv G level numcells st)
(hcheap :
(cheapCheck true level
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.snd.snd).noncheaplevel ≤ level)
:
NodeShape n level (State.refined (Graph.ofGraph G.graph) level numcells st).ptn
The guard supplies the shape at a first node, either from a preceding guard or from the actual cheapautom call performed at this level.
theorem
Hex.GraphIso.Nauty.Sparse.FirstShape.child
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel level numcells tv : Nat}
{st : State n}
(h : FirstShape G.graph level numcells st)
(hok : NodeInv G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(hv : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.fst.mem tv = true)
:
have r := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st;
FirstShape G.graph (level + 1) (r.fst + 1)
(Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd))
The inherited shape extends to each actual first child; its refinement retains the shape while using the child's real invalidated scratch.