OAI/Computability/MinUncut/Machines/MachinePreservingLookup.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookup.Alphabet line 13
  2. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookup.initialTapes line 15
  3. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookup.finalTapes line 20
  4. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookup.lookupFramedHaltTrace_some line 27
  5. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookup.preservingLookupTrace line 45
  6. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookup.preservingLookup_steps_le line 95
  7. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookup.preservingLookupInTime line 103
  8. inductive OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookup.Label line 125
  9. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookup.program line 129
  10. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookup.machine line 136
  11. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.Alphabet line 156
  12. inductive OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.Label line 158
  13. def OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.instruction line 163
  14. def OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.steps line 178
  15. def OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.finalTapes line 183
  16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.initialTapes_eq_update line 188
  17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.affineLookupTrace line 208
  18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.steps_le line 236
  19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.steps_le_table line 244
  20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.finalTapes_other line 251
  21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.finalTapes_output line 257
  22. def OAI.MinUncutGames.Foundations.Complexity.MachineAffineLookup.machine line 262