Canonical encoding of finite Boolean assignments and tables -- proof internals

theorem Complexity.BooleanDependency.OrderedAssignment.card_internal {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) : Fintype.card (OrderedAssignment coordinates) = 2 ^ coordinates.card

theorem Complexity.BooleanDependency.length_encodeOrderedFunction_internal {index : Type u_1} [Fintype index] [LinearOrder index] (function : index → Bool) : (encodeOrderedFunction function).length = Fintype.card index

theorem Complexity.BooleanDependency.decodeOrderedFunction?_encodeOrderedFunction_internal {index : Type u_1} [Fintype index] [LinearOrder index] (function : index → Bool) : decodeOrderedFunction? (encodeOrderedFunction function) = some function

theorem Complexity.BooleanDependency.encodeOrderedFunction_injective_internal {index : Type u_1} [Fintype index] [LinearOrder index] : Function.Injective encodeOrderedFunction

theorem Complexity.BooleanDependency.decodeOrderedFunction?_eq_none_iff_internal {index : Type u_1} [Fintype index] [LinearOrder index] (bits : List Bool) : decodeOrderedFunction? bits = none ↔ bits.length ≠ Fintype.card index

theorem Complexity.BooleanDependency.length_encodeAssignment_internal {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (assignment : ↥coordinates → Bool) : (encodeAssignment coordinates assignment).length = coordinates.card

theorem Complexity.BooleanDependency.decodeAssignment?_encodeAssignment_internal {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (assignment : ↥coordinates → Bool) : decodeAssignment? coordinates (encodeAssignment coordinates assignment) = some assignment

theorem Complexity.BooleanDependency.encodeAssignment_injective_internal {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) : Function.Injective (encodeAssignment coordinates)

theorem Complexity.BooleanDependency.decodeAssignment?_eq_none_iff_internal {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (bits : List Bool) : decodeAssignment? coordinates bits = none ↔ bits.length ≠ coordinates.card

theorem Complexity.BooleanDependency.length_encodeTable_internal {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (table : (↥coordinates → Bool) → Bool) : (encodeTable coordinates table).length = 2 ^ coordinates.card

theorem Complexity.BooleanDependency.decodeTable?_encodeTable_internal {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (table : (↥coordinates → Bool) → Bool) : decodeTable? coordinates (encodeTable coordinates table) = some table

theorem Complexity.BooleanDependency.encodeTable_injective_internal {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) : Function.Injective (encodeTable coordinates)

theorem Complexity.BooleanDependency.decodeTable?_eq_none_iff_internal {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (bits : List Bool) : decodeTable? coordinates bits = none ↔ bits.length ≠ 2 ^ coordinates.card