OAI/Computability/Scheduling/RequestBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.Costs.answerMatrix line 8
  2. theorem OAI.ThreeMachine.StackCompiler.Costs.unaryAnswer line 27
  3. def OAI.ThreeMachine.StackCompiler.Request.size line 44
  4. def OAI.ThreeMachine.StackCompiler.Binary.vertices line 48
  5. def OAI.ThreeMachine.StackCompiler.Binary.edges line 49
  6. theorem OAI.ThreeMachine.StackCompiler.Binary.input_eq line 51
  7. theorem OAI.ThreeMachine.StackCompiler.Binary.readHeader_input line 58
  8. theorem OAI.ThreeMachine.StackCompiler.Binary.readVertices_input line 64
  9. theorem OAI.ThreeMachine.StackCompiler.Binary.readEdges_input line 69
  10. theorem OAI.ThreeMachine.StackCompiler.Binary.readNat_tail_input line 75
  11. theorem OAI.ThreeMachine.StackCompiler.Binary.encodeNat_pos line 85
  12. theorem OAI.ThreeMachine.StackCompiler.Binary.length_le_flatMap_encode line 89
  13. theorem OAI.ThreeMachine.StackCompiler.Binary.length_le_encodeList line 98
  14. theorem OAI.ThreeMachine.StackCompiler.Binary.input_length_bounds line 104
  15. theorem OAI.ThreeMachine.StackCompiler.requestSize_le line 120
  16. abbrev OAI.ThreeMachine.StackCompiler.RequestData.Index line 131
  17. def OAI.ThreeMachine.StackCompiler.RequestData.size line 132
  18. def OAI.ThreeMachine.StackCompiler.RequestData.bits line 133
  19. def OAI.ThreeMachine.StackCompiler.RequestData.vbytes line 134
  20. def OAI.ThreeMachine.StackCompiler.RequestData.ebytes line 135
  21. theorem OAI.ThreeMachine.StackCompiler.RequestData.nPoly line 137
  22. theorem OAI.ThreeMachine.StackCompiler.RequestData.edgesPoly line 141
  23. theorem OAI.ThreeMachine.StackCompiler.RequestData.deadlinePoly line 145
  24. theorem OAI.ThreeMachine.StackCompiler.RequestData.bitsPoly line 149
  25. theorem OAI.ThreeMachine.StackCompiler.RequestData.vrestPoly line 153
  26. theorem OAI.ThreeMachine.StackCompiler.RequestData.ebytesPoly line 161
  27. theorem OAI.ThreeMachine.StackCompiler.RequestData.verticesLength line 165
  28. theorem OAI.ThreeMachine.StackCompiler.RequestData.edgesLength line 168
  29. theorem OAI.ThreeMachine.StackCompiler.RequestData.verticesBound line 171
  30. theorem OAI.ThreeMachine.StackCompiler.RequestData.edgesBound line 176
  31. theorem OAI.ThreeMachine.StackCompiler.RequestData.volumeDeadline line 181
  32. theorem OAI.ThreeMachine.StackCompiler.RequestData.volumeVertices line 186
  33. theorem OAI.ThreeMachine.StackCompiler.RequestData.volumeEdges line 196
  34. theorem OAI.ThreeMachine.StackCompiler.RequestData.volumeVrest line 206
  35. theorem OAI.ThreeMachine.StackCompiler.RequestData.volumeEbytes line 211
  36. theorem OAI.ThreeMachine.StackCompiler.RequestData.volumeGraph line 216
  37. theorem OAI.ThreeMachine.StackCompiler.RequestData.volumeRequest line 219