OAI/Computability/DepthThree/TapeInputBlocks.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeInputBlocks.PrepareState line 12
  2. def OAI.DepthThreeLowerBound.TapeInputBlocks.prepareProgram line 14
  3. def OAI.DepthThreeLowerBound.TapeInputBlocks.prepareStart line 18
  4. def OAI.DepthThreeLowerBound.TapeInputBlocks.prepareDone line 19
  5. abbrev OAI.DepthThreeLowerBound.TapeInputBlocks.State line 21
  6. def OAI.DepthThreeLowerBound.TapeInputBlocks.program line 23
  7. def OAI.DepthThreeLowerBound.TapeInputBlocks.start line 27
  8. def OAI.DepthThreeLowerBound.TapeInputBlocks.done line 28
  9. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.prepare_done line 30
  10. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.program_done line 33
  11. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.runs_prepare line 36
  12. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.blockStore_prepared line 68
  13. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.blockStore_finished line 78
  14. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.runs_extract line 87
  15. def OAI.DepthThreeLowerBound.TapeInputBlocks.outputRegister line 109
  16. def OAI.DepthThreeLowerBound.TapeInputBlocks.canonicalRegisters line 115
  17. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.canonical_source line 124
  18. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.canonical_index line 127
  19. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.canonical_count line 130
  20. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.canonical_scratch line 133
  21. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.canonical_destination line 136
  22. def OAI.DepthThreeLowerBound.TapeInputBlocks.canonicalProgram line 139
  23. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.canonical_done line 142
  24. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.canonical_cost_le line 145
  25. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.runs_canonical_block line 154
  26. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.runs_data line 176
  27. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.runs_hash line 187
  28. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.runs_polynomial line 202
  29. theorem OAI.DepthThreeLowerBound.TapeInputBlocks.runs_coefficients line 217