OAI/Computability/DirectedFeedback/Machines/RawInitialMachineFinish.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBody.trace_trans_inline_RawInitialMachineBody line 56
2. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBody.guardTrace_succ line 60
3. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBody.guardTrace_zero line 75
4. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBody.bodyTrace line 89
5. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.tapes_inline_RawInitialMachineFinish line 146
6. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.finishTapes line 154
7. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.trace_trans_inline_RawInitialMachineFinish line 157
8. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.trueRelationWords line 161
9. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.dummyBits_length line 168
10. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.update_reversed_inline_RawInitialMachineFinish line 176
11. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.cleanupTrace_inline_RawInitialMachineFinish line 182
12. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.resetReverseTrace_inline_RawInitialMachineFinish line 231
13. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.update_finish_inline_RawInitialMachineFinish line 262
14. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.copyFinishTrace_inline_RawInitialMachineFinish line 266
15. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.closeDummyTailTrace_inline_RawInitialMachineFinish line 282
16. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.closeDummyReverseTrace_inline_RawInitialMachineFinish line 291
17. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.dummyRelationTrace_inline_RawInitialMachineFinish line 300
18. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.dummyTrace line 311
19. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.finishTrace line 348
20. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineFinish.finishInTime line 366
21. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoop.finalSigns line 390
22. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoop.trace_trans_inline_RawInitialMachineLoop line 395
23. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoop.empty_loopTapes line 399
24. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoop.loopTrace line 404
25. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoop.loopInTime line 428
26. theorem OAI.DFVSGames.Foundations.PCP.MachineRawInitialTable.trace_trans_inline_MachineRawInitialTable line 449
27. def OAI.DFVSGames.Foundations.PCP.MachineRawInitialTable.prefixBits line 453
28. theorem OAI.DFVSGames.Foundations.PCP.MachineRawInitialTable.outputBits line 457
29. theorem OAI.DFVSGames.Foundations.PCP.MachineRawInitialTable.machineTrace line 464
30. def OAI.DFVSGames.Foundations.PCP.MachineRawInitialTable.outputsInTime line 490
31. def OAI.DFVSGames.Foundations.PCP.MachineRawInitialTable.computableInPolyTime line 498
32. abbrev OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Buffer line 526
33. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.readUnarySlots line 532
34. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.unaryBits line 543
35. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.unaryBits_eq_encodeWords line 546
36. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.unaryBits_length_le line 553
37. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.statementPushBound_readUnarySlots line 563
38. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.stepAux_readUnarySlots line 574
39. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.stepAux_readUnaryAll line 598
40. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.unaryBlockMapAt line 611
41. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.stepAux_unaryBlockMapAt line 619
42. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.step_unaryBlockMapAt line 634
43. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.unaryBlockInTime line 647
44. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.unaryBits_relation line 664
45. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.readerStateEquiv line 675
46. abbrev OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.State line 686
47. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.readRelationAt line 688
48. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.stepAux_readRelationAt line 693
49. inductive OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.Tape line 714
50. instance OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.(instance at line 719) line 719
51. abbrev OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient line 721
52. abbrev OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.Plan line 722
53. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.values line 724
54. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan line 727
55. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_length line 731
56. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_bits line 734
57. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.source line 742
58. inductive OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.Label line 745
59. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.guard line 757
60. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.program line 764
61. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.machine line 811
62. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles line 822
63. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_injective line 826
64. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headPhaseInTime line 829
65. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.workingTapes line 845
66. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.workingTapes_operands line 858
67. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_input line 865
68. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_tail line 872
69. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_head line 879
70. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_accumulator line 886
71. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_rowIndex line 893
72. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.source_ne_scratch line 901
73. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.source_ne_accumulator line 904