OAI/Computability/PerfectCompleteness/Machines/BinaryRenameLoop.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.BinaryRenameLoop.Token line 13
  2. def OAI.PerfectCompleteness.BinaryRenameLoop.nextSlot line 15
  3. def OAI.PerfectCompleteness.BinaryRenameLoop.clauseIncrement line 17
  4. def OAI.PerfectCompleteness.BinaryRenameLoop.finalSlot line 19
  5. def OAI.PerfectCompleteness.BinaryRenameLoop.completedClauses line 23
  6. theorem OAI.PerfectCompleteness.BinaryRenameLoop.finalSlot_three line 27
  7. theorem OAI.PerfectCompleteness.BinaryRenameLoop.completedClauses_three line 30
  8. theorem OAI.PerfectCompleteness.BinaryRenameLoop.finalSlot_triples line 34
  9. theorem OAI.PerfectCompleteness.BinaryRenameLoop.completedClauses_triples line 39
  10. def OAI.PerfectCompleteness.BinaryRenameLoop.outputBody line 44
  11. theorem OAI.PerfectCompleteness.BinaryRenameLoop.outputBody_nil line 47
  12. theorem OAI.PerfectCompleteness.BinaryRenameLoop.outputBody_cons line 49
  13. def OAI.PerfectCompleteness.BinaryRenameLoop.steps line 53
  14. theorem OAI.PerfectCompleteness.BinaryRenameLoop.payload_length_le_stream line 57
  15. def OAI.PerfectCompleteness.BinaryRenameLoop.perLiteralBound line 72
  16. theorem OAI.PerfectCompleteness.BinaryRenameLoop.literal_steps_le line 75
  17. theorem OAI.PerfectCompleteness.BinaryRenameLoop.steps_le line 87
  18. theorem OAI.PerfectCompleteness.BinaryRenameLoop.steps_le_cubic line 100
  19. abbrev OAI.PerfectCompleteness.BinaryRenameLoop.Alphabet line 120
  20. abbrev OAI.PerfectCompleteness.BinaryRenameLoop.State line 121
  21. abbrev OAI.PerfectCompleteness.BinaryRenameLoop.clean line 122
  22. inductive OAI.PerfectCompleteness.BinaryRenameLoop.Label line 125
  23. def OAI.PerfectCompleteness.BinaryRenameLoop.literalTapes line 131
  24. theorem OAI.PerfectCompleteness.BinaryRenameLoop.literalTapes_injective line 134
  25. def OAI.PerfectCompleteness.BinaryRenameLoop.finish line 140
  26. def OAI.PerfectCompleteness.BinaryRenameLoop.next line 146
  27. def OAI.PerfectCompleteness.BinaryRenameLoop.instruction line 150
  28. def OAI.PerfectCompleteness.BinaryRenameLoop.loopTapes line 166
  29. theorem OAI.PerfectCompleteness.BinaryRenameLoop.loopTapes_cursor line 171
  30. theorem OAI.PerfectCompleteness.BinaryRenameLoop.loopTapes_output line 177
  31. theorem OAI.PerfectCompleteness.BinaryRenameLoop.loopTapes_variables line 183
  32. theorem OAI.PerfectCompleteness.BinaryRenameLoop.loopTapes_clauses line 189
  33. theorem OAI.PerfectCompleteness.BinaryRenameLoop.update_cursor line 194
  34. theorem OAI.PerfectCompleteness.BinaryRenameLoop.update_output line 204
  35. theorem OAI.PerfectCompleteness.BinaryRenameLoop.update_variables line 214
  36. theorem OAI.PerfectCompleteness.BinaryRenameLoop.update_clauses line 224
  37. theorem OAI.PerfectCompleteness.BinaryRenameLoop.loopTapes_other line 230
  38. theorem OAI.PerfectCompleteness.BinaryRenameLoop.stepAux_finish line 236
  39. theorem OAI.PerfectCompleteness.BinaryRenameLoop.joinTrace line 241
  40. theorem OAI.PerfectCompleteness.BinaryRenameLoop.peekStep line 253
  41. theorem OAI.PerfectCompleteness.BinaryRenameLoop.emptyStep line 265
  42. theorem OAI.PerfectCompleteness.BinaryRenameLoop.tallyStep line 276
  43. theorem OAI.PerfectCompleteness.BinaryRenameLoop.bodyTrace line 291
  44. theorem OAI.PerfectCompleteness.BinaryRenameLoop.loopTrace line 363
  45. theorem OAI.PerfectCompleteness.BinaryRenameLoop.triplesTrace line 407
  46. def OAI.PerfectCompleteness.BinaryRenameLoop.triplesInTime line 424