OAI/Combinatorics/IndependentSets/Machines/PoweringMachineRelationField.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.Alphabet line 16
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.State line 17
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.Label line 18
  4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.lookupTapes line 20
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.lookupTapes_injective line 24
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.source_outside_lookup line 30
  7. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.endpoint line 40
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.endpoint_eq_wordEnd line 43
  9. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.bit line 50
  10. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.instruction line 54
  11. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.afterWord line 63
  12. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes line 69
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.steps line 77
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.afterWord_frame line 83
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes_frame line 98
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes_other line 115
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.fieldTrace line 128
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelationField.steps_le line 185