OAI/Computability/MinUncut/Machines/MachineFixedDivMod.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.Alphabet line 14
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.State line 15
3. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.residue line 17
4. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.nextResidue line 20
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.nextResidue_residue line 23
6. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.scanLoop line 29
7. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.emitter line 42
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.scanPushBound line 49
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.emitterPushBound line 55
10. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.tapes line 62
11. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes line 66
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_source line 71
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_quotient line 79
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_remainder line 86
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_other line 93
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.update_source line 101
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.update_quotient line 119
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.update_remainder line 133
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.scanAux_true line 139
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.scanAux_false line 155
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.scanStep_succ line 168
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.scanStep_zero line 195
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.emitterStep line 218
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.trace_fromCount line 242
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.divModTrace line 279
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.divModFromTapes line 300
27. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.divModInTime line 327
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.scanTrace_fromCount line 351
29. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinish line 384
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishPushBound line 392
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishStep line 400
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.divModTraceWithFinish line 426
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedDivMod.divModFromTapesWithFinish line 454
34. inductive OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.Tape line 491
35. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.Tape.enumList line 498
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.Tape.enumList_getElem?_ctorIdx_eq line 502
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.Tape.enumList_nodup line 506
38. instance OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.(instance at line 508) line 508
39. inductive OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.Label line 512
40. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.Ambient line 530
41. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.State line 531
42. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.divisionStates line 534
43. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.firstFinish line 541
44. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.secondFinish line 545
45. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.affinePlan line 549
46. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.firstPlan line 554
47. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.secondPlan line 558
48. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.outputPlan line 562
49. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupTape line 566
50. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape line 573
51. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.statement line 583
52. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.program line 648
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.controlStatement_inverse line 655
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.transportedDivision line 662
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.divisionStates_apply line 721
56. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.divisionState line 725
57. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.divisionOutput line 730
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.firstDivisionTrace line 736
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.secondDivisionTrace line 777
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_source line 821
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_quotient line 833
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_remainder line 842
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_other line 849
64. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.firstDivisionInTime line 859
65. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.secondDivisionInTime line 883