OAI/Combinatorics/IndependentSets/Machines/MachineCompare.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.Alphabet line 15
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.State line 16
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.exitAt line 18
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.finish line 23
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.loop line 26
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.mismatch line 36
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.mismatch_nil_nil line 39
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.mismatch_nil_cons line 42
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.mismatch_cons_nil line 45
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.mismatch_true line 48
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.mismatch_cons line 51
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.stepAux_exitAt line 56
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.stepAux_finish line 61
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.update_left line 67
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.update_right line 80
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.step_empty line 86
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.step_nil_cons line 103
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.step_cons_nil line 118
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.step_cons_cons line 133
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.trace_left_empty line 150
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.compareTrace_flag line 175
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.compareTrace line 210
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.compareTrace_fromTapes line 225
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.drained_other line 238
  25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.compareInTime line 242
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCompare.compareInTime_steps line 257