OAI/Computability/MinUncut/PCP/ExpanderRowControl.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.degree line 11
  2. abbrev OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.cloudSize line 12
  3. abbrev OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.rowFactor line 13
  4. structure OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.Control line 15
  5. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.squarePorts line 23
  6. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.start line 26
  7. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.receiveFirst line 37
  8. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.receiveSecond line 40
  9. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.firstOffset line 47
  10. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.secondOffset line 48
  11. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.outputPort line 50
  12. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.outputOffset line 53
  13. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.firstAddress line 56
  14. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.secondAddress line 59
  15. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.outputAddress line 62
  16. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.firstOffset_receiveFirst line 65
  17. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.secondOffset_receiveFirst line 68
  18. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.receiveFirst_port line 71
  19. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.receiveSecond_port line 74
  20. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.firstAddress_eq_rowIndex line 77
  21. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.secondAddress_eq_rowIndex line 83
  22. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.firstAddress_lt line 89
  23. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.secondAddress_lt line 94
  24. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.lookup_vertex_div line 99
  25. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.lookup_port_mod line 102
  26. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.lookup_port_eq_remainder line 105
  27. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.rowIndex_lookup line 109
  28. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.outputPair line 113
  29. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_rowIndex line 117
  30. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.outputAddress_lt line 123
  31. def OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.evaluateRow line 128
  32. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.evaluateRow_eq_lookup_step line 137
  33. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_row line 146
  34. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_reverseIndex line 154
  35. def OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.rotationWords line 173
  36. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.rotationWords_length line 175
  37. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem line 179
  38. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.rotationWords_get line 185
  39. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem? line 191
  40. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem?_none line 197
  41. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.rotationWords_entry_lt line 201
  42. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.rotationWords_lookup line 206
  43. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.rotationWords_row_order line 212
  44. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.decode_rotationWords line 217
  45. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.decoded_lookup line 221
  46. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.decoded_coordinate_lookup line 227
  47. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_eq line 234
  48. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_le line 238