OAI/Computability/BinPacking/PCP/NormalizationReadMachine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingCompleteness.NormalizationReadMachine.Signs line 13
  2. abbrev OAI.BinPackingCompleteness.NormalizationReadMachine.Counters line 14
  3. abbrev OAI.BinPackingCompleteness.NormalizationReadMachine.State line 15
  4. abbrev OAI.BinPackingCompleteness.NormalizationReadMachine.Alphabet line 16
  5. def OAI.BinPackingCompleteness.NormalizationReadMachine.clean line 18
  6. def OAI.BinPackingCompleteness.NormalizationReadMachine.clauseSigns line 20
  7. def OAI.BinPackingCompleteness.NormalizationReadMachine.clauseCounters line 22
  8. inductive OAI.BinPackingCompleteness.NormalizationReadMachine.Label line 25
  9. def OAI.BinPackingCompleteness.NormalizationReadMachine.afterSign line 34
  10. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.afterSign_zero line 38
  11. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.afterSign_one line 41
  12. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.afterSign_two line 44
  13. def OAI.BinPackingCompleteness.NormalizationReadMachine.saveSign line 47
  14. def OAI.BinPackingCompleteness.NormalizationReadMachine.rejectSign line 52
  15. def OAI.BinPackingCompleteness.NormalizationReadMachine.signInstruction line 56
  16. def OAI.BinPackingCompleteness.NormalizationReadMachine.instruction line 67
  17. def OAI.BinPackingCompleteness.NormalizationReadMachine.tapes line 73
  18. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.tapes_input line 78
  19. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.tapes_counter line 84
  20. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.tapes_other line 90
  21. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.update_input line 95
  22. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.update_counter line 106
  23. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.fieldTapes_eq line 123
  24. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.fieldTrace line 140
  25. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.signStep line 159
  26. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.joinTrace line 173
  27. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.literalTrace line 177
  28. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.clauseTrace line 201
  29. def OAI.BinPackingCompleteness.NormalizationReadMachine.clauseInTime line 249
  30. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.steps_le_encoded_length line 264
  31. abbrev OAI.BinPackingCompleteness.NormalizationReadMachine.ConcreteLabel line 271
  32. def OAI.BinPackingCompleteness.NormalizationReadMachine.concreteProgram line 273
  33. abbrev OAI.BinPackingCompleteness.NormalizationReadMachine.machine line 277
  34. def OAI.BinPackingCompleteness.NormalizationReadMachine.machineInTime line 288
  35. theorem OAI.BinPackingCompleteness.NormalizationReadMachine.machine_finiteAlphabet line 298