OAI/Computability/PerfectCompleteness/Machines/SourceTupleResetMachine.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceTupleResetMachine.Alphabet line 15
  2. abbrev OAI.PerfectCompleteness.SourceTupleResetMachine.State line 16
  3. def OAI.PerfectCompleteness.SourceTupleResetMachine.chosen line 18
  4. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.chosen_length line 22
  5. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.table_not_mem_chosen line 35
  6. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.digit_not_mem_chosen line 38
  7. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.work_not_mem_chosen line 42
  8. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.variable_mem_chosen line 46
  9. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.finalTapes_eq line 52
  10. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.variable_count_le_table line 64
  11. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.clause_count_le_table line 70
  12. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.stack_length_le line 76
  13. def OAI.PerfectCompleteness.SourceTupleResetMachine.steps line 95
  14. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.steps_le line 99
  15. abbrev OAI.PerfectCompleteness.SourceTupleResetMachine.Label line 107
  16. def OAI.PerfectCompleteness.SourceTupleResetMachine.instruction line 111
  17. def OAI.PerfectCompleteness.SourceTupleResetMachine.entry line 115
  18. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.resetTrace line 118
  19. def OAI.PerfectCompleteness.SourceTupleResetMachine.resetInTime line 132
  20. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.finiteState line 146
  21. theorem OAI.PerfectCompleteness.SourceTupleResetMachine.finiteAlphabet line 148