OAI/Computability/Scheduling/RunCertificates.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.Structure.RankTail line 11
  2. theorem OAI.ThreeMachine.Structure.rankTail_upset line 13
  3. structure OAI.ThreeMachine.Structure.RunData line 19
  4. def OAI.ThreeMachine.Structure.RunData.narrow line 35
  5. def OAI.ThreeMachine.Structure.RunData.carry line 40
  6. def OAI.ThreeMachine.Structure.RunData.prune line 73
  7. def OAI.ThreeMachine.Structure.RunData.append line 89
  8. theorem OAI.ThreeMachine.Structure.RunData.entry_small line 125
  9. def OAI.ThreeMachine.Structure.RunData.flatEntry line 134
  10. theorem OAI.ThreeMachine.Structure.RunData.flat_union_agrees line 137
  11. theorem OAI.ThreeMachine.Structure.RunData.short_upset_extension line 164
  12. def OAI.ThreeMachine.Structure.GlobalList.empty line 208
  13. def OAI.ThreeMachine.Structure.GlobalList.one line 210
  14. def OAI.ThreeMachine.Structure.GlobalList.pair line 212
  15. theorem OAI.ThreeMachine.Structure.GlobalList.qual_empty line 214
  16. theorem OAI.ThreeMachine.Structure.GlobalList.qual_one line 218
  17. theorem OAI.ThreeMachine.Structure.GlobalList.qual_pair line 222
  18. theorem OAI.ThreeMachine.Structure.GlobalList.empty_upsets line 226
  19. theorem OAI.ThreeMachine.Structure.GlobalList.pair_upsets line 231
  20. def OAI.ThreeMachine.Structure.GlobalList.InjectionDisjoint line 237
  21. theorem OAI.ThreeMachine.Structure.GlobalList.InjectionDisjoint.narrow line 241
  22. theorem OAI.ThreeMachine.Structure.GlobalList.InjectionDisjoint.carry line 246
  23. theorem OAI.ThreeMachine.Structure.GlobalList.InjectionDisjoint.prune line 255
  24. theorem OAI.ThreeMachine.Structure.GlobalList.InjectionDisjoint.append line 262
  25. theorem OAI.ThreeMachine.Structure.GlobalList.pruned_length line 276
  26. def OAI.ThreeMachine.Structure.RunData.root line 319
  27. def OAI.ThreeMachine.Structure.RunData.switched line 334
  28. def OAI.ThreeMachine.Structure.PriorityCut line 362
  29. theorem OAI.ThreeMachine.Structure.priorityCut_prefix line 364
  30. theorem OAI.ThreeMachine.Structure.priorityCut_ideal line 371
  31. theorem OAI.ThreeMachine.Structure.numeric_shared_cutoff line 377
  32. structure OAI.ThreeMachine.Structure.NumericWalkData line 410
  33. theorem OAI.ThreeMachine.Structure.exists_numeric_walk line 422