Circuit input reindexing -- proof internals

theorem Complexity.Circuit.reindexInputWire_input_internal {N N' G : ℕ} (mapInput : Fin N → Fin N') (input : Fin N) : reindexInputWire mapInput (Fin.castAdd G input) = Fin.castAdd G (mapInput input)

theorem Complexity.Circuit.reindexInputWire_gate_internal {N N' G : ℕ} (mapInput : Fin N → Fin N') (gate : Fin G) : reindexInputWire mapInput (Fin.natAdd N gate) = Fin.natAdd N' gate

theorem Complexity.Circuit.wireValue_reindexInputs_internal {B : Basis} {N N' M G : ℕ} [NeZero N] [NeZero N'] [NeZero M] (circuit : Circuit B N M G) (mapInput : Fin N → Fin N') (input : BitString N') (wire : Fin (N + G)) : (circuit.reindexInputs mapInput).wireValue input (reindexInputWire mapInput wire) = circuit.wireValue (input ∘ mapInput) wire

theorem Complexity.Circuit.eval_reindexInputs_internal {B : Basis} {N N' M G : ℕ} [NeZero N] [NeZero N'] [NeZero M] (circuit : Circuit B N M G) (mapInput : Fin N → Fin N') (input : BitString N') : (circuit.reindexInputs mapInput).eval input = circuit.eval (input ∘ mapInput)