OAI/Computability/Scheduling/Main.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.enc_request line 8
  2. theorem OAI.ThreeMachine.StackCompiler.requestAnswer_time_charge line 11
  3. theorem OAI.ThreeMachine.StackCompiler.Uniform.exists_requestMachine line 17
  4. def OAI.ThreeMachine.StackCompiler.requestRawBound line 33
  5. theorem OAI.ThreeMachine.StackCompiler.requestRawBound_poly line 37
  6. abbrev OAI.ThreeMachine.StackCompiler.SmallDeadline line 44
  7. theorem OAI.ThreeMachine.StackCompiler.requestRawBound_length line 46
  8. theorem OAI.ThreeMachine.main_theorem line 59

    Distinct definitions of this name: ComparatorChallenges/ThreeMachine.lean:95 (same statement text; different proof or body). Qualify references as OAI.ThreeMachine.main_theorem@path.