OAI/Computability/VertexCover/PCP/PoweringWalks.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniqueGames.Foundations.PCP.PoweringWalks.PortGraph line 9
  2. abbrev OAI.UniqueGames.Foundations.PCP.PoweringWalks.Edge line 13
  3. abbrev OAI.UniqueGames.Foundations.PCP.PoweringWalks.Walk line 14
  4. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.next line 18
  5. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.rot_rot line 20
  6. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.walkEnd line 23
  7. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.walkEnd_nil line 27
  8. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.walkEnd_cons line 29
  9. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.walkEnd_append line 32
  10. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.splitHead line 38
  11. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.rotateHead line 49
  12. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.rotateHead_vertex line 53
  13. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.rotateHead_zero line 56
  14. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.rotateHead_succ line 59
  15. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.permutePorts line 63
  16. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.wordEnd line 77
  17. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.endpoint line 81
  18. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.natCard_walk line 84
  19. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.headTailEquiv line 88
  20. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.advanceTail line 99
  21. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.edgeAt line 102
  22. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.pivotEquiv line 108
  23. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.pivotEquiv_fst line 118
  24. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.edgeAt_port line 132
  25. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.pivotEquiv_zero_apply line 148
  26. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.pivotEquiv_succ_apply line 152
  27. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.projectedFiberEquiv line 159
  28. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.projectedEventEquiv line 171
  29. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_fiber line 189
  30. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_event line 198
  31. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.leftFromPivot line 208
  32. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.rightFromPivot line 214
  33. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.leftFromPivot_zero line 221
  34. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.rightFromPivot_zero line 225
  35. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.leftFromPivot_actual line 230
  36. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.rightFromPivot_actual line 249