OAI/Computability/PerfectCompleteness/Machines/DomainEncoding.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.DomainEncoding.allowed_dropped_iff line 13
  2. theorem OAI.PerfectCompleteness.DomainEncoding.legalAssignments_all_dropped line 17
  3. theorem OAI.PerfectCompleteness.DomainEncoding.localKey_eq_dropped_of_unused line 23
  4. theorem OAI.PerfectCompleteness.DomainEncoding.keyFields_eq_dropped_of_unused line 37
  5. theorem OAI.PerfectCompleteness.DomainEncoding.keyFields_eq_dropped_of_constant line 45
  6. def OAI.PerfectCompleteness.DomainEncoding.retainedFields line 53
  7. theorem OAI.PerfectCompleteness.DomainEncoding.retainedKeys_eq_retainedFields line 57
  8. theorem OAI.PerfectCompleteness.DomainEncoding.mem_retainedFields line 61
  9. def OAI.PerfectCompleteness.DomainEncoding.lookupField line 78
  10. theorem OAI.PerfectCompleteness.DomainEncoding.lookupField_eq_of_mem line 83
  11. theorem OAI.PerfectCompleteness.DomainEncoding.lookupField_eq_dropped line 104
  12. theorem OAI.PerfectCompleteness.DomainEncoding.lookupField_retainedFields line 120
  13. theorem OAI.PerfectCompleteness.DomainEncoding.retainedFields_injective line 135
  14. theorem OAI.PerfectCompleteness.DomainEncoding.keyFields_eq_of_retainedKeys_eq line 142
  15. theorem OAI.PerfectCompleteness.DomainEncoding.legalAssignments_eq_of_retainedKeys_eq line 150
  16. abbrev OAI.PerfectCompleteness.DomainEncoding.RetainedLocation line 159
  17. abbrev OAI.PerfectCompleteness.DomainEncoding.RetainedAssignment line 161
  18. def OAI.PerfectCompleteness.DomainEncoding.restrictAssignment line 164
  19. def OAI.PerfectCompleteness.DomainEncoding.extendAssignment line 168
  20. def OAI.PerfectCompleteness.DomainEncoding.legalRetainedEquiv line 180