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

The checked subgroup generated by successful leaves visited so far.

• group : Group n
• inside : self.group.IsSubgroup G
• satisfies (p : Perm n) : Generated self.group.generators p → P.test p = true

def Hex.PermGroup.Search.Accumulator.empty {n : Nat} (G : Group n) (P : Predicate n) : Accumulator G P

Equations

• Hex.PermGroup.Search.Accumulator.empty G P = { group := Hex.PermGroup.Group.ofGenerators #[], inside := ⋯, satisfies := ⋯ }

def Hex.PermGroup.Search.Accumulator.adjoin {n : Nat} {G : Group n} {P : Predicate n} (a : Accumulator G P) (p : Element G) (hp : P.test p.val = true) : Accumulator G P

Add a successful leaf and rebuild its checked chain. The traversal calls this only after the subtree-containment check has failed.

Equations

• a.adjoin p hp = { group := Hex.PermGroup.Group.ofGenerators (a.group.generators.push p.val), inside := ⋯, satisfies := ⋯ }

theorem Hex.PermGroup.Search.Accumulator.adjoin_grows {n : Nat} {G : Group n} {P : Predicate n} (a : Accumulator G P) (p : Element G) (hp : P.test p.val = true) : a.group.IsSubgroup (a.adjoin p hp).group

theorem Hex.PermGroup.Search.Accumulator.mem_adjoin {n : Nat} {G : Group n} {P : Predicate n} (a : Accumulator G P) (p : Element G) (hp : P.test p.val = true) : Generated (a.adjoin p hp).group.generators p.val

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

A traversal returns a growing checked subgroup and a certificate covering every satisfying completion of its starting node.

• acc : Accumulator G P
• grows : a.group.IsSubgroup self.acc.group
• certificate : Certificate C.Reason
• checked : checkTree C self.acc.group t self.certificate = true