OAI/Computability/Scheduling/SeparatorWalk.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ThreeMachine.Structure.Layout line 10
  2. def OAI.ThreeMachine.Structure.Layout.time line 12
  3. def OAI.ThreeMachine.Structure.Layout.Respects line 15
  4. def OAI.ThreeMachine.Structure.Layout.Full line 19
  5. def OAI.ThreeMachine.Structure.Layout.signature line 23
  6. def OAI.ThreeMachine.Structure.Layout.Normalized line 27
  7. theorem OAI.ThreeMachine.Structure.exists_normalized line 32
  8. theorem OAI.ThreeMachine.Structure.ofFn_lt_of_first_difference line 45
  9. theorem OAI.ThreeMachine.Structure.normalized_no_improvement line 67
  10. def OAI.ThreeMachine.Structure.Layout.exchange line 77
  11. theorem OAI.ThreeMachine.Structure.exchange_time_left line 81
  12. theorem OAI.ThreeMachine.Structure.exchange_time_right line 85
  13. theorem OAI.ThreeMachine.Structure.exchange_time_other line 89
  14. theorem OAI.ThreeMachine.Structure.respects_exchange line 94
  15. theorem OAI.ThreeMachine.Structure.normalized_no_exchange line 136
  16. def OAI.ThreeMachine.Structure.PredAt line 167
  17. def OAI.ThreeMachine.Structure.DescAt line 170
  18. def OAI.ThreeMachine.Structure.IdealOn line 173
  19. def OAI.ThreeMachine.Structure.PrefixOn line 176
  20. def OAI.ThreeMachine.Structure.EarlierHigh line 179
  21. def OAI.ThreeMachine.Structure.LaterLow line 183
  22. def OAI.ThreeMachine.Structure.Separator line 187
  23. def OAI.ThreeMachine.Structure.SlotClosed line 191
  24. def OAI.ThreeMachine.Structure.AdmissiblePosition line 194
  25. def OAI.ThreeMachine.Structure.LocalObstruction line 197
  26. theorem OAI.ThreeMachine.Structure.normalized_local_obstruction line 203
  27. structure OAI.ThreeMachine.Structure.Exception line 217
  28. theorem OAI.ThreeMachine.Structure.exists_exception line 226
  29. theorem OAI.ThreeMachine.Structure.exception_ready line 245
  30. theorem OAI.ThreeMachine.Structure.trace_to_slot line 260
  31. theorem OAI.ThreeMachine.Structure.advance_earlier_high line 298
  32. theorem OAI.ThreeMachine.Structure.advance_shared_earlier line 338
  33. inductive OAI.ThreeMachine.Structure.AdvancePath line 375
  34. theorem OAI.ThreeMachine.Structure.AdvancePath.le line 381
  35. theorem OAI.ThreeMachine.Structure.AdvancePath.endpoint line 387
  36. theorem OAI.ThreeMachine.Structure.AdvancePath.admissible line 394
  37. theorem OAI.ThreeMachine.Structure.AdvancePath.shared_earlier line 401
  38. theorem OAI.ThreeMachine.Structure.shared_cutoff line 418
  39. theorem OAI.ThreeMachine.Structure.separator_congr line 454
  40. theorem OAI.ThreeMachine.Structure.AdvancePath.earlier line 478
  41. theorem OAI.ThreeMachine.Structure.walk_to_separator line 493
  42. theorem OAI.ThreeMachine.Structure.ideal_has_separator line 520
  43. def OAI.ThreeMachine.Structure.BeforeTest line 549
  44. theorem OAI.ThreeMachine.Structure.separator_description line 552