OAI/Computability/PerfectCompleteness/Machines/SignedRuntimeBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SignedRuntimeBounds.KeyBound line 17
  2. def OAI.PerfectCompleteness.SignedRuntimeBounds.KeysBound line 21
  3. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.keysBound_append line 24
  4. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.endpoint_budget_le line 33
  5. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.fold_budget_le line 67
  6. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.completedOrder_length_le line 167
  7. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.left_atIndex_bound line 172
  8. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.right_atIndex_bound line 187
  9. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.left_prefix_bound line 202
  10. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.right_prefix_bound line 210
  11. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.bodyBudget_le_envelope line 218
  12. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.bodyBudget_le_polynomial line 282
  13. theorem OAI.PerfectCompleteness.SignedRuntimeBounds.outerBudget_le_polynomial line 296