OAI/Computability/MinUncut/Machines/Machine.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceMachine.Alphabet line 14
  2. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldLoop line 16
  3. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldStart line 24
  4. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldTapes line 28
  5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldTapes_source line 32
  6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldTapes_destination line 37
  7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldTapes_self line 42
  8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldTapes_other line 46
  9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.update_field_source line 52
  10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.update_field_destination line 63
  11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldStep_delimiter line 69
  12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldStep_true line 83
  13. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldLoopTrace line 97
  14. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldStartStep line 129
  15. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldInTime line 143
  16. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.afterField line 173
  17. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldNext line 177
  18. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fourTapes line 184
  19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fourTapes_source line 191
  20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fourTapes_other line 197
  21. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fourField_time_eq_length line 203
  22. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fourFieldsInTime line 208
  23. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fieldDestination line 252
  24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceMachine.fourTapes_concrete line 254
  25. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.groupingProgram line 266
  26. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.groupingMachine line 273
  27. def OAI.MinUncutGames.Foundations.Hastad.SourceMachine.groupingMachineInTime line 284