OAI/Computability/MeanPayoff/ParserCosts.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Prefix.suffix line 10
  2. theorem OAI.MeanPayoff.TreeDevice.Prefix.fold_suffix line 15
  3. theorem OAI.MeanPayoff.TreeDevice.Prefix.read_suffix line 29
  4. theorem OAI.MeanPayoff.TreeDevice.Prefix.suffix_isSuffix line 31
  5. theorem OAI.MeanPayoff.TreeDevice.listTree_append_right_le line 42
  6. theorem OAI.MeanPayoff.TreeDevice.listTree_drop_le line 48
  7. theorem OAI.MeanPayoff.TreeDevice.Prefix.remainder_size line 54
  8. theorem OAI.MeanPayoff.TreeDevice.Split.fold_rest line 61
  9. theorem OAI.MeanPayoff.TreeDevice.Split.rest line 70
  10. theorem OAI.MeanPayoff.TreeDevice.Split.remainder_size line 72
  11. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.nat_remainder_size line 79
  12. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.int_remainder_size line 83
  13. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.remainder_size line 92
  14. abbrev OAI.MeanPayoff.TreeDevice.StreamFold.State line 100
  15. def OAI.MeanPayoff.TreeDevice.StreamFold.stateData line 101
  16. def OAI.MeanPayoff.TreeDevice.StreamFold.inputData line 102
  17. def OAI.MeanPayoff.TreeDevice.StreamFold.step line 104
  18. def OAI.MeanPayoff.TreeDevice.StreamFold.envDevice line 109
  19. def OAI.MeanPayoff.TreeDevice.StreamFold.localDevice line 111
  20. def OAI.MeanPayoff.TreeDevice.StreamFold.accDevice line 113
  21. def OAI.MeanPayoff.TreeDevice.StreamFold.streamDevice line 115
  22. def OAI.MeanPayoff.TreeDevice.StreamFold.parseDevice line 119
  23. def OAI.MeanPayoff.TreeDevice.StreamFold.itemDevice line 122
  24. def OAI.MeanPayoff.TreeDevice.StreamFold.restDevice line 125
  25. def OAI.MeanPayoff.TreeDevice.StreamFold.newAccDevice line 128
  26. def OAI.MeanPayoff.TreeDevice.StreamFold.stepDevice line 131
  27. theorem OAI.MeanPayoff.TreeDevice.StreamFold.env_linear line 135
  28. theorem OAI.MeanPayoff.TreeDevice.StreamFold.local_linear line 136
  29. theorem OAI.MeanPayoff.TreeDevice.StreamFold.acc_linear line 137
  30. theorem OAI.MeanPayoff.TreeDevice.StreamFold.stream_linear line 138
  31. theorem OAI.MeanPayoff.TreeDevice.StreamFold.parse_polynomial line 140
  32. theorem OAI.MeanPayoff.TreeDevice.StreamFold.item_polynomial line 142
  33. theorem OAI.MeanPayoff.TreeDevice.StreamFold.rest_polynomial line 144
  34. theorem OAI.MeanPayoff.TreeDevice.StreamFold.newAcc_polynomial line 146
  35. theorem OAI.MeanPayoff.TreeDevice.StreamFold.step_polynomial line 148
  36. theorem OAI.MeanPayoff.TreeDevice.StreamFold.fold_bound line 153
  37. theorem OAI.MeanPayoff.TreeDevice.Fold.polynomial_of_prefix line 183
  38. theorem OAI.MeanPayoff.TreeDevice.StreamFold.polynomial line 220
  39. abbrev OAI.MeanPayoff.TreeDevice.EdgesRead.Edge line 250
  40. abbrev OAI.MeanPayoff.TreeDevice.EdgesRead.Count line 251
  41. abbrev OAI.MeanPayoff.TreeDevice.EdgesRead.State line 252
  42. abbrev OAI.MeanPayoff.TreeDevice.EdgesRead.Args line 253
  43. def OAI.MeanPayoff.TreeDevice.EdgesRead.restData line 254
  44. def OAI.MeanPayoff.TreeDevice.EdgesRead.countData line 255
  45. def OAI.MeanPayoff.TreeDevice.EdgesRead.edgesData line 256
  46. def OAI.MeanPayoff.TreeDevice.EdgesRead.stateData line 257
  47. def OAI.MeanPayoff.TreeDevice.EdgesRead.argsData line 258
  48. def OAI.MeanPayoff.TreeDevice.EdgesRead.outputData line 259
  49. def OAI.MeanPayoff.TreeDevice.EdgesRead.read line 261
  50. def OAI.MeanPayoff.TreeDevice.EdgesRead.moreDevice line 265
  51. def OAI.MeanPayoff.TreeDevice.EdgesRead.streamDevice line 266
  52. def OAI.MeanPayoff.TreeDevice.EdgesRead.countDevice line 268
  53. def OAI.MeanPayoff.TreeDevice.EdgesRead.stateDevice line 270
  54. def OAI.MeanPayoff.TreeDevice.EdgesRead.initDevice line 272
  55. def OAI.MeanPayoff.TreeDevice.EdgesRead.finishDevice line 274
  56. def OAI.MeanPayoff.TreeDevice.EdgesRead.foldDevice line 277
  57. def OAI.MeanPayoff.TreeDevice.EdgesRead.device line 280
  58. def OAI.MeanPayoff.TreeDevice.EdgesRead.lower line 282
  59. def OAI.MeanPayoff.TreeDevice.EdgesRead.code line 283
  60. theorem OAI.MeanPayoff.TreeDevice.EdgesRead.fold_exact line 285
  61. theorem OAI.MeanPayoff.TreeDevice.EdgesRead.exact line 305
  62. theorem OAI.MeanPayoff.TreeDevice.EdgesRead.more_linear line 310
  63. theorem OAI.MeanPayoff.TreeDevice.EdgesRead.stream_linear line 311
  64. theorem OAI.MeanPayoff.TreeDevice.EdgesRead.count_linear line 312
  65. theorem OAI.MeanPayoff.TreeDevice.EdgesRead.state_linear line 313
  66. theorem OAI.MeanPayoff.TreeDevice.EdgesRead.init_linear line 315
  67. theorem OAI.MeanPayoff.TreeDevice.EdgesRead.finish_polynomial line 316
  68. theorem OAI.MeanPayoff.TreeDevice.EdgesRead.fold_polynomial line 319
  69. theorem OAI.MeanPayoff.TreeDevice.EdgesRead.polynomial line 321