@[irreducible]

def Hex.PermGroup.Search.checkFailure {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) (certificate : Certificate C.Reason) : Bool

A negative answer accounts for every completion. Subgroup coverage is not a valid reason here: even one satisfying element would refute nonexistence.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Search.checkFailure C t Hex.PermGroup.Search.Certificate.covered = false
• Hex.PermGroup.Search.checkFailure C t (Hex.PermGroup.Search.Certificate.rejected r) = C.reject t r

theorem Hex.PermGroup.Search.checkFailure_branch {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) {level : Level n} {tail : Chain n} (hs : t.suffix = Chain.cons level tail) (children : Array (Certificate C.Reason)) : checkFailure C t (Certificate.branch children) = if hc : children.size = level.orbit.points.size then decide (∀ (i : Fin level.orbit.points.size), checkFailure C (t.child hs i) children[↑i] = true) else false

theorem Hex.PermGroup.Search.checkFailure_sound {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) (certificate : Certificate C.Reason) (hc : checkFailure C t certificate = true) (p : Perm n) (hp : t.Contains p) : test p = false

theorem Hex.PermGroup.Search.checkFailure_spec {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (certificate : Certificate C.Reason) (hc : checkFailure C (Node.root G) certificate = true) : ¬∃ (p : Element G), test p.val = true

def Hex.PermGroup.Search.checkWitness {n : Nat} (G : Group n) (test : Perm n → Bool) (p : Perm n) (word : Program) : Bool

Positive answers need only replay a word in the original generators and the defining test; they make no completeness claim about other branches.

Equations

• Hex.PermGroup.Search.checkWitness G test p word = (Hex.PermGroup.checkWord G.generators p word && test p)

theorem Hex.PermGroup.Search.checkWitness_spec {n : Nat} (G : Group n) (test : Perm n → Bool) (p : Perm n) (word : Program) (h : checkWitness G test p word = true) : Generated G.generators p ∧ test p = true