OAI/Computability/MinUncut/Machines/RawInitialMachineFinish.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.tapes line 12
2. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.finishTapes line 20
3. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.trace_trans line 23
4. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.trueRelationWords line 27
5. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.dummyBits_length line 34
6. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.update_reversed line 42
7. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.cleanupTrace line 48
8. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.resetReverseTrace line 97
9. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.update_finish line 128
10. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.copyFinishTrace line 132
11. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.closeDummyTailTrace line 148
12. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.closeDummyReverseTrace line 157
13. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.dummyRelationTrace line 166
14. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.dummyTrace line 177
15. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.finishTrace line 214
16. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineFinish.finishInTime line 232
17. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoop.finalSigns line 255
18. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoop.trace_trans line 260
19. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoop.empty_loopTapes line 264
20. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoop.loopTrace line 269
21. def OAI.MinUncutGames.Foundations.PCP.RawInitialMachineLoop.loopInTime line 293
22. theorem OAI.MinUncutGames.Foundations.PCP.MachineRawInitialTable.trace_trans line 313
23. def OAI.MinUncutGames.Foundations.PCP.MachineRawInitialTable.prefixBits line 317
24. theorem OAI.MinUncutGames.Foundations.PCP.MachineRawInitialTable.outputBits line 321
25. theorem OAI.MinUncutGames.Foundations.PCP.MachineRawInitialTable.machineTrace line 328
26. def OAI.MinUncutGames.Foundations.PCP.MachineRawInitialTable.outputsInTime line 354
27. def OAI.MinUncutGames.Foundations.PCP.MachineRawInitialTable.computableInPolyTime line 362
28. abbrev OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Buffer line 388
29. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.readUnarySlots line 394
30. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.unaryBits line 405
31. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.unaryBits_eq_encodeWords line 408
32. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.unaryBits_length_le line 415
33. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.statementPushBound_readUnarySlots line 425
34. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.stepAux_readUnarySlots line 436
35. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.stepAux_readUnaryAll line 460
36. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.unaryBlockMapAt line 473
37. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.stepAux_unaryBlockMapAt line 481
38. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.step_unaryBlockMapAt line 496
39. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.unaryBlockInTime line 509
40. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.unaryBits_relation line 526
41. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.readerStateEquiv line 537
42. abbrev OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.State line 548
43. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.readRelationAt line 550
44. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.stepAux_readRelationAt line 555
45. inductive OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape line 576
46. abbrev OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList line 581
47. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList_getElem?_ctorIdx_eq line 584
48. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList_nodup line 588
49. instance OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.(instance at line 590) line 590
50. abbrev OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient line 594
51. abbrev OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan line 595
52. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.values line 597
53. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan line 600
54. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_length line 604
55. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_bits line 607
56. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.source line 615
57. inductive OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.Label line 618
58. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.guard line 630
59. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.program line 637
60. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.machine line 684
61. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles line 695
62. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_injective line 699
63. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headPhaseInTime line 702
64. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.workingTapes line 718
65. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.workingTapes_operands line 731
66. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_input line 738
67. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_tail line 745
68. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_head line 752
69. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_accumulator line 759
70. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_rowIndex line 766
71. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.source_ne_scratch line 774
72. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.source_ne_accumulator line 777