OAI/Probability/SATComputability/MaskDeletionTimes.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FixedClauseThreshold.Computability.maskLifetime_union line 11
  2. theorem OAI.FixedClauseThreshold.Computability.maskLifetime_biUnion line 29
  3. def OAI.FixedClauseThreshold.Computability.deletionMask line 42
  4. def OAI.FixedClauseThreshold.Computability.deletionBudgetMask line 45
  5. def OAI.FixedClauseThreshold.Computability.freeDeletionBudgetMask line 48
  6. theorem OAI.FixedClauseThreshold.Computability.deletionMask_mono line 51
  7. theorem OAI.FixedClauseThreshold.Computability.deletionBudgetMask_union line 55
  8. def OAI.FixedClauseThreshold.Computability.fixedMaskDeletionTime line 66
  9. theorem OAI.FixedClauseThreshold.Computability.fixedMaskDeletionTime_mono line 70
  10. theorem OAI.FixedClauseThreshold.Computability.bestMaskDeletionTime_eq line 75
  11. theorem OAI.FixedClauseThreshold.Computability.freeMaskDeletionTime_eq line 81
  12. theorem OAI.FixedClauseThreshold.Computability.maskLifetime_frontload line 87