OAI/Computability/VertexCover/PCP/PoweringReach.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.PoweringReach.ReachLE line 14
2. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.reach_refl line 17
3. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.reach_mono line 20
4. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.reach_prepend line 25
5. def OAI.UniqueGames.Foundations.PCP.PoweringReach.reversePorts line 32
6. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.reversePorts_length line 36
7. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.walkEnd_reversePorts line 42
8. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.wordEnd_eq_walkEnd_ofFn line 53
9. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.reach_reverse line 63
10. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.tail_reach line 75
11. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.head_reach_endpoint line 89
12. def OAI.UniqueGames.Foundations.PCP.PoweringReach.tailFromStart line 103
13. def OAI.UniqueGames.Foundations.PCP.PoweringReach.headFromEnd line 107
14. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.tailFromStart_val line 111
15. theorem OAI.UniqueGames.Foundations.PCP.PoweringReach.headFromEnd_val line 115