OAI/Combinatorics/IndependentSets/Machines/MachineRegularOriginalRow.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedIndex line 15
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow line 20
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_eq line 25
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_tail line 33
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_reverse line 38
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_relation line 51
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_words line 64
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.prefixWords line 71
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.suffixWords line 74
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.prefixWords_length line 77
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.tableWords_at_row line 82
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.tableWords_drop_row line 94
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.selected_reverse line 100
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.remaining_relation line 107
  15. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.Tape line 114
  16. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.Buffer line 115
  17. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.State line 116
  18. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.Alphabet line 117
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer line 119
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTape line 121
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTape_injective line 123
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.source_outside line 130
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.fields line 136
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.fields_zero line 138
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.fields_one line 139
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.fields_two line 140
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.fields_separate line 142
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.copyStateEquiv line 145
  29. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.Label line 151
  30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopyAt line 157
  31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.instruction line 162
  32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.machine line 174
  33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.looked line 185
  34. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.copied line 189
  35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.affined line 194
  36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.looked_other line 199
  37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.looked_reverse line 204
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.looked_relation line 208
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.vectorBits_eq_encodedBlock line 218
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.relationBits_eq_encodedBlock line 230
  41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_step line 234
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_pushBound line 263
  43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.copied_other line 268
  44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.copied_reverse line 274
  45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.copied_relation line 279
  46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.affined_other line 283
  47. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.affined_reverse line 288
  48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.affined_relation line 292
  49. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.Input line 296
  50. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.emittedWords line 305
  51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.affined_fields line 308
  52. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.rowSteps line 318
  53. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.steps line 321
  54. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalRow.finalTapes line 325