Pointwise output semantics -- proof internals

Proofs supporting the public API in Complexitylib.Models.TuringMachine.OutputSemantics.

theorem Complexity.TM.runCfg_add_internal {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) (first second : ℕ) : tm.runCfg c (first + second) = tm.runCfg (tm.runCfg c first) second

theorem Complexity.TM.runCfg_of_halted_internal {n : ℕ} (tm : TM n) {c : Cfg n tm.Q} (hhalt : tm.halted c) (steps : ℕ) : tm.runCfg c steps = c

theorem Complexity.TM.runCfg_of_reachesIn_internal {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} {steps : ℕ} (hreach : tm.reachesIn steps c c') : tm.runCfg c steps = c'

theorem Complexity.TM.runCfg_reachesIn_internal {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) (time : ℕ) : ∃ steps ≤ time, tm.reachesIn steps c (tm.runCfg c time)

The bounded evaluator's endpoint is reachable in some number of actual transitions no greater than its clock.

theorem Complexity.TM.runCfg_initCfg_congr_of_input_cells_internal {n : ℕ} (tm : TM n) (first second : List Bool) (time : ℕ) (hinput : ∀ position ≤ time, (tm.initCfg first).input.cells position = (tm.initCfg second).input.cells position) : (tm.runCfg (tm.initCfg first) time).state = (tm.runCfg (tm.initCfg second) time).state ∧ (tm.runCfg (tm.initCfg first) time).work = (tm.runCfg (tm.initCfg second) time).work ∧ (tm.runCfg (tm.initCfg first) time).output = (tm.runCfg (tm.initCfg second) time).output

theorem Complexity.TM.runCfg_eq_of_reachesIn_halted_internal {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} {steps time : ℕ} (hreach : tm.reachesIn steps c c') (hhalt : tm.halted c') (hsteps : steps ≤ time) : tm.runCfg c time = c'

A halted exact-step endpoint is the bounded evaluator's endpoint at every larger clock.

theorem Complexity.TM.haltsInTime_iff_runCfg_internal {n : ℕ} (tm : TM n) (program : List Bool) (time : ℕ) : tm.HaltsInTime program time ↔ tm.halted (tm.runCfg (tm.initCfg program) time)

theorem Complexity.TM.haltsInTime_mono_internal {n : ℕ} {tm : TM n} {program : List Bool} {first second : ℕ} (hbound : first ≤ second) (hhalt : tm.HaltsInTime program first) : tm.HaltsInTime program second

theorem Complexity.TM.halts_of_haltsInTime_internal {n : ℕ} {tm : TM n} {program : List Bool} {time : ℕ} (hhalt : tm.HaltsInTime program time) : tm.Halts program

theorem Complexity.TM.halts_iff_exists_haltsInTime_internal {n : ℕ} (tm : TM n) (program : List Bool) : tm.Halts program ↔ ∃ (time : ℕ), tm.HaltsInTime program time

theorem Complexity.TM.producesInTime_iff_runCfg_internal {n : ℕ} (tm : TM n) (program output : List Bool) (time : ℕ) : tm.ProducesInTime program output time ↔ tm.halted (tm.runCfg (tm.initCfg program) time) ∧ (tm.runCfg (tm.initCfg program) time).output.HasOutput output

theorem Complexity.TM.initCfg_take_input_cells_le_internal {n : ℕ} (tm : TM n) (program : List Bool) (time position : ℕ) (hposition : position ≤ time) : (tm.initCfg program).input.cells position = (tm.initCfg (List.take time program)).input.cells position

theorem Complexity.TM.producesInTime_take_internal {n : ℕ} {tm : TM n} {program output : List Bool} {time : ℕ} (hproduce : tm.ProducesInTime program output time) : tm.ProducesInTime (List.take time program) output time

theorem Complexity.TM.producesInTime_mono_internal {n : ℕ} {tm : TM n} {program output : List Bool} {first second : ℕ} (hbound : first ≤ second) (hproduce : tm.ProducesInTime program output first) : tm.ProducesInTime program output second

theorem Complexity.TM.produces_of_producesInTime_internal {n : ℕ} {tm : TM n} {program output : List Bool} {time : ℕ} (hproduce : tm.ProducesInTime program output time) : tm.Produces program output

theorem Complexity.TM.haltsInTime_of_producesInTime_internal {n : ℕ} {tm : TM n} {program output : List Bool} {time : ℕ} (hproduce : tm.ProducesInTime program output time) : tm.HaltsInTime program time

theorem Complexity.TM.halts_of_produces_internal {n : ℕ} {tm : TM n} {program output : List Bool} (hproduce : tm.Produces program output) : tm.Halts program

theorem Complexity.TM.produces_iff_exists_producesInTime_internal {n : ℕ} (tm : TM n) (program output : List Bool) : tm.Produces program output ↔ ∃ (time : ℕ), tm.ProducesInTime program output time

theorem Complexity.TM.hasOutput_length_eq_internal {tape : Tape} {left right : List Bool} (hleft : tape.HasOutput left) (hright : tape.HasOutput right) : left.length = right.length

theorem Complexity.TM.hasOutput_eq_internal {tape : Tape} {left right : List Bool} (hleft : tape.HasOutput left) (hright : tape.HasOutput right) : left = right

theorem Complexity.TM.producesInTime_output_unique_internal {n : ℕ} {tm : TM n} {program left right : List Bool} {leftTime rightTime : ℕ} (hleft : tm.ProducesInTime program left leftTime) (hright : tm.ProducesInTime program right rightTime) : left = right

theorem Complexity.TM.produces_output_unique_internal {n : ℕ} {tm : TM n} {program left right : List Bool} (hleft : tm.Produces program left) (hright : tm.Produces program right) : left = right

theorem Complexity.TM.computesInTime_iff_forall_producesInTime_internal {n : ℕ} (tm : TM n) (function : List Bool → List Bool) (time : ℕ → ℕ) : tm.ComputesInTime function time ↔ ∀ (input : List Bool), tm.ProducesInTime input (function input) (time input.length)

theorem Complexity.TM.computes_iff_forall_produces_internal {n : ℕ} (tm : TM n) (function : List Bool → List Bool) : tm.Computes function ↔ ∀ (input : List Bool), tm.Produces input (function input)