OAI/Computability/PerfectCompleteness/Foundations/RetainedKeyTransport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.RetainedKeyTransport.retainedSlots_eq line 16
  2. def OAI.PerfectCompleteness.RetainedKeyTransport.retainedAssignmentEquiv line 22
  3. theorem OAI.PerfectCompleteness.RetainedKeyTransport.assignment_cast_apply line 27
  4. theorem OAI.PerfectCompleteness.RetainedKeyTransport.retainedAssignmentEquiv_apply line 34
  5. theorem OAI.PerfectCompleteness.RetainedKeyTransport.retainedAssignmentEquiv_agree_heq line 41
  6. theorem OAI.PerfectCompleteness.RetainedKeyTransport.exists_retained_factor line 52
  7. theorem OAI.PerfectCompleteness.RetainedKeyTransport.retainedKey_cast line 78
  8. theorem OAI.PerfectCompleteness.RetainedKeyTransport.retainedResponse_cast line 85
  9. theorem OAI.PerfectCompleteness.RetainedKeyTransport.key_eq line 93
  10. theorem OAI.PerfectCompleteness.RetainedKeyTransport.label_val_eq line 112
  11. theorem OAI.PerfectCompleteness.RetainedKeyTransport.response_eq line 124