OAI/Computability/PerfectCompleteness/Algebra/HierarchicalMatrixTable.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.HierarchicalMatrixTable.Background line 19
  2. abbrev OAI.PerfectCompleteness.HierarchicalMatrixTable.SideOutput line 22
  3. abbrev OAI.PerfectCompleteness.HierarchicalMatrixTable.Matrix line 25
  4. def OAI.PerfectCompleteness.HierarchicalMatrixTable.backgroundOf line 27
  5. def OAI.PerfectCompleteness.HierarchicalMatrixTable.nativeRows line 30
  6. def OAI.PerfectCompleteness.HierarchicalMatrixTable.assemble line 35
  7. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.assemble_selected line 39
  8. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.assemble_other line 44
  9. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.embedded_assembled_rows line 49
  10. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.matrix_assemble line 58
  11. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.nativeRows_matrix line 64
  12. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.assemble_original line 74
  13. def OAI.PerfectCompleteness.HierarchicalMatrixTable.other line 82
  14. def OAI.PerfectCompleteness.HierarchicalMatrixTable.displayed line 86
  15. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.displayed_original line 91
  16. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.query_eq_split_displayed line 97
  17. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.response_eq_split_response line 120
  18. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.rightQuery_eq line 134
  19. theorem OAI.PerfectCompleteness.HierarchicalMatrixTable.accepts_iff_canonical line 143