@[irreducible]

def Hex.PermGroup.Search.visit {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (t : Node G) (a : Accumulator G P) : Result C t a

Exact deterministic backtracking. A successful leaf contributes a new generator only if needed; subsequent subtrees can be covered by the growing subgroup. Rejected subtrees retain the constraint's replayable reason.

Equations

• One or more equations did not get rendered due to their size.

structure Hex.PermGroup.Search.Solution {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) : Type

An accepted completeness certificate accompanies every exact result.

• group : Group n
• certificate : Certificate C.Reason
• checked : checkSearch C self.group self.certificate = true

theorem Hex.PermGroup.Search.Solution.spec {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (s : Solution C) (p : Perm n) : Generated s.group.generators p ↔ Generated G.generators p ∧ P.test p = true

def Hex.PermGroup.Search.solve {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) : Solution C

Search starts with the trivial subgroup and follows the input group's checked chain. No list of all input elements is constructed.

Equations

• One or more equations did not get rendered due to their size.