OAI/Computability/DepthThree/MachineCompilation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.MachineCompilation.stmtCost line 14
  2. theorem OAI.DepthThreeLowerBound.MachineCompilation.stmtCost_pos line 22
  3. def OAI.DepthThreeLowerBound.MachineCompilation.subCfg line 34
  4. theorem OAI.DepthThreeLowerBound.MachineCompilation.stepAux_counted line 38
  5. def OAI.DepthThreeLowerBound.MachineCompilation.programCost line 99
  6. theorem OAI.DepthThreeLowerBound.MachineCompilation.stmtCost_le_programCost line 102
  7. theorem OAI.DepthThreeLowerBound.MachineCompilation.programCost_pos line 114
  8. theorem OAI.DepthThreeLowerBound.MachineCompilation.step_counted line 117
  9. theorem OAI.DepthThreeLowerBound.MachineCompilation.run_counted line 129
  10. theorem OAI.DepthThreeLowerBound.MachineCompilation.runsIn_counted line 151
  11. theorem OAI.DepthThreeLowerBound.MachineCompilation.compiled_halt line 158
  12. theorem OAI.DepthThreeLowerBound.MachineCompilation.compiled_init line 174
  13. theorem OAI.DepthThreeLowerBound.MachineCompilation.source_supports line 186
  14. def OAI.DepthThreeLowerBound.MachineCompilation.compileFinite line 210
  15. theorem OAI.DepthThreeLowerBound.MachineCompilation.compileFinite_haltsIn line 215
  16. theorem OAI.DepthThreeLowerBound.MachineCompilation.polynomialTimeDecider_of_counted_TM1 line 230