OAI/Computability/Scheduling/FrameInvariants.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.Structure.Layout.time_bounds line 11
  2. def OAI.ThreeMachine.Structure.Layout.slot line 18
  3. theorem OAI.ThreeMachine.Structure.Layout.mem_slot line 22
  4. theorem OAI.ThreeMachine.Structure.Layout.card_slot line 27
  5. def OAI.ThreeMachine.Structure.Layout.triple line 63
  6. theorem OAI.ThreeMachine.Structure.Layout.triple_at line 67
  7. def OAI.ThreeMachine.Structure.Layout.reverse line 72
  8. theorem OAI.ThreeMachine.Structure.Layout.reverse_reverse line 74
  9. theorem OAI.ThreeMachine.Structure.Layout.reverse_time line 78
  10. theorem OAI.ThreeMachine.Structure.Layout.reverse_respects line 86
  11. theorem OAI.ThreeMachine.Structure.Layout.reverse_full line 96
  12. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.reverse line 99
  13. theorem OAI.ThreeMachine.Structure.Boundary.at_reverse line 109
  14. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.window line 131
  15. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.boundary line 146
  16. theorem OAI.ThreeMachine.Structure.PastInvariant.reorder line 165
  17. def OAI.ThreeMachine.Structure.SwapInvariant line 178
  18. theorem OAI.ThreeMachine.Structure.SwapInvariant.reorder line 184
  19. theorem OAI.ThreeMachine.Structure.ideal_has_separator_interval line 191
  20. theorem OAI.ThreeMachine.Structure.exception_global_ready line 238
  21. theorem OAI.ThreeMachine.Structure.advance_carry_descendant line 257
  22. theorem OAI.ThreeMachine.Structure.first_boundary_force line 292
  23. inductive OAI.ThreeMachine.Structure.CutoffWalk line 322
  24. theorem OAI.ThreeMachine.Structure.CutoffWalk.le line 332
  25. theorem OAI.ThreeMachine.Structure.CutoffWalk.mono line 338
  26. theorem OAI.ThreeMachine.Structure.CutoffWalk.trans_advance line 345
  27. theorem OAI.ThreeMachine.Structure.CutoffWalk.carry line 355
  28. theorem OAI.ThreeMachine.Structure.Boundary.weakPred_witness line 387
  29. theorem OAI.ThreeMachine.Structure.past_update line 399
  30. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.earlier_positions line 452
  31. theorem OAI.ThreeMachine.Structure.swap_from_normalized line 466
  32. theorem OAI.ThreeMachine.Structure.swap_inherited line 493
  33. theorem OAI.ThreeMachine.Structure.swap_prune line 504