OAI/Computability/MeanPayoff/BatchDevices.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MeanPayoff.TreeDevice.EnvMap.Acc line 10
  2. def OAI.MeanPayoff.TreeDevice.EnvMap.step line 12
  3. def OAI.MeanPayoff.TreeDevice.EnvMap.argument line 15
  4. def OAI.MeanPayoff.TreeDevice.EnvMap.stepDevice line 21
  5. theorem OAI.MeanPayoff.TreeDevice.EnvMap.fold_eq line 28
  6. def OAI.MeanPayoff.TreeDevice.EnvMap.device line 37
  7. abbrev OAI.MeanPayoff.TreeDevice.Graph.W line 56
  8. abbrev OAI.MeanPayoff.TreeDevice.Graph.Count line 57
  9. abbrev OAI.MeanPayoff.TreeDevice.Graph.Pot line 58
  10. abbrev OAI.MeanPayoff.TreeDevice.Graph.Edge line 59
  11. abbrev OAI.MeanPayoff.TreeDevice.Graph.Edges line 60
  12. abbrev OAI.MeanPayoff.TreeDevice.Graph.Vertex line 61
  13. abbrev OAI.MeanPayoff.TreeDevice.Graph.Batch line 62
  14. def OAI.MeanPayoff.TreeDevice.Graph.countData line 64
  15. def OAI.MeanPayoff.TreeDevice.Graph.potData line 65
  16. def OAI.MeanPayoff.TreeDevice.Graph.edgeData line 66
  17. def OAI.MeanPayoff.TreeDevice.Graph.edgesData line 67
  18. def OAI.MeanPayoff.TreeDevice.Graph.vertexData line 68
  19. def OAI.MeanPayoff.TreeDevice.Graph.valuePairData line 69
  20. def OAI.MeanPayoff.TreeDevice.Graph.batchData line 70
  21. def OAI.MeanPayoff.TreeDevice.Graph.lookup line 72
  22. def OAI.MeanPayoff.TreeDevice.Graph.lookupDevice line 74
  23. def OAI.MeanPayoff.TreeDevice.Graph.edgePair line 77
  24. def OAI.MeanPayoff.TreeDevice.Graph.edgeDevice line 79
  25. def OAI.MeanPayoff.TreeDevice.Graph.batch line 84
  26. def OAI.MeanPayoff.TreeDevice.Graph.batchDevice line 87
  27. def OAI.MeanPayoff.TreeDevice.Graph.vertex line 93
  28. def OAI.MeanPayoff.TreeDevice.Graph.vertexDevice line 96
  29. def OAI.MeanPayoff.TreeDevice.Graph.device line 102
  30. def OAI.MeanPayoff.TreeDevice.Graph.codeEdge line 105
  31. def OAI.MeanPayoff.TreeDevice.Graph.codePot line 108
  32. theorem OAI.MeanPayoff.TreeDevice.Graph.lookup_exact line 110
  33. theorem OAI.MeanPayoff.TreeDevice.Graph.edgePair_exact line 116
  34. theorem OAI.MeanPayoff.TreeDevice.Graph.batch_represents line 120
  35. theorem OAI.MeanPayoff.TreeDevice.Graph.vertex_exact line 141
  36. theorem OAI.MeanPayoff.TreeDevice.EnvMap.step_limit line 154
  37. def OAI.MeanPayoff.TreeDevice.EnvMap.resource line 164
  38. theorem OAI.MeanPayoff.TreeDevice.EnvMap.resource_decrease line 169
  39. theorem OAI.MeanPayoff.TreeDevice.EnvMap.fold_time line 177
  40. theorem OAI.MeanPayoff.TreeDevice.EnvMap.fold_polynomial line 199
  41. theorem OAI.MeanPayoff.TreeDevice.EnvMap.polynomial line 240
  42. theorem OAI.MeanPayoff.TreeDevice.PolynomialCost.branch line 255
  43. theorem OAI.MeanPayoff.TreeDevice.EdgeScan.max_polynomial line 265
  44. theorem OAI.MeanPayoff.TreeDevice.EdgeScan.min_polynomial line 272
  45. theorem OAI.MeanPayoff.TreeDevice.Graph.lookup_polynomial line 282
  46. theorem OAI.MeanPayoff.TreeDevice.Graph.edge_polynomial line 285
  47. theorem OAI.MeanPayoff.TreeDevice.Graph.batch_polynomial line 292
  48. theorem OAI.MeanPayoff.TreeDevice.Graph.vertex_polynomial line 302
  49. theorem OAI.MeanPayoff.TreeDevice.Graph.polynomial line 312