OAI/Combinatorics/IndependentSets/Machines/Machine.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.Alphabet line 15
  2. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldLoop line 17
  3. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldStart line 25
  4. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldTapes line 29
  5. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldTapes_source line 33
  6. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldTapes_destination line 38
  7. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldTapes_self line 43
  8. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldTapes_other line 47
  9. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.update_field_source line 53
  10. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.update_field_destination line 64
  11. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldStep_delimiter line 70
  12. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldStep_true line 84
  13. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldLoopTrace line 98
  14. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldStartStep line 130
  15. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldInTime line 144
  16. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.afterField line 174
  17. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldNext line 178
  18. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fourTapes line 185
  19. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fourTapes_source line 192
  20. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fourTapes_other line 198
  21. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fourField_time_eq_length line 204
  22. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fourFieldsInTime line 209
  23. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fieldDestination line 253
  24. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.fourTapes_concrete line 255
  25. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.groupingProgram line 267
  26. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.groupingMachine line 274
  27. def OAI.IndependentSetsGames.Foundations.Hastad.SourceMachine.groupingMachineInTime line 285