Fixed-width multiplexers -- proof internals

theorem Complexity.Circuit.wireValue_multiplexer_left_internal (width : ℕ) [NeZero width] (input : BitString (1 + (width + width))) (coordinate : Fin width) : (multiplexer width).wireValue input ⟨1 + (width + width) + ↑coordinate, ⋯⟩ = (input ⟨0, ⋯⟩ && input ⟨1 + ↑coordinate, ⋯⟩)

theorem Complexity.Circuit.wireValue_multiplexer_right_internal (width : ℕ) [NeZero width] (input : BitString (1 + (width + width))) (coordinate : Fin width) : (multiplexer width).wireValue input ⟨1 + (width + width) + width + ↑coordinate, ⋯⟩ = (!input ⟨0, ⋯⟩ && input ⟨1 + width + ↑coordinate, ⋯⟩)

theorem Complexity.Circuit.eval_multiplexer_packed_internal (width : ℕ) [NeZero width] (input : BitString (1 + (width + width))) (coordinate : Fin width) : (multiplexer width).eval input coordinate = if input ⟨0, ⋯⟩ = true then input ⟨1 + ↑coordinate, ⋯⟩ else input ⟨1 + width + ↑coordinate, ⋯⟩

theorem Complexity.Circuit.eval_multiplexer_internal (width : ℕ) [NeZero width] (control : Bool) (left right : BitString width) : (multiplexer width).eval (BitString.multiplexerInput control left right) = if control = true then left else right