theorem
Hex.GraphIso.Nauty.Max.SweepInput.reference
{n k : Nat}
{G : Colored n k}
{tcLevel fuel cfuel boundary level numcells tc tv1 index : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G { g := rowsOf G } tcLevel fuel cfuel false level numcells tc tv1 cursor cell index st l bs fs parents)
(hn : (contract G tcLevel).nodeValid fuel (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel fuel))
{R : RefineSt n}
{targets : List Nat}
{key : Key n}
(hit : IterOk { g := rowsOf G } level R)
(hlab : R.lab = (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.snd.lab)
(hptn : R.ptn = (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.snd.ptn)
(hboundary : level < boundary)
(hvisit :
∀ {cfuel tv index : Nat} {cell : VSet n} {st : Search n} {bs fs : List Nat},
SweepInput G { g := rowsOf G } tcLevel fuel cfuel false level numcells tc tv1 (some tv) cell index st l bs fs
parents →
Generation.Matches { g := rowsOf G } (level + 1) st targets key →
st.eqlevFirst = level →
boundary ≤ st.allsamelevel →
st.gcaFirst < level →
∀ (o : Nat),
o < (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.fst →
R.lab[tc + o]! = tv →
Generation.ChildPath { g := rowsOf G } tcLevel boundary level R tc targets key o →
have out :=
Nauty.node false { g := rowsOf G } (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(child false level tc tv st);
∀ (target : Nat) (short : Bool),
out.fst = Generic.Exit.unwind target short → RefReturn { g := rowsOf G } target out.snd)
{previous : Option Nat}
(hnext : cell.nextElem previous = cursor)
(hcover :
Generation.PathCover { g := rowsOf G } tcLevel boundary level R tc
(Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.fst targets key cell previous)
(hocc :
∃ (o : Nat), o < (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.fst ∧ Generation.ChildPath { g := rowsOf G } tcLevel boundary level R tc targets key o)
(hpast : Generation.CanonPast level tc previous st)
(hm : Generation.Matches { g := rowsOf G } (level + 1) st targets key)
(heq : st.eqlevFirst = level)
(hsame : boundary ≤ st.allsamelevel)
(hguide : st.gcaFirst < level)
(hcheap : level < st.noncheaplevel)
:
An actual off-path sweep containing a matching reference returns emitted evidence. The child premise is restricted to the actual smaller calls; reception and both workspace filters preserve reference absence.