inductive Hex.PermGroup.Search.Bounded.Status {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (t : Node G) (a : Accumulator G P) (budget : Budget) : Type

• complete {n : Nat} {G : Group n} {P : Predicate n} {C : Constraint G P} {t : Node G} {a : Accumulator G P} {budget : Budget} (certificate : Certificate C.Reason) (checked : checkTree C a.group t certificate = true) (meter : Meter budget) : Status C t a budget
• incomplete {n : Nat} {G : Group n} {P : Predicate n} {C : Constraint G P} {t : Node G} {a : Accumulator G P} {budget : Budget} (failure : Exhausted budget) : Status C t a budget

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

Even on exhaustion the accumulated subgroup remains checked, satisfies the predicate, and contains every generator found before the stopping point.

• acc : Accumulator G P
• grows : a.group.IsSubgroup self.acc.group
• status : Status C t self.acc budget

def Hex.PermGroup.Search.Bounded.Result.stop {n : Nat} {G : Group n} {P : Predicate n} {budget : Budget} (C : Constraint G P) (t : Node G) (a : Accumulator G P) (failure : Exhausted budget) : Result C t a budget

Equations

• Hex.PermGroup.Search.Bounded.Result.stop C t a failure = { acc := a, grows := ⋯, status := Hex.PermGroup.Search.Bounded.Status.incomplete failure }

def Hex.PermGroup.Search.Bounded.Result.finish {n : Nat} {G : Group n} {P : Predicate n} {budget : Budget} (C : Constraint G P) (t : Node G) (a b : Accumulator G P) (grows : a.group.IsSubgroup b.group) (certificate : Unit → Certificate C.Reason) (checked : checkTree C b.group t (certificate ()) = true) (m : Meter budget) : Result C t a budget

Reserve a certificate node before constructing it. Failure preserves the current subgroup, including any successful leaf just inserted into it.

Equations

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

inductive Hex.PermGroup.Search.Bounded.ChildrenStatus {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) {size : Nat} (nodes : Fin size → Node G) (k : Nat) (hk : k ≤ size) (a : Accumulator G P) (budget : Budget) : Type

• complete {n : Nat} {G : Group n} {P : Predicate n} {C : Constraint G P} {size : Nat} {nodes : Fin size → Node G} {k : Nat} {hk : k ≤ size} {a : Accumulator G P} {budget : Budget} (certificates : Vector (Certificate C.Reason) k) (checked : ∀ (i : Fin k), checkTree C a.group (nodes ⟨↑i, ⋯⟩) certificates[↑i] = true) (meter : Meter budget) : ChildrenStatus C nodes k hk a budget
• incomplete {n : Nat} {G : Group n} {P : Predicate n} {C : Constraint G P} {size : Nat} {nodes : Fin size → Node G} {k : Nat} {hk : k ≤ size} {a : Accumulator G P} {budget : Budget} (failure : Exhausted budget) : ChildrenStatus C nodes k hk a budget

structure Hex.PermGroup.Search.Bounded.Children {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) {size : Nat} (nodes : Fin size → Node G) (a : Accumulator G P) (k : Nat) (hk : k ≤ size) (budget : Budget) : Type

• acc : Accumulator G P
• grows : a.group.IsSubgroup self.acc.group
• status : ChildrenStatus C nodes k hk self.acc budget

def Hex.PermGroup.Search.Bounded.collect {n : Nat} {G : Group n} {P : Predicate n} {budget : Budget} (C : Constraint G P) {size : Nat} (nodes : Fin size → Node G) (visit : (a : Accumulator G P) → Meter budget → (i : Fin size) → Result C (nodes i) a budget) (a : Accumulator G P) (m : Meter budget) (k : Nat) (hk : k ≤ size) : Children C nodes a k hk budget

Process children in orbit order. An incomplete child stops the loop and retains its lower bound; completed earlier certificates are transported along each enlargement of the accumulator.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Search.Bounded.collect C nodes visit a m 0 hk_2 = { acc := a, grows := ⋯, status := Hex.PermGroup.Search.Bounded.ChildrenStatus.complete #v[] ⋯ m }