OAI/Computability/MinUncut/PCP/ExpanderTableEnumeration.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.globalIndex line 14
  2. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.globalIndex_val line 20
  3. def OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.rowValue line 33
  4. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.rowValue_eq_reverseIndex line 39
  5. def OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords line 46
  6. def OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords line 49
  7. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_length line 52
  8. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_succ line 56
  9. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_full line 63
  10. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_last line 68
  11. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.ofFn_cast line 74
  12. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.rotationWords_eq_ofFn line 79
  13. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.rowCount_eq line 87
  14. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_eq_flat_ofFn line 90
  15. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_eq_rotationWords line 108
  16. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_length line 115
  17. def OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices line 120
  18. def OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows line 123
  19. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_zero line 127
  20. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_full line 130
  21. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_succ line 135
  22. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_zero line 142
  23. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_succ line 146
  24. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_complete line 154
  25. def OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate line 160
  26. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_eq line 163
  27. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_append line 171
  28. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_prefixRows_succ line 175
  29. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_generatedWords line 183
  30. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.encode_generatedWords_length_le line 189
  31. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_generatedWords_length_le line 195