OAI/Computability/PerfectCompleteness/Construction/CutNodeRows.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.CutNodeRows.nativeH_eq line 20
  2. def OAI.PerfectCompleteness.CutNodeRows.nativeEquiv line 26
  3. def OAI.PerfectCompleteness.CutNodeRows.cutRowEquiv line 32
  4. def OAI.PerfectCompleteness.CutNodeRows.rowIndexEquiv line 37
  5. def OAI.PerfectCompleteness.CutNodeRows.directionEquiv line 41
  6. theorem OAI.PerfectCompleteness.CutNodeRows.native_selectedRows line 47
  7. def OAI.PerfectCompleteness.CutNodeRows.transportRows line 57
  8. theorem OAI.PerfectCompleteness.CutNodeRows.transportRows_selectedRows line 63
  9. def OAI.PerfectCompleteness.CutNodeRows.matrixOfRows line 71
  10. theorem OAI.PerfectCompleteness.CutNodeRows.ofRows_selectedRows line 78
  11. theorem OAI.PerfectCompleteness.CutNodeRows.matrixOfRows_selectedRows line 86
  12. def OAI.PerfectCompleteness.CutNodeRows.bucketTapeEquiv line 92
  13. def OAI.PerfectCompleteness.CutNodeRows.bucketSampleEquiv line 99
  14. theorem OAI.PerfectCompleteness.CutNodeRows.tape_equiv_update line 110
  15. theorem OAI.PerfectCompleteness.CutNodeRows.bucketTapeEquiv_update line 124
  16. theorem OAI.PerfectCompleteness.CutNodeRows.evaluate_equiv line 134
  17. theorem OAI.PerfectCompleteness.CutNodeRows.transportRows_evaluate line 147
  18. theorem OAI.PerfectCompleteness.CutNodeRows.matrixOfRows_evaluate line 156