OAI/Computability/MeanPayoff/Sorting.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.RegisterBits.Flow.finish_at line 9
  2. abbrev OAI.MeanPayoff.TreeDevice.Tail.discard line 24
  3. abbrev OAI.MeanPayoff.TreeDevice.Tail.flow line 26
  4. abbrev OAI.MeanPayoff.TreeDevice.Tail.program line 33
  5. def OAI.MeanPayoff.TreeDevice.Tail.limit line 35
  6. theorem OAI.MeanPayoff.TreeDevice.Tail.runs line 39
  7. def OAI.MeanPayoff.TreeDevice.Tail.device line 67
  8. def OAI.MeanPayoff.TreeDevice.Halve.halve line 76
  9. theorem OAI.MeanPayoff.TreeDevice.Halve.halve_val line 78
  10. theorem OAI.MeanPayoff.TreeDevice.Halve.listTree_boolData line 87
  11. def OAI.MeanPayoff.TreeDevice.Halve.device line 92
  12. def OAI.MeanPayoff.TreeDevice.Halve.average line 99
  13. def OAI.MeanPayoff.TreeDevice.Halve.averageDevice line 101
  14. theorem OAI.MeanPayoff.TreeDevice.Halve.average_val line 104
  15. def OAI.MeanPayoff.TreeDevice.Halve.averageVectorDevice line 108
  16. theorem OAI.MeanPayoff.TreeDevice.Halve.average_exact line 112
  17. def OAI.MeanPayoff.TreeDevice.Device.recode line 122
  18. def OAI.MeanPayoff.TreeDevice.pairSwap line 132
  19. def OAI.MeanPayoff.TreeDevice.Forest.pushNil line 138
  20. def OAI.MeanPayoff.TreeDevice.Lists.nilPrefix line 154
  21. def OAI.MeanPayoff.TreeDevice.Lists.nilSuffix line 159
  22. def OAI.MeanPayoff.TreeDevice.Lists.consDevice line 163
  23. def OAI.MeanPayoff.TreeDevice.Lists.consAcc line 168
  24. def OAI.MeanPayoff.TreeDevice.Lists.reverseDevice line 172
  25. abbrev OAI.MeanPayoff.TreeDevice.Sort.W line 184
  26. abbrev OAI.MeanPayoff.TreeDevice.Sort.Acc line 185
  27. abbrev OAI.MeanPayoff.TreeDevice.Sort.InStep line 186
  28. def OAI.MeanPayoff.TreeDevice.Sort.carryStep line 188
  29. def OAI.MeanPayoff.TreeDevice.Sort.pairDevice line 191
  30. def OAI.MeanPayoff.TreeDevice.Sort.tailDevice line 196
  31. def OAI.MeanPayoff.TreeDevice.Sort.carryDevice line 200
  32. def OAI.MeanPayoff.TreeDevice.Sort.insert line 205
  33. def OAI.MeanPayoff.TreeDevice.Sort.initialDevice line 209
  34. def OAI.MeanPayoff.TreeDevice.Sort.insertDevice line 215
  35. def OAI.MeanPayoff.TreeDevice.Sort.sort line 219
  36. def OAI.MeanPayoff.TreeDevice.Sort.sortDevice line 221
  37. def OAI.MeanPayoff.TreeDevice.Sort.bubble line 226
  38. theorem OAI.MeanPayoff.TreeDevice.Sort.fold_carry line 230
  39. theorem OAI.MeanPayoff.TreeDevice.Sort.insert_eq line 239
  40. def OAI.MeanPayoff.TreeDevice.Sort.bubbleInt line 242
  41. theorem OAI.MeanPayoff.TreeDevice.Sort.bubble_val line 246
  42. theorem OAI.MeanPayoff.TreeDevice.Sort.bubble_perm line 256
  43. theorem OAI.MeanPayoff.TreeDevice.Sort.bubbleInt_perm line 266
  44. theorem OAI.MeanPayoff.TreeDevice.Sort.bubbleInt_sorted line 275
  45. theorem OAI.MeanPayoff.TreeDevice.Sort.insert_perm line 289
  46. theorem OAI.MeanPayoff.TreeDevice.Sort.insert_sorted line 293
  47. theorem OAI.MeanPayoff.TreeDevice.Sort.fold_sort_perm line 298
  48. theorem OAI.MeanPayoff.TreeDevice.Sort.fold_sort_sorted line 309
  49. theorem OAI.MeanPayoff.TreeDevice.Sort.sort_perm line 315
  50. theorem OAI.MeanPayoff.TreeDevice.Sort.sort_sorted line 318
  51. theorem OAI.MeanPayoff.TreeDevice.Sort.sort_values line 321
  52. theorem OAI.MeanPayoff.TreeDevice.Sort.insert_size line 326
  53. theorem OAI.MeanPayoff.TreeDevice.Sort.sort_size line 335