inductive Hex.PermGroup.Search.BoundedFirst.Decision {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) (budget : Budget) : Type

• found {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {t : Node G} {budget : Budget} (p : Element G) (inside : t.Contains p.val) (satisfies : test p.val = true) (meter : Meter budget) : Decision C t budget
• absent {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {t : Node G} {budget : Budget} (certificate : Certificate C.Reason) (checked : checkFailure C t certificate = true) (meter : Meter budget) : Decision C t budget
• incomplete {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {t : Node G} {budget : Budget} (failure : Exhausted budget) : Decision C t budget

def Hex.PermGroup.Search.BoundedFirst.finish {n : Nat} {G : Group n} {test : Perm n → Bool} {budget : Budget} (C : Pruner G test) (t : Node G) (certificate : Unit → Certificate C.Reason) (checked : checkFailure C t (certificate ()) = true) (m : Meter budget) : Decision C t budget

Equations

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

inductive Hex.PermGroup.Search.BoundedFirst.Children {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) {size : Nat} (nodes : Fin size → Node G) (k : Nat) (hk : k ≤ size) (budget : Budget) : Type

• found {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {size : Nat} {nodes : Fin size → Node G} {k : Nat} {hk : k ≤ size} {budget : Budget} (i : Fin k) (p : Element G) (inside : (nodes ⟨↑i, ⋯⟩).Contains p.val) (satisfies : test p.val = true) (meter : Meter budget) : Children C nodes k hk budget
• absent {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {size : Nat} {nodes : Fin size → Node G} {k : Nat} {hk : k ≤ size} {budget : Budget} (certificates : Vector (Certificate C.Reason) k) (checked : ∀ (i : Fin k), checkFailure C (nodes ⟨↑i, ⋯⟩) certificates[↑i] = true) (meter : Meter budget) : Children C nodes k hk budget
• incomplete {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {size : Nat} {nodes : Fin size → Node G} {k : Nat} {hk : k ≤ size} {budget : Budget} (failure : Exhausted budget) : Children C nodes k hk budget

def Hex.PermGroup.Search.BoundedFirst.collect {n : Nat} {G : Group n} {test : Perm n → Bool} {budget : Budget} (C : Pruner G test) {size : Nat} (nodes : Fin size → Node G) (visit : Meter budget → (i : Fin size) → Decision C (nodes i) budget) (m : Meter budget) (k : Nat) (hk : k ≤ size) : Children C nodes k hk budget

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Search.BoundedFirst.collect C nodes visit m 0 hk_2 = Hex.PermGroup.Search.BoundedFirst.Children.absent #v[] ⋯ m

@[irreducible]

def Hex.PermGroup.Search.BoundedFirst.visit {n : Nat} {G : Group n} {test : Perm n → Bool} {budget : Budget} (C : Pruner G test) (Q : Evaluator test budget) (t : Node G) (m : Meter budget) : Decision C t budget

Exhaustion propagates immediately without becoming a negative answer. Successful leaves stop child traversal before constructing a witness program.

Equations

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

inductive Hex.PermGroup.Search.AnswerOutcome {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (budget : Budget) : Type

Incomplete existence search exposes no negative answer. A complete answer retains either its checked witness or its full nonexistence certificate.

• complete {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {budget : Budget} (answer : Answer C) (meter : Meter budget) : AnswerOutcome C budget
• incomplete {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {budget : Budget} (failure : Exhausted budget) : AnswerOutcome C budget

def Hex.PermGroup.Search.firstBudgeted {n : Nat} (budget : Budget) {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (Q : Evaluator test budget) : AnswerOutcome C budget

Equations

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