OAI/Computability/Scheduling/ScheduleRoutines.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ThreeMachine.StackCompiler.(instance at line 12) line 12
  2. instance OAI.ThreeMachine.StackCompiler.(instance at line 15) line 15
  3. theorem OAI.ThreeMachine.StackCompiler.enc_instance line 17
  4. theorem OAI.ThreeMachine.StackCompiler.enc_map_eq line 19
  5. def OAI.ThreeMachine.StackCompiler.Uniform.matrixMapAny line 29
  6. def OAI.ThreeMachine.StackCompiler.Uniform.instanceEdges line 39
  7. def OAI.ThreeMachine.StackCompiler.Uniform.edgePairEq line 42
  8. def OAI.ThreeMachine.StackCompiler.Uniform.edgeAt line 49
  9. def OAI.ThreeMachine.StackCompiler.Uniform.edgeMatrix line 58
  10. def OAI.ThreeMachine.StackCompiler.Uniform.matrixRows line 61
  11. def OAI.ThreeMachine.StackCompiler.Uniform.readMatrix line 66
  12. def OAI.ThreeMachine.StackCompiler.Uniform.matrixReadNat line 69
  13. theorem OAI.ThreeMachine.StackCompiler.Uniform.readMatrix_eq line 74
  14. def OAI.ThreeMachine.StackCompiler.Uniform.paddedMatrix line 79
  15. def OAI.ThreeMachine.StackCompiler.nextMatrix line 120
  16. def OAI.ThreeMachine.StackCompiler.closureMatrix line 123
  17. theorem OAI.ThreeMachine.StackCompiler.closureMatrix_zero line 126
  18. theorem OAI.ThreeMachine.StackCompiler.nextMatrix_closure line 132
  19. def OAI.ThreeMachine.StackCompiler.Uniform.nextMatrixCell line 143
  20. def OAI.ThreeMachine.StackCompiler.Uniform.nextMatrix line 156
  21. def OAI.ThreeMachine.StackCompiler.Uniform.closureMatrixStep line 160
  22. def OAI.ThreeMachine.StackCompiler.Uniform.reachMatrix line 164
  23. def OAI.ThreeMachine.StackCompiler.Realizer.triple line 189
  24. def OAI.ThreeMachine.StackCompiler.scheduleMatrix line 196
  25. theorem OAI.ThreeMachine.StackCompiler.scheduleMatrix_closure line 202
  26. def OAI.ThreeMachine.StackCompiler.Uniform.restrictTime line 211
  27. def OAI.ThreeMachine.StackCompiler.Uniform.paddedSolve line 218
  28. def OAI.ThreeMachine.StackCompiler.Uniform.scheduleMatrixFixed line 231
  29. def OAI.ThreeMachine.StackCompiler.Uniform.scheduleMatrix line 256
  30. def OAI.ThreeMachine.StackCompiler.bestMatrix line 267
  31. theorem OAI.ThreeMachine.StackCompiler.bestMatrix_closure line 273
  32. def OAI.ThreeMachine.StackCompiler.bestMatrixStep line 281
  33. theorem OAI.ThreeMachine.StackCompiler.bestMatrix_iterate line 287
  34. def OAI.ThreeMachine.StackCompiler.answerMatrix line 293
  35. theorem OAI.ThreeMachine.StackCompiler.answerMatrix_closure line 297
  36. def OAI.ThreeMachine.StackCompiler.Uniform.bestMatrixStep line 304
  37. def OAI.ThreeMachine.StackCompiler.Uniform.bestMatrix line 314
  38. def OAI.ThreeMachine.StackCompiler.Uniform.answerMatrix line 321
  39. def OAI.ThreeMachine.StackCompiler.Uniform.unaryAnswer line 335
  40. def OAI.ThreeMachine.Algorithm.Block.Bounded line 347
  41. theorem OAI.ThreeMachine.Algorithm.Block.bounded_empty line 349
  42. theorem OAI.ThreeMachine.Algorithm.Block.bounded_triple line 351
  43. theorem OAI.ThreeMachine.Algorithm.Block.Bounded.append line 353
  44. theorem OAI.ThreeMachine.Algorithm.Block.Valid.length_le line 361
  45. theorem OAI.ThreeMachine.Algorithm.State.bounded_advance line 375
  46. theorem OAI.ThreeMachine.Algorithm.State.bounded_finish line 378
  47. def OAI.ThreeMachine.Algorithm.TableBounded line 386
  48. def OAI.ThreeMachine.Algorithm.MarksBounded line 389
  49. theorem OAI.ThreeMachine.Algorithm.tryAdvance_bounded line 393
  50. theorem OAI.ThreeMachine.Algorithm.markings_bounded line 405
  51. theorem OAI.ThreeMachine.Algorithm.solve_bounded line 423
  52. theorem OAI.ThreeMachine.Algorithm.layers_bounded line 438