OAI/Computability/MinUncut/PCP/ProfileBridge.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Hastad.SourceProfileBridge.positionEncoding line 13
2. def OAI.MinUncutGames.Foundations.Hastad.SourceProfileBridge.names line 16
3. def OAI.MinUncutGames.Foundations.Hastad.SourceProfileBridge.nameWords line 20
4. def OAI.MinUncutGames.Foundations.Hastad.SourceProfileBridge.reindexProfile line 24
5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceProfileBridge.computed_profile_eq line 28
6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceProfileBridge.prepared_signature_eq line 36
7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceProfileBridge.nameWords_length_le_input line 44
8. def OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.positions line 60
9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.mem_positions line 63
10. def OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.fillSigns line 66
11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.fillSigns_apply line 70
12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.fillSigns_positions line 84
13. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.State line 92
14. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.Alphabet line 93
15. def OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.finish line 95
16. def OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.peekChain line 100
17. def OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.statement line 108
18. def OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.readSigns line 112
19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.stepAux_peekChain line 115
20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.stepAux_statement line 128
21. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.peekChain_pushBound line 135
22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.statement_pushBound line 143
23. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.readSigns_of_unary line 148
24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.loadStep line 156
25. def OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.loadInTime line 167
26. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.loaded_ofContext line 185
27. def OAI.MinUncutGames.Foundations.Hastad.SourceSignLoad.loadContextInTime line 197
28. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.Width line 223
29. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.Arena line 224
30. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.ProfileState line 225
31. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.State line 226
32. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.ProfileLabel line 227
33. inductive OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.Label line 229
34. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.variableField line 236
35. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.polarityField line 239
36. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.place line 242
37. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.unplace line 246
38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.unplace_place line 256
39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.place_injective line 269
40. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.place_unplace line 274
41. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.fill line 306
42. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.fill_place line 312
43. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.fill_self line 317
44. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.fill_frame line 325
45. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.fill_update line 332
46. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.placedLabel line 355
47. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.placedConfiguration line 359
48. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.placedStatement line 365
49. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.placed_stepAux line 380
50. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.signStateEquiv line 407
51. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.commitStatement line 414
52. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.program line 420
53. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.placed_step line 425
54. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.stepAux_commit line 442
55. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.profileInTime line 454
56. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.commitInTime line 474
57. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.prepareInTime line 487
58. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.loaded_name_field line 526
59. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.loaded_sign_field line 544
60. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.loadedPrepareInTime line 557
61. def OAI.MinUncutGames.Foundations.Hastad.SourceSignaturePrepare.machine line 587