OAI/Combinatorics/IndependentSets/Machines/MachineFixedDivMod.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.Alphabet line 14
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.State line 15
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.residue line 17
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.nextResidue line 20
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.nextResidue_residue line 23
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.scanLoop line 29
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.emitter line 42
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.scanPushBound line 49
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.emitterPushBound line 55
  10. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.tapes line 62
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes line 66
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_source line 71
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_quotient line 79
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_remainder line 86
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_other line 93
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.update_source line 101
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.update_quotient line 119
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.update_remainder line 133
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.scanAux_true line 139
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.scanAux_false line 155
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.scanStep_succ line 168
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.scanStep_zero line 195
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.emitterStep line 218
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.trace_fromCount line 242
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.divModTrace line 279
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.divModFromTapes line 300
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.divModInTime line 327
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.scanTrace_fromCount line 351
  29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinish line 384
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishPushBound line 392
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishStep line 400
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.divModTraceWithFinish line 426
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedDivMod.divModFromTapesWithFinish line 454