OAI/Computability/MeanPayoff/BinaryData.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.WorkStack.RegisterCompile.signed_adds line 9
  2. def OAI.MeanPayoff.BinaryData.boolData line 19
  3. def OAI.MeanPayoff.BinaryData.listData line 23
  4. def OAI.MeanPayoff.BinaryData.wordData line 27
  5. def OAI.MeanPayoff.BinaryData.consCode line 29
  6. theorem OAI.MeanPayoff.BinaryData.encode_list_nil line 33
  7. theorem OAI.MeanPayoff.BinaryData.encode_list_cons line 34
  8. theorem OAI.MeanPayoff.BinaryData.consCode_length_le line 37
  9. def OAI.MeanPayoff.BinaryData.feedCost line 39
  10. theorem OAI.MeanPayoff.BinaryData.feedCost_append line 43
  11. theorem OAI.MeanPayoff.BinaryData.feedCost_reverse line 48
  12. theorem OAI.MeanPayoff.BinaryData.feedCost_le line 53
  13. theorem OAI.MeanPayoff.BinaryData.encode_list_length_le line 58
  14. inductive OAI.MeanPayoff.BinaryData.Unbox.Label line 70
  15. def OAI.MeanPayoff.BinaryData.Unbox.equiv line 73
  16. def OAI.MeanPayoff.BinaryData.Unbox.enc line 74
  17. theorem OAI.MeanPayoff.BinaryData.Unbox.decode line 75
  18. def OAI.MeanPayoff.BinaryData.Unbox.program line 77
  19. def OAI.MeanPayoff.BinaryData.Unbox.cfg line 93
  20. def OAI.MeanPayoff.BinaryData.Unbox.stopped line 95
  21. theorem OAI.MeanPayoff.BinaryData.Unbox.read_nil line 97
  22. theorem OAI.MeanPayoff.BinaryData.Unbox.feed_one line 102
  23. theorem OAI.MeanPayoff.BinaryData.Unbox.feeds line 110
  24. theorem OAI.MeanPayoff.BinaryData.Unbox.restore_read line 120
  25. theorem OAI.MeanPayoff.BinaryData.Unbox.restore_put line 124
  26. theorem OAI.MeanPayoff.BinaryData.Unbox.restore_done line 128
  27. theorem OAI.MeanPayoff.BinaryData.Unbox.restores line 132
  28. theorem OAI.MeanPayoff.BinaryData.Unbox.read_nil_advance line 142
  29. theorem OAI.MeanPayoff.BinaryData.Unbox.unboxes line 146
  30. theorem OAI.MeanPayoff.BinaryData.Unbox.unboxes_bound line 155
  31. inductive OAI.MeanPayoff.BinaryData.Box.Label line 165
  32. def OAI.MeanPayoff.BinaryData.Box.equiv line 168
  33. def OAI.MeanPayoff.BinaryData.Box.enc line 169
  34. theorem OAI.MeanPayoff.BinaryData.Box.decode line 170
  35. def OAI.MeanPayoff.BinaryData.Box.program line 172
  36. def OAI.MeanPayoff.BinaryData.Box.cfg line 192
  37. def OAI.MeanPayoff.BinaryData.Box.stopped line 194
  38. theorem OAI.MeanPayoff.BinaryData.Box.reverse_read line 196
  39. theorem OAI.MeanPayoff.BinaryData.Box.reverse_put line 200
  40. theorem OAI.MeanPayoff.BinaryData.Box.reverses line 205
  41. theorem OAI.MeanPayoff.BinaryData.Box.initializes line 215
  42. theorem OAI.MeanPayoff.BinaryData.Box.feed_one line 220
  43. theorem OAI.MeanPayoff.BinaryData.Box.feeds line 228
  44. theorem OAI.MeanPayoff.BinaryData.Box.feed_done line 238
  45. theorem OAI.MeanPayoff.BinaryData.Box.boxes line 242
  46. theorem OAI.MeanPayoff.BinaryData.Box.boxes_bound line 254
  47. theorem OAI.MeanPayoff.RegisterBits.Flow.hop line 261
  48. theorem OAI.MeanPayoff.RegisterBits.Flow.finish line 272