def
Hex.GraphIso.Nauty.Sparse.Compact.checkChildren
{n : Nat}
(G : SparseGraph n)
(level : Nat)
(lab ptn : Array Nat)
(tc : Nat)
(check : Nat → CertNode → Option Bool)
(cs : List CertNode)
:
Check all target positions, replaying ordinary children once and copying earlier attainment flags only through checked automorphisms of child cells.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Compact.checkChildren_valid
{n : Nat}
{G : SparseGraph n}
{B : Key n}
{tcLevel fuel level numcells tc : Nat}
{lab ptn : Array Nat}
{active : VSet n}
{check : Nat → CertNode → Option Bool}
{cs : List CertNode}
{a : Bool}
(hp : SpecNode G level lab ptn active numcells)
(heq : Equitable (Graph.context G) level lab ptn)
(hc : IsCell ptn level tc cs.length)
(hb : tc + cs.length ≤ n)
(hn : 1 < cs.length)
(hcheck :
∀ (o : Nat) (c : CertNode) (b : Bool),
o < cs.length →
check o c = some b →
have child := breakout n lab ptn (level + 1) tc lab[tc + o]!;
Replay.Valid G B (specLeaves G tcLevel fuel (level + 1) child.fst child.snd.fst child.snd.snd (numcells + 1)) b)
(h : checkChildren G level lab ptn tc check cs = some a)
:
Replay.Valid G B
(List.flatMap
(fun (o : Nat) =>
have child := breakout n lab ptn (level + 1) tc lab[tc + o]!;
specLeaves G tcLevel fuel (level + 1) child.fst child.snd.fst child.snd.snd (numcells + 1))
(List.range cs.length))
a
Sibling reference replay covers the whole target cell. Both the ordinary child rule and the automorphism rule preserve exact attainment.
theorem
Hex.GraphIso.Nauty.Sparse.Compact.checkChildren_exists
{n : Nat}
{G : SparseGraph n}
{level tc : Nat}
{lab ptn : Array Nat}
{check : Nat → CertNode → Option Bool}
{cs : List CertNode}
(hsteps :
∀ (o : Nat) (ho : o < cs.length) (seen : Array Bool),
seen.size = o →
have child := fun (j : Nat) => breakout n lab ptn (level + 1) tc lab[tc + j]!;
∃ (a : Bool), Replay.sibling check
(fun (j earlier : Nat) (raw : Array Nat) =>
Replay.checkAutom G (level + 1) (child earlier).fst (child j).fst (child j).snd.fst raw)
seen cs[o] = some a)
:
If every emitted record succeeds at its actual target offset, the full ordered scan succeeds. Earlier attainment flags may have either value.