Oracle-uniform universal-machine interfaces -- proof internals #
theorem
Complexity.OracleTM.simulates_comp_internal
{firstTapes secondTapes thirdTapes : ℕ}
{first : OracleTM firstTapes}
{second : OracleTM secondTapes}
{third : OracleTM thirdTapes}
{compileFirst compileSecond : List Bool → List Bool}
(hfirst : first.Simulates second compileFirst)
(hsecond : second.Simulates third compileSecond)
:
theorem
Complexity.OracleTM.simulatesInTime_refl_internal
{firstTapes : ℕ}
(machine : OracleTM firstTapes)
:
machine.SimulatesInTime machine id fun (x : List Bool) (sourceTime : ℕ) => sourceTime
theorem
Complexity.OracleTM.simulatesInTime_comp_internal
{firstTapes secondTapes thirdTapes : ℕ}
{first : OracleTM firstTapes}
{second : OracleTM secondTapes}
{third : OracleTM thirdTapes}
{compileFirst compileSecond : List Bool → List Bool}
{clockFirst clockSecond : TM.TimeOverhead}
(hfirst : first.SimulatesInTime second compileFirst clockFirst)
(hsecond : second.SimulatesInTime third compileSecond clockSecond)
:
first.SimulatesInTime third (compileFirst ∘ compileSecond) fun (program : List Bool) (sourceTime : ℕ) =>
clockFirst (compileSecond program) (clockSecond program sourceTime)
theorem
Complexity.OracleTM.efficientlyUniversalFor_isUniversal_internal
{firstTapes : ℕ}
{simulator : OracleTM firstTapes}
{admissible : TM.TimeOverhead → Prop}
(h : simulator.IsEfficientlyUniversalFor admissible)
:
simulator.IsUniversal
theorem
Complexity.OracleTM.efficientlyUniversalFor_mono_internal
{firstTapes : ℕ}
{simulator : OracleTM firstTapes}
{firstPolicy secondPolicy : TM.TimeOverhead → Prop}
(hpolicy : ∀ (clock : TM.TimeOverhead), firstPolicy clock → secondPolicy clock)
(h : simulator.IsEfficientlyUniversalFor firstPolicy)
:
simulator.IsEfficientlyUniversalFor secondPolicy