Self-delimiting input-pair circuits -- proof internals

theorem Complexity.Circuit.eval_pairInputSources_internal {inputWidth leftWidth rightWidth : ℕ} [NeZero inputWidth] (left : Fin leftWidth → InputSource inputWidth) (right : Fin rightWidth → InputSource inputWidth) (input : BitString inputWidth) : ((pairInputSources left right).eval input).toList = pair (BitString.toList fun (i : Fin leftWidth) => (left i).eval input) (BitString.toList fun (i : Fin rightWidth) => (right i).eval input)

theorem Complexity.Circuit.size_pairInputSources_internal {inputWidth leftWidth rightWidth : ℕ} [NeZero inputWidth] (left : Fin leftWidth → InputSource inputWidth) (right : Fin rightWidth → InputSource inputWidth) : (pairInputSources left right).size = pairSourceWidth leftWidth rightWidth