OAI/Computability/MinUncut/Machines/MachineCompare.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCompare.Alphabet line 13
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCompare.State line 14
3. def OAI.MinUncutGames.Foundations.Complexity.MachineCompare.exitAt line 16
4. def OAI.MinUncutGames.Foundations.Complexity.MachineCompare.finish line 21
5. def OAI.MinUncutGames.Foundations.Complexity.MachineCompare.loop line 24
6. def OAI.MinUncutGames.Foundations.Complexity.MachineCompare.mismatch line 34
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.mismatch_nil_nil line 37
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.mismatch_nil_cons line 40
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.mismatch_cons_nil line 43
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.mismatch_true line 46
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.mismatch_cons line 49
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.stepAux_exitAt line 54
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.stepAux_finish line 59
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.update_left line 65
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.update_right line 78
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.step_empty line 84
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.step_nil_cons line 101
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.step_cons_nil line 116
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.step_cons_cons line 131
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.trace_left_empty line 148
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.compareTrace_flag line 173
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.compareTrace line 208
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.compareTrace_fromTapes line 223
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.drained_other line 236
25. def OAI.MinUncutGames.Foundations.Complexity.MachineCompare.compareInTime line 240
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCompare.compareInTime_steps line 255
27. def OAI.MinUncutGames.Foundations.Complexity.MachineControl.configuration line 272
28. def OAI.MinUncutGames.Foundations.Complexity.MachineControl.statement line 278
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineControl.stepAux_simulation line 293
30. def OAI.MinUncutGames.Foundations.Complexity.MachineControl.program line 320
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineControl.step_simulation line 323
32. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.Profile line 343
33. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.equalityProfile line 345
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.equalityProfile_encodeWord line 348
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.statement_roundtrip line 363
36. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.copyStateEquiv line 368
37. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.normalState line 375
38. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.copyStatement line 377
39. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.copyInCompareState line 382
40. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.nonDestructiveCompareInTime line 429
41. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.setEntry line 486
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.setEntry_apply line 489
43. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.setExpected line 495
44. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.foldProfile line 499
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.foldProfile_apply line 502
46. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.Tape line 518
47. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.Label line 519
48. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.labelAt line 521
49. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.storePair line 524
50. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.profileProgram line 529
51. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.pairTime line 549
52. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.prefixProfile line 553
53. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.prefixTime line 557
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.prefixProfile_succ line 561
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.prefixTime_succ line 569
56. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.stageInTime line 576
57. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.prefixInTime line 621
58. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.allPairs line 641
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.mem_allPairs line 644
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.length_allPairs line 647
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.foldProfile_allPairs line 650
62. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.profileMachine line 655
63. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.profileInTime line 666
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.pairTime_le line 692
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.totalTime_le line 701
66. def OAI.MinUncutGames.Foundations.Complexity.MachineFieldProfile.profileInTime_bounded line 711