OAI/Computability/Scheduling/FiniteRoutines.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ThreeMachine.StackCompiler.(instance at line 11) line 11
  2. instance OAI.ThreeMachine.StackCompiler.(instance at line 12) line 12
  3. theorem OAI.ThreeMachine.StackCompiler.enc_fin line 14
  4. theorem OAI.ThreeMachine.StackCompiler.volume_fin line 15
  5. theorem OAI.ThreeMachine.StackCompiler.enc_finset line 16
  6. structure OAI.ThreeMachine.StackCompiler.Cardinal line 19
  7. instance OAI.ThreeMachine.StackCompiler.(instance at line 21) line 21
  8. structure OAI.ThreeMachine.StackCompiler.Universe line 23
  9. instance OAI.ThreeMachine.StackCompiler.(instance at line 25) line 25
  10. theorem OAI.ThreeMachine.StackCompiler.enc_list_map line 27
  11. theorem OAI.ThreeMachine.StackCompiler.sort_filter line 33
  12. def OAI.ThreeMachine.StackCompiler.Uniform.finVal line 43
  13. def OAI.ThreeMachine.StackCompiler.Uniform.finEq line 45
  14. def OAI.ThreeMachine.StackCompiler.Uniform.cardinal line 49
  15. def OAI.ThreeMachine.StackCompiler.Uniform.universeList line 51
  16. def OAI.ThreeMachine.StackCompiler.Uniform.universeSet line 54
  17. def OAI.ThreeMachine.StackCompiler.Uniform.setList line 57
  18. def OAI.ThreeMachine.StackCompiler.Uniform.setEmpty line 60
  19. def OAI.ThreeMachine.StackCompiler.Uniform.setIsEmpty line 66
  20. def OAI.ThreeMachine.StackCompiler.Uniform.setCard line 75
  21. def OAI.ThreeMachine.StackCompiler.Uniform.setFilter line 78
  22. def OAI.ThreeMachine.StackCompiler.Uniform.setMem line 88
  23. def OAI.ThreeMachine.StackCompiler.Uniform.setInter line 94
  24. def OAI.ThreeMachine.StackCompiler.Uniform.setDiff line 97
  25. def OAI.ThreeMachine.StackCompiler.Uniform.setSubset line 100
  26. def OAI.ThreeMachine.StackCompiler.Uniform.setEq line 106
  27. def OAI.ThreeMachine.StackCompiler.Uniform.setDisjoint line 111
  28. def OAI.ThreeMachine.StackCompiler.Uniform.setUnionBody line 115
  29. def OAI.ThreeMachine.StackCompiler.Uniform.setUnion line 120
  30. def OAI.ThreeMachine.StackCompiler.Uniform.setCompl line 125
  31. def OAI.ThreeMachine.StackCompiler.Realizer.rangeStep line 134
  32. theorem OAI.ThreeMachine.StackCompiler.Realizer.rangeStep_iterate line 137
  33. def OAI.ThreeMachine.StackCompiler.Realizer.range line 143
  34. theorem OAI.ThreeMachine.StackCompiler.finRange_val line 149
  35. def OAI.ThreeMachine.StackCompiler.Uniform.makeUniverse line 159
  36. def OAI.ThreeMachine.StackCompiler.Uniform.numLength line 168
  37. theorem OAI.ThreeMachine.StackCompiler.volume_append line 176
  38. theorem OAI.ThreeMachine.StackCompiler.volume_reverse line 181
  39. theorem OAI.ThreeMachine.StackCompiler.volume_filter line 190
  40. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_id line 203
  41. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_fst line 205
  42. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_snd line 207
  43. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_nil line 209
  44. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_unit line 211
  45. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_zero line 213
  46. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_false line 215
  47. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_congr line 217
  48. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_reinterpret line 220
  49. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_cons line 222
  50. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_comp line 224
  51. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_pair line 228
  52. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_fold line 232
  53. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_choose line 236
  54. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_constant line 243
  55. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_reverse line 247
  56. instance OAI.ThreeMachine.StackCompiler.(instance at line 271) line 271
  57. theorem OAI.ThreeMachine.StackCompiler.enc_function line 273
  58. def OAI.ThreeMachine.StackCompiler.Uniform.tail line 279
  59. def OAI.ThreeMachine.StackCompiler.Uniform.drop line 282
  60. def OAI.ThreeMachine.StackCompiler.Uniform.getElem? line 291
  61. def OAI.ThreeMachine.StackCompiler.Uniform.getElemD line 294
  62. def OAI.ThreeMachine.StackCompiler.Uniform.functionList line 302
  63. def OAI.ThreeMachine.StackCompiler.Uniform.functionGetOption line 305
  64. def OAI.ThreeMachine.StackCompiler.Uniform.functionGet line 309
  65. def OAI.ThreeMachine.StackCompiler.Uniform.vectorMap line 316