Deterministic Boolean-oracle Turing machines -- proof internals

theorem Complexity.Tape.length_oracleQuery_internal (tape : Tape) : tape.oracleQuery.length = tape.head - 1

theorem Complexity.OracleCfg.erase_init_internal {Q : Type} {n : ℕ} (qstart : Q) (input : List Bool) : (init qstart input).erase = Cfg.init qstart input

theorem Complexity.OracleTM.step_eq_none_iff_halted_internal {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} : machine.step oracle cfg = none ↔ machine.halted cfg

theorem Complexity.OracleTM.stepRel_functional_internal {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg first second : OracleCfg n machine.Q} (hfirst : machine.stepRel oracle cfg first) (hsecond : machine.stepRel oracle cfg second) : first = second

theorem Complexity.OracleTM.reachesIn_functional_internal {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {time : ℕ} {start first second : OracleCfg n machine.Q} (hfirst : machine.reachesIn oracle time start first) (hsecond : machine.reachesIn oracle time start second) : first = second

theorem Complexity.OracleTM.reachesIn_map_internal {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {workTapes : ℕ} {target : TM workTapes} (mapCfg : OracleCfg n machine.Q → Cfg workTapes target.Q) (hstep : ∀ {cfg next : OracleCfg n machine.Q}, machine.step oracle cfg = some next → target.step (mapCfg cfg) = some (mapCfg next)) {time : ℕ} {start result : OracleCfg n machine.Q} (hreach : machine.reachesIn oracle time start result) : target.reachesIn time (mapCfg start) (mapCfg result)

theorem Complexity.OracleTM.step_query_true_internal {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} {yesState noState : machine.Q} (hhalt : cfg.state ≠ machine.qhalt) (hquery : machine.queryTransition cfg.state = some (yesState, noState)) (hanswer : oracle cfg.query.oracleQuery = true) : machine.step oracle cfg = some { state := yesState, input := cfg.input, query := cfg.query, work := cfg.work, output := cfg.output }

theorem Complexity.OracleTM.step_query_false_internal {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} {yesState noState : machine.Q} (hhalt : cfg.state ≠ machine.qhalt) (hquery : machine.queryTransition cfg.state = some (yesState, noState)) (hanswer : oracle cfg.query.oracleQuery = false) : machine.step oracle cfg = some { state := noState, input := cfg.input, query := cfg.query, work := cfg.work, output := cfg.output }

theorem Complexity.OracleTM.reachesIn_one_query_true_internal {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} {yesState noState : machine.Q} (hhalt : cfg.state ≠ machine.qhalt) (hquery : machine.queryTransition cfg.state = some (yesState, noState)) (hanswer : oracle cfg.query.oracleQuery = true) : machine.reachesIn oracle 1 cfg { state := yesState, input := cfg.input, query := cfg.query, work := cfg.work, output := cfg.output }

theorem Complexity.OracleTM.reachesIn_one_query_false_internal {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} {yesState noState : machine.Q} (hhalt : cfg.state ≠ machine.qhalt) (hquery : machine.queryTransition cfg.state = some (yesState, noState)) (hanswer : oracle cfg.query.oracleQuery = false) : machine.reachesIn oracle 1 cfg { state := noState, input := cfg.input, query := cfg.query, work := cfg.work, output := cfg.output }

theorem Complexity.TM.toOracleTM_queryTransition_internal {n : ℕ} (machine : TM n) (state : machine.Q) : machine.toOracleTM.queryTransition state = none

theorem Complexity.TM.toOracleTM_step_oracle_independent_internal {n : ℕ} (machine : TM n) (first second : BooleanOracle) (cfg : OracleCfg n machine.Q) : machine.toOracleTM.step first cfg = machine.toOracleTM.step second cfg

theorem Complexity.TM.erase_toOracleTM_step_internal {n : ℕ} (machine : TM n) (oracle : BooleanOracle) (cfg : OracleCfg n machine.Q) : Option.map OracleCfg.erase (machine.toOracleTM.step oracle cfg) = machine.step cfg.erase

theorem Complexity.TM.erase_toOracleTM_step_some_internal {n : ℕ} (machine : TM n) (oracle : BooleanOracle) {cfg next : OracleCfg n machine.Q} (hstep : machine.toOracleTM.step oracle cfg = some next) : machine.step cfg.erase = some next.erase

theorem Complexity.TM.erase_toOracleTM_reachesIn_internal {n : ℕ} (machine : TM n) (oracle : BooleanOracle) {time : ℕ} {start result : OracleCfg n machine.Q} (hreach : machine.toOracleTM.reachesIn oracle time start result) : machine.reachesIn time start.erase result.erase

theorem Complexity.TM.exists_toOracleTM_step_of_step_erase_internal {n : ℕ} (machine : TM n) (oracle : BooleanOracle) {cfg : OracleCfg n machine.Q} {next : Cfg n machine.Q} (hstep : machine.step cfg.erase = some next) : ∃ (oracleNext : OracleCfg n machine.toOracleTM.Q), machine.toOracleTM.step oracle cfg = some oracleNext ∧ oracleNext.erase = next

theorem Complexity.TM.exists_toOracleTM_reachesIn_of_reachesIn_erase_internal {n : ℕ} (machine : TM n) (oracle : BooleanOracle) {time : ℕ} (start : OracleCfg n machine.Q) {result : Cfg n machine.Q} (hreach : machine.reachesIn time start.erase result) : ∃ (oracleResult : OracleCfg n machine.toOracleTM.Q), machine.toOracleTM.reachesIn oracle time start oracleResult ∧ oracleResult.erase = result

theorem Complexity.TM.toOracleTM_decidesInTime_iff_internal {n : ℕ} (machine : TM n) (oracle : BooleanOracle) (language : Language) (timeBound : ℕ → ℕ) : machine.toOracleTM.DecidesInTime oracle language timeBound ↔ machine.DecidesInTime language timeBound