OAI/Computability/Scheduling/SplitPaths.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.Structure.RelativeDescription line 11
  2. structure OAI.ThreeMachine.Structure.SplitVertex line 14
  3. theorem OAI.ThreeMachine.Structure.SplitVertex.ext line 32
  4. def OAI.ThreeMachine.Structure.SplitVertex.reverse line 41
  5. theorem OAI.ThreeMachine.Structure.SplitVertex.reverse_reverse line 52
  6. def OAI.ThreeMachine.Structure.SplitVertex.AtTime line 55
  7. theorem OAI.ThreeMachine.Structure.SplitVertex.AtTime.unique line 60
  8. theorem OAI.ThreeMachine.Structure.SplitVertex.left_subset line 68
  9. theorem OAI.ThreeMachine.Structure.SplitVertex.middle_subset line 71
  10. theorem OAI.ThreeMachine.Structure.SplitVertex.right_subset line 74
  11. theorem OAI.ThreeMachine.Structure.SplitVertex.right_eq line 77
  12. theorem OAI.ThreeMachine.Structure.SplitVertex.left_eq line 91
  13. def OAI.ThreeMachine.Structure.SplitVertex.Step line 95
  14. theorem OAI.ThreeMachine.Structure.SplitVertex.gap_reverse line 98
  15. theorem OAI.ThreeMachine.Structure.SplitVertex.step_reverse line 116
  16. theorem OAI.ThreeMachine.Structure.SplitVertex.step_mono line 132
  17. theorem OAI.ThreeMachine.Structure.SplitVertex.path_reverse line 136
  18. def OAI.ThreeMachine.Structure.AcceptedAt line 145
  19. theorem OAI.ThreeMachine.Structure.AcceptedAt.empty line 155
  20. theorem OAI.ThreeMachine.Structure.AcceptedAt.succ line 161
  21. theorem OAI.ThreeMachine.Structure.AcceptedAt.mono line 171
  22. theorem OAI.ThreeMachine.Structure.AcceptedAt.reverse line 179
  23. theorem OAI.ThreeMachine.Structure.before_small line 201
  24. def OAI.ThreeMachine.Structure.SplitVertex.ofTime line 207
  25. theorem OAI.ThreeMachine.Structure.SplitVertex.ofTime_at line 283
  26. theorem OAI.ThreeMachine.Structure.EdgeData.target_description line 296
  27. def OAI.ThreeMachine.Structure.EdgeData.targetVertex line 323
  28. theorem OAI.ThreeMachine.Structure.EdgeData.targetVertex_at line 336
  29. theorem OAI.ThreeMachine.Structure.SplitVertex.AtTime.congr line 353
  30. def OAI.ThreeMachine.Structure.Reached line 366
  31. theorem OAI.ThreeMachine.Structure.reached_start line 371
  32. theorem OAI.ThreeMachine.Structure.EdgeData.reached line 373
  33. theorem OAI.ThreeMachine.Structure.Reached.congr_time line 416
  34. theorem OAI.ThreeMachine.Structure.NumericWalkData.reached line 432
  35. theorem OAI.ThreeMachine.Structure.separator_at line 451
  36. theorem OAI.ThreeMachine.Structure.Boundary.Separates.mono_domain line 462
  37. theorem OAI.ThreeMachine.Structure.Boundary.at_bounds line 466
  38. theorem OAI.ThreeMachine.Structure.Boundary.actual_of_interior line 473