OAI/Combinatorics/IndependentSets/Expansion/PoweringFieldPlan.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.tailPorts line 13
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.tailPorts_length line 17
3. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.walkEnd_tailPorts line 27
4. def OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.headPorts line 38
5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.walkEnd_headPorts line 41
6. def OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.addressPorts line 49
7. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.walkEnd_addressPorts line 52
8. inductive OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.Instruction line 57
9. def OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.Instruction.radius line 61
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.addressPorts_length_le line 65
11. def OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.evaluate line 70
12. def OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.fieldPlan line 78
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.evaluate_fieldPlan line 84
14. def OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.directedFieldPlan line 104
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.fieldPlan_radius line 108
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.directedFieldPlan_radius line 123
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.evaluate_directedFieldPlan line 128
18. def OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.rowPlan line 135
19. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.evaluate_rowPlan line 141
20. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFieldPlan.dataTape_eq_plan line 152