OAI/Computability/PerfectCompleteness/Machines/KeyMetadataMachine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.KeyMetadataMachine.actualSlot line 22
  2. def OAI.PerfectCompleteness.KeyMetadataMachine.fieldValue line 27
  3. def OAI.PerfectCompleteness.KeyMetadataMachine.sourceField line 30
  4. def OAI.PerfectCompleteness.KeyMetadataMachine.prefixWords line 36
  5. def OAI.PerfectCompleteness.KeyMetadataMachine.suffixWords line 39
  6. def OAI.PerfectCompleteness.KeyMetadataMachine.retainedWords line 45
  7. def OAI.PerfectCompleteness.KeyMetadataMachine.retainedBits line 49
  8. theorem OAI.PerfectCompleteness.KeyMetadataMachine.retainedWords_eq line 52
  9. abbrev OAI.PerfectCompleteness.KeyMetadataMachine.Alphabet line 66
  10. abbrev OAI.PerfectCompleteness.KeyMetadataMachine.State line 67
  11. def OAI.PerfectCompleteness.KeyMetadataMachine.clean line 69
  12. inductive OAI.PerfectCompleteness.KeyMetadataMachine.Label line 71
  13. abbrev OAI.PerfectCompleteness.KeyMetadataMachine.Label.enumList line 78
  14. theorem OAI.PerfectCompleteness.KeyMetadataMachine.Label.enumList_getElem?_ctorIdx_eq line 80
  15. theorem OAI.PerfectCompleteness.KeyMetadataMachine.Label.enumList_nodup line 84
  16. instance OAI.PerfectCompleteness.KeyMetadataMachine.(instance at line 86) line 86
  17. def OAI.PerfectCompleteness.KeyMetadataMachine.idIndex line 90
  18. def OAI.PerfectCompleteness.KeyMetadataMachine.idTape line 92
  19. def OAI.PerfectCompleteness.KeyMetadataMachine.finish line 94
  20. theorem OAI.PerfectCompleteness.KeyMetadataMachine.stepAux_finish line 98
  21. theorem OAI.PerfectCompleteness.KeyMetadataMachine.finish_pushBound line 104
  22. def OAI.PerfectCompleteness.KeyMetadataMachine.literal line 108
  23. theorem OAI.PerfectCompleteness.KeyMetadataMachine.literal_pushBound line 113
  24. theorem OAI.PerfectCompleteness.KeyMetadataMachine.literal_step line 118
  25. def OAI.PerfectCompleteness.KeyMetadataMachine.instruction line 131
  26. theorem OAI.PerfectCompleteness.KeyMetadataMachine.instruction_pushBound line 147
  27. theorem OAI.PerfectCompleteness.KeyMetadataMachine.joinTrace line 166
  28. theorem OAI.PerfectCompleteness.KeyMetadataMachine.droppedTrace line 170
  29. theorem OAI.PerfectCompleteness.KeyMetadataMachine.selectedTrace line 184
  30. def OAI.PerfectCompleteness.KeyMetadataMachine.sourceLength line 274
  31. theorem OAI.PerfectCompleteness.KeyMetadataMachine.selected_length_le line 278
  32. def OAI.PerfectCompleteness.KeyMetadataMachine.metadataInTime line 285
  33. theorem OAI.PerfectCompleteness.KeyMetadataMachine.output_frame line 336
  34. theorem OAI.PerfectCompleteness.KeyMetadataMachine.label_finite line 341
  35. theorem OAI.PerfectCompleteness.KeyMetadataMachine.state_finite line 343