OAI/Computability/Scheduling/VolumeBounds.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_iterate_le line 12
  2. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_add_le line 18
  3. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_sub_le line 25
  4. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_le_le line 32
  5. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_eqNat_le line 43
  6. theorem OAI.ThreeMachine.StackCompiler.Uniform.foldTime_length_le line 57
  7. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_length_le line 72
  8. theorem OAI.ThreeMachine.StackCompiler.Uniform.volume_drop_le line 79
  9. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_drop_le line 82
  10. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_getElem?_le line 95
  11. theorem OAI.ThreeMachine.StackCompiler.volume_prod line 111
  12. theorem OAI.ThreeMachine.StackCompiler.volume_state line 114
  13. theorem OAI.ThreeMachine.StackCompiler.volume_finRange_le line 119
  14. theorem OAI.ThreeMachine.StackCompiler.volume_universe_le line 124
  15. theorem OAI.ThreeMachine.StackCompiler.volume_cardinal line 127
  16. theorem OAI.ThreeMachine.StackCompiler.volume_bool_vector_le line 129
  17. theorem OAI.ThreeMachine.StackCompiler.volume_matrix_le line 133
  18. theorem OAI.ThreeMachine.StackCompiler.volume_state_le line 137
  19. theorem OAI.ThreeMachine.StackCompiler.volume_block_le line 145
  20. theorem OAI.ThreeMachine.StackCompiler.Poly.precomp line 155
  21. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeNat line 157
  22. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeBool line 161
  23. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeUnit line 164
  24. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeFin line 168
  25. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeFinset line 172
  26. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeUniverse line 177
  27. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeCardinal line 182
  28. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeBoolVector line 187
  29. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeMatrix line 192
  30. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeState line 197
  31. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeProd line 204
  32. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeList line 211
  33. theorem OAI.ThreeMachine.StackCompiler.volume_ofFn line 226
  34. theorem OAI.ThreeMachine.StackCompiler.volume_sort line 229
  35. theorem OAI.ThreeMachine.StackCompiler.volume_function_apply_le line 231
  36. theorem OAI.ThreeMachine.StackCompiler.nat_function_apply_le line 234
  37. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_functionListAny line 242
  38. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_finValue line 245
  39. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_functionGetOptionAny_le line 248
  40. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_functionGetAny_eq line 257
  41. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_functionGetAny_le line 267
  42. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_functionGet_le line 274
  43. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_reindex line 279