OAI/Computability/PerfectCompleteness/Machines/DescriptorProjectionMachine.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.DescriptorProjectionMachine.projection line 20
  2. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.projection_apply line 26
  3. def OAI.PerfectCompleteness.DescriptorProjectionMachine.outputWords line 32
  4. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.outputWords_eq line 35
  5. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.outputWords_length line 43
  6. def OAI.PerfectCompleteness.DescriptorProjectionMachine.outputBits line 48
  7. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.outputBits_length_le line 51
  8. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.outputBits_parse line 63
  9. def OAI.PerfectCompleteness.DescriptorProjectionMachine.keys line 74
  10. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.keys_complete line 77
  11. def OAI.PerfectCompleteness.DescriptorProjectionMachine.pushBound line 80
  12. def OAI.PerfectCompleteness.DescriptorProjectionMachine.statement line 83
  13. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.statement_trace line 88
  14. def OAI.PerfectCompleteness.DescriptorProjectionMachine.emitInTime line 98
  15. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.output_frame line 113
  16. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.statement_pushBound line 120
  17. def OAI.PerfectCompleteness.DescriptorProjectionMachine.reverseStatement line 129
  18. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.reverse_statement_trace line 134
  19. def OAI.PerfectCompleteness.DescriptorProjectionMachine.reverseEmitInTime line 145
  20. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.reverse_output_frame line 161
  21. theorem OAI.PerfectCompleteness.DescriptorProjectionMachine.reverse_statement_pushBound line 168