OAI/Computability/DepthThree/TapeConvolutionRows.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeConvolutionRows.ReadState line 10
  2. abbrev OAI.DepthThreeLowerBound.TapeConvolutionRows.ClearState line 11
  3. abbrev OAI.DepthThreeLowerBound.TapeConvolutionRows.BodyState line 12
  4. def OAI.DepthThreeLowerBound.TapeConvolutionRows.readProgram line 14
  5. def OAI.DepthThreeLowerBound.TapeConvolutionRows.clearProgram line 18
  6. def OAI.DepthThreeLowerBound.TapeConvolutionRows.bodyProgram line 21
  7. def OAI.DepthThreeLowerBound.TapeConvolutionRows.bodyStart line 24
  8. def OAI.DepthThreeLowerBound.TapeConvolutionRows.bodyDone line 25
  9. def OAI.DepthThreeLowerBound.TapeConvolutionRows.bodyResult line 27
  10. theorem OAI.DepthThreeLowerBound.TapeConvolutionRows.runs_body line 30
  11. theorem OAI.DepthThreeLowerBound.TapeConvolutionRows.body_done line 96
  12. abbrev OAI.DepthThreeLowerBound.TapeConvolutionRows.State line 98
  13. def OAI.DepthThreeLowerBound.TapeConvolutionRows.program line 100
  14. def OAI.DepthThreeLowerBound.TapeConvolutionRows.start line 103
  15. def OAI.DepthThreeLowerBound.TapeConvolutionRows.done line 104
  16. def OAI.DepthThreeLowerBound.TapeConvolutionRows.frame line 106
  17. theorem OAI.DepthThreeLowerBound.TapeConvolutionRows.frame_counter line 111
  18. theorem OAI.DepthThreeLowerBound.TapeConvolutionRows.frame_index line 114
  19. theorem OAI.DepthThreeLowerBound.TapeConvolutionRows.frame_output line 117
  20. theorem OAI.DepthThreeLowerBound.TapeConvolutionRows.update_counter line 120
  21. theorem OAI.DepthThreeLowerBound.TapeConvolutionRows.bodyResult_frame line 128
  22. theorem OAI.DepthThreeLowerBound.TapeConvolutionRows.runs_rows line 139
  23. theorem OAI.DepthThreeLowerBound.TapeConvolutionRows.program_done line 192