OAI/Computability/PerfectCompleteness/Machines/LowerCutInstalledInput.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.LowerCutInstalledInput.NodeRows line 23
  2. abbrev OAI.PerfectCompleteness.LowerCutInstalledInput.NodeMatrix line 24
  3. def OAI.PerfectCompleteness.LowerCutInstalledInput.rowCast line 27
  4. def OAI.PerfectCompleteness.LowerCutInstalledInput.matrixCast line 32
  5. def OAI.PerfectCompleteness.LowerCutInstalledInput.scalarCast line 37
  6. def OAI.PerfectCompleteness.LowerCutInstalledInput.directionCast line 42
  7. theorem OAI.PerfectCompleteness.LowerCutInstalledInput.rows_matrixCast line 48
  8. theorem OAI.PerfectCompleteness.LowerCutInstalledInput.shift_matrixCast line 55
  9. theorem OAI.PerfectCompleteness.LowerCutInstalledInput.update_rowCast line 64
  10. def OAI.PerfectCompleteness.LowerCutInstalledInput.lowerMatrixEquiv line 79
  11. def OAI.PerfectCompleteness.LowerCutInstalledInput.lowerScalarEquiv line 83
  12. def OAI.PerfectCompleteness.LowerCutInstalledInput.lowerDirectionEquiv line 87
  13. theorem OAI.PerfectCompleteness.LowerCutInstalledInput.rows_lowerMatrixEquiv line 91
  14. theorem OAI.PerfectCompleteness.LowerCutInstalledInput.shift_lowerMatrixEquiv line 101
  15. theorem OAI.PerfectCompleteness.LowerCutInstalledInput.uniform_lowerMatrixEquiv line 127
  16. theorem OAI.PerfectCompleteness.LowerCutInstalledInput.uniform_lowerMatrix_scalarEquiv line 137
  17. theorem OAI.PerfectCompleteness.LowerCutInstalledInput.actualInput_installMatrix line 157