OAI/Computability/PerfectCompleteness/Construction/TreeCanonical.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.TreeCanonical.Location line 16
  2. def OAI.PerfectCompleteness.TreeCanonical.locationCount line 18
  3. def OAI.PerfectCompleteness.TreeCanonical.numbering line 21
  4. def OAI.PerfectCompleteness.TreeCanonical.numberedSlots line 27
  5. def OAI.PerfectCompleteness.TreeCanonical.assignmentEquiv line 31
  6. theorem OAI.PerfectCompleteness.TreeCanonical.assignmentEquiv_apply line 37
  7. def OAI.PerfectCompleteness.TreeCanonical.numberedProjection line 43
  8. theorem OAI.PerfectCompleteness.TreeCanonical.assignmentEquiv_projection line 48
  9. theorem OAI.PerfectCompleteness.TreeCanonical.assignmentEquiv_symm_projection line 54
  10. def OAI.PerfectCompleteness.TreeCanonical.numberedFunction line 64
  11. theorem OAI.PerfectCompleteness.TreeCanonical.numberedFunction_projection line 68
  12. def OAI.PerfectCompleteness.TreeCanonical.key line 76
  13. theorem OAI.PerfectCompleteness.TreeCanonical.key_projection line 81
  14. theorem OAI.PerfectCompleteness.TreeCanonical.H_key_projection line 89
  15. abbrev OAI.PerfectCompleteness.TreeCanonical.Label line 95
  16. def OAI.PerfectCompleteness.TreeCanonical.evaluateLabel line 99
  17. def OAI.PerfectCompleteness.TreeCanonical.restore line 104
  18. theorem OAI.PerfectCompleteness.TreeCanonical.restore_evaluateLabel line 108
  19. theorem OAI.PerfectCompleteness.TreeCanonical.restore_injective line 117