OAI/Computability/BinPacking/PCP/NormalizationLoopMachine.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingCompleteness.NormalizationStream.blocks line 12
  2. theorem OAI.BinPackingCompleteness.NormalizationStream.blocks_eq_finRange line 17
  3. theorem OAI.BinPackingCompleteness.NormalizationStream.body_eq_blocks line 32
  4. theorem OAI.BinPackingCompleteness.NormalizationStream.encoded_normalize line 37
  5. theorem OAI.BinPackingCompleteness.NormalizationStream.blocks_length_le line 43
  6. def OAI.BinPackingCompleteness.NormalizationLoopMachine.nameSum line 91
  7. def OAI.BinPackingCompleteness.NormalizationLoopMachine.bodySteps line 94
  8. def OAI.BinPackingCompleteness.NormalizationLoopMachine.steps line 99
  9. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.bodySteps_le line 103
  10. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.steps_le line 117
  11. abbrev OAI.BinPackingCompleteness.NormalizationLoopMachine.Alphabet line 134
  12. abbrev OAI.BinPackingCompleteness.NormalizationLoopMachine.State line 135
  13. abbrev OAI.BinPackingCompleteness.NormalizationLoopMachine.clean line 136
  14. def OAI.BinPackingCompleteness.NormalizationLoopMachine.reset line 137
  15. def OAI.BinPackingCompleteness.NormalizationLoopMachine.readerIndex line 139
  16. def OAI.BinPackingCompleteness.NormalizationLoopMachine.emitterIndex line 145
  17. def OAI.BinPackingCompleteness.NormalizationLoopMachine.oldIndex line 153
  18. def OAI.BinPackingCompleteness.NormalizationLoopMachine.readerTapes line 155
  19. def OAI.BinPackingCompleteness.NormalizationLoopMachine.emitterTapes line 156
  20. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.readerTapes_injective line 159
  21. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.emitterTapes_injective line 164
  22. inductive OAI.BinPackingCompleteness.NormalizationLoopMachine.Label line 168
  23. def OAI.BinPackingCompleteness.NormalizationLoopMachine.afterDrain line 176
  24. def OAI.BinPackingCompleteness.NormalizationLoopMachine.finish line 179
  25. def OAI.BinPackingCompleteness.NormalizationLoopMachine.instruction line 185
  26. def OAI.BinPackingCompleteness.NormalizationLoopMachine.loopTapes line 202
  27. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.loopTapes_input line 208
  28. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.loopTapes_fresh line 215
  29. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.loopTapes_remaining line 223
  30. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.loopTapes_count line 231
  31. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.loopTapes_output line 239
  32. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.update_remaining line 244
  33. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.update_fresh line 256
  34. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.update_count line 268
  35. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.stepAux_finish line 280
  36. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.joinTrace line 284
  37. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.guardStep line 296
  38. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.emptyStep line 308
  39. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.tallyStep line 318
  40. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.bodyTrace line 336
  41. theorem OAI.BinPackingCompleteness.NormalizationLoopMachine.loopTrace line 481
  42. def OAI.BinPackingCompleteness.NormalizationLoopMachine.loopInTime line 516