OAI/Computability/PerfectCompleteness/Foundations/SourceKeyBoundsLemmas.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SourceKeyBounds.SlotIDsLe line 18
  2. theorem OAI.PerfectCompleteness.SourceKeyBounds.recover_entryID_le line 22
  3. theorem OAI.PerfectCompleteness.SourceKeyBounds.actualSlot_IDs_le line 27
  4. theorem OAI.PerfectCompleteness.SourceKeyBounds.retained_length_le line 35
  5. theorem OAI.PerfectCompleteness.SourceKeyBounds.retained_entryID_le line 40
  6. theorem OAI.PerfectCompleteness.SourceKeyBounds.key_retained_length line 48
  7. theorem OAI.PerfectCompleteness.SourceKeyBounds.key_entryID_le line 54
  8. theorem OAI.PerfectCompleteness.SourceKeyBounds.variableCount_le_bits line 62
  9. theorem OAI.PerfectCompleteness.SourceKeyBounds.clauseCount_le_bits line 68
  10. theorem OAI.PerfectCompleteness.SourceKeyBounds.source_variable_le_bits line 74
  11. theorem OAI.PerfectCompleteness.SourceKeyBounds.numberedSlots_IDs_le line 83
  12. theorem OAI.PerfectCompleteness.SourceKeyBounds.source_key_retained_length line 101
  13. theorem OAI.PerfectCompleteness.SourceKeyBounds.source_key_entryID_le line 111
  14. theorem OAI.PerfectCompleteness.SourceKeyBounds.left_retained_length line 129
  15. theorem OAI.PerfectCompleteness.SourceKeyBounds.right_retained_length line 134
  16. theorem OAI.PerfectCompleteness.SourceKeyBounds.left_entryID_le line 139
  17. theorem OAI.PerfectCompleteness.SourceKeyBounds.right_entryID_le line 146
  18. theorem OAI.PerfectCompleteness.SignedSourceCost.fieldValue_le_bits line 171
  19. theorem OAI.PerfectCompleteness.SignedSourceCost.prepared_metadata line 186
  20. theorem OAI.PerfectCompleteness.SignedSourceCost.prepared_sourceLength_le line 212