OAI/Computability/MeanPayoff/OperatorCosts.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Graph.outList line 10
  2. theorem OAI.MeanPayoff.TreeDevice.Graph.mem_outList line 12
  3. theorem OAI.MeanPayoff.TreeDevice.Graph.outList_ne_nil line 16
  4. def OAI.MeanPayoff.TreeDevice.Graph.firstEdge line 21
  5. def OAI.MeanPayoff.TreeDevice.Graph.codeVertex line 23
  6. def OAI.MeanPayoff.TreeDevice.Graph.codeVertices line 26
  7. theorem OAI.MeanPayoff.TreeDevice.Graph.codeVertex_exact line 29
  8. theorem OAI.MeanPayoff.TreeDevice.Graph.operator_list_exact line 37
  9. theorem OAI.MeanPayoff.SignedBits.value_complement line 51
  10. def OAI.MeanPayoff.SignedBits.Word.complement line 60
  11. theorem OAI.MeanPayoff.SignedBits.Word.complement_val line 62
  12. def OAI.MeanPayoff.TreeDevice.Negate.one line 71
  13. theorem OAI.MeanPayoff.TreeDevice.Negate.one_val line 72
  14. def OAI.MeanPayoff.TreeDevice.Negate.rawNot line 74
  15. def OAI.MeanPayoff.TreeDevice.Negate.complement line 81
  16. def OAI.MeanPayoff.TreeDevice.Negate.negate line 86
  17. def OAI.MeanPayoff.TreeDevice.Negate.device line 88
  18. theorem OAI.MeanPayoff.TreeDevice.Negate.exact line 91
  19. theorem OAI.MeanPayoff.TreeDevice.Negate.rawNot_linear line 94
  20. theorem OAI.MeanPayoff.TreeDevice.Negate.complement_polynomial line 99
  21. theorem OAI.MeanPayoff.TreeDevice.Negate.polynomial line 105
  22. theorem OAI.MeanPayoff.TreeDevice.Fold.time_of_prefix_bound line 114
  23. theorem OAI.MeanPayoff.BinaryStack.Addition.value_append line 149
  24. theorem OAI.MeanPayoff.BinaryStack.Addition.value_bits line 154
  25. abbrev OAI.MeanPayoff.TreeDevice.Multiply.W line 164
  26. abbrev OAI.MeanPayoff.TreeDevice.Multiply.State line 165
  27. def OAI.MeanPayoff.TreeDevice.Multiply.stateData line 167
  28. def OAI.MeanPayoff.TreeDevice.Multiply.double line 169
  29. theorem OAI.MeanPayoff.TreeDevice.Multiply.double_val line 170
  30. theorem OAI.MeanPayoff.TreeDevice.Multiply.double_length line 171
  31. def OAI.MeanPayoff.TreeDevice.Multiply.doubleDevice line 173
  32. def OAI.MeanPayoff.TreeDevice.Multiply.rawTest line 181
  33. def OAI.MeanPayoff.TreeDevice.Multiply.step line 185
  34. def OAI.MeanPayoff.TreeDevice.Multiply.baseDevice line 188
  35. def OAI.MeanPayoff.TreeDevice.Multiply.accDevice line 191
  36. def OAI.MeanPayoff.TreeDevice.Multiply.testDevice line 194
  37. def OAI.MeanPayoff.TreeDevice.Multiply.sumDevice line 197
  38. def OAI.MeanPayoff.TreeDevice.Multiply.choiceDevice line 200
  39. def OAI.MeanPayoff.TreeDevice.Multiply.stepDevice line 204
  40. def OAI.MeanPayoff.TreeDevice.Multiply.multiply line 207
  41. def OAI.MeanPayoff.TreeDevice.Multiply.initDevice line 209
  42. def OAI.MeanPayoff.TreeDevice.Multiply.device line 214
  43. theorem OAI.MeanPayoff.TreeDevice.Multiply.step_first line 218
  44. theorem OAI.MeanPayoff.TreeDevice.Multiply.step_val line 220
  45. theorem OAI.MeanPayoff.TreeDevice.Multiply.fold_first line 223
  46. theorem OAI.MeanPayoff.TreeDevice.Multiply.fold_val line 228
  47. theorem OAI.MeanPayoff.TreeDevice.Multiply.exact line 239
  48. theorem OAI.MeanPayoff.TreeDevice.Multiply.nat_exact line 243
  49. theorem OAI.MeanPayoff.TreeDevice.Multiply.double_linear line 246
  50. theorem OAI.MeanPayoff.TreeDevice.Multiply.rawTest_linear line 253
  51. theorem OAI.MeanPayoff.TreeDevice.Multiply.base_linear line 255
  52. theorem OAI.MeanPayoff.TreeDevice.Multiply.acc_linear line 258
  53. theorem OAI.MeanPayoff.TreeDevice.Multiply.test_linear line 262
  54. theorem OAI.MeanPayoff.TreeDevice.Multiply.sum_linear line 264
  55. theorem OAI.MeanPayoff.TreeDevice.Multiply.choice_linear line 267
  56. theorem OAI.MeanPayoff.TreeDevice.Multiply.step_linear line 269