OAI/Computability/BinPacking/Computation/MachineUnaryEqualityBit.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCompare.Alphabet line 12
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCompare.State line 13
3. def OAI.BinPackingGames.Foundations.Complexity.MachineCompare.exitAt line 15
4. def OAI.BinPackingGames.Foundations.Complexity.MachineCompare.finish line 20
5. def OAI.BinPackingGames.Foundations.Complexity.MachineCompare.loop line 23
6. def OAI.BinPackingGames.Foundations.Complexity.MachineCompare.mismatch line 33
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.mismatch_nil_nil line 36
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.mismatch_nil_cons line 39
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.mismatch_cons_nil line 42
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.mismatch_true line 45
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.mismatch_cons line 48
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.stepAux_exitAt line 53
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.stepAux_finish line 58
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.update_left line 64
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.update_right line 77
16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.step_empty line 83
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.step_nil_cons line 100
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.step_cons_nil line 115
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.step_cons_cons line 130
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.trace_left_empty line 147
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.compareTrace_flag line 172
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.compareTrace line 207
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.compareTrace_fromTapes line 222
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.drained_other line 235
25. def OAI.BinPackingGames.Foundations.Complexity.MachineCompare.compareInTime line 239
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCompare.compareInTime_steps line 254
27. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.Profile line 269
28. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.equalityProfile line 271
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.equalityProfile_encodeWord line 274
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.statement_roundtrip line 289
31. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.copyStateEquiv line 294
32. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.normalState line 301
33. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.copyStatement line 303
34. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.copyInCompareState line 308
35. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.nonDestructiveCompareInTime line 355
36. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.setEntry line 412
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.setEntry_apply line 415
38. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.setExpected line 421
39. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.foldProfile line 425
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.foldProfile_apply line 428
41. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.Tape line 444
42. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.Label line 445
43. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.labelAt line 447
44. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.storePair line 450
45. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.profileProgram line 455
46. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.pairTime line 475
47. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.prefixProfile line 479
48. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.prefixTime line 483
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.prefixProfile_succ line 487
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.prefixTime_succ line 495
51. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.stageInTime line 502
52. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.prefixInTime line 547
53. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.allPairs line 567
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.mem_allPairs line 570
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.length_allPairs line 573
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.foldProfile_allPairs line 576
57. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.profileMachine line 581
58. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.profileInTime line 592
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.pairTime_le line 618
60. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.totalTime_le line 627
61. def OAI.BinPackingGames.Foundations.Complexity.MachineFieldProfile.profileInTime_bounded line 637
62. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet line 659
63. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.State line 660
64. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.clean line 662
65. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.compareStateEquiv line 664
66. inductive OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.Label line 670
67. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList line 676
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList_getElem?_ctorIdx_eq line 679
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.Label.enumList_nodup line 683
70. instance OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.(instance at line 685) line 685
71. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.exitAt line 689
72. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.bitEncoding line 694
73. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.emit line 696
74. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.instruction line 701
75. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.copySteps line 719
76. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.compareSteps line 720
77. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.steps line 721
78. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.steps_le line 723
79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.encodeWord_eq_iff line 727
80. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.emit_step line 736
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.joinTrace line 748
82. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityTrace line 752
83. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityInTime line 854
84. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.machine line 873
85. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryEqualityBit.machineInTime line 884