Relocating raw circuit fragments -- proof internals

theorem Complexity.CircuitCode.RawGate.eval_shift_internal (offset : ℕ) (gate : RawGate) (value₀ value₁ : Bool) : (shift offset gate).eval value₀ value₁ = gate.eval value₀ value₁

theorem Complexity.CircuitCode.RawGate.wellFormedAt_shift_iff_internal (offset available : ℕ) (gate : RawGate) : (shift offset gate).WellFormedAt (offset + available) ↔ gate.WellFormedAt available

theorem Complexity.CircuitCode.RawCircuit.length_shift_internal (offset : ℕ) (circuit : RawCircuit) : List.length (shift offset circuit) = List.length circuit

theorem Complexity.CircuitCode.RawCircuit.topologicallyWellFormed_shift_iff_internal (offset available : ℕ) (circuit : RawCircuit) : TopologicallyWellFormed (offset + available) (shift offset circuit) ↔ TopologicallyWellFormed available circuit

theorem Complexity.CircuitCode.RawCircuit.evalAux?_shift_internal (offset : ℕ) (circuit : RawCircuit) (leading wires : Array Bool) (hleading : leading.size = offset) : (shift offset circuit).evalAux? (leading ++ wires) = Option.map (fun (result : Array Bool) => leading ++ result) (circuit.evalAux? wires)