OAI/Computability/MeanPayoff/Decoding.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.nodeRandomBound line 9
  2. theorem OAI.MeanPayoff.SolveBox.resource_repeated line 12
  3. def OAI.MeanPayoff.CountedAlgorithm.LowerResource line 19
  4. theorem OAI.MeanPayoff.CountedAlgorithm.resource_centerUpdate line 22
  5. theorem OAI.MeanPayoff.CountedAlgorithm.resource_centerSteps line 31
  6. theorem OAI.MeanPayoff.CountedAlgorithm.resource_orientationTail line 41
  7. theorem OAI.MeanPayoff.CountedAlgorithm.resource_orient line 57
  8. theorem OAI.MeanPayoff.CountedAlgorithm.resource_orient_global line 90
  9. theorem OAI.MeanPayoff.CountedAlgorithm.resource_tighten line 100
  10. theorem OAI.MeanPayoff.CountedAlgorithm.resource_finishChoice line 123
  11. theorem OAI.MeanPayoff.CountedAlgorithm.resource_solveWidth line 140
  12. theorem OAI.MeanPayoff.CountedAlgorithm.resource_solve line 173
  13. theorem OAI.MeanPayoff.CountedAlgorithm.solve_bitDepth line 183
  14. theorem OAI.MeanPayoff.nodeRandomBound_scale line 192
  15. def OAI.MeanPayoff.rootRandomBound line 200
  16. theorem OAI.MeanPayoff.game_bitDepth line 203
  17. theorem OAI.MeanPayoff.rootRandomBound_nat line 207
  18. theorem OAI.MeanPayoff.rootRandomBound_real line 227
  19. theorem OAI.MeanPayoff.game_bounded_randomness_success line 245
  20. def OAI.MeanPayoff.BinaryInput.bitsValue line 259
  21. theorem OAI.MeanPayoff.BinaryInput.bitsValue_bits line 263
  22. def OAI.MeanPayoff.BinaryInput.readLength line 268
  23. theorem OAI.MeanPayoff.BinaryInput.readLength_replicate line 273
  24. def OAI.MeanPayoff.BinaryInput.readNat line 279
  25. theorem OAI.MeanPayoff.BinaryInput.readNat_encode line 286
  26. def OAI.MeanPayoff.BinaryInput.readInt line 290
  27. theorem OAI.MeanPayoff.BinaryInput.readInt_encode line 294
  28. abbrev OAI.MeanPayoff.BinaryInput.Edge line 302
  29. def OAI.MeanPayoff.BinaryInput.encodeEdge line 304
  30. def OAI.MeanPayoff.BinaryInput.readEdge line 306
  31. theorem OAI.MeanPayoff.BinaryInput.readEdge_encode line 312
  32. def OAI.MeanPayoff.BinaryInput.readEdges line 317
  33. theorem OAI.MeanPayoff.BinaryInput.readEdges_encode line 324
  34. structure OAI.MeanPayoff.BinaryInput.RawGame line 330
  35. def OAI.MeanPayoff.BinaryInput.lower line 337
  36. def OAI.MeanPayoff.BinaryInput.rawCode line 343
  37. theorem OAI.MeanPayoff.BinaryInput.rawCode_lower line 346
  38. def OAI.MeanPayoff.BinaryInput.readRaw line 349
  39. theorem OAI.MeanPayoff.BinaryInput.readRaw_code line 358
  40. theorem OAI.MeanPayoff.BinaryInput.readRaw_input line 366
  41. def OAI.MeanPayoff.BinaryInput.RawGame.Valid line 370
  42. instance OAI.MeanPayoff.BinaryInput.(instance at line 375) line 375
  43. theorem OAI.MeanPayoff.BinaryInput.lower_valid line 377
  44. def OAI.MeanPayoff.BinaryInput.RawGame.toGame line 389
  45. theorem OAI.MeanPayoff.BinaryInput.toGame_lower line 405
  46. def OAI.MeanPayoff.BinaryInput.decodeGame line 410
  47. theorem OAI.MeanPayoff.BinaryInput.decodeGame_input line 416
  48. def OAI.MeanPayoff.BinaryInput.programTree line 419
  49. theorem OAI.MeanPayoff.BinaryInput.programTree_input line 424