def Hex.PermGroup.Search.Tester.normalizer {n : Nat} {budget : Budget} (H : Group n) : Tester (Predicate.normalizer H) budget

Both directions of the generator-conjugation test use the shared sift allowance. The second direction is skipped after a failed forward test.

Equations

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

def Hex.PermGroup.Group.intersectionBudgeted {n : Nat} (budget : Execution.Budget) (G H : Group n) : Search.Outcome (Search.Intersection.constraint G H) budget

Equations

• Hex.PermGroup.Group.intersectionBudgeted budget G H = Hex.PermGroup.Search.solveBudgeted budget (Hex.PermGroup.Search.Intersection.constraint G H) (Hex.PermGroup.Search.Tester.subgroup H)

def Hex.PermGroup.Group.centralizerBudgeted {n : Nat} (budget : Execution.Budget) (G H : Group n) : Search.Outcome (Search.Centralizer.constraint G H) budget

Equations

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

def Hex.PermGroup.Group.centerBudgeted {n : Nat} (budget : Execution.Budget) (G : Group n) : Search.Outcome (Search.Centralizer.constraint G G) budget

Equations

• Hex.PermGroup.Group.centerBudgeted budget G = Hex.PermGroup.Group.centralizerBudgeted budget G G

def Hex.PermGroup.Group.centralizerPermBudgeted {n : Nat} (budget : Execution.Budget) (G : Group n) (p : Perm n) : Search.Outcome (Search.Centralizer.constraint G (ofGenerators #[p])) budget

Equations

• Hex.PermGroup.Group.centralizerPermBudgeted budget G p = Hex.PermGroup.Group.centralizerBudgeted budget G (Hex.PermGroup.Group.ofGenerators #[p])

def Hex.PermGroup.Group.normalizerBudgeted {n : Nat} (budget : Execution.Budget) (G H : Group n) : Search.Outcome (Search.Normalizer.constraint G H) budget

Equations

• Hex.PermGroup.Group.normalizerBudgeted budget G H = Hex.PermGroup.Search.solveBudgeted budget (Hex.PermGroup.Search.Normalizer.constraint G H) (Hex.PermGroup.Search.Tester.normalizer H)

def Hex.PermGroup.Group.setStabilizerBudgeted {n : Nat} (budget : Execution.Budget) (G : Group n) (A : Vector Bool n) : Search.Outcome (Search.Sets.constraint G A) budget

Equations

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

def Hex.PermGroup.Group.setTransporterBudgeted {n : Nat} (budget : Execution.Budget) (G : Group n) (A B : Vector Bool n) : Search.AnswerOutcome (Search.Sets.transporter G A B) budget

The budget includes the original-generator witness program for a positive answer. Exhaustion has a separate constructor and cannot mean nonexistence.

Equations

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