OAI/Computability/Scheduling/Realizers.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.StackCompiler.Data.fold line 13
  2. def OAI.ThreeMachine.StackCompiler.Data.foldCost line 17
  3. def OAI.ThreeMachine.StackCompiler.Routine.foldStore line 26
  4. theorem OAI.ThreeMachine.StackCompiler.Routine.foldStore_zero line 27
  5. theorem OAI.ThreeMachine.StackCompiler.Routine.foldStore_one line 28
  6. theorem OAI.ThreeMachine.StackCompiler.Routine.foldStore_two line 29
  7. theorem OAI.ThreeMachine.StackCompiler.Routine.foldStore_update_one line 31
  8. theorem OAI.ThreeMachine.StackCompiler.Routine.foldStore_update_two line 35
  9. def OAI.ThreeMachine.StackCompiler.Routine.foldBody line 39
  10. def OAI.ThreeMachine.StackCompiler.Routine.foldCode line 47
  11. theorem OAI.ThreeMachine.StackCompiler.Routine.foldBody_correct line 51
  12. theorem OAI.ThreeMachine.StackCompiler.Routine.foldLoop_correct line 90
  13. def OAI.ThreeMachine.StackCompiler.Routine.fold line 103
  14. class OAI.ThreeMachine.StackCompiler.Coding line 140
  15. def OAI.ThreeMachine.StackCompiler.enc line 143
  16. def OAI.ThreeMachine.StackCompiler.volume line 145
  17. instance OAI.ThreeMachine.StackCompiler.(instance at line 147) line 147
  18. instance OAI.ThreeMachine.StackCompiler.(instance at line 148) line 148
  19. instance OAI.ThreeMachine.StackCompiler.(instance at line 149) line 149
  20. instance OAI.ThreeMachine.StackCompiler.(instance at line 150) line 150
  21. def OAI.ThreeMachine.StackCompiler.encodeList line 153
  22. instance OAI.ThreeMachine.StackCompiler.(instance at line 156) line 156
  23. def OAI.ThreeMachine.StackCompiler.encodeUnary line 158
  24. instance OAI.ThreeMachine.StackCompiler.(instance at line 159) line 159
  25. instance OAI.ThreeMachine.StackCompiler.(instance at line 160) line 160
  26. theorem OAI.ThreeMachine.StackCompiler.enc_data line 163
  27. theorem OAI.ThreeMachine.StackCompiler.enc_unit line 164
  28. theorem OAI.ThreeMachine.StackCompiler.enc_false line 165
  29. theorem OAI.ThreeMachine.StackCompiler.enc_true line 166
  30. theorem OAI.ThreeMachine.StackCompiler.enc_pair line 167
  31. theorem OAI.ThreeMachine.StackCompiler.enc_nil line 169
  32. theorem OAI.ThreeMachine.StackCompiler.enc_cons line 170
  33. theorem OAI.ThreeMachine.StackCompiler.enc_zero line 172
  34. theorem OAI.ThreeMachine.StackCompiler.enc_succ line 173
  35. theorem OAI.ThreeMachine.StackCompiler.enc_none line 174
  36. theorem OAI.ThreeMachine.StackCompiler.enc_some line 175
  37. theorem OAI.ThreeMachine.StackCompiler.volume_pair line 177
  38. theorem OAI.ThreeMachine.StackCompiler.volume_nil line 179
  39. theorem OAI.ThreeMachine.StackCompiler.volume_cons line 180
  40. theorem OAI.ThreeMachine.StackCompiler.volume_nat line 182
  41. structure OAI.ThreeMachine.StackCompiler.Realizer line 191
  42. def OAI.ThreeMachine.StackCompiler.Realizer.time line 201
  43. def OAI.ThreeMachine.StackCompiler.Realizer.id line 203
  44. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_id line 206
  45. def OAI.ThreeMachine.StackCompiler.Realizer.unit line 208
  46. def OAI.ThreeMachine.StackCompiler.Realizer.nil line 211
  47. def OAI.ThreeMachine.StackCompiler.Realizer.zero line 214
  48. def OAI.ThreeMachine.StackCompiler.Realizer.false line 217
  49. def OAI.ThreeMachine.StackCompiler.Realizer.comp line 220
  50. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_comp line 226
  51. def OAI.ThreeMachine.StackCompiler.Realizer.pair line 230
  52. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_pair line 236
  53. def OAI.ThreeMachine.StackCompiler.Realizer.fst line 240
  54. def OAI.ThreeMachine.StackCompiler.Realizer.snd line 243
  55. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_fst line 246
  56. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_snd line 247
  57. def OAI.ThreeMachine.StackCompiler.Realizer.congr line 249
  58. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_congr line 252
  59. theorem OAI.ThreeMachine.StackCompiler.Realizer.fold_correct line 255
  60. def OAI.ThreeMachine.StackCompiler.Realizer.fold line 264
  61. def OAI.ThreeMachine.StackCompiler.Realizer.foldTime line 271
  62. theorem OAI.ThreeMachine.StackCompiler.Realizer.foldTime_eq line 276
  63. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_fold line 286
  64. theorem OAI.ThreeMachine.StackCompiler.Tree.Bounded.branch_true line 296
  65. theorem OAI.ThreeMachine.StackCompiler.Tree.Bounded.branch_false line 300
  66. def OAI.ThreeMachine.StackCompiler.Routine.invoke line 312
  67. theorem OAI.ThreeMachine.StackCompiler.Routine.invoke_correct line 318
  68. def OAI.ThreeMachine.StackCompiler.Routine.chooseCode line 343
  69. def OAI.ThreeMachine.StackCompiler.Routine.choose line 350
  70. def OAI.ThreeMachine.StackCompiler.Routine.constant line 411
  71. def OAI.ThreeMachine.StackCompiler.Realizer.constant line 422
  72. def OAI.ThreeMachine.StackCompiler.Realizer.reinterpret line 425
  73. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_reinterpret line 428
  74. def OAI.ThreeMachine.StackCompiler.Realizer.cons line 431
  75. def OAI.ThreeMachine.StackCompiler.Realizer.choose line 433
  76. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_choose line 445
  77. def OAI.ThreeMachine.StackCompiler.Realizer.ite line 453
  78. def OAI.ThreeMachine.StackCompiler.Realizer.succ line 457