OAI/Computability/PerfectCompleteness/Algebra/CanonicalMatrixTable.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CanonicalMatrixTable.Matrix line 21
  2. def OAI.PerfectCompleteness.CanonicalMatrixTable.query line 23
  3. def OAI.PerfectCompleteness.CanonicalMatrixTable.response line 26
  4. def OAI.PerfectCompleteness.CanonicalMatrixTable.partialTable line 29
  5. theorem OAI.PerfectCompleteness.CanonicalMatrixTable.response_realized line 32
  6. def OAI.PerfectCompleteness.CanonicalMatrixTable.rightQuery line 39
  7. theorem OAI.PerfectCompleteness.CanonicalMatrixTable.rightQuery_shift line 42
  8. theorem OAI.PerfectCompleteness.CanonicalMatrixTable.rightResponse_shift line 56
  9. def OAI.PerfectCompleteness.CanonicalMatrixTable.Accepts line 62
  10. theorem OAI.PerfectCompleteness.CanonicalMatrixTable.accepts_iff line 67
  11. theorem OAI.PerfectCompleteness.CanonicalMatrixTable.accepted_response_in_fiber line 74
  12. theorem OAI.PerfectCompleteness.CanonicalMatrixTable.card_accepted_responses_le_two line 82