Circuit-level oracle inlining -- proof internals

theorem Complexity.Circuit.eval_appendOracleAnswer_internal {inputWidth historyWidth queryWidth historyGates queryGates oracleGates : ℕ} [NeZero inputWidth] [NeZero historyWidth] [NeZero queryWidth] (history : Circuit Basis.andOr2 inputWidth historyWidth historyGates) (query : Circuit Basis.andOr2 historyWidth queryWidth queryGates) (oracle : Circuit Basis.andOr2 queryWidth 1 oracleGates) (input : BitString inputWidth) : (history.appendOracleAnswer query oracle).eval input = Fin.append (history.eval input) (oracle.eval (query.eval (history.eval input)))

Internal exact evaluation law for one inlined oracle answer.