OAI/Computability/MeanPayoff/VectorDevices.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.TreeDevice.treeSize_pos line 10
  2. theorem OAI.MeanPayoff.TreeDevice.listTree_reverse_size line 13
  3. def OAI.MeanPayoff.TreeDevice.Map.resource line 19
  4. theorem OAI.MeanPayoff.TreeDevice.Map.resource_nil line 22
  5. theorem OAI.MeanPayoff.TreeDevice.Map.resource_cons line 25
  6. theorem OAI.MeanPayoff.TreeDevice.Map.input_size_le line 30
  7. theorem OAI.MeanPayoff.TreeDevice.Map.output_size_le line 33
  8. theorem OAI.MeanPayoff.TreeDevice.Map.reverse_cost line 42
  9. theorem OAI.MeanPayoff.TreeDevice.Map.forward_cost line 51
  10. theorem OAI.MeanPayoff.TreeDevice.Map.limit_le line 61
  11. def OAI.MeanPayoff.RegisterBits.quieten line 77
  12. def OAI.MeanPayoff.RegisterBits.quietConfig line 83
  13. theorem OAI.MeanPayoff.RegisterBits.quieten_coinFree line 86
  14. theorem OAI.MeanPayoff.RegisterBits.quieten_step line 88
  15. theorem OAI.MeanPayoff.RegisterBits.quieten_advance line 98
  16. def OAI.MeanPayoff.TreeDevice.ofProgram line 110
  17. theorem OAI.MeanPayoff.WorkStack.RegisterCompile.signed_compares line 126
  18. def OAI.MeanPayoff.ComparisonForest.test line 141
  19. theorem OAI.MeanPayoff.ComparisonForest.test_eq line 143
  20. abbrev OAI.MeanPayoff.ComparisonForest.flow line 147
  21. def OAI.MeanPayoff.ComparisonForest.program line 162
  22. def OAI.MeanPayoff.ComparisonForest.store3 line 164
  23. def OAI.MeanPayoff.ComparisonForest.store4 line 166
  24. theorem OAI.MeanPayoff.ComparisonForest.stage2 line 169
  25. theorem OAI.MeanPayoff.ComparisonForest.stage3 line 181
  26. theorem OAI.MeanPayoff.ComparisonForest.total_bound line 191
  27. theorem OAI.MeanPayoff.ComparisonForest.program_compares line 203
  28. def OAI.MeanPayoff.TreeDevice.Compare.pairWord line 229
  29. def OAI.MeanPayoff.TreeDevice.Compare.bitTree line 230
  30. def OAI.MeanPayoff.TreeDevice.Compare.testPair line 231
  31. abbrev OAI.MeanPayoff.TreeDevice.Compare.flow line 233
  32. abbrev OAI.MeanPayoff.TreeDevice.Compare.program line 243
  33. def OAI.MeanPayoff.TreeDevice.Compare.limit line 245
  34. theorem OAI.MeanPayoff.TreeDevice.Compare.runs line 248
  35. def OAI.MeanPayoff.TreeDevice.Compare.device line 276
  36. theorem OAI.MeanPayoff.TreeDevice.Compare.limit_le line 279
  37. theorem OAI.MeanPayoff.TreeDevice.Compare.testPair_eq line 286
  38. def OAI.MeanPayoff.TreeDevice.Compare.vectorDevice line 289
  39. theorem OAI.MeanPayoff.TreeDevice.Compare.vector_exact line 292