OAI/Computability/PerfectCompleteness/Machines/FiniteConstraintMachine.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.FiniteConstraintMachine.localInput line 21
  2. def OAI.PerfectCompleteness.FiniteConstraintMachine.result line 25
  3. theorem OAI.PerfectCompleteness.FiniteConstraintMachine.result_correct line 28
  4. def OAI.PerfectCompleteness.FiniteConstraintMachine.keyWords line 32
  5. def OAI.PerfectCompleteness.FiniteConstraintMachine.keyWidth line 36
  6. theorem OAI.PerfectCompleteness.FiniteConstraintMachine.keyWords_length line 40
  7. def OAI.PerfectCompleteness.FiniteConstraintMachine.outputWords line 45
  8. def OAI.PerfectCompleteness.FiniteConstraintMachine.outputBits line 48
  9. theorem OAI.PerfectCompleteness.FiniteConstraintMachine.outputWords_drop_keys line 51
  10. theorem OAI.PerfectCompleteness.FiniteConstraintMachine.parse_output_payload line 56
  11. theorem OAI.PerfectCompleteness.FiniteConstraintMachine.decode_outputBits line 64
  12. theorem OAI.PerfectCompleteness.FiniteConstraintMachine.outputWords_length_le line 68
  13. def OAI.PerfectCompleteness.FiniteConstraintMachine.emit line 74
  14. def OAI.PerfectCompleteness.FiniteConstraintMachine.computation line 78
  15. def OAI.PerfectCompleteness.FiniteConstraintMachine.machine_output line 85
  16. theorem OAI.PerfectCompleteness.FiniteConstraintMachine.recover_right_key line 100
  17. theorem OAI.PerfectCompleteness.FiniteConstraintMachine.parsed_projection line 114
  18. theorem OAI.PerfectCompleteness.FiniteConstraintMachine.workAlphabet_finite line 120