OAI/Computability/BinPacking/PCP/RawInitialMachineFinish.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.tapes line 9
2. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.finishTapes line 17
3. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.trace_trans line 20
4. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.trueRelationWords line 24
5. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.dummyBits_length line 31
6. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.update_reversed line 39
7. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.cleanupTrace line 45
8. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.resetReverseTrace line 94
9. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.update_finish line 125
10. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.copyFinishTrace line 129
11. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.closeDummyTailTrace line 145
12. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.closeDummyReverseTrace line 154
13. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.dummyRelationTrace line 163
14. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.dummyTrace line 174
15. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.finishTrace line 211
16. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineFinish.finishInTime line 229