OAI/Computability/BinPacking/PCP/Emitter.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.Command line 11
2. inductive OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.Phase line 18
3. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet line 23
4. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.State line 24
5. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.transition line 26
6. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.payload line 27
7. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.commandBits line 30
8. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.commandSteps line 39
9. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.commandStatement line 48
10. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.output_encodeWord line 82
11. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.commandTrace line 96
12. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.Label line 173
13. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.labelAt line 175
14. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.commandAt line 178
15. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.statement line 182
16. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.program line 192
17. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.machine line 197
18. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.prefixBits line 210
19. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.prefixSteps line 216
20. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes line 221
21. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes_output line 224
22. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes_other line 228
23. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.prefixTrace line 232
24. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.planTrace line 271
25. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.prefixSteps_le line 292
26. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.planInTime line 311
27. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.listCommands line 332
28. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.prefixBits_listCommands line 335
29. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.bits_listCommands line 347
30. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands line 353
31. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.affineValue line 357
32. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.scaleBits line 360
33. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands_bits line 370
34. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands_length line 378
35. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.bitCommands line 382
36. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.bitCommands_bits line 384
37. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.affineInTime line 393
38. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.Command.mapAmbient line 417
39. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.commandBits_mapAmbient line 425
40. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Emitter.commandSteps_mapAmbient line 431