OAI/Computability/MeanPayoff/LoopDevices.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Forest.encode line 10
  2. theorem OAI.MeanPayoff.TreeDevice.Forest.encode_nil line 11
  3. theorem OAI.MeanPayoff.TreeDevice.Forest.encode_cons line 12
  4. theorem OAI.MeanPayoff.TreeDevice.Forest.encode_append line 14
  5. structure OAI.MeanPayoff.TreeDevice.Forest.Layout line 16
  6. def OAI.MeanPayoff.TreeDevice.Forest.stack line 21
  7. structure OAI.MeanPayoff.TreeDevice.Forest.Segment line 23
  8. abbrev OAI.MeanPayoff.TreeDevice.Forest.seqFlow line 30
  9. def OAI.MeanPayoff.TreeDevice.Forest.Segment.seq line 38
  10. def OAI.MeanPayoff.TreeDevice.Forest.Segment.cast line 51
  11. def OAI.MeanPayoff.TreeDevice.Forest.move01 line 54
  12. def OAI.MeanPayoff.TreeDevice.Forest.move02 line 62
  13. def OAI.MeanPayoff.TreeDevice.Forest.move10 line 70
  14. def OAI.MeanPayoff.TreeDevice.Forest.move20 line 78
  15. def OAI.MeanPayoff.TreeDevice.Forest.swap line 86
  16. def OAI.MeanPayoff.TreeDevice.Forest.bitOp line 93
  17. theorem OAI.MeanPayoff.TreeDevice.Forest.bitOp_runs line 99
  18. def OAI.MeanPayoff.TreeDevice.Forest.unpair line 105
  19. def OAI.MeanPayoff.TreeDevice.Forest.pair line 117
  20. def OAI.MeanPayoff.TreeDevice.Forest.applyDevice line 129
  21. def OAI.MeanPayoff.TreeDevice.Forest.toDevice line 138
  22. def OAI.MeanPayoff.TreeDevice.Forest.copy01 line 148
  23. def OAI.MeanPayoff.TreeDevice.Forest.duplicate line 163
  24. def OAI.MeanPayoff.TreeDevice.Forest.erase line 168
  25. theorem OAI.MeanPayoff.TreeDevice.Forest.erase_runs line 176
  26. def OAI.MeanPayoff.TreeDevice.Forest.drop line 190
  27. def OAI.MeanPayoff.TreeDevice.product line 210
  28. def OAI.MeanPayoff.TreeDevice.pairMap line 212
  29. def OAI.MeanPayoff.TreeDevice.dup line 224
  30. def OAI.MeanPayoff.TreeDevice.fanout line 228
  31. def OAI.MeanPayoff.TreeDevice.first line 233
  32. def OAI.MeanPayoff.TreeDevice.second line 240
  33. abbrev OAI.MeanPayoff.TreeDevice.Fold.flow line 250
  34. abbrev OAI.MeanPayoff.TreeDevice.Fold.program line 264
  35. abbrev OAI.MeanPayoff.TreeDevice.Fold.cfg line 267
  36. def OAI.MeanPayoff.TreeDevice.Fold.fold line 271
  37. def OAI.MeanPayoff.TreeDevice.Fold.time line 273
  38. theorem OAI.MeanPayoff.TreeDevice.Fold.loop line 278
  39. def OAI.MeanPayoff.TreeDevice.Fold.device line 339