OAI/Computability/BinPacking/PCP/PoweringFieldPlan.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.firstMatch_of_first line 16
2. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.firstMatch_firstIndex line 26
3. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.endpointMask line 35
4. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.firstMatch_endpointMask line 39
5. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.slotCount line 49
6. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringRowData.RowBuffer line 51
7. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.fixedLabelAt line 53
8. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.fixedLabelAt_addressIndex line 57
9. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.walkData line 65
10. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.walkBits line 75
11. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.basePredicate_walkBits line 79
12. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.leftMatches_walkBits line 86
13. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rightMatches_walkBits line 93
14. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.firstMatch_walkBits_left line 101
15. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.firstMatch_walkBits_right line 111
16. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.edgeAccept_walkBits line 122
17. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rowAccept_walkBits line 135
18. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.transposeField line 146
19. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.transposeBits line 151
20. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.basePredicate_transposeBits line 154
21. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.leftMatches_transposeBits line 159
22. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rightMatches_transposeBits line 165
23. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.edgeAccept_transposeBits line 171
24. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rowAccept_transposeBits line 180
25. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rowBits line 187
26. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rowData line 191
27. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rowBits_packData line 196
28. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rowBits_field line 203
29. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rowAccept_rowBits line 210
30. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rowBlock_at_rowBits line 220
31. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.dataWords line 228
32. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.dataTape line 232
33. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.dataTape_eq line 236
34. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.dataWords_length line 241
35. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.dataTape_length_le line 247
36. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.emittedRelation line 253
37. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.emittedRelation_eq line 258
38. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rowBlock_unary line 266
39. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.emittedRelation_table line 278
40. theorem OAI.BinPackingGames.Foundations.PCP.PoweringRowData.rowBlock_unary_table line 305
41. def OAI.BinPackingGames.Foundations.PCP.PoweringRowData.tableRowMachineInTime line 312
42. def OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.tailPorts line 338
43. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.tailPorts_length line 342
44. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.walkEnd_tailPorts line 352
45. def OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.headPorts line 363
46. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.walkEnd_headPorts line 366
47. def OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.addressPorts line 374
48. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.walkEnd_addressPorts line 377
49. inductive OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.Instruction line 382
50. def OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.Instruction.radius line 386
51. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.addressPorts_length_le line 390
52. def OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.evaluate line 395
53. def OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.fieldPlan line 403
54. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.evaluate_fieldPlan line 409
55. def OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.directedFieldPlan line 429
56. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.fieldPlan_radius line 433
57. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.directedFieldPlan_radius line 448
58. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.evaluate_directedFieldPlan line 453
59. def OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.rowPlan line 460
60. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.evaluate_rowPlan line 466
61. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFieldPlan.dataTape_eq_plan line 477