theorem Hex.PermGroup.Kernel.levelsOk_cons_of {n : Nat} {L : Level} {rest : List Level} {N : Nat} (hl : levelOk n (width n) (ident n (width n)) L rest = true) (hN : L.gens.length.mul L.size = N) (hp : pairsOk n (width n) (ident n (width n)) L rest 0 N = true) (hr : levelsOk n (width n) (ident n (width n)) rest = true) : levelsOk n (width n) (ident n (width n)) (L :: rest) = true

theorem Hex.PermGroup.Kernel.levelsOk_nil {n : Nat} : levelsOk n (width n) (ident n (width n)) [] = true

theorem Hex.PermGroup.Kernel.check_of {n : Nat} {inputs : List Nat} {c : Certificate} (hi : inputsOk n (width n) (ident n (width n)) inputs c = true) (hl : levelsOk n (width n) (ident n (width n)) c = true) : check n inputs c = true

theorem Hex.PermGroup.Kernel.pack_nil {n : Nat} : List.map pack [] = []

Combine the per-generator packing ties.

theorem Hex.PermGroup.Kernel.pack_cons {n : Nat} {g : Perm n} {gs : List (Perm n)} {x : Nat} {xs : List Nat} (h : pack g = x) (t : List.map pack gs = xs) : List.map pack (g :: gs) = x :: xs

theorem Hex.PermGroup.Kernel.check_list {n : Nat} {gs : List (Perm n)} {inputs : List Nat} {c : Certificate} (hS : List.map pack gs = inputs) (h : check n inputs c = true) : check n (List.map pack gs.toArray.toList) c = true

theorem Hex.PermGroup.Kernel.hasOrder_of_check {n : Nat} {gs : List (Perm n)} {inputs : List Nat} {c : Certificate} {N : Nat} (hS : List.map pack gs = inputs) (h : check n inputs c = true) (hN : order c = N) : HasOrder gs.toArray N

theorem Hex.PermGroup.Kernel.generated_of_check {n : Nat} {gs : List (Perm n)} {inputs : List Nat} {c : Certificate} {g : Perm n} {x : Nat} (hS : List.map pack gs = inputs) (h : check n inputs c = true) (hx : pack g = x) (hs : sift n (width n) (ident n (width n)) c x = true) : Generated gs.toArray g

theorem Hex.PermGroup.Kernel.not_generated_of_check {n : Nat} {gs : List (Perm n)} {inputs : List Nat} {c : Certificate} {g : Perm n} {x : Nat} (hS : List.map pack gs = inputs) (h : check n inputs c = true) (hx : pack g = x) (hs : sift n (width n) (ident n (width n)) c x = false) : ¬Generated gs.toArray g