Pointwise output semantics for deterministic oracle TMs -- proof internals #
theorem
Complexity.OracleTM.HaltsInTime.mono_internal
{n : ℕ}
{machine : OracleTM n}
{oracle : BooleanOracle}
{program : List Bool}
{first second : ℕ}
(hbound : first ≤ second)
(hhalt : machine.HaltsInTime oracle program first)
:
machine.HaltsInTime oracle program second
theorem
Complexity.OracleTM.halts_of_haltsInTime_internal
{n : ℕ}
{machine : OracleTM n}
{oracle : BooleanOracle}
{program : List Bool}
{time : ℕ}
(hhalt : machine.HaltsInTime oracle program time)
:
machine.Halts oracle program
theorem
Complexity.OracleTM.ProducesInTime.mono_internal
{n : ℕ}
{machine : OracleTM n}
{oracle : BooleanOracle}
{program output : List Bool}
{first second : ℕ}
(hbound : first ≤ second)
(hproduce : machine.ProducesInTime oracle program output first)
:
machine.ProducesInTime oracle program output second
theorem
Complexity.OracleTM.produces_of_producesInTime_internal
{n : ℕ}
{machine : OracleTM n}
{oracle : BooleanOracle}
{program output : List Bool}
{time : ℕ}
(hproduce : machine.ProducesInTime oracle program output time)
:
machine.Produces oracle program output
theorem
Complexity.TM.toOracleTM_producesInTime_iff_internal
{n : ℕ}
(machine : TM n)
(oracle : BooleanOracle)
(program output : List Bool)
(time : ℕ)
:
machine.toOracleTM.ProducesInTime oracle program output time ↔ machine.ProducesInTime program output time