An executable Barrington compiler -- proof internals

theorem Complexity.mem_allPermutationsFin_internal {n : ℕ} (permutation : Equiv.Perm (Fin n)) : permutation ∈ allPermutationsFin n

theorem Complexity.firstConjugator5_spec_internal (source target : Equiv.Perm (Fin 5)) (hexists : ∃ (g : Equiv.Perm (Fin 5)), g * source * g⁻¹ = target) : firstConjugator5 source target * source * (firstConjugator5 source target)⁻¹ = target

theorem Complexity.barringtonLeftBase_spec_internal : barringtonLeftBase.IsCycle ∧ orderOf barringtonLeftBase = 5

theorem Complexity.barringtonRightBase_spec_internal : barringtonRightBase.IsCycle ∧ orderOf barringtonRightBase = 5

theorem Complexity.barringtonTargetBase_spec_internal : barringtonTargetBase.IsCycle ∧ orderOf barringtonTargetBase = 5

theorem Complexity.barringtonConjugator_spec_internal (target : Equiv.Perm (Fin 5)) (hcycle : target.IsCycle) (horder : orderOf target = 5) : barringtonConjugator target * barringtonTargetBase * (barringtonConjugator target)⁻¹ = target

theorem Complexity.barringtonLeft_spec_internal (target : Equiv.Perm (Fin 5)) : (barringtonLeft target).IsCycle ∧ orderOf (barringtonLeft target) = 5

theorem Complexity.barringtonRight_spec_internal (target : Equiv.Perm (Fin 5)) : (barringtonRight target).IsCycle ∧ orderOf (barringtonRight target) = 5

theorem Complexity.barrington_commutator_internal (target : Equiv.Perm (Fin 5)) (hcycle : target.IsCycle) (horder : orderOf target = 5) : ⁅barringtonLeft target, barringtonRight target⁆ = target

theorem Complexity.BP.length_commutatorProgram_internal {w : ℕ} (p q : BP w) : List.length (p.commutatorProgram q) = 2 * List.length p + 2 * List.length q

theorem Complexity.barringtonCompile_computes_internal (formula : BoolFormula) (target : Equiv.Perm (Fin 5)) : target.IsCycle → orderOf target = 5 → BP.Computes target (barringtonCompile formula target) fun (assignment : ℕ → Bool) => BoolFormula.eval assignment formula

theorem Complexity.barringtonCompile_length_le_internal (formula : BoolFormula) (target : Equiv.Perm (Fin 5)) : List.length (barringtonCompile formula target) ≤ 4 ^ formula.depth

theorem Complexity.barringtonCompile_var_bound_internal (formula : BoolFormula) (target : Equiv.Perm (Fin 5)) (bound : ℕ) (hvars : ∀ index ∈ formula.vars, index ≤ bound) (instruction : BPInstr 5) : instruction ∈ barringtonCompile formula target → instruction.var ≤ bound

Internal variable-locality theorem for the executable compiler.