OAI/Computability/MeanPayoff/InputCode.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.count line 8
  2. def OAI.MeanPayoff.TreeDevice.Certified.Word.digitCount line 24
  3. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.digitCount_length line 32
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.half_size line 36
  5. abbrev OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.State line 46
  6. def OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.positive line 47
  7. def OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.step line 48
  8. theorem OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.step_eval line 50
  9. def OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.loop line 53
  10. def OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.length line 63
  11. def OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.ceil line 66
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.recurrence line 69
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.fold_stopped line 74
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.fold_length line 85
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.length_exact line 116
  16. theorem OAI.MeanPayoff.TreeDevice.Certified.NaturalLog.ceil_exact line 120
  17. def OAI.MeanPayoff.TreeDevice.Certified.Word.powerStep line 137
  18. def OAI.MeanPayoff.TreeDevice.Certified.Word.powerFold line 138
  19. def OAI.MeanPayoff.TreeDevice.Certified.Word.power line 143
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.powerFold_val line 145
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.power_val line 153
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.false_data line 159
  23. def OAI.MeanPayoff.TreeDevice.Certified.Counter.bounded line 166
  24. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.bounded_exact line 180
  25. def OAI.MeanPayoff.TreeDevice.Certified.Counter.power line 183
  26. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.power_exact line 184
  27. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.pow_clog_le line 188
  28. structure OAI.MeanPayoff.TreeDevice.Certified.Parsed line 209
  29. instance OAI.MeanPayoff.TreeDevice.Certified.(instance at line 211) line 211
  30. def OAI.MeanPayoff.TreeDevice.Certified.InputCode.parse line 213
  31. def OAI.MeanPayoff.TreeDevice.Certified.InputCode.n line 218
  32. def OAI.MeanPayoff.TreeDevice.Certified.InputCode.edges line 223
  33. def OAI.MeanPayoff.TreeDevice.Certified.InputCode.rows line 230
  34. def OAI.MeanPayoff.TreeDevice.Certified.InputCode.game line 236
  35. theorem OAI.MeanPayoff.TreeDevice.Certified.InputCode.parse_game line 237
  36. theorem OAI.MeanPayoff.TreeDevice.Certified.InputCode.n_game line 241
  37. theorem OAI.MeanPayoff.TreeDevice.Certified.InputCode.rows_game line 242
  38. def OAI.MeanPayoff.TreeDevice.Certified.InputCode.absolute line 244
  39. theorem OAI.MeanPayoff.TreeDevice.Certified.InputCode.absolute_val line 245
  40. def OAI.MeanPayoff.TreeDevice.Certified.InputCode.maximumFold line 246
  41. def OAI.MeanPayoff.TreeDevice.Certified.InputCode.maximum line 251
  42. def OAI.MeanPayoff.TreeDevice.Certified.InputCode.bound line 252
  43. def OAI.MeanPayoff.TreeDevice.Certified.InputCode.width line 253
  44. theorem OAI.MeanPayoff.TreeDevice.Certified.InputCode.fold_upper line 255
  45. theorem OAI.MeanPayoff.TreeDevice.Certified.InputCode.fold_lower line 263
  46. theorem OAI.MeanPayoff.TreeDevice.Certified.InputCode.fold_mem line 269
  47. theorem OAI.MeanPayoff.TreeDevice.Certified.InputCode.bound_val line 278
  48. theorem OAI.MeanPayoff.TreeDevice.Certified.InputCode.width_val line 305