OAI/Computability/MinUncut/Machines/PoweringMachineRelation.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelation.Alphabet line 15
  2. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelation.address line 17
  3. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelation.value line 20
  4. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelation.selected line 24
  5. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelation.instruction line 36
  6. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelation.relationTrace line 42
  7. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelation.steps_le line 62
  8. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelation.value_eq_accepts line 72
  9. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelation.machine line 77
  10. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.Alphabet line 91
  11. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.State line 92
  12. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.Label line 93
  13. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.lookupTapes line 95
  14. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.lookupTapes_injective line 99
  15. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.source_outside_lookup line 105
  16. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.endpoint line 115
  17. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.endpoint_eq_wordEnd line 118
  18. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.bit line 125
  19. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.instruction line 129
  20. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.afterWord line 138
  21. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes line 144
  22. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.steps line 152
  23. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.afterWord_frame line 158
  24. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes_frame line 173
  25. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes_other line 190
  26. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.fieldTrace line 203
  27. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRelationField.steps_le line 260
  28. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.Alphabet line 281
  29. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.Tape line 282
  30. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.State line 283
  31. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.Label line 284
  32. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.entry line 287
  33. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.instruction line 289
  34. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.endpoint line 305
  35. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.resultBit line 309
  36. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes line 313
  37. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes line 319
  38. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.steps line 329
  39. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.steps_le line 336
  40. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_other line 352
  41. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_role line 372
  42. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_other line 393
  43. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_role line 408
  44. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_output line 419
  45. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.joinTrace line 432
  46. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.fieldTrace line 436
  47. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.fieldInTime line 538
  48. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineEqualityField.machine line 561