OAI/Computability/PerfectCompleteness/Foundations/HierarchicalArrays.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.HierarchicalArrays.Nodes line 14
  2. instance OAI.PerfectCompleteness.HierarchicalArrays.nodesFintype line 18
  3. instance OAI.PerfectCompleteness.HierarchicalArrays.nodesDecidableEq line 25
  4. def OAI.PerfectCompleteness.HierarchicalArrays.Nodes.height line 37
  5. def OAI.PerfectCompleteness.HierarchicalArrays.Nodes.path line 42
  6. theorem OAI.PerfectCompleteness.HierarchicalArrays.Nodes.height_pos line 48
  7. theorem OAI.PerfectCompleteness.HierarchicalArrays.Nodes.height_le line 60
  8. def OAI.PerfectCompleteness.HierarchicalArrays.nodeSlots line 67
  9. def OAI.PerfectCompleteness.HierarchicalArrays.restrictNode line 72
  10. theorem OAI.PerfectCompleteness.HierarchicalArrays.restrictNode_surjective line 76
  11. abbrev OAI.PerfectCompleteness.HierarchicalArrays.Block line 81
  12. abbrev OAI.PerfectCompleteness.HierarchicalArrays.Arrays line 83
  13. theorem OAI.PerfectCompleteness.HierarchicalArrays.arrays_finite line 87
  14. def OAI.PerfectCompleteness.HierarchicalArrays.joint line 92
  15. theorem OAI.PerfectCompleteness.HierarchicalArrays.joint_component line 97
  16. theorem OAI.PerfectCompleteness.HierarchicalArrays.row_mem_root line 103
  17. abbrev OAI.PerfectCompleteness.HierarchicalArrays.Output line 112
  18. def OAI.PerfectCompleteness.HierarchicalArrays.fullJoint line 115
  19. def OAI.PerfectCompleteness.HierarchicalArrays.sourceSlots line 121
  20. def OAI.PerfectCompleteness.HierarchicalArrays.numberedEndpoints line 128
  21. theorem OAI.PerfectCompleteness.HierarchicalArrays.numberedSlots_sourceSlots line 134
  22. def OAI.PerfectCompleteness.HierarchicalArrays.presentation line 139
  23. theorem OAI.PerfectCompleteness.HierarchicalArrays.presentation_key line 147
  24. theorem OAI.PerfectCompleteness.HierarchicalArrays.presentation_evaluate line 154
  25. def OAI.PerfectCompleteness.HierarchicalArrays.sourceAssignment line 163
  26. theorem OAI.PerfectCompleteness.HierarchicalArrays.sourceAssignment_numbered line 169
  27. theorem OAI.PerfectCompleteness.HierarchicalArrays.presentation_realizing line 176