OAI/Computability/MeanPayoff/TreeDevices.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.RegisterBits.CoinFree line 10
  2. theorem OAI.MeanPayoff.RegisterBits.step_coinFree line 13
  3. theorem OAI.MeanPayoff.RegisterBits.advance_coinFree line 19
  4. theorem OAI.MeanPayoff.RegisterBits.advance_pad line 25
  5. theorem OAI.MeanPayoff.RegisterBits.Flow.compile_coinFree line 30
  6. def OAI.MeanPayoff.TreeDevice.store line 44
  7. def OAI.MeanPayoff.TreeDevice.treeSize line 47
  8. structure OAI.MeanPayoff.TreeDevice.Device line 49
  9. def OAI.MeanPayoff.TreeDevice.skip line 57
  10. def OAI.MeanPayoff.TreeDevice.identity line 63
  11. abbrev OAI.MeanPayoff.TreeDevice.compFlow line 69
  12. def OAI.MeanPayoff.TreeDevice.compose line 77
  13. theorem OAI.MeanPayoff.TreeDevice.store_size line 93
  14. theorem OAI.MeanPayoff.TreeDevice.output_size line 97
  15. theorem OAI.MeanPayoff.RegisterBits.Flow.hop_update line 109
  16. def OAI.MeanPayoff.TreeDevice.core line 126
  17. theorem OAI.MeanPayoff.TreeDevice.core_zero line 127
  18. def OAI.MeanPayoff.TreeDevice.moveCode line 128
  19. theorem OAI.MeanPayoff.TreeDevice.move01 line 130
  20. theorem OAI.MeanPayoff.TreeDevice.move02 line 141
  21. theorem OAI.MeanPayoff.TreeDevice.move10 line 152
  22. theorem OAI.MeanPayoff.TreeDevice.move20 line 163
  23. theorem OAI.MeanPayoff.TreeDevice.core_update line 174
  24. def OAI.MeanPayoff.TreeDevice.listTree line 179
  25. theorem OAI.MeanPayoff.TreeDevice.listTree_nil line 183
  26. theorem OAI.MeanPayoff.TreeDevice.listTree_cons line 184
  27. theorem OAI.MeanPayoff.TreeDevice.encode_listTree_cons line 187
  28. theorem OAI.MeanPayoff.TreeDevice.treeSize_nil line 190
  29. theorem OAI.MeanPayoff.TreeDevice.treeSize_pair line 191
  30. theorem OAI.MeanPayoff.TreeDevice.listTree_size line 194
  31. def OAI.MeanPayoff.RegisterBits.Reaches line 205
  32. theorem OAI.MeanPayoff.RegisterBits.Reaches.trans line 208
  33. theorem OAI.MeanPayoff.RegisterBits.Reaches.mono line 216
  34. theorem OAI.MeanPayoff.RegisterBits.Reaches.pad line 222
  35. abbrev OAI.MeanPayoff.TreeDevice.Map.flow line 231
  36. abbrev OAI.MeanPayoff.TreeDevice.Map.program line 252
  37. abbrev OAI.MeanPayoff.TreeDevice.Map.cfg line 255
  38. def OAI.MeanPayoff.TreeDevice.Map.revTime line 259
  39. theorem OAI.MeanPayoff.TreeDevice.Map.reverse_runs line 264
  40. def OAI.MeanPayoff.TreeDevice.Map.frontTime line 335
  41. theorem OAI.MeanPayoff.TreeDevice.Map.forward_runs line 341
  42. def OAI.MeanPayoff.TreeDevice.Map.limit line 414
  43. theorem OAI.MeanPayoff.TreeDevice.Map.runs line 419
  44. def OAI.MeanPayoff.TreeDevice.Map.device line 451